P. 342 of Theorem List - Metamath Proof Explorer

Home	Metamath Proof Explorer Theorem List (p. 342 of 402)	< Previous Next >
		Browser slow? Try the Unicode version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List

Color key:

Metamath Proof Explorer
(1-26513)

Hilbert Space Explorer
(26514-28036)

Users' Mathboxes
(28037-40133)

**Theorem List for Metamath Proof Explorer -** 34101-34200 *Has distinct variable group(s)
Type	Label	Description
Statement

Theorem	cdlemg6e 34101	TODO: FIX COMMENT. (Contributed by NM, 27-Apr-2013.)
$.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$

Theorem	cdlemg6 34102	TODO: FIX COMMENT. (Contributed by NM, 27-Apr-2013.)
$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemg7fvN 34103	Value of a translation composition in terms of an associated atom. (Contributed by NM, 28-Apr-2013.) (New usage is discouraged.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg7aN 34104	TODO: FIX COMMENT. (Contributed by NM, 28-Apr-2013.) (New usage is discouraged.)
$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemg7N 34105	TODO: FIX COMMENT. (Contributed by NM, 28-Apr-2013.) (New usage is discouraged.)
$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemg8a 34106	TODO: FIX COMMENT. (Contributed by NM, 29-Apr-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg8b 34107	TODO: FIX COMMENT. (Contributed by NM, 29-Apr-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$

Theorem	cdlemg8c 34108	TODO: FIX COMMENT. (Contributed by NM, 29-Apr-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$

Theorem	cdlemg8d 34109	TODO: FIX COMMENT. (Contributed by NM, 29-Apr-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg8 34110	TODO: FIX COMMENT. (Contributed by NM, 29-Apr-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg9a 34111	TODO: FIX COMMENT. (Contributed by NM, 1-May-2013.)
$.\/$ $./\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$

Theorem	cdlemg9b 34112	The triples and are centrally perspective. TODO: FIX COMMENT. (Contributed by NM, 1-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$

Theorem	cdlemg9 34113	The triples and are axially perspective by dalaw 33363. Part of Lemma G of [Crawley] p. 116, last 2 lines. TODO: FIX COMMENT. (Contributed by NM, 1-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$

Theorem	cdlemg10b 34114	TODO: FIX COMMENT. TODO: Can this be moved up as a stand-alone theorem in ltrn* area? (Contributed by NM, 4-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg10bALTN 34115	TODO: FIX COMMENT. TODO: Can this be moved up as a stand-alone theorem in ltrn* area? TODO: Compare this proof to cdlemg2m 34083 and pick best, if moved to ltrn* area. (Contributed by NM, 4-May-2013.) (New usage is discouraged.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg11a 34116	TODO: FIX COMMENT. (Contributed by NM, 4-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$

Theorem	cdlemg11aq 34117	TODO: FIX COMMENT. TODO: can proof using this be restructured to use cdlemg11a 34116? (Contributed by NM, 4-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$

Theorem	cdlemg10c 34118	TODO: FIX COMMENT. TODO: Can this be moved up as a stand-alone theorem in trl* area? (Contributed by NM, 4-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$

Theorem	cdlemg10a 34119	TODO: FIX COMMENT. (Contributed by NM, 3-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$

Theorem	cdlemg10 34120	TODO: FIX COMMENT. (Contributed by NM, 4-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$

Theorem	cdlemg11b 34121	TODO: FIX COMMENT. (Contributed by NM, 5-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$

Theorem	cdlemg12a 34122	TODO: FIX COMMENT. (Contributed by NM, 5-May-2013.)
$.\/$ $./\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$

Theorem	cdlemg12b 34123	The triples and are centrally perspective. TODO: FIX COMMENT. (Contributed by NM, 5-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$

Theorem	cdlemg12c 34124	The triples and are axially perspective by dalaw 33363. TODO: FIX COMMENT. (Contributed by NM, 5-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$

Theorem	cdlemg12d 34125	TODO: FIX COMMENT. (Contributed by NM, 5-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$

Theorem	cdlemg12e 34126	TODO: FIX COMMENT. (Contributed by NM, 6-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$

Theorem	cdlemg12f 34127	TODO: FIX COMMENT. (Contributed by NM, 6-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$

Theorem	cdlemg12g 34128	TODO: FIX COMMENT. TODO: Combine with cdlemg12f 34127. (Contributed by NM, 6-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$

Theorem	cdlemg12 34129	TODO: FIX COMMENT. (Contributed by NM, 6-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg13a 34130	TODO: FIX COMMENT. (Contributed by NM, 6-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$

Theorem	cdlemg13 34131	TODO: FIX COMMENT. (Contributed by NM, 6-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg14f 34132	TODO: FIX COMMENT. (Contributed by NM, 6-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg14g 34133	TODO: FIX COMMENT. (Contributed by NM, 22-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg15a 34134	Eliminate the condition from cdlemg13 34131. TODO: FIX COMMENT. (Contributed by NM, 6-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg15 34135	Eliminate the $.\/$ $.\/$ condition from cdlemg13 34131. TODO: FIX COMMENT. (Contributed by NM, 25-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg16 34136	Part of proof of Lemma G of [Crawley] p. 116; 2nd line p. 117, which says that (our) cdlemg10 34120 "implies (2)" (of p. 116). No details are provided by the authors, so there may be a shorter proof; but ours requires the 14 lemmas, one using Desargues' law dalaw 33363, in order to make this inference. This final step eliminates the condition from cdlemg12 34129. TODO: FIX COMMENT. TODO: should we also eliminate here (or earlier)? Do it if we don't need to add it in for something else later. (Contributed by NM, 6-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg16ALTN 34137	This version of cdlemg16 34136 uses cdlemg15a 34134 instead of cdlemg15 34135, in case cdlemg15 34135 ends up not being needed. TODO: FIX COMMENT. (Contributed by NM, 6-May-2013.) (New usage is discouraged.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg16z 34138	Eliminate $.\/$ $.\/$ condition from cdlemg16 34136. TODO: would it help to also eliminate here or later? (Contributed by NM, 25-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg16zz 34139	Eliminate from cdlemg16z 34138. TODO: Use this only if needed. (Contributed by NM, 26-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg17a 34140	TODO: FIX COMMENT. (Contributed by NM, 8-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$

Theorem	cdlemg17b 34141*	Part of proof of Lemma G in [Crawley] p. 117, 4th line. Whenever (in their terminology) p $\/$ q/0 (i.e. the sublattice from 0 to p $\/$ q) contains precisely three atoms and g is not the identity, g(p) = q. See also comments under cdleme0nex 33768. (Contributed by NM, 8-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$

Theorem	cdlemg17dN 34142*	TODO: fix comment. (Contributed by NM, 9-May-2013.) (New usage is discouraged.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$

Theorem	cdlemg17dALTN 34143	Same as cdlemg17dN 34142 with fewer antecedents but longer proof TODO: fix comment. (Contributed by NM, 9-May-2013.) (New usage is discouraged.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$

Theorem	cdlemg17e 34144*	TODO: fix comment. (Contributed by NM, 8-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$

Theorem	cdlemg17f 34145*	TODO: fix comment. (Contributed by NM, 8-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$

Theorem	cdlemg17g 34146*	TODO: fix comment. (Contributed by NM, 9-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$

Theorem	cdlemg17h 34147*	TODO: fix comment. (Contributed by NM, 10-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $\/$

Theorem	cdlemg17i 34148*	TODO: fix comment. (Contributed by NM, 10-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$

Theorem	cdlemg17ir 34149*	TODO: fix comment. (Contributed by NM, 13-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$

Theorem	cdlemg17j 34150*	TODO: fix comment. (Contributed by NM, 11-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$

Theorem	cdlemg17pq 34151*	Utility theorem for swapping and . TODO: fix comment. (Contributed by NM, 11-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$

Theorem	cdlemg17bq 34152*	cdlemg17b 34141 with and swapped. Antecedent is redundant for easier use. TODO: should we have redundant antecedent for cdlemg17b 34141 also? (Contributed by NM, 13-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$

Theorem	cdlemg17iqN 34153*	cdlemg17i 34148 with and swapped. (Contributed by NM, 13-May-2013.) (New usage is discouraged.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$

Theorem	cdlemg17irq 34154*	cdlemg17ir 34149 with and swapped. (Contributed by NM, 13-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$

Theorem	cdlemg17jq 34155*	cdlemg17j 34150 with and swapped. (Contributed by NM, 13-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$

Theorem	cdlemg17 34156*	Part of Lemma G of [Crawley] p. 117, lines 7 and 8. We show an argument whose value at equals itself. TODO: fix comment. (Contributed by NM, 12-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$

Theorem	cdlemg18a 34157	Show two lines are different. TODO: fix comment. (Contributed by NM, 14-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$

Theorem	cdlemg18b 34158	Lemma for cdlemg18c 34159. TODO: fix comment. (Contributed by NM, 15-May-2013.)
$.\/$ $./\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$

Theorem	cdlemg18c 34159	Show two lines intersect at an atom. TODO: fix comment. (Contributed by NM, 15-May-2013.)
$.\/$ $./\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$

Theorem	cdlemg18d 34160*	Show two lines intersect at an atom. TODO: fix comment. (Contributed by NM, 15-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$

Theorem	cdlemg18 34161*	Show two lines intersect at an atom. TODO: fix comment. (Contributed by NM, 15-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$

Theorem	cdlemg19a 34162*	Show two lines intersect at an atom. TODO: fix comment. (Contributed by NM, 15-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$

Theorem	cdlemg19 34163*	Show two lines intersect at an atom. TODO: fix comment. (Contributed by NM, 15-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg20 34164*	Show two lines intersect at an atom. TODO: fix comment. (Contributed by NM, 23-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg21 34165*	Version of cdlemg19 with $.\/$ instead of $.\/$ as a condition. (Contributed by NM, 23-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg22 34166*	cdlemg21 34165 with condition removed. (Contributed by NM, 23-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg24 34167*	Combine cdlemg16z 34138 and cdlemg22 34166. TODO: Fix comment. (Contributed by NM, 24-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg37 34168*	Use cdlemg8 34110 to eliminate the $.\/$ condition of cdlemg24 34167. (Contributed by NM, 31-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg25zz 34169	cdlemg16zz 34139 restated for easier studying. TODO: Discard this after everything is figured out. (Contributed by NM, 26-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg26zz 34170	cdlemg16zz 34139 restated for easier studying. TODO: Discard this after everything is figured out. (Contributed by NM, 26-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg27a 34171	For use with case when $.\/$ $./\$ $.\/$ or $.\/$ $./\$ $.\/$ is zero, letting us establish $/\$ $.\/$ via 4atex 33553. TODO: Fix comment. (Contributed by NM, 28-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$

Theorem	cdlemg28a 34172	Part of proof of Lemma G of [Crawley] p. 116. First equality of the equation of line 14 on p. 117. (Contributed by NM, 29-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg31b0N 34173	TODO: Fix comment. (Contributed by NM, 30-May-2013.) (New usage is discouraged.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$

Theorem	cdlemg31b0a 34174	TODO: Fix comment. (Contributed by NM, 30-May-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$

Theorem	cdlemg27b 34175	TODO: Fix comment. (Contributed by NM, 28-May-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$

Theorem	cdlemg31a 34176	TODO: fix comment. (Contributed by NM, 29-May-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$

Theorem	cdlemg31b 34177	TODO: fix comment. (Contributed by NM, 29-May-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$

Theorem	cdlemg31c 34178	Show that when is an atom, it is not under . TODO: Is there a shorter direct proof? TODO: should we eliminate here? (Contributed by NM, 29-May-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemg31d 34179	Eliminate from cdlemg31c 34178. TODO: Prove directly. TODO: do we need to eliminate ? It might be better to do this all at once at the end. See also cdlemg29 34184 vs. cdlemg28 34183. (Contributed by NM, 29-May-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemg33b0 34180*	TODO: Fix comment. (Contributed by NM, 30-May-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$

Theorem	cdlemg33c0 34181*	TODO: Fix comment. (Contributed by NM, 30-May-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$

Theorem	cdlemg28b 34182*	Part of proof of Lemma G of [Crawley] p. 116. Second equality of the equation of line 14 on p. 117. Note that is redundant here (but simplifies cdlemg28 34183.) (Contributed by NM, 29-May-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg28 34183*	Part of proof of Lemma G of [Crawley] p. 116. Chain the equalities of line 14 on p. 117. TODO: rearrange hypotheses in the order of cdlemg29 34184 (and maybe leading up to this too)? (Contributed by NM, 29-May-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg29 34184*	Eliminate and from cdlemg28 34183. TODO: would it be better to do this later? (Contributed by NM, 29-May-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg33a 34185*	TODO: Fix comment. (Contributed by NM, 29-May-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $.\/$

Theorem	cdlemg33b 34186*	TODO: Fix comment. (Contributed by NM, 30-May-2013.)
$.\/$ $./\$