Proof of Theorem djajN
Step | Hyp | Ref
| Expression |
1 | | hllat 34650 |
. . . . . 6
|
2 | 1 | ad2antrr 762 |
. . . . 5
|
3 | | hlop 34649 |
. . . . . . . . 9
|
4 | 3 | ad2antrr 762 |
. . . . . . . 8
|
5 | | eqid 2622 |
. . . . . . . . . 10
|
6 | | djaj.h |
. . . . . . . . . 10
|
7 | | djaj.i |
. . . . . . . . . 10
|
8 | 5, 6, 7 | diadmclN 36326 |
. . . . . . . . 9
|
9 | 8 | adantrr 753 |
. . . . . . . 8
|
10 | | eqid 2622 |
. . . . . . . . 9
|
11 | 5, 10 | opoccl 34481 |
. . . . . . . 8
|
12 | 4, 9, 11 | syl2anc 693 |
. . . . . . 7
|
13 | 5, 6 | lhpbase 35284 |
. . . . . . . . 9
|
14 | 13 | ad2antlr 763 |
. . . . . . . 8
|
15 | 5, 10 | opoccl 34481 |
. . . . . . . 8
|
16 | 4, 14, 15 | syl2anc 693 |
. . . . . . 7
|
17 | | djaj.k |
. . . . . . . 8
|
18 | 5, 17 | latjcl 17051 |
. . . . . . 7
|
19 | 2, 12, 16, 18 | syl3anc 1326 |
. . . . . 6
|
20 | | eqid 2622 |
. . . . . . 7
|
21 | 5, 20 | latmcl 17052 |
. . . . . 6
|
22 | 2, 19, 14, 21 | syl3anc 1326 |
. . . . 5
|
23 | 5, 6, 7 | diadmclN 36326 |
. . . . . . . . 9
|
24 | 23 | adantrl 752 |
. . . . . . . 8
|
25 | 5, 10 | opoccl 34481 |
. . . . . . . 8
|
26 | 4, 24, 25 | syl2anc 693 |
. . . . . . 7
|
27 | 5, 17 | latjcl 17051 |
. . . . . . 7
|
28 | 2, 26, 16, 27 | syl3anc 1326 |
. . . . . 6
|
29 | 5, 20 | latmcl 17052 |
. . . . . 6
|
30 | 2, 28, 14, 29 | syl3anc 1326 |
. . . . 5
|
31 | 5, 20 | latmcl 17052 |
. . . . 5
|
32 | 2, 22, 30, 31 | syl3anc 1326 |
. . . 4
|
33 | | eqid 2622 |
. . . . 5
|
34 | 5, 33, 20 | latmle2 17077 |
. . . . . 6
|
35 | 2, 22, 30, 34 | syl3anc 1326 |
. . . . 5
|
36 | 5, 33, 20 | latmle2 17077 |
. . . . . 6
|
37 | 2, 28, 14, 36 | syl3anc 1326 |
. . . . 5
|
38 | 5, 33, 2, 32, 30, 14, 35, 37 | lattrd 17058 |
. . . 4
|
39 | 5, 33, 6, 7 | diaeldm 36325 |
. . . . 5
|
40 | 39 | adantr 481 |
. . . 4
|
41 | 32, 38, 40 | mpbir2and 957 |
. . 3
|
42 | | eqid 2622 |
. . . 4
|
43 | | eqid 2622 |
. . . 4
|
44 | 17, 20, 10, 6, 42, 7, 43 | diaocN 36414 |
. . 3
|
45 | 41, 44 | syldan 487 |
. 2
|
46 | | hloml 34644 |
. . . . . 6
|
47 | 46 | ad2antrr 762 |
. . . . 5
|
48 | 5, 17 | latjcl 17051 |
. . . . . 6
|
49 | 2, 9, 24, 48 | syl3anc 1326 |
. . . . 5
|
50 | 33, 6, 7 | diadmleN 36327 |
. . . . . . 7
|
51 | 50 | adantrr 753 |
. . . . . 6
|
52 | 33, 6, 7 | diadmleN 36327 |
. . . . . . 7
|
53 | 52 | adantrl 752 |
. . . . . 6
|
54 | 5, 33, 17 | latjle12 17062 |
. . . . . . 7
|
55 | 2, 9, 24, 14, 54 | syl13anc 1328 |
. . . . . 6
|
56 | 51, 53, 55 | mpbi2and 956 |
. . . . 5
|
57 | 5, 33, 17, 20, 10 | omlspjN 34548 |
. . . . 5
|
58 | 47, 49, 14, 56, 57 | syl121anc 1331 |
. . . 4
|
59 | 5, 17 | latjidm 17074 |
. . . . . . . 8
|
60 | 2, 16, 59 | syl2anc 693 |
. . . . . . 7
|
61 | 60 | oveq2d 6666 |
. . . . . 6
|
62 | 5, 17 | latjass 17095 |
. . . . . . . 8
|
63 | 2, 49, 16, 16, 62 | syl13anc 1328 |
. . . . . . 7
|
64 | | hlol 34648 |
. . . . . . . . . . 11
|
65 | 64 | ad2antrr 762 |
. . . . . . . . . 10
|
66 | 5, 17, 20, 10 | oldmm2 34505 |
. . . . . . . . . 10
|
67 | 65, 49, 14, 66 | syl3anc 1326 |
. . . . . . . . 9
|
68 | 5, 17, 20, 10 | oldmj1 34508 |
. . . . . . . . . . . . . 14
|
69 | 65, 9, 24, 68 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
70 | 5, 33, 20 | latleeqm1 17079 |
. . . . . . . . . . . . . . . . . 18
|
71 | 2, 9, 14, 70 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
|
72 | 51, 71 | mpbid 222 |
. . . . . . . . . . . . . . . 16
|
73 | 72 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
|
74 | 5, 17, 20, 10 | oldmm1 34504 |
. . . . . . . . . . . . . . . 16
|
75 | 65, 9, 14, 74 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
|
76 | 73, 75 | eqtr3d 2658 |
. . . . . . . . . . . . . 14
|
77 | 5, 33, 20 | latleeqm1 17079 |
. . . . . . . . . . . . . . . . . 18
|
78 | 2, 24, 14, 77 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
|
79 | 53, 78 | mpbid 222 |
. . . . . . . . . . . . . . . 16
|
80 | 79 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
|
81 | 5, 17, 20, 10 | oldmm1 34504 |
. . . . . . . . . . . . . . . 16
|
82 | 65, 24, 14, 81 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
|
83 | 80, 82 | eqtr3d 2658 |
. . . . . . . . . . . . . 14
|
84 | 76, 83 | oveq12d 6668 |
. . . . . . . . . . . . 13
|
85 | 69, 84 | eqtrd 2656 |
. . . . . . . . . . . 12
|
86 | 85 | oveq1d 6665 |
. . . . . . . . . . 11
|
87 | 5, 20 | latmmdir 34522 |
. . . . . . . . . . . 12
|
88 | 65, 19, 28, 14, 87 | syl13anc 1328 |
. . . . . . . . . . 11
|
89 | 86, 88 | eqtrd 2656 |
. . . . . . . . . 10
|
90 | 89 | fveq2d 6195 |
. . . . . . . . 9
|
91 | 67, 90 | eqtr3d 2658 |
. . . . . . . 8
|
92 | 91 | oveq1d 6665 |
. . . . . . 7
|
93 | 63, 92 | eqtr3d 2658 |
. . . . . 6
|
94 | 61, 93 | eqtr3d 2658 |
. . . . 5
|
95 | 94 | oveq1d 6665 |
. . . 4
|
96 | 58, 95 | eqtr3d 2658 |
. . 3
|
97 | 96 | fveq2d 6195 |
. 2
|
98 | | simpl 473 |
. . . 4
|
99 | 6, 7 | diaclN 36339 |
. . . . . 6
|
100 | 99 | adantrr 753 |
. . . . 5
|
101 | 6, 42, 7 | diaelrnN 36334 |
. . . . 5
|
102 | 100, 101 | syldan 487 |
. . . 4
|
103 | 6, 7 | diaclN 36339 |
. . . . . 6
|
104 | 103 | adantrl 752 |
. . . . 5
|
105 | 6, 42, 7 | diaelrnN 36334 |
. . . . 5
|
106 | 104, 105 | syldan 487 |
. . . 4
|
107 | | djaj.j |
. . . . 5
|
108 | 6, 42, 7, 43, 107 | djavalN 36424 |
. . . 4
|
109 | 98, 102, 106, 108 | syl12anc 1324 |
. . 3
|
110 | 5, 33, 20 | latmle2 17077 |
. . . . . . . 8
|
111 | 2, 19, 14, 110 | syl3anc 1326 |
. . . . . . 7
|
112 | 5, 33, 6, 7 | diaeldm 36325 |
. . . . . . . 8
|
113 | 112 | adantr 481 |
. . . . . . 7
|
114 | 22, 111, 113 | mpbir2and 957 |
. . . . . 6
|
115 | 5, 33, 6, 7 | diaeldm 36325 |
. . . . . . . 8
|
116 | 115 | adantr 481 |
. . . . . . 7
|
117 | 30, 37, 116 | mpbir2and 957 |
. . . . . 6
|
118 | 20, 6, 7 | diameetN 36345 |
. . . . . 6
|
119 | 98, 114, 117, 118 | syl12anc 1324 |
. . . . 5
|
120 | 17, 20, 10, 6, 42, 7, 43 | diaocN 36414 |
. . . . . . 7
|
121 | 120 | adantrr 753 |
. . . . . 6
|
122 | 17, 20, 10, 6, 42, 7, 43 | diaocN 36414 |
. . . . . . 7
|
123 | 122 | adantrl 752 |
. . . . . 6
|
124 | 121, 123 | ineq12d 3815 |
. . . . 5
|
125 | 119, 124 | eqtrd 2656 |
. . . 4
|
126 | 125 | fveq2d 6195 |
. . 3
|
127 | 109, 126 | eqtr4d 2659 |
. 2
|
128 | 45, 97, 127 | 3eqtr4d 2666 |
1
|