Step | Hyp | Ref
| Expression |
1 | | logf1o 24311 |
. . . 4
|
2 | | f1of1 6136 |
. . . 4
|
3 | 1, 2 | ax-mp 5 |
. . 3
|
4 | | logcn.d |
. . . 4
|
5 | 4 | logdmss 24388 |
. . 3
|
6 | | f1ores 6151 |
. . 3
|
7 | 3, 5, 6 | mp2an 708 |
. 2
|
8 | | f1ofun 6139 |
. . . . . . 7
|
9 | 1, 8 | ax-mp 5 |
. . . . . 6
|
10 | | f1of 6137 |
. . . . . . . . 9
|
11 | 1, 10 | ax-mp 5 |
. . . . . . . 8
|
12 | 11 | fdmi 6052 |
. . . . . . 7
|
13 | 5, 12 | sseqtr4i 3638 |
. . . . . 6
|
14 | | funimass4 6247 |
. . . . . 6
|
15 | 9, 13, 14 | mp2an 708 |
. . . . 5
|
16 | 4 | ellogdm 24385 |
. . . . . . . 8
|
17 | 16 | simplbi 476 |
. . . . . . 7
|
18 | 4 | logdmn0 24386 |
. . . . . . 7
|
19 | 17, 18 | logcld 24317 |
. . . . . 6
|
20 | 19 | imcld 13935 |
. . . . . . 7
|
21 | 17, 18 | logimcld 24318 |
. . . . . . . 8
|
22 | 21 | simpld 475 |
. . . . . . 7
|
23 | 4 | logdmnrp 24387 |
. . . . . . . . . 10
|
24 | | lognegb 24336 |
. . . . . . . . . . . 12
|
25 | 17, 18, 24 | syl2anc 693 |
. . . . . . . . . . 11
|
26 | 25 | necon3bbid 2831 |
. . . . . . . . . 10
|
27 | 23, 26 | mpbid 222 |
. . . . . . . . 9
|
28 | 27 | necomd 2849 |
. . . . . . . 8
|
29 | | pire 24210 |
. . . . . . . . . 10
|
30 | 29 | a1i 11 |
. . . . . . . . 9
|
31 | 21 | simprd 479 |
. . . . . . . . 9
|
32 | 20, 30, 31 | leltned 10190 |
. . . . . . . 8
|
33 | 28, 32 | mpbird 247 |
. . . . . . 7
|
34 | 29 | renegcli 10342 |
. . . . . . . . 9
|
35 | 34 | rexri 10097 |
. . . . . . . 8
|
36 | 29 | rexri 10097 |
. . . . . . . 8
|
37 | | elioo2 12216 |
. . . . . . . 8
|
38 | 35, 36, 37 | mp2an 708 |
. . . . . . 7
|
39 | 20, 22, 33, 38 | syl3anbrc 1246 |
. . . . . 6
|
40 | | imf 13853 |
. . . . . . 7
|
41 | | ffn 6045 |
. . . . . . 7
|
42 | | elpreima 6337 |
. . . . . . 7
|
43 | 40, 41, 42 | mp2b 10 |
. . . . . 6
|
44 | 19, 39, 43 | sylanbrc 698 |
. . . . 5
|
45 | 15, 44 | mprgbir 2927 |
. . . 4
|
46 | | elpreima 6337 |
. . . . . . 7
|
47 | 40, 41, 46 | mp2b 10 |
. . . . . 6
|
48 | | simpl 473 |
. . . . . . . . 9
|
49 | | eliooord 12233 |
. . . . . . . . . . 11
|
50 | 49 | adantl 482 |
. . . . . . . . . 10
|
51 | 50 | simpld 475 |
. . . . . . . . 9
|
52 | 50 | simprd 479 |
. . . . . . . . . 10
|
53 | | imcl 13851 |
. . . . . . . . . . . 12
|
54 | 53 | adantr 481 |
. . . . . . . . . . 11
|
55 | | ltle 10126 |
. . . . . . . . . . 11
|
56 | 54, 29, 55 | sylancl 694 |
. . . . . . . . . 10
|
57 | 52, 56 | mpd 15 |
. . . . . . . . 9
|
58 | | ellogrn 24306 |
. . . . . . . . 9
|
59 | 48, 51, 57, 58 | syl3anbrc 1246 |
. . . . . . . 8
|
60 | | logef 24328 |
. . . . . . . 8
|
61 | 59, 60 | syl 17 |
. . . . . . 7
|
62 | | efcl 14813 |
. . . . . . . . . 10
|
63 | 62 | adantr 481 |
. . . . . . . . 9
|
64 | 54 | adantr 481 |
. . . . . . . . . . . . . 14
|
65 | 64 | recnd 10068 |
. . . . . . . . . . . . 13
|
66 | | picn 24211 |
. . . . . . . . . . . . . 14
|
67 | 66 | a1i 11 |
. . . . . . . . . . . . 13
|
68 | | pipos 24212 |
. . . . . . . . . . . . . . 15
|
69 | 29, 68 | gt0ne0ii 10564 |
. . . . . . . . . . . . . 14
|
70 | 69 | a1i 11 |
. . . . . . . . . . . . 13
|
71 | 52 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
72 | 66 | mulid1i 10042 |
. . . . . . . . . . . . . . . . . 18
|
73 | 71, 72 | syl6breqr 4695 |
. . . . . . . . . . . . . . . . 17
|
74 | | 1re 10039 |
. . . . . . . . . . . . . . . . . . 19
|
75 | 74 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
|
76 | 29 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
|
77 | 68 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
|
78 | | ltdivmul 10898 |
. . . . . . . . . . . . . . . . . 18
|
79 | 64, 75, 76, 77, 78 | syl112anc 1330 |
. . . . . . . . . . . . . . . . 17
|
80 | 73, 79 | mpbird 247 |
. . . . . . . . . . . . . . . 16
|
81 | | 1e0p1 11552 |
. . . . . . . . . . . . . . . 16
|
82 | 80, 81 | syl6breq 4694 |
. . . . . . . . . . . . . . 15
|
83 | 64 | recoscld 14874 |
. . . . . . . . . . . . . . . . . . 19
|
84 | 64 | resincld 14873 |
. . . . . . . . . . . . . . . . . . 19
|
85 | 83, 84 | crimd 13972 |
. . . . . . . . . . . . . . . . . 18
|
86 | | efeul 14892 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
87 | 86 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . 22
|
88 | 87 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . 21
|
89 | 83 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
90 | | ax-icn 9995 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
91 | 84 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
92 | | mulcl 10020 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
93 | 90, 91, 92 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
94 | 89, 93 | addcld 10059 |
. . . . . . . . . . . . . . . . . . . . . 22
|
95 | | recl 13850 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
96 | 95 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
97 | 96 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
98 | | efcl 14813 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
99 | 97, 98 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
|
100 | | efne0 14827 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
101 | 97, 100 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
|
102 | 94, 99, 101 | divcan3d 10806 |
. . . . . . . . . . . . . . . . . . . . 21
|
103 | 88, 102 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . 20
|
104 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . 21
|
105 | 96 | reefcld 14818 |
. . . . . . . . . . . . . . . . . . . . 21
|
106 | 104, 105,
101 | redivcld 10853 |
. . . . . . . . . . . . . . . . . . . 20
|
107 | 103, 106 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . . . . 19
|
108 | 107 | reim0d 13965 |
. . . . . . . . . . . . . . . . . 18
|
109 | 85, 108 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . 17
|
110 | | sineq0 24273 |
. . . . . . . . . . . . . . . . . 18
|
111 | 65, 110 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
112 | 109, 111 | mpbid 222 |
. . . . . . . . . . . . . . . 16
|
113 | | 0z 11388 |
. . . . . . . . . . . . . . . 16
|
114 | | zleltp1 11428 |
. . . . . . . . . . . . . . . 16
|
115 | 112, 113,
114 | sylancl 694 |
. . . . . . . . . . . . . . 15
|
116 | 82, 115 | mpbird 247 |
. . . . . . . . . . . . . 14
|
117 | | df-neg 10269 |
. . . . . . . . . . . . . . . 16
|
118 | 66 | mulm1i 10475 |
. . . . . . . . . . . . . . . . . 18
|
119 | 51 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
120 | 118, 119 | syl5eqbr 4688 |
. . . . . . . . . . . . . . . . 17
|
121 | 74 | renegcli 10342 |
. . . . . . . . . . . . . . . . . . 19
|
122 | 121 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
|
123 | | ltmuldiv 10896 |
. . . . . . . . . . . . . . . . . 18
|
124 | 122, 64, 76, 77, 123 | syl112anc 1330 |
. . . . . . . . . . . . . . . . 17
|
125 | 120, 124 | mpbid 222 |
. . . . . . . . . . . . . . . 16
|
126 | 117, 125 | syl5eqbrr 4689 |
. . . . . . . . . . . . . . 15
|
127 | | zlem1lt 11429 |
. . . . . . . . . . . . . . . 16
|
128 | 113, 112,
127 | sylancr 695 |
. . . . . . . . . . . . . . 15
|
129 | 126, 128 | mpbird 247 |
. . . . . . . . . . . . . 14
|
130 | 64, 76, 70 | redivcld 10853 |
. . . . . . . . . . . . . . 15
|
131 | | 0re 10040 |
. . . . . . . . . . . . . . 15
|
132 | | letri3 10123 |
. . . . . . . . . . . . . . 15
|
133 | 130, 131,
132 | sylancl 694 |
. . . . . . . . . . . . . 14
|
134 | 116, 129,
133 | mpbir2and 957 |
. . . . . . . . . . . . 13
|
135 | 65, 67, 70, 134 | diveq0d 10808 |
. . . . . . . . . . . 12
|
136 | | reim0b 13859 |
. . . . . . . . . . . . 13
|
137 | 136 | ad2antrr 762 |
. . . . . . . . . . . 12
|
138 | 135, 137 | mpbird 247 |
. . . . . . . . . . 11
|
139 | 138 | rpefcld 14835 |
. . . . . . . . . 10
|
140 | 139 | ex 450 |
. . . . . . . . 9
|
141 | 4 | ellogdm 24385 |
. . . . . . . . 9
|
142 | 63, 140, 141 | sylanbrc 698 |
. . . . . . . 8
|
143 | | funfvima2 6493 |
. . . . . . . . 9
|
144 | 9, 13, 143 | mp2an 708 |
. . . . . . . 8
|
145 | 142, 144 | syl 17 |
. . . . . . 7
|
146 | 61, 145 | eqeltrrd 2702 |
. . . . . 6
|
147 | 47, 146 | sylbi 207 |
. . . . 5
|
148 | 147 | ssriv 3607 |
. . . 4
|
149 | 45, 148 | eqssi 3619 |
. . 3
|
150 | | f1oeq3 6129 |
. . 3
|
151 | 149, 150 | ax-mp 5 |
. 2
|
152 | 7, 151 | mpbi 220 |
1
|