P. 361 of Theorem List - Metamath Proof Explorer

Home	Metamath Proof Explorer Theorem List (p. 361 of 374)	< 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-25658)

Hilbert Space Explorer
(25659-27183)

Users' Mathboxes
(27184-37324)

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

Theorem	erngplus2 36001	Ring addition operation. (Contributed by NM, 10-Jun-2013.)
$/\$ $/\$ $/\$ $/\$

Theorem	erngfmul 36002*	Ring multiplication operation. (Contributed by NM, 9-Jun-2013.)
$/\$

Theorem	erngmul 36003	Ring addition operation. (Contributed by NM, 10-Jun-2013.)
$/\$ $/\$ $/\$

Theorem	erngfset-rN 36004*	The division rings on trace-preserving endomorphisms for a lattice . (Contributed by NM, 8-Jun-2013.) (New usage is discouraged.)


Theorem	erngset-rN 36005*	The division ring on trace-preserving endomorphisms for a fiducial co-atom . (Contributed by NM, 5-Jun-2013.) (New usage is discouraged.)
$/\$

Theorem	erngbase-rN 36006	The base set of the division ring on trace-preserving endomorphisms is the set of all trace-preserving endomorphisms (for a fiducial co-atom ). (Contributed by NM, 9-Jun-2013.) (New usage is discouraged.)
$/\$

Theorem	erngfplus-rN 36007*	Ring addition operation. (Contributed by NM, 9-Jun-2013.) (New usage is discouraged.)
$/\$

Theorem	erngplus-rN 36008*	Ring addition operation. (Contributed by NM, 10-Jun-2013.) (New usage is discouraged.)
$/\$ $/\$ $/\$

Theorem	erngplus2-rN 36009	Ring addition operation. (Contributed by NM, 10-Jun-2013.) (New usage is discouraged.)
$/\$ $/\$ $/\$ $/\$

Theorem	erngfmul-rN 36010*	Ring multiplication operation. (Contributed by NM, 9-Jun-2013.) (New usage is discouraged.)
$/\$

Theorem	erngmul-rN 36011	Ring addition operation. (Contributed by NM, 10-Jun-2013.) (New usage is discouraged.)
$/\$ $/\$ $/\$

