P. 359 of Theorem List - Metamath Proof Explorer

Home	Metamath Proof Explorer Theorem List (p. 359 of 377)	< 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-25707)

Hilbert Space Explorer
(25708-27232)

Users' Mathboxes
(27233-37662)

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

Theorem	cdleme21i 35801*	Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$

Theorem	cdleme21j 35802*	Combine cdleme20 35790 and cdleme21i 35801 to eliminate $.\/$ condition. (Contributed by NM, 29-Nov-2012.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$

Theorem	cdleme21 35803	Part of proof of Lemma E in [Crawley] p. 113, 3rd line on p. 115. , , , , , represent s₂, f(s), f_s(r), t₂, f(t), f_t(r) respectively. Combine cdleme18d 35760 and cdleme21j 35802 to eliminate existence condition, proving f_s(r) = f_t(r) with fewer conditions. (Contributed by NM, 29-Nov-2012.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$

Theorem	cdleme21k 35804	Eliminate condition in cdleme21 35803. (Contributed by NM, 26-Dec-2012.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$

Theorem	cdleme22aa 35805	Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 3rd line on p. 115. Show that t $\/$ v = p $\/$ q implies v = u. (Contributed by NM, 2-Dec-2012.)
$.\/$ $./\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$

Theorem	cdleme22a 35806	Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 3rd line on p. 115. Show that t $\/$ v = p $\/$ q implies v = u. (Contributed by NM, 30-Nov-2012.)
$.\/$ $./\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$

Theorem	cdleme22b 35807	Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 5th line on p. 115. Show that t $\/$ v =/= p $\/$ q and s p $\/$ q implies t p $\/$ q. (Contributed by NM, 2-Dec-2012.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$

Theorem	cdleme22cN 35808	Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 5th line on p. 115. Show that t $\/$ v =/= p $\/$ q and s p $\/$ q implies v p $\/$ q. (Contributed by NM, 3-Dec-2012.) (New usage is discouraged.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$

Theorem	cdleme22d 35809	Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 9th line on p. 115. (Contributed by NM, 4-Dec-2012.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$

Theorem	cdleme22e 35810	Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 4th line on p. 115. , , represent f(z), f_z(s), f_z(t) respectively. When t $\/$ v = p $\/$ q, f_z(s) f_z(t) $\/$ v. (Contributed by NM, 6-Dec-2012.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$

Theorem	cdleme22eALTN 35811	Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 4th line on p. 115. , , represent f(z), f_z(s), f_z(t) respectively. When t $\/$ v = p $\/$ q, f_z(s) f_z(t) $\/$ v. (Contributed by NM, 6-Dec-2012.) (New usage is discouraged.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$

Theorem	cdleme22f 35812	Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 6th and 7th lines on p. 115. , represent f(t), f_t(s) respectively. If s t $\/$ v, then f_t(s) f(t) $\/$ v. (Contributed by NM, 6-Dec-2012.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$

Theorem	cdleme22f2 35813	Part of proof of Lemma E in [Crawley] p. 113. cdleme22f 35812 with s and t swapped (this case is not mentioned by them). If s t $\/$ v, then f(s) f_s(t) $\/$ v. (Contributed by NM, 7-Dec-2012.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$

Theorem	cdleme22g 35814	Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 6th and 7th lines on p. 115. , represent f(s), f(t) respectively. If s t $\/$ v and s p $\/$ q, then f(s) f(t) $\/$ v. (Contributed by NM, 6-Dec-2012.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$

Theorem	cdleme23a 35815	Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Dec-2012.)
$.\/$ $./\$ $.\/$ $./\$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$

Theorem	cdleme23b 35816	Part of proof of Lemma E in [Crawley] p. 113, 4th paragraph, 6th line on p. 115. (Contributed by NM, 8-Dec-2012.)
$.\/$ $./\$ $.\/$ $./\$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$

Theorem	cdleme23c 35817	Part of proof of Lemma E in [Crawley] p. 113, 4th paragraph, 6th line on p. 115. (Contributed by NM, 8-Dec-2012.)
$.\/$ $./\$ $.\/$ $./\$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$ $.\/$

Theorem	cdleme24 35818*	Quantified version of cdleme21k 35804. (Contributed by NM, 26-Dec-2012.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$

Theorem	cdleme25a 35819*	Lemma for cdleme25b 35820. (Contributed by NM, 1-Jan-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$

Theorem	cdleme25b 35820*	Transform cdleme24 35818. TODO get rid of $d's on , (Contributed by NM, 1-Jan-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$

Theorem	cdleme25c 35821*	Transform cdleme25b 35820. (Contributed by NM, 1-Jan-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$

Theorem	cdleme25dN 35822*	Transform cdleme25c 35821. (Contributed by NM, 19-Jan-2013.) (New usage is discouraged.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$

Theorem	cdleme25cl 35823*	Show closure of the unique element in cdleme25c 35821. (Contributed by NM, 2-Feb-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$

Theorem	cdleme25cv 35824*	Change bound variables in cdleme25c 35821. (Contributed by NM, 2-Feb-2013.)
$.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $/\$ $.\/$

Theorem	cdleme26e 35825*	Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 4th line on p. 115. , , represent f(z), f_z(s), f_z(t) respectively. When t $\/$ v = p $\/$ q, f_z(s) f_z(t) $\/$ v. TODO: FIX COMMENT. (Contributed by NM, 2-Feb-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$

Theorem	cdleme26ee 35826*	Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 4th line on p. 115. , , represent f(z), f_z(s), f_z(t) respectively. When t $\/$ v = p $\/$ q, f_z(s) f_z(t) $\/$ v. TODO: FIX COMMENT. (Contributed by NM, 2-Feb-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$

Theorem	cdleme26eALTN 35827*	Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 4th line on p. 115. , , represent f(z), f_z(s), f_z(t) respectively. When t $\/$ v = p $\/$ q, f_z(s) f_z(t) $\/$ v. TODO: FIX COMMENT. (Contributed by NM, 1-Feb-2013.) (New usage is discouraged.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$

Theorem	cdleme26fALTN 35828*	Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 6th and 7th lines on p. 115. , represent f(t), f_t(s) respectively. If t t $\/$ v, then f_t(s) f(t) $\/$ v. TODO: FIX COMMENT. (Contributed by NM, 1-Feb-2013.) (New usage is discouraged.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$

Theorem	cdleme26f 35829*	Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 6th and 7th lines on p. 115. , represent f(t), f_t(s) respectively. If t t $\/$ v, then f_t(s) f(t) $\/$ v. TODO: FIX COMMENT. (Contributed by NM, 1-Feb-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$

Theorem	cdleme26f2ALTN 35830*	Part of proof of Lemma E in [Crawley] p. 113. cdleme26fALTN 35828 with s and t swapped (this case is not mentioned by them). If s t $\/$ v, then f(s) f_s(t) $\/$ v. TODO: FIX COMMENT. (Contributed by NM, 1-Feb-2013.) (New usage is discouraged.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$

Theorem	cdleme26f2 35831*	Part of proof of Lemma E in [Crawley] p. 113. cdleme26fALTN 35828 with s and t swapped (this case is not mentioned by them). If s t $\/$ v, then f(s) f_s(t) $\/$ v. TODO: FIX COMMENT. (Contributed by NM, 1-Feb-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$

Theorem	cdleme27cl 35832*	Part of proof of Lemma E in [Crawley] p. 113. Closure of . (Contributed by NM, 6-Feb-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdleme27a 35833*	Part of proof of Lemma E in [Crawley] p. 113. cdleme26f 35829 with s and t swapped (this case is not mentioned by them). If s t $\/$ v, then f(s) f_s(t) $\/$ v. TODO: FIX COMMENT. (Contributed by NM, 3-Feb-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$

Theorem	cdleme27b 35834*	Lemma for cdleme27N 35835. (Contributed by NM, 3-Feb-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $.\/$

Theorem	cdleme27N 35835*	Part of proof of Lemma E in [Crawley] p. 113. Eliminate the antecedent in cdleme27a 35833. (Contributed by NM, 3-Feb-2013.) (New usage is discouraged.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$

Theorem	cdleme28a 35836*	Lemma for cdleme25b 35820. TODO: FIX COMMENT (Contributed by NM, 4-Feb-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdleme28b 35837*	Lemma for cdleme25b 35820. TODO: FIX COMMENT (Contributed by NM, 6-Feb-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdleme28c 35838*	Part of proof of Lemma E in [Crawley] p. 113. Eliminate the antecedent in cdleme28b 35837. TODO: FIX COMMENT (Contributed by NM, 6-Feb-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdleme28 35839*	Quantified version of cdleme28c 35838. (Compare cdleme24 35818.) (Contributed by NM, 7-Feb-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdleme29ex 35840*	Lemma for cdleme29b 35841. (Compare cdleme25a 35819.) TODO: FIX COMMENT (Contributed by NM, 7-Feb-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$

Theorem	cdleme29b 35841*	Transform cdleme28 35839. (Compare cdleme25b 35820.) TODO: FIX COMMENT (Contributed by NM, 7-Feb-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdleme29c 35842*	Transform cdleme28b 35837. (Compare cdleme25c 35821.) TODO: FIX COMMENT (Contributed by NM, 8-Feb-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdleme29cl 35843*	Show closure of the unique element in cdleme28c 35838. (Contributed by NM, 8-Feb-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdleme30a 35844	Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 9-Feb-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$

Theorem	cdleme31so 35845*	Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 25-Feb-2013.)
$/\$ $.\/$ $./\$ $.\/$ $./\$ $/\$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdleme31sn 35846*	Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 26-Feb-2013.)
$.\/$ $.\/$

Theorem	cdleme31sn1 35847*	Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 26-Feb-2013.)
$/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$

Theorem	cdleme31se 35848*	Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 26-Feb-2013.)
$.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$

Theorem	cdleme31se2 35849*	Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 3-Apr-2013.)
$.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$

Theorem	cdleme31sc 35850*	Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 31-Mar-2013.)
$.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$

Theorem	cdleme31sde 35851*	Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 31-Mar-2013.)
$.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$

Theorem	cdleme31snd 35852*	Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 1-Apr-2013.)
$.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$

Theorem	cdleme31sdnN 35853*	Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 31-Mar-2013.) (New usage is discouraged.)
$.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$

Theorem	cdleme31sn1c 35854*	Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 1-Mar-2013.)
$.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $/\$ $.\/$

Theorem	cdleme31sn2 35855*	Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 26-Feb-2013.)
$.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$

Theorem	cdleme31fv 35856*	Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 10-Feb-2013.)
$/\$ $.\/$ $./\$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$ $/\$

Theorem	cdleme31fv1 35857*	Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 10-Feb-2013.)
$/\$ $.\/$ $./\$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$ $/\$ $/\$

Theorem	cdleme31fv1s 35858*	Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 25-Feb-2013.)
$/\$ $.\/$ $./\$ $.\/$ $./\$ $/\$ $/\$ $/\$

Theorem	cdleme31fv2 35859*	Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 23-Feb-2013.)
$/\$ $/\$ $/\$

Theorem	cdleme31id 35860*	Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 18-Apr-2013.)
$/\$ $/\$

Theorem	cdlemefrs29pre00 35861	*START OF VALUE AT ATOM STUFF TO REPLACE ONES BELOW* FIX COMMENT. TODO: see if this is the optimal utility theorem using lhpmat 35494. (Contributed by NM, 29-Mar-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$

Theorem	cdlemefrs29bpre0 35862*	TODO fix comment. (Contributed by NM, 29-Mar-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemefrs29bpre1 35863*	TODO FIX COMMENT (Contributed by NM, 29-Mar-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemefrs29cpre1 35864*	TODO FIX COMMENT (Contributed by NM, 29-Mar-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemefrs29clN 35865*	TODO: NOT USED? Show closure of the unique element in cdlemefrs29cpre1 35864. (Contributed by NM, 29-Mar-2013.) (New usage is discouraged.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemefrs32fva 35866*	Part of proof of Lemma E in [Crawley] p. 113. Value of at an atom not under . TODO: FIX COMMENT TODO: consolidate uses of lhpmat 35494 here and elsewhere, and presence/absence of $.\/$ term. Also, why can proof be shortened with cdleme29cl 35843? What is difference from cdlemefs27cl 35879? (Contributed by NM, 29-Mar-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemefrs32fva1 35867*	Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 29-Mar-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemefr29exN 35868*	Lemma for cdlemefs29bpre1N 35883. (Compare cdleme25a 35819.) TODO: FIX COMMENT TODO: IS THIS NEEDED? (Contributed by NM, 28-Mar-2013.) (New usage is discouraged.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$

Theorem	cdlemefr27cl 35869	Part of proof of Lemma E in [Crawley] p. 113. Closure of . (Contributed by NM, 23-Mar-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$

Theorem	cdlemefr32sn2aw 35870*	Show that is an atom not under when $.\/$ . (Contributed by NM, 28-Mar-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$

Theorem	cdlemefr32snb 35871*	Show closure of . (Contributed by NM, 28-Mar-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$

Theorem	cdlemefr29bpre0N 35872*	TODO fix comment. (Contributed by NM, 28-Mar-2013.) (New usage is discouraged.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemefr29clN 35873*	Show closure of the unique element in cdleme29c 35842. TODO fix comment. TODO Not needed? (Contributed by NM, 29-Mar-2013.) (New usage is discouraged.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$

Theorem	cdleme43frv1snN 35874*	Value of when $.\/$ . (Contributed by NM, 30-Mar-2013.) (New usage is discouraged.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$