Proof of Theorem cdleme20j
Step | Hyp | Ref
| Expression |
1 | | simp33 1099 |
. 2
|
2 | | simp11l 1172 |
. . . . . . . . . 10
|
3 | | simp22l 1180 |
. . . . . . . . . 10
|
4 | | simp21l 1178 |
. . . . . . . . . . 11
|
5 | | eqid 2622 |
. . . . . . . . . . . 12
|
6 | | cdleme19.j |
. . . . . . . . . . . 12
|
7 | | cdleme19.a |
. . . . . . . . . . . 12
|
8 | 5, 6, 7 | hlatjcl 34653 |
. . . . . . . . . . 11
|
9 | 2, 4, 3, 8 | syl3anc 1326 |
. . . . . . . . . 10
|
10 | | simp11r 1173 |
. . . . . . . . . . 11
|
11 | | cdleme19.h |
. . . . . . . . . . . 12
|
12 | 5, 11 | lhpbase 35284 |
. . . . . . . . . . 11
|
13 | 10, 12 | syl 17 |
. . . . . . . . . 10
|
14 | | cdleme19.l |
. . . . . . . . . . . 12
|
15 | 14, 6, 7 | hlatlej2 34662 |
. . . . . . . . . . 11
|
16 | 2, 4, 3, 15 | syl3anc 1326 |
. . . . . . . . . 10
|
17 | | cdleme19.m |
. . . . . . . . . . 11
|
18 | 5, 14, 6, 17, 7 | atmod2i1 35147 |
. . . . . . . . . 10
|
19 | 2, 3, 9, 13, 16, 18 | syl131anc 1339 |
. . . . . . . . 9
|
20 | | simp22 1095 |
. . . . . . . . . . 11
|
21 | | eqid 2622 |
. . . . . . . . . . . 12
|
22 | 14, 6, 21, 7, 11 | lhpjat1 35306 |
. . . . . . . . . . 11
|
23 | 2, 10, 20, 22 | syl21anc 1325 |
. . . . . . . . . 10
|
24 | 23 | oveq2d 6666 |
. . . . . . . . 9
|
25 | | hlol 34648 |
. . . . . . . . . . 11
|
26 | 2, 25 | syl 17 |
. . . . . . . . . 10
|
27 | 5, 17, 21 | olm11 34514 |
. . . . . . . . . 10
|
28 | 26, 9, 27 | syl2anc 693 |
. . . . . . . . 9
|
29 | 19, 24, 28 | 3eqtrd 2660 |
. . . . . . . 8
|
30 | 29 | adantr 481 |
. . . . . . 7
|
31 | | cdleme19.d |
. . . . . . . . . 10
|
32 | | cdleme20.v |
. . . . . . . . . . 11
|
33 | | simp1 1061 |
. . . . . . . . . . . . . . . 16
|
34 | | simp23 1096 |
. . . . . . . . . . . . . . . 16
|
35 | | simp21 1094 |
. . . . . . . . . . . . . . . 16
|
36 | | simp31 1097 |
. . . . . . . . . . . . . . . 16
|
37 | | simp321 1211 |
. . . . . . . . . . . . . . . . 17
|
38 | | simp322 1212 |
. . . . . . . . . . . . . . . . 17
|
39 | 37, 38 | jca 554 |
. . . . . . . . . . . . . . . 16
|
40 | | simp323 1213 |
. . . . . . . . . . . . . . . 16
|
41 | | cdleme19.u |
. . . . . . . . . . . . . . . . 17
|
42 | | cdleme19.f |
. . . . . . . . . . . . . . . . 17
|
43 | | cdleme19.g |
. . . . . . . . . . . . . . . . 17
|
44 | | cdleme19.y |
. . . . . . . . . . . . . . . . 17
|
45 | 14, 6, 17, 7, 11, 41, 42, 43, 31, 44, 32 | cdleme20d 35600 |
. . . . . . . . . . . . . . . 16
|
46 | 33, 20, 34, 35, 36, 39, 40, 45 | syl133anc 1349 |
. . . . . . . . . . . . . . 15
|
47 | | hllat 34650 |
. . . . . . . . . . . . . . . . 17
|
48 | 2, 47 | syl 17 |
. . . . . . . . . . . . . . . 16
|
49 | | simp12l 1174 |
. . . . . . . . . . . . . . . . . 18
|
50 | | simp13l 1176 |
. . . . . . . . . . . . . . . . . 18
|
51 | 14, 6, 17, 7, 11, 41, 42, 5 | cdleme1b 35513 |
. . . . . . . . . . . . . . . . . 18
|
52 | 2, 10, 49, 50, 3, 51 | syl23anc 1333 |
. . . . . . . . . . . . . . . . 17
|
53 | | simp23l 1182 |
. . . . . . . . . . . . . . . . . 18
|
54 | 14, 6, 17, 7, 11, 41, 43, 5 | cdleme1b 35513 |
. . . . . . . . . . . . . . . . . 18
|
55 | 2, 10, 49, 50, 53, 54 | syl23anc 1333 |
. . . . . . . . . . . . . . . . 17
|
56 | 5, 6 | latjcl 17051 |
. . . . . . . . . . . . . . . . 17
|
57 | 48, 52, 55, 56 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
|
58 | | simp22r 1181 |
. . . . . . . . . . . . . . . . . 18
|
59 | 14, 6, 17, 7, 11, 31 | cdlemeda 35585 |
. . . . . . . . . . . . . . . . . 18
|
60 | 2, 10, 3, 58, 4, 40, 37, 59 | syl223anc 1352 |
. . . . . . . . . . . . . . . . 17
|
61 | | simp23r 1183 |
. . . . . . . . . . . . . . . . . 18
|
62 | 14, 6, 17, 7, 11, 44 | cdlemeda 35585 |
. . . . . . . . . . . . . . . . . 18
|
63 | 2, 10, 53, 61, 4, 40, 38, 62 | syl223anc 1352 |
. . . . . . . . . . . . . . . . 17
|
64 | 5, 6, 7 | hlatjcl 34653 |
. . . . . . . . . . . . . . . . 17
|
65 | 2, 60, 63, 64 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
|
66 | 5, 14, 17 | latmle2 17077 |
. . . . . . . . . . . . . . . 16
|
67 | 48, 57, 65, 66 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
|
68 | 46, 67 | eqbrtrrd 4677 |
. . . . . . . . . . . . . 14
|
69 | 68 | adantr 481 |
. . . . . . . . . . . . 13
|
70 | 6, 7 | hlatjidm 34655 |
. . . . . . . . . . . . . . 15
|
71 | 2, 60, 70 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
72 | | oveq2 6658 |
. . . . . . . . . . . . . 14
|
73 | 71, 72 | sylan9req 2677 |
. . . . . . . . . . . . 13
|
74 | 69, 73 | breqtrrd 4681 |
. . . . . . . . . . . 12
|
75 | | hlatl 34647 |
. . . . . . . . . . . . . . 15
|
76 | 2, 75 | syl 17 |
. . . . . . . . . . . . . 14
|
77 | | simp31r 1185 |
. . . . . . . . . . . . . . 15
|
78 | 14, 6, 17, 7, 11, 32 | lhpat2 35331 |
. . . . . . . . . . . . . . 15
|
79 | 2, 10, 3, 58, 53, 77, 78 | syl222anc 1342 |
. . . . . . . . . . . . . 14
|
80 | 14, 7 | atcmp 34598 |
. . . . . . . . . . . . . 14
|
81 | 76, 79, 60, 80 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
82 | 81 | adantr 481 |
. . . . . . . . . . . 12
|
83 | 74, 82 | mpbid 222 |
. . . . . . . . . . 11
|
84 | 32, 83 | syl5reqr 2671 |
. . . . . . . . . 10
|
85 | 31, 84 | syl5eqr 2670 |
. . . . . . . . 9
|
86 | 5, 6, 7 | hlatjcl 34653 |
. . . . . . . . . . . 12
|
87 | 2, 3, 53, 86 | syl3anc 1326 |
. . . . . . . . . . 11
|
88 | 5, 14, 17 | latmle1 17076 |
. . . . . . . . . . 11
|
89 | 48, 87, 13, 88 | syl3anc 1326 |
. . . . . . . . . 10
|
90 | 89 | adantr 481 |
. . . . . . . . 9
|
91 | 85, 90 | eqbrtrd 4675 |
. . . . . . . 8
|
92 | 14, 6, 7 | hlatlej1 34661 |
. . . . . . . . . 10
|
93 | 2, 3, 53, 92 | syl3anc 1326 |
. . . . . . . . 9
|
94 | 93 | adantr 481 |
. . . . . . . 8
|
95 | 5, 17 | latmcl 17052 |
. . . . . . . . . . 11
|
96 | 48, 9, 13, 95 | syl3anc 1326 |
. . . . . . . . . 10
|
97 | 5, 7 | atbase 34576 |
. . . . . . . . . . 11
|
98 | 3, 97 | syl 17 |
. . . . . . . . . 10
|
99 | 5, 14, 6 | latjle12 17062 |
. . . . . . . . . 10
|
100 | 48, 96, 98, 87, 99 | syl13anc 1328 |
. . . . . . . . 9
|
101 | 100 | adantr 481 |
. . . . . . . 8
|
102 | 91, 94, 101 | mpbi2and 956 |
. . . . . . 7
|
103 | 30, 102 | eqbrtrrd 4677 |
. . . . . 6
|
104 | 5, 7 | atbase 34576 |
. . . . . . . . 9
|
105 | 4, 104 | syl 17 |
. . . . . . . 8
|
106 | 5, 14, 6 | latjle12 17062 |
. . . . . . . 8
|
107 | 48, 105, 98, 87, 106 | syl13anc 1328 |
. . . . . . 7
|
108 | 107 | adantr 481 |
. . . . . 6
|
109 | 103, 108 | mpbird 247 |
. . . . 5
|
110 | 109 | simpld 475 |
. . . 4
|
111 | 110 | ex 450 |
. . 3
|
112 | 111 | necon3bd 2808 |
. 2
|
113 | 1, 112 | mpd 15 |
1
|