P. 344 of Theorem List - Metamath Proof Explorer

Home	Metamath Proof Explorer Theorem List (p. 344 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 -** 34301-34400 *Has distinct variable group(s)
Type	Label	Description
Statement

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

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

Theorem	tendocan 34303	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 34304*	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 34305*	Additive identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 1-Aug-2013.)
$/\$ $/\$

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

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

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

Theorem	tendotr 34309*	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 34310	Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 22-Jun-2013.)
$.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$

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

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

Theorem	cdlemk4 34313	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 34314	Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$

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

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

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

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

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

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

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

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

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

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

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

Theorem	cdlemksv2 34326*	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 34327*	Part of proof of Lemma K of [Crawley] p. 118. Line 5, p. 119. (Contributed by NM, 27-Jun-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$

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

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

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

Theorem	cdlemk13 34331*	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 34332*	Utility lemma. (Contributed by NM, 2-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$

Theorem	cdlemk14 34333*	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 34334*	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 34335*	Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$

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

Theorem	cdlemk17 34337*	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 34338*	Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$

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

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

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

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

Theorem	cdlemkuvN 34343*	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 34344*	Part of proof of Lemma K of [Crawley] p. 118. Conditions for the sigma₁ (p) function to be a translation. TODO: combine cdlemkj 34342? (Contributed by NM, 2-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

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

Theorem	cdlemkuv2 34346*	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 34347*	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 34348*	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 34349*	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 34350*	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 34351*	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 34352*	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 34353*	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 34354*	Utility lemma. (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemk13-2N 34355*	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 34356*	Utility lemma. (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$

Theorem	cdlemk14-2N 34357*	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 34358*	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 34359*	Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 1-Jul-2013.) (New usage is discouraged.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$

Theorem	cdlemk17-2N 34360*	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	cdlemkj-2N 34361*	Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

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

Theorem	cdlemkuel-2N 34363*	Part of proof of Lemma K of [Crawley] p. 118. Conditions for the sigma₂ (p) function to be a translation. TODO: combine cdlemkj 34342? (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

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

Theorem	cdlemk18-2N 34365*	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.) (New usage is discouraged.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemk19-2N 34366*	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.) (New usage is discouraged.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemk7u-2N 34367*	Part of proof of Lemma K of [Crawley] p. 118. Line 5, p. 119 for the sigma₂ case. (Contributed by NM, 5-Jul-2013.) (New usage is discouraged.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$

Theorem	cdlemk11u-2N 34368*	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, 5-Jul-2013.) (New usage is discouraged.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$