P. 340 of Theorem List - Metamath Proof Explorer

Home	Metamath Proof Explorer Theorem List (p. 340 of 394)	< 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-26406)

Hilbert Space Explorer
(26407-27929)

Users' Mathboxes
(27930-39313)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem	cdlemg10b 33914	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 33915	TODO: FIX COMMENT TODO: Can this be moved up as a stand-alone theorem in ltrn* area? TODO: Compare this proof to cdlemg2m 33883 and pick best, if moved to ltrn* area. (Contributed by NM, 4-May-2013.) (New usage is discouraged.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$

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

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

Theorem	cdlemg10c 33918	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 33919	TODO: FIX COMMENT (Contributed by NM, 3-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem	cdlemg16 33936	Part of proof of Lemma G of [Crawley] p. 116; 2nd line p. 117, which says that (our) cdlemg10 33920 "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 33163, in order to make this inference. This final step eliminates the condition from cdlemg12 33929. 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 33937	This version of cdlemg16 33936 uses cdlemg15a 33934 instead of cdlemg15 33935, in case cdlemg15 33935 ends up not being needed. TODO: FIX COMMENT (Contributed by NM, 6-May-2013.) (New usage is discouraged.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$

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

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

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

Theorem	cdlemg17b 33941*	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 33568. (Contributed by NM, 8-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem	cdlemg17 33956*	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 33957	Show two lines are different. TODO: fix comment. (Contributed by NM, 14-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem	cdlemg28a 33972	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 33973	TODO: Fix comment. (Contributed by NM, 30-May-2013.) (New usage is discouraged.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$

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

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

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

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

Theorem	cdlemg31c 33978	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 33979	Eliminate from cdlemg31c 33978. 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 33984 vs. cdlemg28 33983. (Contributed by NM, 29-May-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

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

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

Theorem	cdlemg28b 33982*	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 33983.) (Contributed by NM, 29-May-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg28 33983*	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 33984 (and maybe leading up to this too)? (Contributed by NM, 29-May-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$

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

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

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