Proof of Theorem cdlemk12
Step | Hyp | Ref
| Expression |
1 | | simp11l 1172 |
. 2
|
2 | | simp22l 1180 |
. 2
|
3 | | simp11 1091 |
. . 3
|
4 | | simp13 1093 |
. . 3
|
5 | | cdlemk.l |
. . . 4
|
6 | | cdlemk.a |
. . . 4
|
7 | | cdlemk.h |
. . . 4
|
8 | | cdlemk.t |
. . . 4
|
9 | 5, 6, 7, 8 | ltrnat 35426 |
. . 3
|
10 | 3, 4, 2, 9 | syl3anc 1326 |
. 2
|
11 | | simp12 1092 |
. . . 4
|
12 | | simp21r 1179 |
. . . 4
|
13 | 3, 11, 12 | 3jca 1242 |
. . 3
|
14 | | simp21l 1178 |
. . . 4
|
15 | | simp22 1095 |
. . . 4
|
16 | | simp23 1096 |
. . . 4
|
17 | 14, 15, 16 | 3jca 1242 |
. . 3
|
18 | | simp311 1208 |
. . 3
|
19 | | simp313 1210 |
. . 3
|
20 | | simp32r 1187 |
. . 3
|
21 | | cdlemk.b |
. . . 4
|
22 | | cdlemk.j |
. . . 4
|
23 | | cdlemk.r |
. . . 4
|
24 | | cdlemk.m |
. . . 4
|
25 | | cdlemk.s |
. . . 4
|
26 | 21, 5, 22, 6, 7, 8,
23, 24, 25 | cdlemksat 36134 |
. . 3
|
27 | 13, 17, 18, 19, 20, 26 | syl113anc 1338 |
. 2
|
28 | | simp33 1099 |
. . . 4
|
29 | 28 | necomd 2849 |
. . 3
|
30 | 6, 7, 8, 23 | trlcocnvat 36012 |
. . 3
|
31 | 3, 12, 4, 29, 30 | syl121anc 1331 |
. 2
|
32 | | simp1 1061 |
. . 3
|
33 | | simp312 1209 |
. . 3
|
34 | | simp32l 1186 |
. . 3
|
35 | 21, 5, 22, 6, 7, 8,
23, 24, 25 | cdlemksat 36134 |
. . 3
|
36 | 32, 17, 18, 33, 34, 35 | syl113anc 1338 |
. 2
|
37 | 21, 5, 22, 6, 7, 8,
23, 24, 25 | cdlemksv2 36135 |
. . . . 5
|
38 | 32, 17, 18, 33, 34, 37 | syl113anc 1338 |
. . . 4
|
39 | | hllat 34650 |
. . . . . 6
|
40 | 1, 39 | syl 17 |
. . . . 5
|
41 | 21, 6, 7, 8, 23 | trlnidat 35460 |
. . . . . . 7
|
42 | 3, 4, 33, 41 | syl3anc 1326 |
. . . . . 6
|
43 | 21, 22, 6 | hlatjcl 34653 |
. . . . . 6
|
44 | 1, 2, 42, 43 | syl3anc 1326 |
. . . . 5
|
45 | 5, 6, 7, 8 | ltrnat 35426 |
. . . . . . 7
|
46 | 3, 14, 2, 45 | syl3anc 1326 |
. . . . . 6
|
47 | 6, 7, 8, 23 | trlcocnvat 36012 |
. . . . . . 7
|
48 | 3, 4, 11, 34, 47 | syl121anc 1331 |
. . . . . 6
|
49 | 21, 22, 6 | hlatjcl 34653 |
. . . . . 6
|
50 | 1, 46, 48, 49 | syl3anc 1326 |
. . . . 5
|
51 | 21, 5, 24 | latmle1 17076 |
. . . . 5
|
52 | 40, 44, 50, 51 | syl3anc 1326 |
. . . 4
|
53 | 38, 52 | eqbrtrd 4675 |
. . 3
|
54 | 5, 22, 6, 7, 8, 23 | trljat1 35453 |
. . . 4
|
55 | 3, 4, 15, 54 | syl3anc 1326 |
. . 3
|
56 | 53, 55 | breqtrd 4679 |
. 2
|
57 | | simp2 1062 |
. . 3
|
58 | | simp31 1097 |
. . 3
|
59 | | eqid 2622 |
. . . 4
|
60 | 21, 5, 22, 6, 7, 8,
23, 24, 25, 59 | cdlemk11 36137 |
. . 3
|
61 | 32, 57, 58, 34, 20, 60 | syl113anc 1338 |
. 2
|
62 | 5, 22, 6 | hlatlej2 34662 |
. . . . 5
|
63 | 1, 2, 42, 62 | syl3anc 1326 |
. . . 4
|
64 | 63, 55 | breqtrd 4679 |
. . 3
|
65 | 21, 5, 22, 6, 7, 8,
23, 24, 25 | cdlemksel 36133 |
. . . . . 6
|
66 | 13, 17, 18, 19, 20, 65 | syl113anc 1338 |
. . . . 5
|
67 | 5, 6, 7, 8 | ltrnel 35425 |
. . . . 5
|
68 | 3, 66, 15, 67 | syl3anc 1326 |
. . . 4
|
69 | 7, 8 | ltrncnv 35432 |
. . . . . . . 8
|
70 | 3, 4, 69 | syl2anc 693 |
. . . . . . 7
|
71 | 7, 8, 23 | trlcnv 35452 |
. . . . . . . . 9
|
72 | 3, 4, 71 | syl2anc 693 |
. . . . . . . 8
|
73 | 72, 28 | eqnetrd 2861 |
. . . . . . 7
|
74 | 21, 7, 8, 23 | trlcone 36016 |
. . . . . . 7
|
75 | 3, 70, 12, 73, 19, 74 | syl122anc 1335 |
. . . . . 6
|
76 | 75 | necomd 2849 |
. . . . 5
|
77 | 7, 8 | ltrncom 36026 |
. . . . . . 7
|
78 | 3, 70, 12, 77 | syl3anc 1326 |
. . . . . 6
|
79 | 78 | fveq2d 6195 |
. . . . 5
|
80 | 76, 79, 72 | 3netr3d 2870 |
. . . 4
|
81 | 7, 8 | ltrnco 36007 |
. . . . . 6
|
82 | 3, 12, 70, 81 | syl3anc 1326 |
. . . . 5
|
83 | 5, 7, 8, 23 | trlle 35471 |
. . . . 5
|
84 | 3, 82, 83 | syl2anc 693 |
. . . 4
|
85 | 5, 7, 8, 23 | trlle 35471 |
. . . . 5
|
86 | 3, 4, 85 | syl2anc 693 |
. . . 4
|
87 | 5, 22, 6, 7 | lhp2atnle 35319 |
. . . 4
|
88 | 3, 68, 80, 31, 84, 42, 86, 87 | syl322anc 1354 |
. . 3
|
89 | | nbrne1 4672 |
. . 3
|
90 | 64, 88, 89 | syl2anc 693 |
. 2
|
91 | 5, 22, 24, 6 | 2atm 34813 |
. 2
|
92 | 1, 2, 10, 27, 31, 36, 56, 61, 90, 91 | syl333anc 1358 |
1
|