Proof of Theorem logcnlem4
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | logcnlem.a | . . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ 𝐷) | 
| 2 |  | logcn.d | . . . . . . . . . 10
⊢ 𝐷 = (ℂ ∖
(-∞(,]0)) | 
| 3 | 2 | ellogdm 26682 | . . . . . . . . 9
⊢ (𝐴 ∈ 𝐷 ↔ (𝐴 ∈ ℂ ∧ (𝐴 ∈ ℝ → 𝐴 ∈
ℝ+))) | 
| 4 | 3 | simplbi 497 | . . . . . . . 8
⊢ (𝐴 ∈ 𝐷 → 𝐴 ∈ ℂ) | 
| 5 | 1, 4 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℂ) | 
| 6 | 2 | logdmn0 26683 | . . . . . . . 8
⊢ (𝐴 ∈ 𝐷 → 𝐴 ≠ 0) | 
| 7 | 1, 6 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝐴 ≠ 0) | 
| 8 | 5, 7 | logcld 26613 | . . . . . 6
⊢ (𝜑 → (log‘𝐴) ∈
ℂ) | 
| 9 | 8 | imcld 15235 | . . . . 5
⊢ (𝜑 →
(ℑ‘(log‘𝐴)) ∈ ℝ) | 
| 10 | 9 | recnd 11290 | . . . 4
⊢ (𝜑 →
(ℑ‘(log‘𝐴)) ∈ ℂ) | 
| 11 |  | logcnlem.b | . . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ 𝐷) | 
| 12 | 2 | ellogdm 26682 | . . . . . . . . 9
⊢ (𝐵 ∈ 𝐷 ↔ (𝐵 ∈ ℂ ∧ (𝐵 ∈ ℝ → 𝐵 ∈
ℝ+))) | 
| 13 | 12 | simplbi 497 | . . . . . . . 8
⊢ (𝐵 ∈ 𝐷 → 𝐵 ∈ ℂ) | 
| 14 | 11, 13 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℂ) | 
| 15 | 2 | logdmn0 26683 | . . . . . . . 8
⊢ (𝐵 ∈ 𝐷 → 𝐵 ≠ 0) | 
| 16 | 11, 15 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝐵 ≠ 0) | 
| 17 | 14, 16 | logcld 26613 | . . . . . 6
⊢ (𝜑 → (log‘𝐵) ∈
ℂ) | 
| 18 | 17 | imcld 15235 | . . . . 5
⊢ (𝜑 →
(ℑ‘(log‘𝐵)) ∈ ℝ) | 
| 19 | 18 | recnd 11290 | . . . 4
⊢ (𝜑 →
(ℑ‘(log‘𝐵)) ∈ ℂ) | 
| 20 | 10, 19 | abssubd 15493 | . . 3
⊢ (𝜑 →
(abs‘((ℑ‘(log‘𝐴)) − (ℑ‘(log‘𝐵)))) =
(abs‘((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))))) | 
| 21 | 17, 8 | imsubd 15257 | . . . . 5
⊢ (𝜑 →
(ℑ‘((log‘𝐵) − (log‘𝐴))) = ((ℑ‘(log‘𝐵)) −
(ℑ‘(log‘𝐴)))) | 
| 22 |  | efsub 16137 | . . . . . . . . . 10
⊢
(((log‘𝐵)
∈ ℂ ∧ (log‘𝐴) ∈ ℂ) →
(exp‘((log‘𝐵)
− (log‘𝐴))) =
((exp‘(log‘𝐵))
/ (exp‘(log‘𝐴)))) | 
| 23 | 17, 8, 22 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 →
(exp‘((log‘𝐵)
− (log‘𝐴))) =
((exp‘(log‘𝐵))
/ (exp‘(log‘𝐴)))) | 
| 24 |  | eflog 26619 | . . . . . . . . . . 11
⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) →
(exp‘(log‘𝐵)) =
𝐵) | 
| 25 | 14, 16, 24 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝜑 →
(exp‘(log‘𝐵)) =
𝐵) | 
| 26 |  | eflog 26619 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(exp‘(log‘𝐴)) =
𝐴) | 
| 27 | 5, 7, 26 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝜑 →
(exp‘(log‘𝐴)) =
𝐴) | 
| 28 | 25, 27 | oveq12d 7450 | . . . . . . . . 9
⊢ (𝜑 →
((exp‘(log‘𝐵))
/ (exp‘(log‘𝐴))) = (𝐵 / 𝐴)) | 
| 29 | 23, 28 | eqtrd 2776 | . . . . . . . 8
⊢ (𝜑 →
(exp‘((log‘𝐵)
− (log‘𝐴))) =
(𝐵 / 𝐴)) | 
| 30 | 14, 5, 7 | divcld 12044 | . . . . . . . . 9
⊢ (𝜑 → (𝐵 / 𝐴) ∈ ℂ) | 
| 31 | 14, 5, 16, 7 | divne0d 12060 | . . . . . . . . 9
⊢ (𝜑 → (𝐵 / 𝐴) ≠ 0) | 
| 32 | 17, 8 | subcld 11621 | . . . . . . . . . 10
⊢ (𝜑 → ((log‘𝐵) − (log‘𝐴)) ∈
ℂ) | 
| 33 |  | logcnlem.s | . . . . . . . . . . . . 13
⊢ 𝑆 = if(𝐴 ∈ ℝ+, 𝐴,
(abs‘(ℑ‘𝐴))) | 
| 34 |  | logcnlem.t | . . . . . . . . . . . . 13
⊢ 𝑇 = ((abs‘𝐴) · (𝑅 / (1 + 𝑅))) | 
| 35 |  | logcnlem.r | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑅 ∈
ℝ+) | 
| 36 |  | logcnlem.l | . . . . . . . . . . . . 13
⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) < if(𝑆 ≤ 𝑇, 𝑆, 𝑇)) | 
| 37 | 2, 33, 34, 1, 35, 11, 36 | logcnlem3 26687 | . . . . . . . . . . . 12
⊢ (𝜑 → (-π <
((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) ∧
((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) ≤ π)) | 
| 38 | 37 | simpld 494 | . . . . . . . . . . 11
⊢ (𝜑 → -π <
((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴)))) | 
| 39 | 38, 21 | breqtrrd 5170 | . . . . . . . . . 10
⊢ (𝜑 → -π <
(ℑ‘((log‘𝐵) − (log‘𝐴)))) | 
| 40 | 37 | simprd 495 | . . . . . . . . . . 11
⊢ (𝜑 →
((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) ≤ π) | 
| 41 | 21, 40 | eqbrtrd 5164 | . . . . . . . . . 10
⊢ (𝜑 →
(ℑ‘((log‘𝐵) − (log‘𝐴))) ≤ π) | 
| 42 |  | ellogrn 26602 | . . . . . . . . . 10
⊢
(((log‘𝐵)
− (log‘𝐴))
∈ ran log ↔ (((log‘𝐵) − (log‘𝐴)) ∈ ℂ ∧ -π <
(ℑ‘((log‘𝐵) − (log‘𝐴))) ∧ (ℑ‘((log‘𝐵) − (log‘𝐴))) ≤ π)) | 
| 43 | 32, 39, 41, 42 | syl3anbrc 1343 | . . . . . . . . 9
⊢ (𝜑 → ((log‘𝐵) − (log‘𝐴)) ∈ ran
log) | 
| 44 |  | logeftb 26626 | . . . . . . . . 9
⊢ (((𝐵 / 𝐴) ∈ ℂ ∧ (𝐵 / 𝐴) ≠ 0 ∧ ((log‘𝐵) − (log‘𝐴)) ∈ ran log) → ((log‘(𝐵 / 𝐴)) = ((log‘𝐵) − (log‘𝐴)) ↔ (exp‘((log‘𝐵) − (log‘𝐴))) = (𝐵 / 𝐴))) | 
| 45 | 30, 31, 43, 44 | syl3anc 1372 | . . . . . . . 8
⊢ (𝜑 → ((log‘(𝐵 / 𝐴)) = ((log‘𝐵) − (log‘𝐴)) ↔ (exp‘((log‘𝐵) − (log‘𝐴))) = (𝐵 / 𝐴))) | 
| 46 | 29, 45 | mpbird 257 | . . . . . . 7
⊢ (𝜑 → (log‘(𝐵 / 𝐴)) = ((log‘𝐵) − (log‘𝐴))) | 
| 47 | 46 | eqcomd 2742 | . . . . . 6
⊢ (𝜑 → ((log‘𝐵) − (log‘𝐴)) = (log‘(𝐵 / 𝐴))) | 
| 48 | 47 | fveq2d 6909 | . . . . 5
⊢ (𝜑 →
(ℑ‘((log‘𝐵) − (log‘𝐴))) = (ℑ‘(log‘(𝐵 / 𝐴)))) | 
| 49 | 21, 48 | eqtr3d 2778 | . . . 4
⊢ (𝜑 →
((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) =
(ℑ‘(log‘(𝐵 / 𝐴)))) | 
| 50 | 49 | fveq2d 6909 | . . 3
⊢ (𝜑 →
(abs‘((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴)))) =
(abs‘(ℑ‘(log‘(𝐵 / 𝐴))))) | 
| 51 | 20, 50 | eqtrd 2776 | . 2
⊢ (𝜑 →
(abs‘((ℑ‘(log‘𝐴)) − (ℑ‘(log‘𝐵)))) =
(abs‘(ℑ‘(log‘(𝐵 / 𝐴))))) | 
| 52 | 30, 31 | logcld 26613 | . . . . . 6
⊢ (𝜑 → (log‘(𝐵 / 𝐴)) ∈ ℂ) | 
| 53 | 52 | imcld 15235 | . . . . 5
⊢ (𝜑 →
(ℑ‘(log‘(𝐵 / 𝐴))) ∈ ℝ) | 
| 54 | 53 | recnd 11290 | . . . 4
⊢ (𝜑 →
(ℑ‘(log‘(𝐵 / 𝐴))) ∈ ℂ) | 
| 55 | 54 | abscld 15476 | . . 3
⊢ (𝜑 →
(abs‘(ℑ‘(log‘(𝐵 / 𝐴)))) ∈ ℝ) | 
| 56 |  | 0red 11265 | . . . . . . . . . 10
⊢ (𝜑 → 0 ∈
ℝ) | 
| 57 |  | 1re 11262 | . . . . . . . . . . 11
⊢ 1 ∈
ℝ | 
| 58 | 5, 14 | subcld 11621 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℂ) | 
| 59 | 58 | abscld 15476 | . . . . . . . . . . . 12
⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) ∈ ℝ) | 
| 60 | 5, 7 | absrpcld 15488 | . . . . . . . . . . . 12
⊢ (𝜑 → (abs‘𝐴) ∈
ℝ+) | 
| 61 | 59, 60 | rerpdivcld 13109 | . . . . . . . . . . 11
⊢ (𝜑 → ((abs‘(𝐴 − 𝐵)) / (abs‘𝐴)) ∈ ℝ) | 
| 62 |  | resubcl 11574 | . . . . . . . . . . 11
⊢ ((1
∈ ℝ ∧ ((abs‘(𝐴 − 𝐵)) / (abs‘𝐴)) ∈ ℝ) → (1 −
((abs‘(𝐴 −
𝐵)) / (abs‘𝐴))) ∈
ℝ) | 
| 63 | 57, 61, 62 | sylancr 587 | . . . . . . . . . 10
⊢ (𝜑 → (1 −
((abs‘(𝐴 −
𝐵)) / (abs‘𝐴))) ∈
ℝ) | 
| 64 | 30 | recld 15234 | . . . . . . . . . 10
⊢ (𝜑 → (ℜ‘(𝐵 / 𝐴)) ∈ ℝ) | 
| 65 | 5 | abscld 15476 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (abs‘𝐴) ∈
ℝ) | 
| 66 | 35 | rpred 13078 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑅 ∈ ℝ) | 
| 67 |  | 1rp 13039 | . . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℝ+ | 
| 68 |  | rpaddcl 13058 | . . . . . . . . . . . . . . . . . 18
⊢ ((1
∈ ℝ+ ∧ 𝑅 ∈ ℝ+) → (1 +
𝑅) ∈
ℝ+) | 
| 69 | 67, 35, 68 | sylancr 587 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (1 + 𝑅) ∈
ℝ+) | 
| 70 | 66, 69 | rerpdivcld 13109 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑅 / (1 + 𝑅)) ∈ ℝ) | 
| 71 | 65, 70 | remulcld 11292 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((abs‘𝐴) · (𝑅 / (1 + 𝑅))) ∈ ℝ) | 
| 72 | 34, 71 | eqeltrid 2844 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑇 ∈ ℝ) | 
| 73 |  | rpre 13044 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℝ) | 
| 74 | 73 | adantl 481 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝐴 ∈ ℝ+) → 𝐴 ∈
ℝ) | 
| 75 | 5 | imcld 15235 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (ℑ‘𝐴) ∈
ℝ) | 
| 76 | 75 | recnd 11290 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (ℑ‘𝐴) ∈
ℂ) | 
| 77 | 76 | abscld 15476 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 →
(abs‘(ℑ‘𝐴)) ∈ ℝ) | 
| 78 | 77 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ ℝ+) →
(abs‘(ℑ‘𝐴)) ∈ ℝ) | 
| 79 | 74, 78 | ifclda 4560 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → if(𝐴 ∈ ℝ+, 𝐴,
(abs‘(ℑ‘𝐴))) ∈ ℝ) | 
| 80 | 33, 79 | eqeltrid 2844 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑆 ∈ ℝ) | 
| 81 |  | ltmin 13237 | . . . . . . . . . . . . . . . . 17
⊢
(((abs‘(𝐴
− 𝐵)) ∈ ℝ
∧ 𝑆 ∈ ℝ
∧ 𝑇 ∈ ℝ)
→ ((abs‘(𝐴
− 𝐵)) < if(𝑆 ≤ 𝑇, 𝑆, 𝑇) ↔ ((abs‘(𝐴 − 𝐵)) < 𝑆 ∧ (abs‘(𝐴 − 𝐵)) < 𝑇))) | 
| 82 | 59, 80, 72, 81 | syl3anc 1372 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((abs‘(𝐴 − 𝐵)) < if(𝑆 ≤ 𝑇, 𝑆, 𝑇) ↔ ((abs‘(𝐴 − 𝐵)) < 𝑆 ∧ (abs‘(𝐴 − 𝐵)) < 𝑇))) | 
| 83 | 36, 82 | mpbid 232 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((abs‘(𝐴 − 𝐵)) < 𝑆 ∧ (abs‘(𝐴 − 𝐵)) < 𝑇)) | 
| 84 | 83 | simprd 495 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) < 𝑇) | 
| 85 | 69 | rpred 13078 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (1 + 𝑅) ∈ ℝ) | 
| 86 | 66 | ltp1d 12199 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑅 < (𝑅 + 1)) | 
| 87 | 66 | recnd 11290 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑅 ∈ ℂ) | 
| 88 |  | ax-1cn 11214 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 ∈
ℂ | 
| 89 |  | addcom 11448 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑅 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑅 + 1) =
(1 + 𝑅)) | 
| 90 | 87, 88, 89 | sylancl 586 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑅 + 1) = (1 + 𝑅)) | 
| 91 | 86, 90 | breqtrd 5168 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑅 < (1 + 𝑅)) | 
| 92 | 66, 85, 91 | ltled 11410 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑅 ≤ (1 + 𝑅)) | 
| 93 | 85 | recnd 11290 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (1 + 𝑅) ∈ ℂ) | 
| 94 | 93 | mulridd 11279 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((1 + 𝑅) · 1) = (1 + 𝑅)) | 
| 95 | 92, 94 | breqtrrd 5170 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑅 ≤ ((1 + 𝑅) · 1)) | 
| 96 | 57 | a1i 11 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 1 ∈
ℝ) | 
| 97 | 66, 96, 69 | ledivmuld 13131 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑅 / (1 + 𝑅)) ≤ 1 ↔ 𝑅 ≤ ((1 + 𝑅) · 1))) | 
| 98 | 95, 97 | mpbird 257 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑅 / (1 + 𝑅)) ≤ 1) | 
| 99 | 70, 96, 60 | lemul2d 13122 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑅 / (1 + 𝑅)) ≤ 1 ↔ ((abs‘𝐴) · (𝑅 / (1 + 𝑅))) ≤ ((abs‘𝐴) · 1))) | 
| 100 | 98, 99 | mpbid 232 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((abs‘𝐴) · (𝑅 / (1 + 𝑅))) ≤ ((abs‘𝐴) · 1)) | 
| 101 | 65 | recnd 11290 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (abs‘𝐴) ∈
ℂ) | 
| 102 | 101 | mulridd 11279 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((abs‘𝐴) · 1) = (abs‘𝐴)) | 
| 103 | 100, 102 | breqtrd 5168 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((abs‘𝐴) · (𝑅 / (1 + 𝑅))) ≤ (abs‘𝐴)) | 
| 104 | 34, 103 | eqbrtrid 5177 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑇 ≤ (abs‘𝐴)) | 
| 105 | 59, 72, 65, 84, 104 | ltletrd 11422 | . . . . . . . . . . . . 13
⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) < (abs‘𝐴)) | 
| 106 | 105, 102 | breqtrrd 5170 | . . . . . . . . . . . 12
⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) < ((abs‘𝐴) · 1)) | 
| 107 | 59, 96, 60 | ltdivmuld 13129 | . . . . . . . . . . . 12
⊢ (𝜑 → (((abs‘(𝐴 − 𝐵)) / (abs‘𝐴)) < 1 ↔ (abs‘(𝐴 − 𝐵)) < ((abs‘𝐴) · 1))) | 
| 108 | 106, 107 | mpbird 257 | . . . . . . . . . . 11
⊢ (𝜑 → ((abs‘(𝐴 − 𝐵)) / (abs‘𝐴)) < 1) | 
| 109 |  | posdif 11757 | . . . . . . . . . . . 12
⊢
((((abs‘(𝐴
− 𝐵)) /
(abs‘𝐴)) ∈
ℝ ∧ 1 ∈ ℝ) → (((abs‘(𝐴 − 𝐵)) / (abs‘𝐴)) < 1 ↔ 0 < (1 −
((abs‘(𝐴 −
𝐵)) / (abs‘𝐴))))) | 
| 110 | 61, 57, 109 | sylancl 586 | . . . . . . . . . . 11
⊢ (𝜑 → (((abs‘(𝐴 − 𝐵)) / (abs‘𝐴)) < 1 ↔ 0 < (1 −
((abs‘(𝐴 −
𝐵)) / (abs‘𝐴))))) | 
| 111 | 108, 110 | mpbid 232 | . . . . . . . . . 10
⊢ (𝜑 → 0 < (1 −
((abs‘(𝐴 −
𝐵)) / (abs‘𝐴)))) | 
| 112 | 58, 5, 7 | divcld 12044 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐴 − 𝐵) / 𝐴) ∈ ℂ) | 
| 113 | 112 | releabsd 15491 | . . . . . . . . . . . 12
⊢ (𝜑 → (ℜ‘((𝐴 − 𝐵) / 𝐴)) ≤ (abs‘((𝐴 − 𝐵) / 𝐴))) | 
| 114 | 5, 14, 5, 7 | divsubdird 12083 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐴 − 𝐵) / 𝐴) = ((𝐴 / 𝐴) − (𝐵 / 𝐴))) | 
| 115 | 5, 7 | dividd 12042 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐴 / 𝐴) = 1) | 
| 116 | 115 | oveq1d 7447 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐴 / 𝐴) − (𝐵 / 𝐴)) = (1 − (𝐵 / 𝐴))) | 
| 117 | 114, 116 | eqtrd 2776 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐴 − 𝐵) / 𝐴) = (1 − (𝐵 / 𝐴))) | 
| 118 | 117 | fveq2d 6909 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (ℜ‘((𝐴 − 𝐵) / 𝐴)) = (ℜ‘(1 − (𝐵 / 𝐴)))) | 
| 119 |  | resub 15167 | . . . . . . . . . . . . . . 15
⊢ ((1
∈ ℂ ∧ (𝐵 /
𝐴) ∈ ℂ) →
(ℜ‘(1 − (𝐵
/ 𝐴))) = ((ℜ‘1)
− (ℜ‘(𝐵 /
𝐴)))) | 
| 120 | 88, 30, 119 | sylancr 587 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (ℜ‘(1 −
(𝐵 / 𝐴))) = ((ℜ‘1) −
(ℜ‘(𝐵 / 𝐴)))) | 
| 121 | 118, 120 | eqtrd 2776 | . . . . . . . . . . . . 13
⊢ (𝜑 → (ℜ‘((𝐴 − 𝐵) / 𝐴)) = ((ℜ‘1) −
(ℜ‘(𝐵 / 𝐴)))) | 
| 122 |  | re1 15194 | . . . . . . . . . . . . . 14
⊢
(ℜ‘1) = 1 | 
| 123 | 122 | oveq1i 7442 | . . . . . . . . . . . . 13
⊢
((ℜ‘1) − (ℜ‘(𝐵 / 𝐴))) = (1 − (ℜ‘(𝐵 / 𝐴))) | 
| 124 | 121, 123 | eqtrdi 2792 | . . . . . . . . . . . 12
⊢ (𝜑 → (ℜ‘((𝐴 − 𝐵) / 𝐴)) = (1 − (ℜ‘(𝐵 / 𝐴)))) | 
| 125 | 58, 5, 7 | absdivd 15495 | . . . . . . . . . . . 12
⊢ (𝜑 → (abs‘((𝐴 − 𝐵) / 𝐴)) = ((abs‘(𝐴 − 𝐵)) / (abs‘𝐴))) | 
| 126 | 113, 124,
125 | 3brtr3d 5173 | . . . . . . . . . . 11
⊢ (𝜑 → (1 −
(ℜ‘(𝐵 / 𝐴))) ≤ ((abs‘(𝐴 − 𝐵)) / (abs‘𝐴))) | 
| 127 | 96, 64, 61, 126 | subled 11867 | . . . . . . . . . 10
⊢ (𝜑 → (1 −
((abs‘(𝐴 −
𝐵)) / (abs‘𝐴))) ≤ (ℜ‘(𝐵 / 𝐴))) | 
| 128 | 56, 63, 64, 111, 127 | ltletrd 11422 | . . . . . . . . 9
⊢ (𝜑 → 0 <
(ℜ‘(𝐵 / 𝐴))) | 
| 129 |  | argregt0 26653 | . . . . . . . . 9
⊢ (((𝐵 / 𝐴) ∈ ℂ ∧ 0 <
(ℜ‘(𝐵 / 𝐴))) →
(ℑ‘(log‘(𝐵 / 𝐴))) ∈ (-(π / 2)(,)(π /
2))) | 
| 130 | 30, 128, 129 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 →
(ℑ‘(log‘(𝐵 / 𝐴))) ∈ (-(π / 2)(,)(π /
2))) | 
| 131 |  | cosq14gt0 26553 | . . . . . . . 8
⊢
((ℑ‘(log‘(𝐵 / 𝐴))) ∈ (-(π / 2)(,)(π / 2)) →
0 < (cos‘(ℑ‘(log‘(𝐵 / 𝐴))))) | 
| 132 | 130, 131 | syl 17 | . . . . . . 7
⊢ (𝜑 → 0 <
(cos‘(ℑ‘(log‘(𝐵 / 𝐴))))) | 
| 133 | 132 | gt0ne0d 11828 | . . . . . 6
⊢ (𝜑 →
(cos‘(ℑ‘(log‘(𝐵 / 𝐴)))) ≠ 0) | 
| 134 | 53, 133 | retancld 16182 | . . . . 5
⊢ (𝜑 →
(tan‘(ℑ‘(log‘(𝐵 / 𝐴)))) ∈ ℝ) | 
| 135 | 134 | recnd 11290 | . . . 4
⊢ (𝜑 →
(tan‘(ℑ‘(log‘(𝐵 / 𝐴)))) ∈ ℂ) | 
| 136 | 135 | abscld 15476 | . . 3
⊢ (𝜑 →
(abs‘(tan‘(ℑ‘(log‘(𝐵 / 𝐴))))) ∈ ℝ) | 
| 137 |  | tanabsge 26549 | . . . 4
⊢
((ℑ‘(log‘(𝐵 / 𝐴))) ∈ (-(π / 2)(,)(π / 2)) →
(abs‘(ℑ‘(log‘(𝐵 / 𝐴)))) ≤
(abs‘(tan‘(ℑ‘(log‘(𝐵 / 𝐴)))))) | 
| 138 | 130, 137 | syl 17 | . . 3
⊢ (𝜑 →
(abs‘(ℑ‘(log‘(𝐵 / 𝐴)))) ≤
(abs‘(tan‘(ℑ‘(log‘(𝐵 / 𝐴)))))) | 
| 139 | 128 | gt0ne0d 11828 | . . . . . . 7
⊢ (𝜑 → (ℜ‘(𝐵 / 𝐴)) ≠ 0) | 
| 140 |  | tanarg 26662 | . . . . . . 7
⊢ (((𝐵 / 𝐴) ∈ ℂ ∧ (ℜ‘(𝐵 / 𝐴)) ≠ 0) →
(tan‘(ℑ‘(log‘(𝐵 / 𝐴)))) = ((ℑ‘(𝐵 / 𝐴)) / (ℜ‘(𝐵 / 𝐴)))) | 
| 141 | 30, 139, 140 | syl2anc 584 | . . . . . 6
⊢ (𝜑 →
(tan‘(ℑ‘(log‘(𝐵 / 𝐴)))) = ((ℑ‘(𝐵 / 𝐴)) / (ℜ‘(𝐵 / 𝐴)))) | 
| 142 | 141 | fveq2d 6909 | . . . . 5
⊢ (𝜑 →
(abs‘(tan‘(ℑ‘(log‘(𝐵 / 𝐴))))) = (abs‘((ℑ‘(𝐵 / 𝐴)) / (ℜ‘(𝐵 / 𝐴))))) | 
| 143 | 30 | imcld 15235 | . . . . . . 7
⊢ (𝜑 → (ℑ‘(𝐵 / 𝐴)) ∈ ℝ) | 
| 144 | 143 | recnd 11290 | . . . . . 6
⊢ (𝜑 → (ℑ‘(𝐵 / 𝐴)) ∈ ℂ) | 
| 145 | 64 | recnd 11290 | . . . . . 6
⊢ (𝜑 → (ℜ‘(𝐵 / 𝐴)) ∈ ℂ) | 
| 146 | 144, 145,
139 | absdivd 15495 | . . . . 5
⊢ (𝜑 →
(abs‘((ℑ‘(𝐵 / 𝐴)) / (ℜ‘(𝐵 / 𝐴)))) = ((abs‘(ℑ‘(𝐵 / 𝐴))) / (abs‘(ℜ‘(𝐵 / 𝐴))))) | 
| 147 | 56, 64, 128 | ltled 11410 | . . . . . . 7
⊢ (𝜑 → 0 ≤
(ℜ‘(𝐵 / 𝐴))) | 
| 148 | 64, 147 | absidd 15462 | . . . . . 6
⊢ (𝜑 →
(abs‘(ℜ‘(𝐵
/ 𝐴))) =
(ℜ‘(𝐵 / 𝐴))) | 
| 149 | 148 | oveq2d 7448 | . . . . 5
⊢ (𝜑 →
((abs‘(ℑ‘(𝐵 / 𝐴))) / (abs‘(ℜ‘(𝐵 / 𝐴)))) = ((abs‘(ℑ‘(𝐵 / 𝐴))) / (ℜ‘(𝐵 / 𝐴)))) | 
| 150 | 142, 146,
149 | 3eqtrd 2780 | . . . 4
⊢ (𝜑 →
(abs‘(tan‘(ℑ‘(log‘(𝐵 / 𝐴))))) = ((abs‘(ℑ‘(𝐵 / 𝐴))) / (ℜ‘(𝐵 / 𝐴)))) | 
| 151 | 144 | abscld 15476 | . . . . . 6
⊢ (𝜑 →
(abs‘(ℑ‘(𝐵 / 𝐴))) ∈ ℝ) | 
| 152 | 64, 66 | remulcld 11292 | . . . . . 6
⊢ (𝜑 → ((ℜ‘(𝐵 / 𝐴)) · 𝑅) ∈ ℝ) | 
| 153 | 14, 5 | subcld 11621 | . . . . . . . . 9
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℂ) | 
| 154 | 153, 5, 7 | divcld 12044 | . . . . . . . 8
⊢ (𝜑 → ((𝐵 − 𝐴) / 𝐴) ∈ ℂ) | 
| 155 |  | absimle 15349 | . . . . . . . 8
⊢ (((𝐵 − 𝐴) / 𝐴) ∈ ℂ →
(abs‘(ℑ‘((𝐵 − 𝐴) / 𝐴))) ≤ (abs‘((𝐵 − 𝐴) / 𝐴))) | 
| 156 | 154, 155 | syl 17 | . . . . . . 7
⊢ (𝜑 →
(abs‘(ℑ‘((𝐵 − 𝐴) / 𝐴))) ≤ (abs‘((𝐵 − 𝐴) / 𝐴))) | 
| 157 | 14, 5, 5, 7 | divsubdird 12083 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝐵 − 𝐴) / 𝐴) = ((𝐵 / 𝐴) − (𝐴 / 𝐴))) | 
| 158 | 115 | oveq2d 7448 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝐵 / 𝐴) − (𝐴 / 𝐴)) = ((𝐵 / 𝐴) − 1)) | 
| 159 | 157, 158 | eqtrd 2776 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐵 − 𝐴) / 𝐴) = ((𝐵 / 𝐴) − 1)) | 
| 160 | 159 | fveq2d 6909 | . . . . . . . . 9
⊢ (𝜑 → (ℑ‘((𝐵 − 𝐴) / 𝐴)) = (ℑ‘((𝐵 / 𝐴) − 1))) | 
| 161 |  | imsub 15175 | . . . . . . . . . . 11
⊢ (((𝐵 / 𝐴) ∈ ℂ ∧ 1 ∈ ℂ)
→ (ℑ‘((𝐵 /
𝐴) − 1)) =
((ℑ‘(𝐵 / 𝐴)) −
(ℑ‘1))) | 
| 162 | 30, 88, 161 | sylancl 586 | . . . . . . . . . 10
⊢ (𝜑 → (ℑ‘((𝐵 / 𝐴) − 1)) = ((ℑ‘(𝐵 / 𝐴)) −
(ℑ‘1))) | 
| 163 |  | im1 15195 | . . . . . . . . . . 11
⊢
(ℑ‘1) = 0 | 
| 164 | 163 | oveq2i 7443 | . . . . . . . . . 10
⊢
((ℑ‘(𝐵 /
𝐴)) −
(ℑ‘1)) = ((ℑ‘(𝐵 / 𝐴)) − 0) | 
| 165 | 162, 164 | eqtrdi 2792 | . . . . . . . . 9
⊢ (𝜑 → (ℑ‘((𝐵 / 𝐴) − 1)) = ((ℑ‘(𝐵 / 𝐴)) − 0)) | 
| 166 | 144 | subid1d 11610 | . . . . . . . . 9
⊢ (𝜑 → ((ℑ‘(𝐵 / 𝐴)) − 0) = (ℑ‘(𝐵 / 𝐴))) | 
| 167 | 160, 165,
166 | 3eqtrrd 2781 | . . . . . . . 8
⊢ (𝜑 → (ℑ‘(𝐵 / 𝐴)) = (ℑ‘((𝐵 − 𝐴) / 𝐴))) | 
| 168 | 167 | fveq2d 6909 | . . . . . . 7
⊢ (𝜑 →
(abs‘(ℑ‘(𝐵 / 𝐴))) = (abs‘(ℑ‘((𝐵 − 𝐴) / 𝐴)))) | 
| 169 | 5, 14 | abssubd 15493 | . . . . . . . . 9
⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) = (abs‘(𝐵 − 𝐴))) | 
| 170 | 169 | oveq1d 7447 | . . . . . . . 8
⊢ (𝜑 → ((abs‘(𝐴 − 𝐵)) / (abs‘𝐴)) = ((abs‘(𝐵 − 𝐴)) / (abs‘𝐴))) | 
| 171 | 153, 5, 7 | absdivd 15495 | . . . . . . . 8
⊢ (𝜑 → (abs‘((𝐵 − 𝐴) / 𝐴)) = ((abs‘(𝐵 − 𝐴)) / (abs‘𝐴))) | 
| 172 | 170, 171 | eqtr4d 2779 | . . . . . . 7
⊢ (𝜑 → ((abs‘(𝐴 − 𝐵)) / (abs‘𝐴)) = (abs‘((𝐵 − 𝐴) / 𝐴))) | 
| 173 | 156, 168,
172 | 3brtr4d 5174 | . . . . . 6
⊢ (𝜑 →
(abs‘(ℑ‘(𝐵 / 𝐴))) ≤ ((abs‘(𝐴 − 𝐵)) / (abs‘𝐴))) | 
| 174 | 65, 59 | resubcld 11692 | . . . . . . . . 9
⊢ (𝜑 → ((abs‘𝐴) − (abs‘(𝐴 − 𝐵))) ∈ ℝ) | 
| 175 | 174, 66 | remulcld 11292 | . . . . . . . 8
⊢ (𝜑 → (((abs‘𝐴) − (abs‘(𝐴 − 𝐵))) · 𝑅) ∈ ℝ) | 
| 176 | 65, 152 | remulcld 11292 | . . . . . . . 8
⊢ (𝜑 → ((abs‘𝐴) · ((ℜ‘(𝐵 / 𝐴)) · 𝑅)) ∈ ℝ) | 
| 177 | 59 | recnd 11290 | . . . . . . . . . . . . 13
⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) ∈ ℂ) | 
| 178 | 88 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝜑 → 1 ∈
ℂ) | 
| 179 | 177, 178,
87 | adddid 11286 | . . . . . . . . . . . 12
⊢ (𝜑 → ((abs‘(𝐴 − 𝐵)) · (1 + 𝑅)) = (((abs‘(𝐴 − 𝐵)) · 1) + ((abs‘(𝐴 − 𝐵)) · 𝑅))) | 
| 180 | 177 | mulridd 11279 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((abs‘(𝐴 − 𝐵)) · 1) = (abs‘(𝐴 − 𝐵))) | 
| 181 | 180 | oveq1d 7447 | . . . . . . . . . . . 12
⊢ (𝜑 → (((abs‘(𝐴 − 𝐵)) · 1) + ((abs‘(𝐴 − 𝐵)) · 𝑅)) = ((abs‘(𝐴 − 𝐵)) + ((abs‘(𝐴 − 𝐵)) · 𝑅))) | 
| 182 | 179, 181 | eqtrd 2776 | . . . . . . . . . . 11
⊢ (𝜑 → ((abs‘(𝐴 − 𝐵)) · (1 + 𝑅)) = ((abs‘(𝐴 − 𝐵)) + ((abs‘(𝐴 − 𝐵)) · 𝑅))) | 
| 183 | 69 | rpne0d 13083 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (1 + 𝑅) ≠ 0) | 
| 184 | 101, 87, 93, 183 | divassd 12079 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (((abs‘𝐴) · 𝑅) / (1 + 𝑅)) = ((abs‘𝐴) · (𝑅 / (1 + 𝑅)))) | 
| 185 | 184, 34 | eqtr4di 2794 | . . . . . . . . . . . . 13
⊢ (𝜑 → (((abs‘𝐴) · 𝑅) / (1 + 𝑅)) = 𝑇) | 
| 186 | 84, 185 | breqtrrd 5170 | . . . . . . . . . . . 12
⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) < (((abs‘𝐴) · 𝑅) / (1 + 𝑅))) | 
| 187 | 65, 66 | remulcld 11292 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((abs‘𝐴) · 𝑅) ∈ ℝ) | 
| 188 | 59, 187, 69 | ltmuldivd 13125 | . . . . . . . . . . . 12
⊢ (𝜑 → (((abs‘(𝐴 − 𝐵)) · (1 + 𝑅)) < ((abs‘𝐴) · 𝑅) ↔ (abs‘(𝐴 − 𝐵)) < (((abs‘𝐴) · 𝑅) / (1 + 𝑅)))) | 
| 189 | 186, 188 | mpbird 257 | . . . . . . . . . . 11
⊢ (𝜑 → ((abs‘(𝐴 − 𝐵)) · (1 + 𝑅)) < ((abs‘𝐴) · 𝑅)) | 
| 190 | 182, 189 | eqbrtrrd 5166 | . . . . . . . . . 10
⊢ (𝜑 → ((abs‘(𝐴 − 𝐵)) + ((abs‘(𝐴 − 𝐵)) · 𝑅)) < ((abs‘𝐴) · 𝑅)) | 
| 191 | 59, 66 | remulcld 11292 | . . . . . . . . . . 11
⊢ (𝜑 → ((abs‘(𝐴 − 𝐵)) · 𝑅) ∈ ℝ) | 
| 192 | 59, 191, 187 | ltaddsubd 11864 | . . . . . . . . . 10
⊢ (𝜑 → (((abs‘(𝐴 − 𝐵)) + ((abs‘(𝐴 − 𝐵)) · 𝑅)) < ((abs‘𝐴) · 𝑅) ↔ (abs‘(𝐴 − 𝐵)) < (((abs‘𝐴) · 𝑅) − ((abs‘(𝐴 − 𝐵)) · 𝑅)))) | 
| 193 | 190, 192 | mpbid 232 | . . . . . . . . 9
⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) < (((abs‘𝐴) · 𝑅) − ((abs‘(𝐴 − 𝐵)) · 𝑅))) | 
| 194 | 101, 177,
87 | subdird 11721 | . . . . . . . . 9
⊢ (𝜑 → (((abs‘𝐴) − (abs‘(𝐴 − 𝐵))) · 𝑅) = (((abs‘𝐴) · 𝑅) − ((abs‘(𝐴 − 𝐵)) · 𝑅))) | 
| 195 | 193, 194 | breqtrrd 5170 | . . . . . . . 8
⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) < (((abs‘𝐴) − (abs‘(𝐴 − 𝐵))) · 𝑅)) | 
| 196 | 60 | rpne0d 13083 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (abs‘𝐴) ≠ 0) | 
| 197 | 101, 177,
101, 196 | divsubdird 12083 | . . . . . . . . . . . . 13
⊢ (𝜑 → (((abs‘𝐴) − (abs‘(𝐴 − 𝐵))) / (abs‘𝐴)) = (((abs‘𝐴) / (abs‘𝐴)) − ((abs‘(𝐴 − 𝐵)) / (abs‘𝐴)))) | 
| 198 | 101, 196 | dividd 12042 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((abs‘𝐴) / (abs‘𝐴)) = 1) | 
| 199 | 198 | oveq1d 7447 | . . . . . . . . . . . . 13
⊢ (𝜑 → (((abs‘𝐴) / (abs‘𝐴)) − ((abs‘(𝐴 − 𝐵)) / (abs‘𝐴))) = (1 − ((abs‘(𝐴 − 𝐵)) / (abs‘𝐴)))) | 
| 200 | 197, 199 | eqtrd 2776 | . . . . . . . . . . . 12
⊢ (𝜑 → (((abs‘𝐴) − (abs‘(𝐴 − 𝐵))) / (abs‘𝐴)) = (1 − ((abs‘(𝐴 − 𝐵)) / (abs‘𝐴)))) | 
| 201 | 200, 127 | eqbrtrd 5164 | . . . . . . . . . . 11
⊢ (𝜑 → (((abs‘𝐴) − (abs‘(𝐴 − 𝐵))) / (abs‘𝐴)) ≤ (ℜ‘(𝐵 / 𝐴))) | 
| 202 | 174, 64, 60 | ledivmuld 13131 | . . . . . . . . . . 11
⊢ (𝜑 → ((((abs‘𝐴) − (abs‘(𝐴 − 𝐵))) / (abs‘𝐴)) ≤ (ℜ‘(𝐵 / 𝐴)) ↔ ((abs‘𝐴) − (abs‘(𝐴 − 𝐵))) ≤ ((abs‘𝐴) · (ℜ‘(𝐵 / 𝐴))))) | 
| 203 | 201, 202 | mpbid 232 | . . . . . . . . . 10
⊢ (𝜑 → ((abs‘𝐴) − (abs‘(𝐴 − 𝐵))) ≤ ((abs‘𝐴) · (ℜ‘(𝐵 / 𝐴)))) | 
| 204 | 65, 64 | remulcld 11292 | . . . . . . . . . . 11
⊢ (𝜑 → ((abs‘𝐴) · (ℜ‘(𝐵 / 𝐴))) ∈ ℝ) | 
| 205 | 174, 204,
35 | lemul1d 13121 | . . . . . . . . . 10
⊢ (𝜑 → (((abs‘𝐴) − (abs‘(𝐴 − 𝐵))) ≤ ((abs‘𝐴) · (ℜ‘(𝐵 / 𝐴))) ↔ (((abs‘𝐴) − (abs‘(𝐴 − 𝐵))) · 𝑅) ≤ (((abs‘𝐴) · (ℜ‘(𝐵 / 𝐴))) · 𝑅))) | 
| 206 | 203, 205 | mpbid 232 | . . . . . . . . 9
⊢ (𝜑 → (((abs‘𝐴) − (abs‘(𝐴 − 𝐵))) · 𝑅) ≤ (((abs‘𝐴) · (ℜ‘(𝐵 / 𝐴))) · 𝑅)) | 
| 207 | 101, 145,
87 | mulassd 11285 | . . . . . . . . 9
⊢ (𝜑 → (((abs‘𝐴) · (ℜ‘(𝐵 / 𝐴))) · 𝑅) = ((abs‘𝐴) · ((ℜ‘(𝐵 / 𝐴)) · 𝑅))) | 
| 208 | 206, 207 | breqtrd 5168 | . . . . . . . 8
⊢ (𝜑 → (((abs‘𝐴) − (abs‘(𝐴 − 𝐵))) · 𝑅) ≤ ((abs‘𝐴) · ((ℜ‘(𝐵 / 𝐴)) · 𝑅))) | 
| 209 | 59, 175, 176, 195, 208 | ltletrd 11422 | . . . . . . 7
⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) < ((abs‘𝐴) · ((ℜ‘(𝐵 / 𝐴)) · 𝑅))) | 
| 210 | 59, 152, 60 | ltdivmuld 13129 | . . . . . . 7
⊢ (𝜑 → (((abs‘(𝐴 − 𝐵)) / (abs‘𝐴)) < ((ℜ‘(𝐵 / 𝐴)) · 𝑅) ↔ (abs‘(𝐴 − 𝐵)) < ((abs‘𝐴) · ((ℜ‘(𝐵 / 𝐴)) · 𝑅)))) | 
| 211 | 209, 210 | mpbird 257 | . . . . . 6
⊢ (𝜑 → ((abs‘(𝐴 − 𝐵)) / (abs‘𝐴)) < ((ℜ‘(𝐵 / 𝐴)) · 𝑅)) | 
| 212 | 151, 61, 152, 173, 211 | lelttrd 11420 | . . . . 5
⊢ (𝜑 →
(abs‘(ℑ‘(𝐵 / 𝐴))) < ((ℜ‘(𝐵 / 𝐴)) · 𝑅)) | 
| 213 |  | ltdivmul 12144 | . . . . . 6
⊢
(((abs‘(ℑ‘(𝐵 / 𝐴))) ∈ ℝ ∧ 𝑅 ∈ ℝ ∧ ((ℜ‘(𝐵 / 𝐴)) ∈ ℝ ∧ 0 <
(ℜ‘(𝐵 / 𝐴)))) →
(((abs‘(ℑ‘(𝐵 / 𝐴))) / (ℜ‘(𝐵 / 𝐴))) < 𝑅 ↔ (abs‘(ℑ‘(𝐵 / 𝐴))) < ((ℜ‘(𝐵 / 𝐴)) · 𝑅))) | 
| 214 | 151, 66, 64, 128, 213 | syl112anc 1375 | . . . . 5
⊢ (𝜑 →
(((abs‘(ℑ‘(𝐵 / 𝐴))) / (ℜ‘(𝐵 / 𝐴))) < 𝑅 ↔ (abs‘(ℑ‘(𝐵 / 𝐴))) < ((ℜ‘(𝐵 / 𝐴)) · 𝑅))) | 
| 215 | 212, 214 | mpbird 257 | . . . 4
⊢ (𝜑 →
((abs‘(ℑ‘(𝐵 / 𝐴))) / (ℜ‘(𝐵 / 𝐴))) < 𝑅) | 
| 216 | 150, 215 | eqbrtrd 5164 | . . 3
⊢ (𝜑 →
(abs‘(tan‘(ℑ‘(log‘(𝐵 / 𝐴))))) < 𝑅) | 
| 217 | 55, 136, 66, 138, 216 | lelttrd 11420 | . 2
⊢ (𝜑 →
(abs‘(ℑ‘(log‘(𝐵 / 𝐴)))) < 𝑅) | 
| 218 | 51, 217 | eqbrtrd 5164 | 1
⊢ (𝜑 →
(abs‘((ℑ‘(log‘𝐴)) − (ℑ‘(log‘𝐵)))) < 𝑅) |