Theorem	cdlemh1 36012	Part of proof of Lemma H of [Crawley] p. 118. (Contributed by NM, 17-Jun-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$

Theorem	cdlemh2 36013	Part of proof of Lemma H of [Crawley] p. 118. (Contributed by NM, 16-Jun-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $./\$

Theorem	cdlemh 36014	Lemma H of [Crawley] p. 118. (Contributed by NM, 17-Jun-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemi1 36015	Part of proof of Lemma I of [Crawley] p. 118. (Contributed by NM, 18-Jun-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$

Theorem	cdlemi2 36016	Part of proof of Lemma I of [Crawley] p. 118. (Contributed by NM, 18-Jun-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$

Theorem	cdlemi 36017	Lemma I of [Crawley] p. 118. (Contributed by NM, 19-Jun-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemj1 36018	Part of proof of Lemma J of [Crawley] p. 118. (Contributed by NM, 19-Jun-2013.)
$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemj2 36019	Part of proof of Lemma J of [Crawley] p. 118. Eliminate . (Contributed by NM, 20-Jun-2013.)
$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemj3 36020	Part of proof of Lemma J of [Crawley] p. 118. Eliminate . (Contributed by NM, 20-Jun-2013.)
$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	tendocan 36021	Cancellation law: if the values of two trace-preserving endormorphisms are equal, so are the endormorphisms. Lemma J of [Crawley] p. 118. (Contributed by NM, 21-Jun-2013.)
$/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	tendoid0 36022*	A trace-preserving endomorphism is the additive identity iff at least one of its values (at a non-identity translation) is the identity translation. (Contributed by NM, 1-Aug-2013.)
$/\$ $/\$ $/\$ $/\$

Theorem	tendo0mul 36023*	Additive identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 1-Aug-2013.)
$/\$ $/\$

Theorem	tendo0mulr 36024*	Additive identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 13-Feb-2014.)
$/\$ $/\$

Theorem	tendo1ne0 36025*	The identity (unity) is not equal to the zero trace-preserving endomorphism. (Contributed by NM, 8-Aug-2013.)
$/\$

Theorem	tendoconid 36026*	The composition (product) of trace-preserving endormorphisms is nonzero when each argument is nonzero. (Contributed by NM, 8-Aug-2013.)
$/\$ $/\$ $/\$ $/\$ $/\$

Theorem	tendotr 36027*	The trace of the value of a non-zero trace-preserving endomorphism equals the trace of the argument. (Contributed by NM, 11-Aug-2013.)
$/\$ $/\$ $/\$ $/\$

Theorem	cdlemk1 36028	Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 22-Jun-2013.)
$.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$

Theorem	cdlemk2 36029	Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 22-Jun-2013.)
$.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$

Theorem	cdlemk3 36030	Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$

Theorem	cdlemk4 36031	Part of proof of Lemma K of [Crawley] p. 118, last line. We use for their h, since is already used. (Contributed by NM, 24-Jun-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$

Theorem	cdlemk5a 36032	Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$

Theorem	cdlemk5 36033	Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 25-Jun-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$

Theorem	cdlemk6 36034	Part of proof of Lemma K of [Crawley] p. 118. Apply dalaw 35083. (Contributed by NM, 25-Jun-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$

Theorem	cdlemk8 36035	Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 26-Jun-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$

Theorem	cdlemk9 36036	Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 29-Jun-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$

Theorem	cdlemk9bN 36037	Part of proof of Lemma K of [Crawley] p. 118. TODO: is this needed? If so, shorten with cdlemk9 36036 if that one is also needed. (Contributed by NM, 28-Jun-2013.) (New usage is discouraged.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$

Theorem	cdlemki 36038*	Part of proof of Lemma K of [Crawley] p. 118. TODO: Eliminate and put into cdlemksel 36042. (Contributed by NM, 25-Jun-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemkvcl 36039	Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 27-Jun-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemk10 36040	Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 29-Jun-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemksv 36041*	Part of proof of Lemma K of [Crawley] p. 118. Value of the sigma(p) function. (Contributed by NM, 26-Jun-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$

Theorem	cdlemksel 36042*	Part of proof of Lemma K of [Crawley] p. 118. Conditions for the sigma(p) function to be a translation. TODO: combine cdlemki 36038? (Contributed by NM, 26-Jun-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemksat 36043*	Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 27-Jun-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemksv2 36044*	Part of proof of Lemma K of [Crawley] p. 118. Value of the sigma(p) function at the fixed parameter. (Contributed by NM, 26-Jun-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$

Theorem	cdlemk7 36045*	Part of proof of Lemma K of [Crawley] p. 118. Line 5, p. 119. (Contributed by NM, 27-Jun-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$

Theorem	cdlemk11 36046*	Part of proof of Lemma K of [Crawley] p. 118. Eq. 3, line 8, p. 119. (Contributed by NM, 29-Jun-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$

Theorem	cdlemk12 36047*	Part of proof of Lemma K of [Crawley] p. 118. Eq. 4, line 10, p. 119. (Contributed by NM, 30-Jun-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$

Theorem	cdlemkoatnle 36048*	Utility lemma. (Contributed by NM, 2-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemk13 36049*	Part of proof of Lemma K of [Crawley] p. 118. Line 13 on p. 119. , are k₁, f₁. (Contributed by NM, 1-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$

Theorem	cdlemkole 36050*	Utility lemma. (Contributed by NM, 2-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$

Theorem	cdlemk14 36051*	Part of proof of Lemma K of [Crawley] p. 118. Line 19 on p. 119. , are k₁, f₁. (Contributed by NM, 1-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$

Theorem	cdlemk15 36052*	Part of proof of Lemma K of [Crawley] p. 118. Line 21 on p. 119. , are k₁, f₁. (Contributed by NM, 1-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$

Theorem	cdlemk16a 36053*	Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$

Theorem	cdlemk16 36054*	Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 1-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$

Theorem	cdlemk17 36055*	Part of proof of Lemma K of [Crawley] p. 118. Line 21 on p. 119. , are k₁, f₁. (Contributed by NM, 1-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$

Theorem	cdlemk1u 36056*	Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$

Theorem	cdlemk5auN 36057*	Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.) (New usage is discouraged.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$

Theorem	cdlemk5u 36058*	Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 4-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$

Theorem	cdlemk6u 36059*	Part of proof of Lemma K of [Crawley] p. 118. Apply dalaw 35083. (Contributed by NM, 4-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$

Theorem	cdlemkj 36060*	Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 2-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemkuvN 36061*	Part of proof of Lemma K of [Crawley] p. 118. Value of the sigma₁ (p) function . (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$

Theorem	cdlemkuel 36062*	Part of proof of Lemma K of [Crawley] p. 118. Conditions for the sigma₁ (p) function to be a translation. TODO: combine cdlemkj 36060? (Contributed by NM, 2-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemkuat 36063*	Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 4-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemkuv2 36064*	Part of proof of Lemma K of [Crawley] p. 118. Line 16 on p. 119 for i = 1, where sigma₁ (p) is , f₁ is , and k₁ is . (Contributed by NM, 2-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$

Theorem	cdlemk18 36065*	Part of proof of Lemma K of [Crawley] p. 118. Line 22 on p. 119. , , , are k, sigma₁ (p), k₁, f₁. (Contributed by NM, 2-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemk19 36066*	Part of proof of Lemma K of [Crawley] p. 118. Line 22 on p. 119. , , , are k, sigma₁ (p), k₁, f₁. (Contributed by NM, 2-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemk7u 36067*	Part of proof of Lemma K of [Crawley] p. 118. Line 5, p. 119 for the sigma₁ case. (Contributed by NM, 3-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$

Theorem	cdlemk11u 36068*	Part of proof of Lemma K of [Crawley] p. 118. Line 17, p. 119, showing Eq. 3 (line 8, p. 119) for the sigma₁ () case. (Contributed by NM, 4-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$

Theorem	cdlemk12u 36069*	Part of proof of Lemma K of [Crawley] p. 118. Line 18, p. 119, showing Eq. 4 (line 10, p. 119) for the sigma₁ () case. (Contributed by NM, 4-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$

Theorem	cdlemk21N 36070*	Part of proof of Lemma K of [Crawley] p. 118. Lines 26-27, p. 119 for i=0 and j=1. (Contributed by NM, 5-Jul-2013.) (New usage is discouraged.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemk20 36071*	Part of proof of Lemma K of [Crawley] p. 118. Line 22, p. 119 for the i=2, j=1 case. Note typo on line 22: f should be f_i. Our , , , , , represent their f₁, f₂, k₁, k₂, sigma₁, sigma₂. (Contributed by NM, 5-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemkoatnle-2N 36072*	Utility lemma. (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemk13-2N 36073*	Part of proof of Lemma K of [Crawley] p. 118. Line 13 on p. 119. , are k₂, f₂. (Contributed by NM, 1-Jul-2013.) (New usage is discouraged.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$

Theorem	cdlemkole-2N 36074*	Utility lemma. (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$

Theorem	cdlemk14-2N 36075*	Part of proof of Lemma K of [Crawley] p. 118. Line 19 on p. 119. , are k₂, f₂. (Contributed by NM, 1-Jul-2013.) (New usage is discouraged.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$

Theorem	cdlemk15-2N 36076*	Part of proof of Lemma K of [Crawley] p. 118. Line 21 on p. 119. , are k₂, f₂. (Contributed by NM, 1-Jul-2013.) (New usage is discouraged.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$

Theorem	cdlemk16-2N 36077*	Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 1-Jul-2013.) (New usage is discouraged.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$

Theorem	cdlemk17-2N 36078*	Part of proof of Lemma K of [Crawley] p. 118. Line 21 on p. 119. , are k₂, f₂. (Contributed by NM, 1-Jul-2013.) (New usage is discouraged.)