Metamath Proof Explorer


Theorem logcnlem4

Description: Lemma for logcn . (Contributed by Mario Carneiro, 25-Feb-2015)

Ref Expression
Hypotheses logcn.d D = −∞ 0
logcnlem.s S = if A + A A
logcnlem.t T = A R 1 + R
logcnlem.a φ A D
logcnlem.r φ R +
logcnlem.b φ B D
logcnlem.l φ A B < if S T S T
Assertion logcnlem4 φ log A log B < R

Proof

Step Hyp Ref Expression
1 logcn.d D = −∞ 0
2 logcnlem.s S = if A + A A
3 logcnlem.t T = A R 1 + R
4 logcnlem.a φ A D
5 logcnlem.r φ R +
6 logcnlem.b φ B D
7 logcnlem.l φ A B < if S T S T
8 1 ellogdm A D A A A +
9 8 simplbi A D A
10 4 9 syl φ A
11 1 logdmn0 A D A 0
12 4 11 syl φ A 0
13 10 12 logcld φ log A
14 13 imcld φ log A
15 14 recnd φ log A
16 1 ellogdm B D B B B +
17 16 simplbi B D B
18 6 17 syl φ B
19 1 logdmn0 B D B 0
20 6 19 syl φ B 0
21 18 20 logcld φ log B
22 21 imcld φ log B
23 22 recnd φ log B
24 15 23 abssubd φ log A log B = log B log A
25 21 13 imsubd φ log B log A = log B log A
26 efsub log B log A e log B log A = e log B e log A
27 21 13 26 syl2anc φ e log B log A = e log B e log A
28 eflog B B 0 e log B = B
29 18 20 28 syl2anc φ e log B = B
30 eflog A A 0 e log A = A
31 10 12 30 syl2anc φ e log A = A
32 29 31 oveq12d φ e log B e log A = B A
33 27 32 eqtrd φ e log B log A = B A
34 18 10 12 divcld φ B A
35 18 10 20 12 divne0d φ B A 0
36 21 13 subcld φ log B log A
37 1 2 3 4 5 6 7 logcnlem3 φ π < log B log A log B log A π
38 37 simpld φ π < log B log A
39 38 25 breqtrrd φ π < log B log A
40 37 simprd φ log B log A π
41 25 40 eqbrtrd φ log B log A π
42 ellogrn log B log A ran log log B log A π < log B log A log B log A π
43 36 39 41 42 syl3anbrc φ log B log A ran log
44 logeftb B A B A 0 log B log A ran log log B A = log B log A e log B log A = B A
45 34 35 43 44 syl3anc φ log B A = log B log A e log B log A = B A
46 33 45 mpbird φ log B A = log B log A
47 46 eqcomd φ log B log A = log B A
48 47 fveq2d φ log B log A = log B A
49 25 48 eqtr3d φ log B log A = log B A
50 49 fveq2d φ log B log A = log B A
51 24 50 eqtrd φ log A log B = log B A
52 34 35 logcld φ log B A
53 52 imcld φ log B A
54 53 recnd φ log B A
55 54 abscld φ log B A
56 0red φ 0
57 1re 1
58 10 18 subcld φ A B
59 58 abscld φ A B
60 10 12 absrpcld φ A +
61 59 60 rerpdivcld φ A B A
62 resubcl 1 A B A 1 A B A
63 57 61 62 sylancr φ 1 A B A
64 34 recld φ B A
65 10 abscld φ A
66 5 rpred φ R
67 1rp 1 +
68 rpaddcl 1 + R + 1 + R +
69 67 5 68 sylancr φ 1 + R +
70 66 69 rerpdivcld φ R 1 + R
71 65 70 remulcld φ A R 1 + R
72 3 71 eqeltrid φ T
73 rpre A + A
74 73 adantl φ A + A
75 10 imcld φ A
76 75 recnd φ A
77 76 abscld φ A
78 77 adantr φ ¬ A + A
79 74 78 ifclda φ if A + A A
80 2 79 eqeltrid φ S
81 ltmin A B S T A B < if S T S T A B < S A B < T
82 59 80 72 81 syl3anc φ A B < if S T S T A B < S A B < T
83 7 82 mpbid φ A B < S A B < T
84 83 simprd φ A B < T
85 69 rpred φ 1 + R
86 66 ltp1d φ R < R + 1
87 66 recnd φ R
88 ax-1cn 1
89 addcom R 1 R + 1 = 1 + R
90 87 88 89 sylancl φ R + 1 = 1 + R
91 86 90 breqtrd φ R < 1 + R
92 66 85 91 ltled φ R 1 + R
93 85 recnd φ 1 + R
94 93 mulid1d φ 1 + R 1 = 1 + R
95 92 94 breqtrrd φ R 1 + R 1
96 57 a1i φ 1
97 66 96 69 ledivmuld φ R 1 + R 1 R 1 + R 1
98 95 97 mpbird φ R 1 + R 1
99 70 96 60 lemul2d φ R 1 + R 1 A R 1 + R A 1
100 98 99 mpbid φ A R 1 + R A 1
101 65 recnd φ A
102 101 mulid1d φ A 1 = A
103 100 102 breqtrd φ A R 1 + R A
104 3 103 eqbrtrid φ T A
105 59 72 65 84 104 ltletrd φ A B < A
106 105 102 breqtrrd φ A B < A 1
107 59 96 60 ltdivmuld φ A B A < 1 A B < A 1
108 106 107 mpbird φ A B A < 1
109 posdif A B A 1 A B A < 1 0 < 1 A B A
110 61 57 109 sylancl φ A B A < 1 0 < 1 A B A
111 108 110 mpbid φ 0 < 1 A B A
112 58 10 12 divcld φ A B A
113 112 releabsd φ A B A A B A
114 10 18 10 12 divsubdird φ A B A = A A B A
115 10 12 dividd φ A A = 1
116 115 oveq1d φ A A B A = 1 B A
117 114 116 eqtrd φ A B A = 1 B A
118 117 fveq2d φ A B A = 1 B A
119 resub 1 B A 1 B A = 1 B A
120 88 34 119 sylancr φ 1 B A = 1 B A
121 118 120 eqtrd φ A B A = 1 B A
122 re1 1 = 1
123 122 oveq1i 1 B A = 1 B A
124 121 123 eqtrdi φ A B A = 1 B A
125 58 10 12 absdivd φ A B A = A B A
126 113 124 125 3brtr3d φ 1 B A A B A
127 96 64 61 126 subled φ 1 A B A B A
128 56 63 64 111 127 ltletrd φ 0 < B A
129 argregt0 B A 0 < B A log B A π 2 π 2
130 34 128 129 syl2anc φ log B A π 2 π 2
131 cosq14gt0 log B A π 2 π 2 0 < cos log B A
132 130 131 syl φ 0 < cos log B A
133 132 gt0ne0d φ cos log B A 0
134 53 133 retancld φ tan log B A
135 134 recnd φ tan log B A
136 135 abscld φ tan log B A
137 tanabsge log B A π 2 π 2 log B A tan log B A
138 130 137 syl φ log B A tan log B A
139 128 gt0ne0d φ B A 0
140 tanarg B A B A 0 tan log B A = B A B A
141 34 139 140 syl2anc φ tan log B A = B A B A
142 141 fveq2d φ tan log B A = B A B A
143 34 imcld φ B A
144 143 recnd φ B A
145 64 recnd φ B A
146 144 145 139 absdivd φ B A B A = B A B A
147 56 64 128 ltled φ 0 B A
148 64 147 absidd φ B A = B A
149 148 oveq2d φ B A B A = B A B A
150 142 146 149 3eqtrd φ tan log B A = B A B A
151 144 abscld φ B A
152 64 66 remulcld φ B A R
153 18 10 subcld φ B A
154 153 10 12 divcld φ B A A
155 absimle B A A B A A B A A
156 154 155 syl φ B A A B A A
157 18 10 10 12 divsubdird φ B A A = B A A A
158 115 oveq2d φ B A A A = B A 1
159 157 158 eqtrd φ B A A = B A 1
160 159 fveq2d φ B A A = B A 1
161 imsub B A 1 B A 1 = B A 1
162 34 88 161 sylancl φ B A 1 = B A 1
163 im1 1 = 0
164 163 oveq2i B A 1 = B A 0
165 162 164 eqtrdi φ B A 1 = B A 0
166 144 subid1d φ B A 0 = B A
167 160 165 166 3eqtrrd φ B A = B A A
168 167 fveq2d φ B A = B A A
169 10 18 abssubd φ A B = B A
170 169 oveq1d φ A B A = B A A
171 153 10 12 absdivd φ B A A = B A A
172 170 171 eqtr4d φ A B A = B A A
173 156 168 172 3brtr4d φ B A A B A
174 65 59 resubcld φ A A B
175 174 66 remulcld φ A A B R
176 65 152 remulcld φ A B A R
177 59 recnd φ A B
178 88 a1i φ 1
179 177 178 87 adddid φ A B 1 + R = A B 1 + A B R
180 177 mulid1d φ A B 1 = A B
181 180 oveq1d φ A B 1 + A B R = A B + A B R
182 179 181 eqtrd φ A B 1 + R = A B + A B R
183 69 rpne0d φ 1 + R 0
184 101 87 93 183 divassd φ A R 1 + R = A R 1 + R
185 184 3 eqtr4di φ A R 1 + R = T
186 84 185 breqtrrd φ A B < A R 1 + R
187 65 66 remulcld φ A R
188 59 187 69 ltmuldivd φ A B 1 + R < A R A B < A R 1 + R
189 186 188 mpbird φ A B 1 + R < A R
190 182 189 eqbrtrrd φ A B + A B R < A R
191 59 66 remulcld φ A B R
192 59 191 187 ltaddsubd φ A B + A B R < A R A B < A R A B R
193 190 192 mpbid φ A B < A R A B R
194 101 177 87 subdird φ A A B R = A R A B R
195 193 194 breqtrrd φ A B < A A B R
196 60 rpne0d φ A 0
197 101 177 101 196 divsubdird φ A A B A = A A A B A
198 101 196 dividd φ A A = 1
199 198 oveq1d φ A A A B A = 1 A B A
200 197 199 eqtrd φ A A B A = 1 A B A
201 200 127 eqbrtrd φ A A B A B A
202 174 64 60 ledivmuld φ A A B A B A A A B A B A
203 201 202 mpbid φ A A B A B A
204 65 64 remulcld φ A B A
205 174 204 5 lemul1d φ A A B A B A A A B R A B A R
206 203 205 mpbid φ A A B R A B A R
207 101 145 87 mulassd φ A B A R = A B A R
208 206 207 breqtrd φ A A B R A B A R
209 59 175 176 195 208 ltletrd φ A B < A B A R
210 59 152 60 ltdivmuld φ A B A < B A R A B < A B A R
211 209 210 mpbird φ A B A < B A R
212 151 61 152 173 211 lelttrd φ B A < B A R
213 ltdivmul B A R B A 0 < B A B A B A < R B A < B A R
214 151 66 64 128 213 syl112anc φ B A B A < R B A < B A R
215 212 214 mpbird φ B A B A < R
216 150 215 eqbrtrd φ tan log B A < R
217 55 136 66 138 216 lelttrd φ log B A < R
218 51 217 eqbrtrd φ log A log B < R