Description: Part of proof of Lemma E in Crawley p. 113, last paragraph on p. 115, 3rd line. D , F , N , E , B , Z represent s_2, f(s), f_s(r), z_2, f(z), f_z(r) respectively. We prove f_s(r) = f_z(r). (Contributed by NM, 29-Nov-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cdleme21.l | |
|
cdleme21.j | |
||
cdleme21.m | |
||
cdleme21.a | |
||
cdleme21.h | |
||
cdleme21.u | |
||
cdleme21.f | |
||
cdleme21.b | |
||
cdleme21.d | |
||
cdleme21.e | |
||
cdleme21d.n | |
||
cdleme21d.z | |
||
Assertion | cdleme21d | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdleme21.l | |
|
2 | cdleme21.j | |
|
3 | cdleme21.m | |
|
4 | cdleme21.a | |
|
5 | cdleme21.h | |
|
6 | cdleme21.u | |
|
7 | cdleme21.f | |
|
8 | cdleme21.b | |
|
9 | cdleme21.d | |
|
10 | cdleme21.e | |
|
11 | cdleme21d.n | |
|
12 | cdleme21d.z | |
|
13 | simp11 | |
|
14 | simp12 | |
|
15 | simp13 | |
|
16 | simp2l | |
|
17 | simp2r | |
|
18 | simp33l | |
|
19 | simp31 | |
|
20 | simp11l | |
|
21 | simp12l | |
|
22 | simp13l | |
|
23 | simp2rl | |
|
24 | simp32l | |
|
25 | 18 | simpld | |
26 | simp33r | |
|
27 | 1 2 4 | cdleme21a | |
28 | 20 21 22 23 24 25 26 27 | syl322anc | |
29 | 19 28 | jca | |
30 | 1 2 4 | cdleme21b | |
31 | 20 21 22 23 19 24 25 26 30 | syl332anc | |
32 | simp32r | |
|
33 | 24 31 32 | 3jca | |
34 | 1 2 3 4 5 6 | cdleme21c | |
35 | 13 14 22 23 19 24 25 26 34 | syl332anc | |
36 | eqid | |
|
37 | 1 2 3 4 5 6 7 8 9 10 36 11 12 | cdleme20 | |
38 | 13 14 15 16 17 18 29 33 35 37 | syl333anc | |