Metamath Proof Explorer - Most Recent Proofs

Most Recent Proofs    These are the 100 most recent proofs in the Metamath Proof Explorer and the Hilbert Space Explorer. To understand how to follow the proofs, read How Proofs Work. If this is a mirror site, the live site may have more recent updates. Email comments to Norm Megill.

Also new:
(9-Jan-05) If you are a user of set.mm: The ubiquitous biconditional theorems birand, etc. were renamed to anbi1d, etc. for consistency with the equality analogues ineq1d, etc. See the recent label change list at the beginning of set.mm. Thanks to Raph Levien for pointing out the inconsistency.
(6-Jan-05) Someone assembled an amazon.com list of some of the books in the Metamath Proof Explorer Bibliography.
(4-Jan-05) The definition of ordinal exponentiation was decided on after this Usenet discussion.
(21-Dec-04) The Germany site de.metamath.org was moved to a much faster mirror. Try it!
(20-Dec-04) The us.metamath.org mirror (linked on the Metamath Site Selection page) will be down while it is being revamped, and us.metamath.org has been temporarily changed to an alias for au.metamath.org. If you are curious, here are some site usage statistics for us.metamath.org last year that I grabbed before it went offline: Jan., Apr., Nov., Dec. 1 - Dec. 19, 2004 summary. April 19th shows a spike when this site was mentioned in a slashdot.org comment.
(19-Dec-04) A bit of trivia: my Erdös number is 2, as you can see from this list.
(20-Oct-04) I started this Usenet discussion about the "reals are uncountable" proof (127 comments; last one on Nov. 12).
(18-Oct-04) A description of the proof that the reals are uncountable was added to the Real and Complex Numbers page.
(12-Oct-04) gch-kn shows the equivalence of the Generalized Continuum Hypothesis and Prof. Nambiar's Axiom of Combinatorial Sets. This proof answers his Open Problem 2 (PDF file).
(12-Oct-04) I ran across a comment about the Metamath Music Page.
(16-Aug-04) Mel O'Cat shortened the proofs of com4l and pm2.43.
(15-Aug-04) The Quantum Logic section of the Hilbert Space Explorer now shows theorems that correspond directly to the axioms for the Quantum Logic Explorer, thus eliminating the previous "exercise for the reader" (which is doubtful that any reader actually worked out :)).
(5-Aug-04) I gave a talk on "Hilbert Lattice Equations" at the Argonne workshop.
(25-Jul-04) The theorem nthruz is the 4000th theorem added to the Metamath Proof Explorer database.
(29-May-04) Bob Solovay wrote a nicely commented Metamath database, peano.mm, that presents Peano arithmetic as a stand-alone axiomatic system (no set theory).
(27-May-04) Josiah Burroughs contributed the proofs u1lemn1b, u1lem3var1, oi3oa3lem1, and oi3oa3 to the Quantum Logic Explorer database ql.mm.
(23-May-04) Some minor typos found by Josh Purinton were corrected in the Metamath book. In addition, Josh simplified the definition of the closure of a pre-statement of a formal system in Appendix C.
(5-May-04) Gregory Bush has found shorter proofs for 67 of the 193 propositional calculus theorems listed in Principia Mathematica, thus establishing 67 new records. (This was challenge #4 on the open problems page.)
(1-Apr-04) (Actually added 26-May-04.) For those people still coming from urgo.org after all this time, the April Fool's theorem (a real, if nonsensical and useless, theorem) is avril1.

Last updated on 12-Jan-05 at 12:52 AM ET.

Recent Additions to the Metamath Proof Explorer   informal notes on recent proofs (last updated 12-Jan-05)

Date	Label	Description
Theorem
12-Jan-05	tfindsg2 2403	Transfinite Induction (inference schema) with implicit substitutions. The first four hypotheses establish the substitutions we need. The last three are the basis, the induction hypothesis for successors, and the induction hypothesis for limit ordinals. The basis of this version is an arbitrary ordinal suc B instead of zero.
|- (x = suc B -> (ph <-> ps))   &   |- (x = y -> (ph <-> ch))   &   |- (x = suc y -> (ph <-> th))   &   |- (x = A -> (ph <-> ta ))   &   |- (B e. On -> ps)   &   |- ((y e. On /\ B e. y) -> (ch -> th))   &   |- ((Lim x /\ B e. x) -> (A.y e. x (B e. y -> ch) -> ph))   =>   |- ((A e. On /\ B e. A) -> ta )
12-Jan-05	bigolden 513	Dijkstra-Scholten's Golden Rule for calculational proofs.
|- (((ph /\ ps) <-> ph) <-> (ps <-> (ph \/ ps)))
11-Jan-05	biluk 512	Lukasiewicz's shortest axiom for equivalential calculus. Storrs McCall, ed., Polish Logic 1920-1939 (Oxford, 1967), p. 96.
|- ((ph <-> ps) <-> ((ch <-> ps) <-> (ph <-> ch)))
11-Jan-05	biass 511	Associative law for the biconditional. An axiom of system DS in Vladimir Lifschitz, "On calculational proofs" (1998), http://citeseer.lcs.mit.edu/lifschitz98calculational.html. Noted by Jan Lukasiewicz c. 1923.
|- (((ph <-> ps) <-> ch) <-> (ph <-> (ps <-> ch)))
11-Jan-05	xor 500	Two ways to express "exclusive or". Theorem *5.22 of [WhiteheadRussell] p. 124.
|- (-. (ph <-> ps) <-> ((ph /\ -. ps) \/ (ps /\ -. ph)))
11-Jan-05	or42 221	Rearrangement of 4 disjuncts.
|- (((ph \/ ps) \/ (ch \/ th)) <-> ((ph \/ ch) \/ (th \/ ps)))
10-Jan-05	oen0 3165	Ordinal exponentiation with a nonzero mantissa is nonzero. Proposition 8.32 of [TakeutiZaring] p. 67.
|- (((A e. On /\ B e. On) /\ (/) e. A) -> (/) e. (A ^o B))
10-Jan-05	omordi 3164	Ordering property of ordinal multiplication. Half of Proposition 8.19 of [TakeutiZaring] p. 63.
|- (((B e. On /\ C e. On) /\ (/) e. C) -> (A e. B -> (C .o A) e. (C .o B)))
9-Jan-05	orbidi 510	Disjunction distributes over the biconditional. An axiom of system DS in Vladimir Lifschitz, "On calculational proofs" (1998), http://citeseer.lcs.mit.edu/lifschitz98calculational.html.
|- ((ph \/ (ps <-> ch)) <-> ((ph \/ ps) <-> (ph \/ ch)))
9-Jan-05	imbi2 473	Theorem *4.85 of [WhiteheadRussell] p. 122.
|- ((ph <-> ps) -> ((ch -> ph) <-> (ch -> ps)))
9-Jan-05	imbi1 472	Theorem *4.84 of [WhiteheadRussell] p. 122.
|- ((ph <-> ps) -> ((ph -> ch) <-> (ps -> ch)))
9-Jan-05	pm2.85 439	Theorem *2.85 of [WhiteheadRussell] p. 108.
|- (((ph \/ ps) -> (ph \/ ch)) -> (ph \/ (ps -> ch)))
9-Jan-05	pm2.48 230	Theorem *2.48 of [WhiteheadRussell] p. 107.
|- (-. (ph \/ ps) -> (ph \/ -. ps))
8-Jan-05	oe1m 3147	Ordinal exponentiation with a mantissa of 1. Proposition 8.31(3) of [TakeutiZaring] p. 67.
|- (A e. On -> (1o ^o A) = 1o)
8-Jan-05	oe1 3146	Ordinal exponentiation with an exponent of 1.
|- (A e. On -> (A ^o 1o) = A)
8-Jan-05	oe0lem 3121	A helper lemma for oe0 3130 and others.
|- ((ph /\ A = (/)) -> ps)   &   |- (((A e. On /\ ph) /\ (/) e. A) -> ps)   =>   |- ((A e. On /\ ph) -> ps)
8-Jan-05	0lt1o 3116	Ordinal zero is less than ordinal one.
|- (/) e. 1o
8-Jan-05	el1o 3115	Membership in ordinal one.
|- (A e. 1o <-> A = (/))
8-Jan-05	pm2.46 229	Theorem *2.46 of [WhiteheadRussell] p. 106.
|- (-. (ph \/ ps) -> -. ps)
8-Jan-05	pm2.45 228	Theorem *2.45 of [WhiteheadRussell] p. 106.
|- (-. (ph \/ ps) -> -. ph)
8-Jan-05	pm2.36 91	Theorem *2.36 of [WhiteheadRussell] p. 105.
|- ((ps -> ch) -> ((-. ph -> ps) -> (-. ch -> ph)))
7-Jan-05	oecl 3140	Closure law for ordinal exponentiation.
|- ((A e. On /\ B e. On) -> (A ^o B) e. On)
7-Jan-05	tfinds3 2406	Principle of Transfinite Induction (inference schema) with implicit substitutions. The first four hypotheses establish the substitutions we need. The last three are the basis, the induction hypothesis for successors, and the induction hypothesis for limit ordinals.
|- (x = (/) -> (ph <-> ps))   &   |- (x = y -> (ph <-> ch))   &   |- (x = suc y -> (ph <-> th))   &   |- (x = A -> (ph <-> ta ))   &   |- (et -> ps)   &   |- (y e. On -> (et -> (ch -> th)))   &   |- (Lim x -> (et -> (A.y e. x ch -> ph)))   =>   |- (A e. On -> (et -> ta ))
7-Jan-05	mpan121 533	An inference based on modus ponens.
|- ps   &   |- (((ph /\ (ps /\ ch)) /\ th) -> ta )   =>   |- (((ph /\ ch) /\ th) -> ta )
7-Jan-05	pm2.1 495	Theorem *2.1 of [WhiteheadRussell] p. 101.
|- (-. ph \/ ph)
6-Jan-05	ledivt 4405	Division of both sides of a less than or equal to relation by a positive number.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> (0 < C -> (A <_ B <-> (A / C) <_ (B / C))))
6-Jan-05	pm2.67 231	Theorem *2.67 of [WhiteheadRussell] p. 107.
|- (((ph \/ ps) -> ps) -> (ph -> ps))
6-Jan-05	pm2.621 211	Theorem *2.621 of [WhiteheadRussell] p. 107.
|- ((ph -> ps) -> ((ph \/ ps) -> ps))
6-Jan-05	pm2.62 210	Theorem *2.62 of [WhiteheadRussell] p. 107.
|- ((ph \/ ps) -> ((ph -> ps) -> ps))
6-Jan-05	pm2.24 72	Theorem *2.24 of [WhiteheadRussell] p. 104.
|- (ph -> (-. ph -> ps))
5-Jan-05	spansnss2t 5480	The span of the singleton of an element of a subspace is included in the subspace.
|- ((A e. SH /\ B e. H~) -> (B e. A <-> (span` {B}) (_ A))
5-Jan-05	oelim 3137	Ordinal exponentiation with a limit exponent and nonzero mantissa. Definition 8.30 of [TakeutiZaring] p. 67.
|- (((A e. On /\ (B e. C /\ Lim B)) /\ (/) e. A) -> (A ^o B) = U.x e. B (A ^o x))
5-Jan-05	oesuc 3134	Ordinal exponentiation with a successor exponent. Definition 8.30 of [TakeutiZaring] p. 67.
|- ((A e. On /\ B e. On) -> (A ^o suc B) = ((A ^o B) .o A))
5-Jan-05	adantlrr 315	Deduction adding a conjunct to an antecedent.
|- (((ph /\ ps) /\ ch) -> th)   =>   |- (((ph /\ (ps /\ ta )) /\ ch) -> th)
4-Jan-05	oe0 3130	Ordinal exponentiation with zero exponent. Definition 8.30 of [TakeutiZaring] p. 67.
|- (A e. On -> (A ^o (/)) = 1o)
4-Jan-05	oe0m1 3129	Ordinal exponentiation with zero mantissa and nonzero exponent. Proposition 8.31(2) of [TakeutiZaring] p. 67.
|- ((A e. On /\ (/) e. A) -> ((/) ^o A) = (/))
3-Jan-05	shjshsel 5413	A closed subspace sum equals Hilbert lattice join. Part of Lemma 31.1.5 of [MaedaMaeda] p. 136.
|- A e. SH   &   |- B e. SH   =>   |- ((A +H B) e. CH <-> (A +H B) = (A vH B))
3-Jan-05	shsvst 5288	Vector subtraction belongs to subspace sum.
|- ((A e. SH /\ B e. SH) -> ((C e. A /\ D e. B) -> (C -v D) e. (A +H B)))
3-Jan-05	shsclt 5283	Closure of subspace sum.
|- ((A e. SH /\ B e. SH) -> (A +H B) e. SH)
3-Jan-05	oe0m0 3128	Ordinal exponentiation with zero mantissa and zero exponent. Proposition 8.31 of [TakeutiZaring] p. 67.
|- ((/) ^o (/)) = 1o
3-Jan-05	oe0m 3127	Ordinal exponentiation with zero mantissa.
|- (A e. On -> ((/) ^o A) = (1o \ A))
3-Jan-05	pm2.61an2 365	Elimination of an antecedent.
|- ((ph /\ ps) -> ch)   &   |- ((ph /\ -. ps) -> ch)   =>   |- (ph -> ch)
3-Jan-05	pm2.61an1 364	Elimination of an antecedent.
|- ((ph /\ ps) -> ch)   &   |- ((-. ph /\ ps) -> ch)   =>   |- (ps -> ch)
2-Jan-05	oevn0 3123	Value of ordinal exponentiation at a nonzero mantissa.
|- (((A e. On /\ B e. On) /\ (/) e. A) -> (A ^o B) = (rec({<.x, y>. | y = (x .o A)}, 1o)` B))
2-Jan-05	iunab 2023	The indexed union of a class abstraction.
|- U.x e. A {y | ph} = {y | E.x e. A ph}
2-Jan-05	syl3anc 629	A syllogism inference combined with contraction.
|- ((ph /\ ps /\ ch) -> th)   &   |- (ta -> ph)   &   |- (ta -> ps)   &   |- (ta -> ch)   =>   |- (ta -> th)
2-Jan-05	sylan12 355	A syllogism inference.
|- (((ph /\ ps) /\ ch) -> th)   &   |- (ta -> ps)   =>   |- (((ph /\ ta ) /\ ch) -> th)
1-Jan-05	oev 3122	Value of ordinal exponentiation.
|- ((A e. On /\ B e. On) -> (A ^o B) = if(A = (/), (1o \ B), (rec({<.x, y>. | y = (x .o A)}, 1o)` B)))
1-Jan-05	ordgt0ge1 3114	Two ways of expressing that an ordinal class is positive.
|- (Ord A -> ((/) e. A <-> 1o (_ A))
1-Jan-05	rabab 1359	A class abstraction restricted to the universe is unrestricted.
|- {x e. V | ph} = {x | ph}
1-Jan-05	pm5.32rd 492	Distribution of implication over biconditional (deduction rule).
|- (ph -> (ps -> (ch <-> th)))   =>   |- (ph -> ((ch /\ ps) <-> (th /\ ps)))
31-Dec-04	elcard 3713	Membership in the class of cardinal numbers.
|- (A e. Card <-> (card` A) = A)
31-Dec-04	adantrrr 319	Deduction adding a conjunct to an antecedent.
|- ((ph /\ (ps /\ ch)) -> th)   =>   |- ((ph /\ (ps /\ (ch /\ ta ))) -> th)
31-Dec-04	adantrrl 318	Deduction adding a conjunct to an antecedent.
|- ((ph /\ (ps /\ ch)) -> th)   =>   |- ((ph /\ (ps /\ (ta /\ ch))) -> th)
31-Dec-04	adantrlr 317	Deduction adding a conjunct to an antecedent.
|- ((ph /\ (ps