Proof of Theorem cdlemk12u
Step | Hyp | Ref
| Expression |
1 | | simp11l 1172 |
. 2
|
2 | | simp22l 1180 |
. 2
|
3 | | simp11 1091 |
. . 3
|
4 | | simp212 1200 |
. . 3
|
5 | | cdlemk1.l |
. . . 4
|
6 | | cdlemk1.a |
. . . 4
|
7 | | cdlemk1.h |
. . . 4
|
8 | | cdlemk1.t |
. . . 4
|
9 | 5, 6, 7, 8 | ltrnat 35426 |
. . 3
|
10 | 3, 4, 2, 9 | syl3anc 1326 |
. 2
|
11 | | simp23 1096 |
. . 3
|
12 | | simp213 1201 |
. . 3
|
13 | | simp12 1092 |
. . 3
|
14 | | simp13 1093 |
. . 3
|
15 | | simp211 1199 |
. . 3
|
16 | | simp331 1214 |
. . . 4
|
17 | | simp333 1216 |
. . . . 5
|
18 | 17 | necomd 2849 |
. . . 4
|
19 | 16, 18 | jca 554 |
. . 3
|
20 | | simp311 1208 |
. . . 4
|
21 | | simp32l 1186 |
. . . 4
|
22 | | simp312 1209 |
. . . 4
|
23 | 20, 21, 22 | 3jca 1242 |
. . 3
|
24 | | simp22 1095 |
. . 3
|
25 | | cdlemk1.b |
. . . 4
|
26 | | cdlemk1.j |
. . . 4
|
27 | | cdlemk1.m |
. . . 4
|
28 | | cdlemk1.r |
. . . 4
|
29 | | cdlemk1.s |
. . . 4
|
30 | | cdlemk1.o |
. . . 4
|
31 | | cdlemk1.u |
. . . 4
|
32 | 25, 5, 26, 27, 6, 7, 8, 28, 29, 30, 31 | cdlemkuat 36154 |
. . 3
|
33 | 3, 11, 12, 13, 14, 15, 19, 23, 24, 32 | syl333anc 1358 |
. 2
|
34 | | simp32r 1187 |
. . . 4
|
35 | 34 | necomd 2849 |
. . 3
|
36 | 6, 7, 8, 28 | trlcocnvat 36012 |
. . 3
|
37 | 3, 12, 4, 35, 36 | syl121anc 1331 |
. 2
|
38 | | simp332 1215 |
. . . . 5
|
39 | 38 | necomd 2849 |
. . . 4
|
40 | 16, 39 | jca 554 |
. . 3
|
41 | | simp313 1210 |
. . . 4
|
42 | 20, 41, 22 | 3jca 1242 |
. . 3
|
43 | 25, 5, 26, 27, 6, 7, 8, 28, 29, 30, 31 | cdlemkuat 36154 |
. . 3
|
44 | 3, 11, 4, 13, 14, 15, 40, 42, 24, 43 | syl333anc 1358 |
. 2
|
45 | 25, 5, 26, 27, 6, 7, 8, 28, 29, 30, 31 | cdlemkuv2 36155 |
. . . . 5
|
46 | 3, 11, 4, 13, 14, 15, 40, 42, 24, 45 | syl333anc 1358 |
. . . 4
|
47 | | hllat 34650 |
. . . . . 6
|
48 | 1, 47 | syl 17 |
. . . . 5
|
49 | 25, 6, 7, 8, 28 | trlnidat 35460 |
. . . . . . 7
|
50 | 3, 4, 41, 49 | syl3anc 1326 |
. . . . . 6
|
51 | 25, 26, 6 | hlatjcl 34653 |
. . . . . 6
|
52 | 1, 2, 50, 51 | syl3anc 1326 |
. . . . 5
|
53 | | simp1 1061 |
. . . . . . 7
|
54 | 15, 24, 11 | 3jca 1242 |
. . . . . . 7
|
55 | 25, 5, 26, 27, 6, 7, 8, 28, 29, 30 | cdlemkoatnle 36139 |
. . . . . . . 8
|
56 | 55 | simpld 475 |
. . . . . . 7
|
57 | 53, 54, 20, 22, 16, 56 | syl113anc 1338 |
. . . . . 6
|
58 | 6, 7, 8, 28 | trlcocnvat 36012 |
. . . . . . 7
|
59 | 3, 4, 14, 38, 58 | syl121anc 1331 |
. . . . . 6
|
60 | 25, 26, 6 | hlatjcl 34653 |
. . . . . 6
|
61 | 1, 57, 59, 60 | syl3anc 1326 |
. . . . 5
|
62 | 25, 5, 27 | latmle1 17076 |
. . . . 5
|
63 | 48, 52, 61, 62 | syl3anc 1326 |
. . . 4
|
64 | 46, 63 | eqbrtrd 4675 |
. . 3
|
65 | 5, 26, 6, 7, 8, 28 | trljat1 35453 |
. . . 4
|
66 | 3, 4, 24, 65 | syl3anc 1326 |
. . 3
|
67 | 64, 66 | breqtrd 4679 |
. 2
|
68 | | simp2 1062 |
. . 3
|
69 | | simp31 1097 |
. . 3
|
70 | | simp33 1099 |
. . 3
|
71 | | eqid 2622 |
. . . 4
|
72 | 25, 5, 26, 27, 6, 7, 8, 28, 29, 30, 31, 71 | cdlemk11u 36159 |
. . 3
|
73 | 53, 68, 69, 21, 70, 72 | syl113anc 1338 |
. 2
|
74 | 5, 26, 6 | hlatlej2 34662 |
. . . . 5
|
75 | 1, 2, 50, 74 | syl3anc 1326 |
. . . 4
|
76 | 75, 66 | breqtrd 4679 |
. . 3
|
77 | 25, 5, 26, 27, 6, 7, 8, 28, 29, 30, 31 | cdlemkuel 36153 |
. . . . . 6
|
78 | 3, 11, 12, 13, 14, 15, 19, 23, 24, 77 | syl333anc 1358 |
. . . . 5
|
79 | 5, 6, 7, 8 | ltrnel 35425 |
. . . . 5
|
80 | 3, 78, 24, 79 | syl3anc 1326 |
. . . 4
|
81 | 7, 8 | ltrncnv 35432 |
. . . . . . . 8
|
82 | 3, 4, 81 | syl2anc 693 |
. . . . . . 7
|
83 | 7, 8, 28 | trlcnv 35452 |
. . . . . . . . 9
|
84 | 3, 4, 83 | syl2anc 693 |
. . . . . . . 8
|
85 | 84, 34 | eqnetrd 2861 |
. . . . . . 7
|
86 | 25, 7, 8, 28 | trlcone 36016 |
. . . . . . 7
|
87 | 3, 82, 12, 85, 21, 86 | syl122anc 1335 |
. . . . . 6
|
88 | 87 | necomd 2849 |
. . . . 5
|
89 | 7, 8 | ltrncom 36026 |
. . . . . . 7
|
90 | 3, 82, 12, 89 | syl3anc 1326 |
. . . . . 6
|
91 | 90 | fveq2d 6195 |
. . . . 5
|
92 | 88, 91, 84 | 3netr3d 2870 |
. . . 4
|
93 | 7, 8 | ltrnco 36007 |
. . . . . 6
|
94 | 3, 12, 82, 93 | syl3anc 1326 |
. . . . 5
|
95 | 5, 7, 8, 28 | trlle 35471 |
. . . . 5
|
96 | 3, 94, 95 | syl2anc 693 |
. . . 4
|
97 | 5, 7, 8, 28 | trlle 35471 |
. . . . 5
|
98 | 3, 4, 97 | syl2anc 693 |
. . . 4
|
99 | 5, 26, 6, 7 | lhp2atnle 35319 |
. . . 4
|
100 | 3, 80, 92, 37, 96, 50, 98, 99 | syl322anc 1354 |
. . 3
|
101 | | nbrne1 4672 |
. . 3
|
102 | 76, 100, 101 | syl2anc 693 |
. 2
|
103 | 5, 26, 27, 6 | 2atm 34813 |
. 2
|
104 | 1, 2, 10, 33, 37, 44, 67, 73, 102, 103 | syl333anc 1358 |
1
|