Proof of Theorem cdleme22cN
Step | Hyp | Ref
| Expression |
1 | | simp11l 1172 |
. . . . 5
|
2 | | hllat 34650 |
. . . . 5
|
3 | 1, 2 | syl 17 |
. . . 4
|
4 | | simp12l 1174 |
. . . . 5
|
5 | | simp13 1093 |
. . . . 5
|
6 | | eqid 2622 |
. . . . . 6
|
7 | | cdleme22.j |
. . . . . 6
|
8 | | cdleme22.a |
. . . . . 6
|
9 | 6, 7, 8 | hlatjcl 34653 |
. . . . 5
|
10 | 1, 4, 5, 9 | syl3anc 1326 |
. . . 4
|
11 | | simp11r 1173 |
. . . . 5
|
12 | | cdleme22.h |
. . . . . 6
|
13 | 6, 12 | lhpbase 35284 |
. . . . 5
|
14 | 11, 13 | syl 17 |
. . . 4
|
15 | | cdleme22.l |
. . . . 5
|
16 | | cdleme22.m |
. . . . 5
|
17 | 6, 15, 16 | latmle2 17077 |
. . . 4
|
18 | 3, 10, 14, 17 | syl3anc 1326 |
. . 3
|
19 | | simp21r 1179 |
. . 3
|
20 | | nbrne2 4673 |
. . 3
|
21 | 18, 19, 20 | syl2anc 693 |
. 2
|
22 | | simp32l 1186 |
. . . . . . . . . 10
|
23 | 22 | adantr 481 |
. . . . . . . . 9
|
24 | 1 | adantr 481 |
. . . . . . . . . . 11
|
25 | 11 | adantr 481 |
. . . . . . . . . . 11
|
26 | | simpl12 1137 |
. . . . . . . . . . 11
|
27 | | simpl13 1138 |
. . . . . . . . . . 11
|
28 | | simp31l 1184 |
. . . . . . . . . . . 12
|
29 | 28 | adantr 481 |
. . . . . . . . . . 11
|
30 | | simp23l 1182 |
. . . . . . . . . . . 12
|
31 | 30 | adantr 481 |
. . . . . . . . . . 11
|
32 | | simp23r 1183 |
. . . . . . . . . . . 12
|
33 | 32 | adantr 481 |
. . . . . . . . . . 11
|
34 | | simpr 477 |
. . . . . . . . . . 11
|
35 | | eqid 2622 |
. . . . . . . . . . . 12
|
36 | 15, 7, 16, 8, 12, 35 | cdleme22aa 35627 |
. . . . . . . . . . 11
|
37 | 24, 25, 26, 27, 29, 31, 33, 34, 36 | syl233anc 1355 |
. . . . . . . . . 10
|
38 | 37 | oveq2d 6666 |
. . . . . . . . 9
|
39 | 23, 38 | breqtrd 4679 |
. . . . . . . 8
|
40 | | simp32r 1187 |
. . . . . . . . 9
|
41 | 40 | adantr 481 |
. . . . . . . 8
|
42 | | simp21l 1178 |
. . . . . . . . . . 11
|
43 | 6, 8 | atbase 34576 |
. . . . . . . . . . 11
|
44 | 42, 43 | syl 17 |
. . . . . . . . . 10
|
45 | | simp22 1095 |
. . . . . . . . . . 11
|
46 | | simp12r 1175 |
. . . . . . . . . . . 12
|
47 | 15, 7, 16, 8, 12 | lhpat 35329 |
. . . . . . . . . . . 12
|
48 | 1, 11, 4, 46, 5, 28, 47 | syl222anc 1342 |
. . . . . . . . . . 11
|
49 | 6, 7, 8 | hlatjcl 34653 |
. . . . . . . . . . 11
|
50 | 1, 45, 48, 49 | syl3anc 1326 |
. . . . . . . . . 10
|
51 | 6, 15, 16 | latlem12 17078 |
. . . . . . . . . 10
|
52 | 3, 44, 50, 10, 51 | syl13anc 1328 |
. . . . . . . . 9
|
53 | 52 | adantr 481 |
. . . . . . . 8
|
54 | 39, 41, 53 | mpbi2and 956 |
. . . . . . 7
|
55 | | simp31r 1185 |
. . . . . . . . . . . . 13
|
56 | 42, 45, 55 | 3jca 1242 |
. . . . . . . . . . . 12
|
57 | | simp33 1099 |
. . . . . . . . . . . . 13
|
58 | 57, 22, 40 | 3jca 1242 |
. . . . . . . . . . . 12
|
59 | 15, 7, 16, 8, 12 | cdleme22b 35629 |
. . . . . . . . . . . 12
|
60 | 1, 56, 4, 5, 28, 30, 58, 59 | syl232anc 1353 |
. . . . . . . . . . 11
|
61 | | hlatl 34647 |
. . . . . . . . . . . . 13
|
62 | 1, 61 | syl 17 |
. . . . . . . . . . . 12
|
63 | | eqid 2622 |
. . . . . . . . . . . . 13
|
64 | 6, 15, 16, 63, 8 | atnle 34604 |
. . . . . . . . . . . 12
|
65 | 62, 45, 10, 64 | syl3anc 1326 |
. . . . . . . . . . 11
|
66 | 60, 65 | mpbid 222 |
. . . . . . . . . 10
|
67 | 66 | oveq1d 6665 |
. . . . . . . . 9
|
68 | 6, 8 | atbase 34576 |
. . . . . . . . . . 11
|
69 | 45, 68 | syl 17 |
. . . . . . . . . 10
|
70 | 6, 15, 16 | latmle1 17076 |
. . . . . . . . . . 11
|
71 | 3, 10, 14, 70 | syl3anc 1326 |
. . . . . . . . . 10
|
72 | 6, 15, 7, 16, 8 | atmod4i1 35152 |
. . . . . . . . . 10
|
73 | 1, 48, 69, 10, 71, 72 | syl131anc 1339 |
. . . . . . . . 9
|
74 | | hlol 34648 |
. . . . . . . . . . 11
|
75 | 1, 74 | syl 17 |
. . . . . . . . . 10
|
76 | 6, 16 | latmcl 17052 |
. . . . . . . . . . 11
|
77 | 3, 10, 14, 76 | syl3anc 1326 |
. . . . . . . . . 10
|
78 | 6, 7, 63 | olj02 34513 |
. . . . . . . . . 10
|
79 | 75, 77, 78 | syl2anc 693 |
. . . . . . . . 9
|
80 | 67, 73, 79 | 3eqtr3d 2664 |
. . . . . . . 8
|
81 | 80 | adantr 481 |
. . . . . . 7
|
82 | 54, 81 | breqtrd 4679 |
. . . . . 6
|
83 | 15, 8 | atcmp 34598 |
. . . . . . . 8
|
84 | 62, 42, 48, 83 | syl3anc 1326 |
. . . . . . 7
|
85 | 84 | adantr 481 |
. . . . . 6
|
86 | 82, 85 | mpbid 222 |
. . . . 5
|
87 | 86 | eqcomd 2628 |
. . . 4
|
88 | 87 | ex 450 |
. . 3
|
89 | 88 | necon3ad 2807 |
. 2
|
90 | 21, 89 | mpd 15 |
1
|