Step | Hyp | Ref
| Expression |
1 | | simplr 792 |
. . . 4
|
2 | | eqid 2622 |
. . . . . 6
|
3 | | eqid 2622 |
. . . . . 6
|
4 | | eqid 2622 |
. . . . . 6
|
5 | | lvolnle3at.v |
. . . . . 6
|
6 | 2, 3, 4, 5 | islvol 34859 |
. . . . 5
|
7 | 6 | ad2antrr 762 |
. . . 4
|
8 | 1, 7 | mpbid 222 |
. . 3
|
9 | 8 | simprd 479 |
. 2
|
10 | | oveq1 6657 |
. . . . . . . . 9
|
11 | 10 | oveq1d 6665 |
. . . . . . . 8
|
12 | 11 | breq2d 4665 |
. . . . . . 7
|
13 | 12 | notbid 308 |
. . . . . 6
|
14 | | simp1l 1085 |
. . . . . . . . . . . 12
|
15 | | simp3l 1089 |
. . . . . . . . . . . 12
|
16 | | simp21 1094 |
. . . . . . . . . . . 12
|
17 | | simp22 1095 |
. . . . . . . . . . . 12
|
18 | | lvolnle3at.l |
. . . . . . . . . . . . 13
|
19 | | lvolnle3at.j |
. . . . . . . . . . . . 13
|
20 | | lvolnle3at.a |
. . . . . . . . . . . . 13
|
21 | 18, 19, 20, 4 | lplnnle2at 34827 |
. . . . . . . . . . . 12
|
22 | 14, 15, 16, 17, 21 | syl13anc 1328 |
. . . . . . . . . . 11
|
23 | 2, 4 | lplnbase 34820 |
. . . . . . . . . . . . . . 15
|
24 | 15, 23 | syl 17 |
. . . . . . . . . . . . . 14
|
25 | | simp1r 1086 |
. . . . . . . . . . . . . . 15
|
26 | 2, 5 | lvolbase 34864 |
. . . . . . . . . . . . . . 15
|
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . 14
|
28 | | simp3r 1090 |
. . . . . . . . . . . . . 14
|
29 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
30 | 2, 29, 3 | cvrlt 34557 |
. . . . . . . . . . . . . 14
|
31 | 14, 24, 27, 28, 30 | syl31anc 1329 |
. . . . . . . . . . . . 13
|
32 | | hlpos 34652 |
. . . . . . . . . . . . . . 15
|
33 | 14, 32 | syl 17 |
. . . . . . . . . . . . . 14
|
34 | 2, 19, 20 | hlatjcl 34653 |
. . . . . . . . . . . . . . 15
|
35 | 14, 16, 17, 34 | syl3anc 1326 |
. . . . . . . . . . . . . 14
|
36 | 2, 18, 29 | pltletr 16971 |
. . . . . . . . . . . . . 14
|
37 | 33, 24, 27, 35, 36 | syl13anc 1328 |
. . . . . . . . . . . . 13
|
38 | 31, 37 | mpand 711 |
. . . . . . . . . . . 12
|
39 | 18, 29 | pltle 16961 |
. . . . . . . . . . . . 13
|
40 | 14, 15, 35, 39 | syl3anc 1326 |
. . . . . . . . . . . 12
|
41 | 38, 40 | syld 47 |
. . . . . . . . . . 11
|
42 | 22, 41 | mtod 189 |
. . . . . . . . . 10
|
43 | 42 | adantr 481 |
. . . . . . . . 9
|
44 | | simprr 796 |
. . . . . . . . . . 11
|
45 | | hllat 34650 |
. . . . . . . . . . . . . 14
|
46 | 14, 45 | syl 17 |
. . . . . . . . . . . . 13
|
47 | | simp23 1096 |
. . . . . . . . . . . . . 14
|
48 | 2, 20 | atbase 34576 |
. . . . . . . . . . . . . 14
|
49 | 47, 48 | syl 17 |
. . . . . . . . . . . . 13
|
50 | 2, 18, 19 | latleeqj2 17064 |
. . . . . . . . . . . . 13
|
51 | 46, 49, 35, 50 | syl3anc 1326 |
. . . . . . . . . . . 12
|
52 | 51 | adantr 481 |
. . . . . . . . . . 11
|
53 | 44, 52 | mpbid 222 |
. . . . . . . . . 10
|
54 | 53 | breq2d 4665 |
. . . . . . . . 9
|
55 | 43, 54 | mtbird 315 |
. . . . . . . 8
|
56 | 55 | anassrs 680 |
. . . . . . 7
|
57 | | simpl1l 1112 |
. . . . . . . . . 10
|
58 | | simpl3l 1116 |
. . . . . . . . . 10
|
59 | | simpl2 1065 |
. . . . . . . . . . 11
|
60 | | simpr 477 |
. . . . . . . . . . 11
|
61 | 18, 19, 20, 4 | lplni2 34823 |
. . . . . . . . . . 11
|
62 | 57, 59, 60, 61 | syl3anc 1326 |
. . . . . . . . . 10
|
63 | 29, 4 | lplnnlt 34851 |
. . . . . . . . . 10
|
64 | 57, 58, 62, 63 | syl3anc 1326 |
. . . . . . . . 9
|
65 | 2, 19 | latjcl 17051 |
. . . . . . . . . . . . 13
|
66 | 46, 35, 49, 65 | syl3anc 1326 |
. . . . . . . . . . . 12
|
67 | 2, 18, 29 | pltletr 16971 |
. . . . . . . . . . . 12
|
68 | 33, 24, 27, 66, 67 | syl13anc 1328 |
. . . . . . . . . . 11
|
69 | 31, 68 | mpand 711 |
. . . . . . . . . 10
|
70 | 69 | adantr 481 |
. . . . . . . . 9
|
71 | 64, 70 | mtod 189 |
. . . . . . . 8
|
72 | 71 | anassrs 680 |
. . . . . . 7
|
73 | 56, 72 | pm2.61dan 832 |
. . . . . 6
|
74 | | eqid 2622 |
. . . . . . . . . 10
|
75 | 74, 19, 20, 4 | lplnnle2at 34827 |
. . . . . . . . 9
|
76 | 14, 15, 17, 47, 75 | syl13anc 1328 |
. . . . . . . 8
|
77 | 2, 19, 20 | hlatjcl 34653 |
. . . . . . . . . . . 12
|
78 | 14, 17, 47, 77 | syl3anc 1326 |
. . . . . . . . . . 11
|
79 | 2, 18, 29 | pltletr 16971 |
. . . . . . . . . . 11
|
80 | 33, 24, 27, 78, 79 | syl13anc 1328 |
. . . . . . . . . 10
|
81 | 31, 80 | mpand 711 |
. . . . . . . . 9
|
82 | 74, 29 | pltle 16961 |
. . . . . . . . . 10
|
83 | 14, 15, 78, 82 | syl3anc 1326 |
. . . . . . . . 9
|
84 | 81, 83 | syld 47 |
. . . . . . . 8
|
85 | 76, 84 | mtod 189 |
. . . . . . 7
|
86 | 19, 20 | hlatjidm 34655 |
. . . . . . . . . 10
|
87 | 14, 17, 86 | syl2anc 693 |
. . . . . . . . 9
|
88 | 87 | oveq1d 6665 |
. . . . . . . 8
|
89 | 88 | breq2d 4665 |
. . . . . . 7
|
90 | 85, 89 | mtbird 315 |
. . . . . 6
|
91 | 13, 73, 90 | pm2.61ne 2879 |
. . . . 5
|
92 | 91 | 3expia 1267 |
. . . 4
|
93 | 92 | expd 452 |
. . 3
|
94 | 93 | rexlimdv 3030 |
. 2
|
95 | 9, 94 | mpd 15 |
1
|