Most Recent Proofs - Metamath Proof Explorer

Most Recent Proofs    These are the 10 (GIF, Unicode) or 100 (GIF, Unicode) most recent proofs in the Metamath Proof Explorer and the Hilbert Space Explorer. The official, cleaned up set.mm database file in the Metamath program download is sometimes several days behind the preproduction set.mm (7MB) that corresponds to this page. Email: Norm Megill. Wikis: AsteroidMeta (Recent Changes); Ghestalt (Recent Changes). Mailing list: Google Groups. Syndication: RSS feed (web version) courtesy of Dan Getz.

Some users have reported that they cannot always access this page, apparently because port 8888 is sometimes mysteriously blocked. I added two other ports, and this page can now be accessed via ports 88, 443, and 8888. You can discuss this problem here. — Norm 24 Jun 2008

Last updated on 19-Jul-2008 at 5:52 PM ET.

Recent Additions to the Metamath Proof Explorer   Notes (last updated 22-May-08 )   News (last updated 23-May-08 )

Date	Label	Description
Theorem
19-Jul-2008	nvoprne 8271	The vector addition and scalar product operations are not identical.
|- (<.<.G, S>., N>. e. NrmCVec -> G =/= S)
18-Jul-2008	expnlbndt 6601	The reciprocal of exponentiation with a mantissa greater than 1 has no lower bound.
|- ((A e. RR+ /\ B e. RR /\ 1 < B) -> E.k e. NN (1 / (B^k)) < A)
18-Jul-2008	rpne0t 6239	A positive real is nonzero.
|- (A e. RR+ -> A =/= 0)
17-Jul-2008	infpss 7535	Every infinite set has an equinumerous proper subset. Exercise 7 of [TakeutiZaring] p. 91.
|- A e. V   =>   |- (om ~<_ A -> E.x(x (. A /\ x ~~ A))
16-Jul-2008	relelrng 3343	The second argument of a binary relation belongs to its range.
|- ((B e. C /\ Rel R /\ ARB) -> B e. ran R)
15-Jul-2008	flfract 6195	The fractional part of a real number is less than one.
|- (A e. RR -> (A - (|_` A)) < 1)
15-Jul-2008	flreclt 6186	The floor (greatest integer) function is real.
|- (A e. RR -> (|_` A) e. RR)
14-Jul-2008	dmdbr7at 10306	Dual modular pair property in terms of atoms.
|- A e. CH   &   |- B e. CH   =>   |- (A MH* B <-> A.x e. Atoms ((A vH B) i^i x) (_ (((x vH B) i^i A) vH B))
14-Jul-2008	syld3an1 870	A syllogism inference.
|- ((ph /\ ps /\ ch) -> th)   &   |- ((ta /\ ps /\ ch) -> ph)   =>   |- ((ta /\ ps /\ ch) -> th)
13-Jul-2008	dmdbr4at 10303	Dual modular pair property in terms of atoms.
|- A e. CH   &   |- B e. CH   =>   |- (A MH* B <-> A.x e. Atoms ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B))
12-Jul-2008	atdmd2 10296	Two Hilbert lattice elements have the dual modular pair property if the second is an atom.
|- ((A e. CH /\ B e. Atoms) -> A MH* B)
12-Jul-2008	dmdbr5 10190	Binary relation expressing the dual modular pair property.
|- ((A e. CH /\ B e. CH) -> (A MH* B <-> A.x e. CH (x (_ (A vH B) -> x (_ (((x vH B) i^i A) vH B))))
11-Jul-2008	clmfnn 7047	Express the predicate F converges to A for an explicit function, using natural numbers.
|- ((F:NN-->CC /\ A e. CC) -> (F ~~> A <-> A.x e. RR+ E.j e. NN A.k e. NN (j <_ k -> (abs` ((F` k) - A)) < x)))
10-Jul-2008	metcls 7929	The closure of a subset of a metric space is equal to its points of convergence. Theorem 1.4-6(a) of [Kreyszig] p. 30.
|- X = dom dom D   &   |- J = (Open` D)   =>   |- ((D e. Met /\ M (_ X) -> ((cls` J)` M) = {x | E.f(f:NN-->M /\ f(~~>m` D)x)})
10-Jul-2008	expne0t 6532	Natural number exponentiation is nonzero iff its mantissa is nonzero.
|- ((A e. CC /\ N e. NN) -> ((A^N) =/= 0 <-> A =/= 0))
9-Jul-2008	iscaunns 7907	Express the property "F is a Cauchy sequence of metric D."
|- X = dom dom D   &   |- (k e. NN -> A = (F` k))   =>   |- ((D e. Met /\ F:NN-->X) -> (F e. (Cau` D) <-> A.x e. RR+ E.j e. NN A.k e. NN (j <_ k -> ([_j / k]_ADA) < x)))
8-Jul-2008	nmopub2t 9790	An upper bound for an operator norm.
|- ((T:H~-->H~ /\ (A e. RR /\ 0 <_ A) /\ A.x e. H~ (normh` (T` x)) <_ (A x. (normh` x))) -> (normop` T) <_ A)
8-Jul-2008	projlem 9172	Lemma 3.6 of [Beran] p. 101: "Let H be a complete subspace of a (pre-)Hilbert space H~ and let A e. H~. Then there exists a vector x e. H such that (norm` (x -h A)) <_ (norm` (y -h A)) for every y e. H." This is a lemma for the projection theorem.
|- A e. H~   &   |- H e. CH   =>   |- E.x e. H A.y e. H (normh` (x -h A)) <_ (normh` (y -h A))
8-Jul-2008	climabs0 7067	Convergence to zero of the absolute value implies convergence to zero.
|- F e. V   &   |- G e. V   &   |- (k e. NN -> (G` k) = (abs` (F` k)))   =>   |- ((A.k e. NN (F` k) e. CC /\ G ~~> 0) -> F ~~> 0)
7-Jul-2008	dmdi2 10186	Consequence of the dual modular pair property.
|- (((A e. CH /\ B e. CH /\ C e. CH) /\ (A MH* B /\ B (_ C)) -> (C i^i (A vH B)) (_ ((C i^i A) vH B))
7-Jul-2008	spwpr2 8614	Property of supremum defining condition for an unordered pair.
|- (ph <-> (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy)))   =>   |- (((R e. T /\ A = {B, C}) /\ (B e. U /\ C e. W)) -> (ph <-> ((BRx /\ CRx) /\ A.y e. X ((BRy /\ CRy) -> xRy))))
7-Jul-2008	2pwuninel 4476	The power set of the power set of the union of a set does not belong to the set. This theorem provides a way of constructing a new set that doesn't belong to a given set.
|- -. P~P~U.A e. A
7-Jul-2008	dmex 3356	The domain of a set is a set. Corollary 6.8(2) of [TakeutiZaring] p. 26.
|- A e. V   =>   |- dom A e. V
6-Jul-2008	lmbrnns 7905	Express the binary relation "sequence F converges to point P " in a metric space."
|- X = dom dom D   &   |- (k e. NN -> A = (F` k))   =>   |- ((D e. Met /\ P e. X /\ F:NN-->X) -> (F(~~>m` D)P <-> A.x e. RR+ E.j e. NN A.k e. NN (j <_ k -> (ADP) < x)))
6-Jul-2008	releldm 3342	The first argument of a binary relation belongs to its domain.
|- ((Rel R /\ ARB) -> A e. dom R)
5-Jul-2008	pjocco 10061	Composition of projections of a subspace and its orthocomplement.
|- H e. CH   =>   |- ((proj` H) o. (proj` (_|_` H))) = 0hop
5-Jul-2008	leoptrt 10025	The positive operator ordering relation is transitive. Exercise 1(iv) of [Retherford] p. 49.
|- (((S e. HrmOp /\ T e. HrmOp /\ U e. HrmOp) /\ (S <_op T /\ T <_op U)) -> S <_op U)
5-Jul-2008	iscau4 7903	Express the property "F is a Cauchy sequence of metric D."
|- X = dom dom D   =>   |- (D e. Met -> (F e. (Cau` D) <-> (F (_ (CC X. X) /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((F` j) e. X /\ (F` k) e. X /\ ((F` j)D(F` k)) < x))))))
4-Jul-2008	bracnlnvalt 10002	The vector that a continuous linear functional is the bra of.
|- (T e. (LinFn i^i ConFn) -> T = (bra` U.{y e. H~ | A.x e. H~ (T` x) = (x .ih y)}))
3-Jul-2008	unisn3 2872	Union of a singleton in the form of a restricted class abstraction.
|- (A e. B -> U.{x e. B | x = A} = A)
2-Jul-2008	nmopcoadj0 9991	An operator composed with its adjoint is zero iff the operator is zero. Theorem 3.11(vii) of [Beran] p. 106.
|- T e. BndLinOp   =>   |- ((T o. (adjh` T)) = 0hop <-> T = 0hop)
2-Jul-2008	sylancom 475	Syllogism inference with commutation of antecents.
|- ((ph /\ ps) -> ch)   &   |- ((ch /\ ps) -> th)   =>   |- ((ph /\ ps) -> th)
1-Jul-2008	supmax 4572	The greatest element of a set is the supremum. Note that the converse is not true; the supremum might not be an element of the set considered. (Contributed by Jeff Hoffman, 17-Jun-2008.)
|- R Or A   =>   |- ((C e. A /\ C e. B /\ A.y e. B -. CRy) -> sup(B, A, R) = C)
1-Jul-2008	supmaxlem 4571	A set that contains a greatest element satisfies the antecedent in supremum theorems. This allows sup(A, B, R) to be used in some situations without the completeness axiom. (Contributed by Jeff Hoffman, 17-Jun-2008.)
|- ((C e. A /\ C e. B /\ A.z e. B -. CRz) -> E.x e. A (A.y e. B -. xRy /\ A.y e. A (yRx -> E.z e. B yRz)))
1-Jul-2008	opelxpex2 3275	The second member of an ordered pair of classes in a cross product exists when the order pair doesn't belong to I.
|- (<.A, B>. e. ((C X. D) \ I) -> B e. V)
30-Jun-2008	adjeq0 9979	An operator is zero iff its adjoint is zero. Theorem 3.11(i) of [Beran] p. 106.
|- (T = 0hop <-> (adjh` T) = 0hop)
30-Jun-2008	hhsshl 9106	Hilbert space property of a closed subspace.
|- W = <.<.( +h |` (H X. H)), ( .h |` (CC X. H))>., (normh |` H)>.   &   |- H e. CH   =>   |- W e. CHil
29-Jun-2008	hhssims2 9100	Induced metric of a subspace.
|- W = <.<.( +h |` (H X. H)), ( .h |` (CC X. H))>., (normh |` H)>.   &   |- D = (IndMet` W)   &   |- H e. SH   =>   |- D = ((normh o. -h ) |` (H X. H))
29-Jun-2008	brelrn 3340	The second argument of a binary relation belongs to its range.
|- A e. V   &   |- B e. V   =>   |- (ACB -> B e. ran C)
29-Jun-2008	brelrng 3339	The second argument of a binary relation belongs to its range.
|- ((A e. F /\ B e. G /\ ACB) -> B e. ran C)
29-Jun-2008	ordtri3or 2975	A trichotomy law for ordinals. Proposition 7.10 of [TakeutiZaring] p. 38.
|- ((Ord A /\ Ord B) -> (A e. B \/ A = B \/ B e. A))
29-Jun-2008	moi2 1921	Consequence of "at most one."
|- (x = A -> (ph <-> ps))   =>   |- (((A e. B /\ E*xph) /\ (ph /\ ps)) -> x = A)
28-Jun-2008	rehaus 7880	The standard topology on the reals is Hausdorff.
|- (topGen` ran (,)) e. Haus
27-Jun-2008	hhssims 9099	Induced metric of a subspace.
|- W = <.<.( +h |` (H X. H)), ( .h |` (CC X. H))>., (normh |` H)>.   &   |- H e. SH   &   |- D = ((normh o. -h ) |` (H X. H))   =>   |- D = (IndMet` W)
27-Jun-2008	hhsssh2 9094	The predicate "H is a subspace of Hilbert space."
|- W = <.<.( +h |` (H X. H)), ( .h |` (CC X. H))>., (normh |` H)>.   =>   |- (H e. SH <-> (W e. NrmCVec /\ H (_ H~))
27-Jun-2008	pwuninel 4475	The power set of the union of a set does not belong to the set. This theorem provides a way of constructing a new set that doesn't belong to a given set.
|- -. P~U.A e. A
26-Jun-2008	oteqex 2795	Equivalence of existence implied by equality of ordered triples.
|- (<.<.A, B>., C>. = <.<.R, S>., T>. -> (A e. V <-> R e. V))
25-Jun-2008	nvdm