Proof of Theorem cdlemh
Step | Hyp | Ref
| Expression |
1 | | simp1 1061 |
. . . . 5
|
2 | | simp21l 1178 |
. . . . 5
|
3 | | simp22l 1180 |
. . . . 5
|
4 | | simp23 1096 |
. . . . 5
|
5 | | simp33 1099 |
. . . . 5
|
6 | | cdlemh.b |
. . . . . 6
|
7 | | cdlemh.l |
. . . . . 6
|
8 | | cdlemh.j |
. . . . . 6
|
9 | | cdlemh.m |
. . . . . 6
|
10 | | cdlemh.a |
. . . . . 6
|
11 | | cdlemh.h |
. . . . . 6
|
12 | | cdlemh.t |
. . . . . 6
|
13 | | cdlemh.r |
. . . . . 6
|
14 | | cdlemh.s |
. . . . . 6
|
15 | 6, 7, 8, 9, 10, 11, 12, 13, 14 | cdlemh1 36103 |
. . . . 5
|
16 | 1, 2, 3, 4, 5, 15 | syl122anc 1335 |
. . . 4
|
17 | | oveq1 6657 |
. . . . . . . 8
|
18 | | simp11l 1172 |
. . . . . . . . . 10
|
19 | | hlol 34648 |
. . . . . . . . . 10
|
20 | 18, 19 | syl 17 |
. . . . . . . . 9
|
21 | | simp11r 1173 |
. . . . . . . . . . . 12
|
22 | 18, 21 | jca 554 |
. . . . . . . . . . 11
|
23 | | simp13 1093 |
. . . . . . . . . . . 12
|
24 | | simp12 1092 |
. . . . . . . . . . . . 13
|
25 | 11, 12 | ltrncnv 35432 |
. . . . . . . . . . . . 13
|
26 | 22, 24, 25 | syl2anc 693 |
. . . . . . . . . . . 12
|
27 | 23, 26 | jca 554 |
. . . . . . . . . . 11
|
28 | 5 | necomd 2849 |
. . . . . . . . . . . 12
|
29 | 11, 12, 13 | trlcnv 35452 |
. . . . . . . . . . . . 13
|
30 | 22, 24, 29 | syl2anc 693 |
. . . . . . . . . . . 12
|
31 | 28, 30 | neeqtrrd 2868 |
. . . . . . . . . . 11
|
32 | 10, 11, 12, 13 | trlcoat 36011 |
. . . . . . . . . . 11
|
33 | 22, 27, 31, 32 | syl3anc 1326 |
. . . . . . . . . 10
|
34 | 6, 10 | atbase 34576 |
. . . . . . . . . 10
|
35 | 33, 34 | syl 17 |
. . . . . . . . 9
|
36 | | eqid 2622 |
. . . . . . . . . 10
|
37 | 6, 8, 36 | olj02 34513 |
. . . . . . . . 9
|
38 | 20, 35, 37 | syl2anc 693 |
. . . . . . . 8
|
39 | 17, 38 | sylan9eqr 2678 |
. . . . . . 7
|
40 | 11, 12 | ltrnco 36007 |
. . . . . . . . . . . . . 14
|
41 | 22, 23, 26, 40 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
42 | 7, 11, 12, 13 | trlle 35471 |
. . . . . . . . . . . . 13
|
43 | 22, 41, 42 | syl2anc 693 |
. . . . . . . . . . . 12
|
44 | | simp22r 1181 |
. . . . . . . . . . . 12
|
45 | | nbrne2 4673 |
. . . . . . . . . . . . 13
|
46 | 45 | necomd 2849 |
. . . . . . . . . . . 12
|
47 | 43, 44, 46 | syl2anc 693 |
. . . . . . . . . . 11
|
48 | | eqid 2622 |
. . . . . . . . . . . 12
|
49 | 8, 10, 48 | llni2 34798 |
. . . . . . . . . . 11
|
50 | 18, 3, 33, 47, 49 | syl31anc 1329 |
. . . . . . . . . 10
|
51 | 10, 48 | llnneat 34800 |
. . . . . . . . . 10
|
52 | 18, 50, 51 | syl2anc 693 |
. . . . . . . . 9
|
53 | | nelne2 2891 |
. . . . . . . . 9
|
54 | 33, 52, 53 | syl2anc 693 |
. . . . . . . 8
|
55 | 54 | adantr 481 |
. . . . . . 7
|
56 | 39, 55 | eqnetrd 2861 |
. . . . . 6
|
57 | 56 | ex 450 |
. . . . 5
|
58 | 57 | necon2d 2817 |
. . . 4
|
59 | 16, 58 | mpd 15 |
. . 3
|
60 | | simp32 1098 |
. . . . . . . 8
|
61 | 6, 10, 11, 12, 13 | trlnidat 35460 |
. . . . . . . 8
|
62 | 22, 23, 60, 61 | syl3anc 1326 |
. . . . . . 7
|
63 | 7, 8, 10 | hlatlej2 34662 |
. . . . . . . . 9
|
64 | 18, 2, 62, 63 | syl3anc 1326 |
. . . . . . . 8
|
65 | | simp22 1095 |
. . . . . . . . 9
|
66 | | simp31 1097 |
. . . . . . . . . . 11
|
67 | 6, 11, 12 | ltrncnvnid 35413 |
. . . . . . . . . . 11
|
68 | 22, 24, 66, 67 | syl3anc 1326 |
. . . . . . . . . 10
|
69 | 6, 11, 12, 13 | trlcone 36016 |
. . . . . . . . . . 11
|
70 | 69 | necomd 2849 |
. . . . . . . . . 10
|
71 | 22, 23, 26, 31, 68, 70 | syl122anc 1335 |
. . . . . . . . 9
|
72 | 7, 11, 12, 13 | trlle 35471 |
. . . . . . . . . 10
|
73 | 22, 23, 72 | syl2anc 693 |
. . . . . . . . 9
|
74 | 7, 8, 10, 11 | lhp2atnle 35319 |
. . . . . . . . 9
|
75 | 22, 65, 71, 33, 43, 62, 73, 74 | syl322anc 1354 |
. . . . . . . 8
|
76 | | nbrne1 4672 |
. . . . . . . 8
|
77 | 64, 75, 76 | syl2anc 693 |
. . . . . . 7
|
78 | 8, 9, 36, 10 | 2atmat0 34812 |
. . . . . . 7
|
79 | 18, 2, 62, 3, 33, 77, 78 | syl33anc 1341 |
. . . . . 6
|
80 | 14 | eleq1i 2692 |
. . . . . . 7
|
81 | 14 | eqeq1i 2627 |
. . . . . . 7
|
82 | 80, 81 | orbi12i 543 |
. . . . . 6
|
83 | 79, 82 | sylibr 224 |
. . . . 5
|
84 | 83 | ord 392 |
. . . 4
|
85 | 84 | necon1ad 2811 |
. . 3
|
86 | 59, 85 | mpd 15 |
. 2
|
87 | | simp21 1094 |
. . . . 5
|
88 | 87, 65 | jca 554 |
. . . 4
|
89 | 6, 7, 8, 9, 10, 11, 12, 13, 14, 36 | cdlemh2 36104 |
. . . 4
|
90 | 88, 89 | syld3an2 1373 |
. . 3
|
91 | 7, 9, 36, 10, 11 | lhpmatb 35317 |
. . . 4
|
92 | 18, 21, 86, 91 | syl21anc 1325 |
. . 3
|
93 | 90, 92 | mpbird 247 |
. 2
|
94 | 86, 93 | jca 554 |
1
|