P. 368 of Theorem List - Metamath Proof Explorer

Home	Metamath Proof Explorer Theorem List (p. 368 of 383)	< 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-25962)

Hilbert Space Explorer
(25963-27487)

Users' Mathboxes
(27488-38213)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem	cdlemkuv2 36736*	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 36737*	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 36738*	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 36739*	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 36740*	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 36741*	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 36742*	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 36743*	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 36744*	Utility lemma. (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

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

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

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

Theorem	cdlemkuv-2N 36752*	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 36753*	Part of proof of Lemma K of [Crawley] p. 118. Conditions for the sigma₂ (p) function to be a translation. TODO: combine cdlemkj 36732? (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemkuv2-2 36754*	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 36755*	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 36756*	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 36757*	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 36758*	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.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$

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

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

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