Proof of Theorem abscxpbnd
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 1le1 11892 | . . . . 5
⊢ 1 ≤
1 | 
| 2 | 1 | a1i 11 | . . . 4
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝐵 = 0) → 1 ≤ 1) | 
| 3 |  | oveq12 7441 | . . . . . . . 8
⊢ ((𝐴 = 0 ∧ 𝐵 = 0) → (𝐴↑𝑐𝐵) =
(0↑𝑐0)) | 
| 4 | 3 | adantll 714 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝐵 = 0) → (𝐴↑𝑐𝐵) =
(0↑𝑐0)) | 
| 5 |  | 0cn 11254 | . . . . . . . 8
⊢ 0 ∈
ℂ | 
| 6 |  | cxp0 26713 | . . . . . . . 8
⊢ (0 ∈
ℂ → (0↑𝑐0) = 1) | 
| 7 | 5, 6 | ax-mp 5 | . . . . . . 7
⊢
(0↑𝑐0) = 1 | 
| 8 | 4, 7 | eqtrdi 2792 | . . . . . 6
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝐵 = 0) → (𝐴↑𝑐𝐵) = 1) | 
| 9 | 8 | fveq2d 6909 | . . . . 5
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝐵 = 0) → (abs‘(𝐴↑𝑐𝐵)) = (abs‘1)) | 
| 10 |  | abs1 15337 | . . . . 5
⊢
(abs‘1) = 1 | 
| 11 | 9, 10 | eqtrdi 2792 | . . . 4
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝐵 = 0) → (abs‘(𝐴↑𝑐𝐵)) = 1) | 
| 12 |  | fveq2 6905 | . . . . . . . . 9
⊢ (𝐵 = 0 → (ℜ‘𝐵) =
(ℜ‘0)) | 
| 13 |  | re0 15192 | . . . . . . . . 9
⊢
(ℜ‘0) = 0 | 
| 14 | 12, 13 | eqtrdi 2792 | . . . . . . . 8
⊢ (𝐵 = 0 → (ℜ‘𝐵) = 0) | 
| 15 | 14 | oveq2d 7448 | . . . . . . 7
⊢ (𝐵 = 0 → (𝑀↑𝑐(ℜ‘𝐵)) = (𝑀↑𝑐0)) | 
| 16 |  | abscxpbnd.4 | . . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℝ) | 
| 17 | 16 | recnd 11290 | . . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℂ) | 
| 18 | 17 | cxp0d 26748 | . . . . . . . 8
⊢ (𝜑 → (𝑀↑𝑐0) =
1) | 
| 19 | 18 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 = 0) → (𝑀↑𝑐0) =
1) | 
| 20 | 15, 19 | sylan9eqr 2798 | . . . . . 6
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝐵 = 0) → (𝑀↑𝑐(ℜ‘𝐵)) = 1) | 
| 21 |  | simpr 484 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝐵 = 0) → 𝐵 = 0) | 
| 22 | 21 | abs00bd 15331 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝐵 = 0) → (abs‘𝐵) = 0) | 
| 23 | 22 | oveq1d 7447 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝐵 = 0) → ((abs‘𝐵) · π) = (0 ·
π)) | 
| 24 |  | picn 26502 | . . . . . . . . . 10
⊢ π
∈ ℂ | 
| 25 | 24 | mul02i 11451 | . . . . . . . . 9
⊢ (0
· π) = 0 | 
| 26 | 23, 25 | eqtrdi 2792 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝐵 = 0) → ((abs‘𝐵) · π) = 0) | 
| 27 | 26 | fveq2d 6909 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝐵 = 0) → (exp‘((abs‘𝐵) · π)) =
(exp‘0)) | 
| 28 |  | ef0 16128 | . . . . . . 7
⊢
(exp‘0) = 1 | 
| 29 | 27, 28 | eqtrdi 2792 | . . . . . 6
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝐵 = 0) → (exp‘((abs‘𝐵) · π)) =
1) | 
| 30 | 20, 29 | oveq12d 7450 | . . . . 5
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝐵 = 0) → ((𝑀↑𝑐(ℜ‘𝐵)) ·
(exp‘((abs‘𝐵)
· π))) = (1 · 1)) | 
| 31 |  | 1t1e1 12429 | . . . . 5
⊢ (1
· 1) = 1 | 
| 32 | 30, 31 | eqtrdi 2792 | . . . 4
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝐵 = 0) → ((𝑀↑𝑐(ℜ‘𝐵)) ·
(exp‘((abs‘𝐵)
· π))) = 1) | 
| 33 | 2, 11, 32 | 3brtr4d 5174 | . . 3
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝐵 = 0) → (abs‘(𝐴↑𝑐𝐵)) ≤ ((𝑀↑𝑐(ℜ‘𝐵)) ·
(exp‘((abs‘𝐵)
· π)))) | 
| 34 |  | simplr 768 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝐵 ≠ 0) → 𝐴 = 0) | 
| 35 | 34 | oveq1d 7447 | . . . . . 6
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝐵 ≠ 0) → (𝐴↑𝑐𝐵) = (0↑𝑐𝐵)) | 
| 36 |  | abscxpbnd.2 | . . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℂ) | 
| 37 | 36 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 = 0) → 𝐵 ∈ ℂ) | 
| 38 |  | 0cxp 26709 | . . . . . . 7
⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) →
(0↑𝑐𝐵) = 0) | 
| 39 | 37, 38 | sylan 580 | . . . . . 6
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝐵 ≠ 0) →
(0↑𝑐𝐵) = 0) | 
| 40 | 35, 39 | eqtrd 2776 | . . . . 5
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝐵 ≠ 0) → (𝐴↑𝑐𝐵) = 0) | 
| 41 | 40 | abs00bd 15331 | . . . 4
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝐵 ≠ 0) → (abs‘(𝐴↑𝑐𝐵)) = 0) | 
| 42 |  | 0red 11265 | . . . . . . . 8
⊢ (𝜑 → 0 ∈
ℝ) | 
| 43 |  | abscxpbnd.1 | . . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℂ) | 
| 44 | 43 | abscld 15476 | . . . . . . . 8
⊢ (𝜑 → (abs‘𝐴) ∈
ℝ) | 
| 45 | 43 | absge0d 15484 | . . . . . . . 8
⊢ (𝜑 → 0 ≤ (abs‘𝐴)) | 
| 46 |  | abscxpbnd.5 | . . . . . . . 8
⊢ (𝜑 → (abs‘𝐴) ≤ 𝑀) | 
| 47 | 42, 44, 16, 45, 46 | letrd 11419 | . . . . . . 7
⊢ (𝜑 → 0 ≤ 𝑀) | 
| 48 | 36 | recld 15234 | . . . . . . 7
⊢ (𝜑 → (ℜ‘𝐵) ∈
ℝ) | 
| 49 | 16, 47, 48 | recxpcld 26766 | . . . . . 6
⊢ (𝜑 → (𝑀↑𝑐(ℜ‘𝐵)) ∈
ℝ) | 
| 50 | 49 | ad2antrr 726 | . . . . 5
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝐵 ≠ 0) → (𝑀↑𝑐(ℜ‘𝐵)) ∈
ℝ) | 
| 51 | 36 | abscld 15476 | . . . . . . . 8
⊢ (𝜑 → (abs‘𝐵) ∈
ℝ) | 
| 52 | 51 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝐵 ≠ 0) → (abs‘𝐵) ∈ ℝ) | 
| 53 |  | pire 26501 | . . . . . . 7
⊢ π
∈ ℝ | 
| 54 |  | remulcl 11241 | . . . . . . 7
⊢
(((abs‘𝐵)
∈ ℝ ∧ π ∈ ℝ) → ((abs‘𝐵) · π) ∈
ℝ) | 
| 55 | 52, 53, 54 | sylancl 586 | . . . . . 6
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝐵 ≠ 0) → ((abs‘𝐵) · π) ∈
ℝ) | 
| 56 | 55 | reefcld 16125 | . . . . 5
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝐵 ≠ 0) → (exp‘((abs‘𝐵) · π)) ∈
ℝ) | 
| 57 | 16, 47, 48 | cxpge0d 26767 | . . . . . 6
⊢ (𝜑 → 0 ≤ (𝑀↑𝑐(ℜ‘𝐵))) | 
| 58 | 57 | ad2antrr 726 | . . . . 5
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝐵 ≠ 0) → 0 ≤ (𝑀↑𝑐(ℜ‘𝐵))) | 
| 59 | 55 | rpefcld 16142 | . . . . . 6
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝐵 ≠ 0) → (exp‘((abs‘𝐵) · π)) ∈
ℝ+) | 
| 60 | 59 | rpge0d 13082 | . . . . 5
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝐵 ≠ 0) → 0 ≤
(exp‘((abs‘𝐵)
· π))) | 
| 61 | 50, 56, 58, 60 | mulge0d 11841 | . . . 4
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝐵 ≠ 0) → 0 ≤ ((𝑀↑𝑐(ℜ‘𝐵)) ·
(exp‘((abs‘𝐵)
· π)))) | 
| 62 | 41, 61 | eqbrtrd 5164 | . . 3
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝐵 ≠ 0) → (abs‘(𝐴↑𝑐𝐵)) ≤ ((𝑀↑𝑐(ℜ‘𝐵)) ·
(exp‘((abs‘𝐵)
· π)))) | 
| 63 | 33, 62 | pm2.61dane 3028 | . 2
⊢ ((𝜑 ∧ 𝐴 = 0) → (abs‘(𝐴↑𝑐𝐵)) ≤ ((𝑀↑𝑐(ℜ‘𝐵)) ·
(exp‘((abs‘𝐵)
· π)))) | 
| 64 | 43 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → 𝐴 ∈ ℂ) | 
| 65 |  | simpr 484 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → 𝐴 ≠ 0) | 
| 66 | 36 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → 𝐵 ∈ ℂ) | 
| 67 | 64, 65, 66 | cxpefd 26755 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (𝐴↑𝑐𝐵) = (exp‘(𝐵 · (log‘𝐴)))) | 
| 68 | 67 | fveq2d 6909 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (abs‘(𝐴↑𝑐𝐵)) =
(abs‘(exp‘(𝐵
· (log‘𝐴))))) | 
| 69 |  | logcl 26611 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (log‘𝐴) ∈
ℂ) | 
| 70 | 43, 69 | sylan 580 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (log‘𝐴) ∈ ℂ) | 
| 71 | 66, 70 | mulcld 11282 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (𝐵 · (log‘𝐴)) ∈ ℂ) | 
| 72 |  | absef 16234 | . . . . 5
⊢ ((𝐵 · (log‘𝐴)) ∈ ℂ →
(abs‘(exp‘(𝐵
· (log‘𝐴)))) =
(exp‘(ℜ‘(𝐵
· (log‘𝐴))))) | 
| 73 | 71, 72 | syl 17 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (abs‘(exp‘(𝐵 · (log‘𝐴)))) =
(exp‘(ℜ‘(𝐵
· (log‘𝐴))))) | 
| 74 | 66 | recld 15234 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (ℜ‘𝐵) ∈
ℝ) | 
| 75 | 70 | recld 15234 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ≠ 0) →
(ℜ‘(log‘𝐴)) ∈ ℝ) | 
| 76 | 74, 75 | remulcld 11292 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ((ℜ‘𝐵) ·
(ℜ‘(log‘𝐴))) ∈ ℝ) | 
| 77 | 76 | recnd 11290 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ((ℜ‘𝐵) ·
(ℜ‘(log‘𝐴))) ∈ ℂ) | 
| 78 | 66 | imcld 15235 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (ℑ‘𝐵) ∈
ℝ) | 
| 79 | 70 | imcld 15235 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ≠ 0) →
(ℑ‘(log‘𝐴)) ∈ ℝ) | 
| 80 | 79 | renegcld 11691 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ≠ 0) →
-(ℑ‘(log‘𝐴)) ∈ ℝ) | 
| 81 | 78, 80 | remulcld 11292 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ((ℑ‘𝐵) ·
-(ℑ‘(log‘𝐴))) ∈ ℝ) | 
| 82 | 81 | recnd 11290 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ((ℑ‘𝐵) ·
-(ℑ‘(log‘𝐴))) ∈ ℂ) | 
| 83 |  | efadd 16131 | . . . . . 6
⊢
((((ℜ‘𝐵)
· (ℜ‘(log‘𝐴))) ∈ ℂ ∧
((ℑ‘𝐵) ·
-(ℑ‘(log‘𝐴))) ∈ ℂ) →
(exp‘(((ℜ‘𝐵) · (ℜ‘(log‘𝐴))) + ((ℑ‘𝐵) ·
-(ℑ‘(log‘𝐴))))) = ((exp‘((ℜ‘𝐵) ·
(ℜ‘(log‘𝐴)))) ·
(exp‘((ℑ‘𝐵) · -(ℑ‘(log‘𝐴)))))) | 
| 84 | 77, 82, 83 | syl2anc 584 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ 0) →
(exp‘(((ℜ‘𝐵) · (ℜ‘(log‘𝐴))) + ((ℑ‘𝐵) ·
-(ℑ‘(log‘𝐴))))) = ((exp‘((ℜ‘𝐵) ·
(ℜ‘(log‘𝐴)))) ·
(exp‘((ℑ‘𝐵) · -(ℑ‘(log‘𝐴)))))) | 
| 85 | 78, 79 | remulcld 11292 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ((ℑ‘𝐵) ·
(ℑ‘(log‘𝐴))) ∈ ℝ) | 
| 86 | 85 | recnd 11290 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ((ℑ‘𝐵) ·
(ℑ‘(log‘𝐴))) ∈ ℂ) | 
| 87 | 77, 86 | negsubd 11627 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (((ℜ‘𝐵) ·
(ℜ‘(log‘𝐴))) + -((ℑ‘𝐵) · (ℑ‘(log‘𝐴)))) = (((ℜ‘𝐵) ·
(ℜ‘(log‘𝐴))) − ((ℑ‘𝐵) ·
(ℑ‘(log‘𝐴))))) | 
| 88 | 78 | recnd 11290 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (ℑ‘𝐵) ∈
ℂ) | 
| 89 | 79 | recnd 11290 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ≠ 0) →
(ℑ‘(log‘𝐴)) ∈ ℂ) | 
| 90 | 88, 89 | mulneg2d 11718 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ((ℑ‘𝐵) ·
-(ℑ‘(log‘𝐴))) = -((ℑ‘𝐵) · (ℑ‘(log‘𝐴)))) | 
| 91 | 90 | oveq2d 7448 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (((ℜ‘𝐵) ·
(ℜ‘(log‘𝐴))) + ((ℑ‘𝐵) · -(ℑ‘(log‘𝐴)))) = (((ℜ‘𝐵) ·
(ℜ‘(log‘𝐴))) + -((ℑ‘𝐵) · (ℑ‘(log‘𝐴))))) | 
| 92 | 66, 70 | remuld 15258 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (ℜ‘(𝐵 · (log‘𝐴))) = (((ℜ‘𝐵) ·
(ℜ‘(log‘𝐴))) − ((ℑ‘𝐵) ·
(ℑ‘(log‘𝐴))))) | 
| 93 | 87, 91, 92 | 3eqtr4d 2786 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (((ℜ‘𝐵) ·
(ℜ‘(log‘𝐴))) + ((ℑ‘𝐵) · -(ℑ‘(log‘𝐴)))) = (ℜ‘(𝐵 · (log‘𝐴)))) | 
| 94 | 93 | fveq2d 6909 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ 0) →
(exp‘(((ℜ‘𝐵) · (ℜ‘(log‘𝐴))) + ((ℑ‘𝐵) ·
-(ℑ‘(log‘𝐴))))) = (exp‘(ℜ‘(𝐵 · (log‘𝐴))))) | 
| 95 |  | relog 26640 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(ℜ‘(log‘𝐴)) = (log‘(abs‘𝐴))) | 
| 96 | 43, 95 | sylan 580 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ≠ 0) →
(ℜ‘(log‘𝐴)) = (log‘(abs‘𝐴))) | 
| 97 | 96 | oveq2d 7448 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ((ℜ‘𝐵) ·
(ℜ‘(log‘𝐴))) = ((ℜ‘𝐵) · (log‘(abs‘𝐴)))) | 
| 98 | 97 | fveq2d 6909 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ≠ 0) →
(exp‘((ℜ‘𝐵) · (ℜ‘(log‘𝐴)))) =
(exp‘((ℜ‘𝐵) · (log‘(abs‘𝐴))))) | 
| 99 | 44 | recnd 11290 | . . . . . . . . 9
⊢ (𝜑 → (abs‘𝐴) ∈
ℂ) | 
| 100 | 99 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈ ℂ) | 
| 101 | 43 | abs00ad 15330 | . . . . . . . . . 10
⊢ (𝜑 → ((abs‘𝐴) = 0 ↔ 𝐴 = 0)) | 
| 102 | 101 | necon3bid 2984 | . . . . . . . . 9
⊢ (𝜑 → ((abs‘𝐴) ≠ 0 ↔ 𝐴 ≠ 0)) | 
| 103 | 102 | biimpar 477 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (abs‘𝐴) ≠ 0) | 
| 104 | 74 | recnd 11290 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (ℜ‘𝐵) ∈
ℂ) | 
| 105 | 100, 103,
104 | cxpefd 26755 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ((abs‘𝐴)↑𝑐(ℜ‘𝐵)) =
(exp‘((ℜ‘𝐵)
· (log‘(abs‘𝐴))))) | 
| 106 | 98, 105 | eqtr4d 2779 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≠ 0) →
(exp‘((ℜ‘𝐵) · (ℜ‘(log‘𝐴)))) = ((abs‘𝐴)↑𝑐(ℜ‘𝐵))) | 
| 107 | 106 | oveq1d 7447 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ 0) →
((exp‘((ℜ‘𝐵) · (ℜ‘(log‘𝐴)))) ·
(exp‘((ℑ‘𝐵) · -(ℑ‘(log‘𝐴))))) = (((abs‘𝐴)↑𝑐(ℜ‘𝐵)) ·
(exp‘((ℑ‘𝐵)
· -(ℑ‘(log‘𝐴)))))) | 
| 108 | 84, 94, 107 | 3eqtr3d 2784 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 0) →
(exp‘(ℜ‘(𝐵
· (log‘𝐴)))) =
(((abs‘𝐴)↑𝑐(ℜ‘𝐵)) ·
(exp‘((ℑ‘𝐵)
· -(ℑ‘(log‘𝐴)))))) | 
| 109 | 68, 73, 108 | 3eqtrd 2780 | . . 3
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (abs‘(𝐴↑𝑐𝐵)) = (((abs‘𝐴)↑𝑐(ℜ‘𝐵)) ·
(exp‘((ℑ‘𝐵)
· -(ℑ‘(log‘𝐴)))))) | 
| 110 | 64 | abscld 15476 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈ ℝ) | 
| 111 | 64 | absge0d 15484 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → 0 ≤ (abs‘𝐴)) | 
| 112 | 110, 111,
74 | recxpcld 26766 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ((abs‘𝐴)↑𝑐(ℜ‘𝐵)) ∈
ℝ) | 
| 113 | 81 | reefcld 16125 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ 0) →
(exp‘((ℑ‘𝐵) · -(ℑ‘(log‘𝐴)))) ∈
ℝ) | 
| 114 | 112, 113 | remulcld 11292 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (((abs‘𝐴)↑𝑐(ℜ‘𝐵)) ·
(exp‘((ℑ‘𝐵)
· -(ℑ‘(log‘𝐴))))) ∈ ℝ) | 
| 115 | 49 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (𝑀↑𝑐(ℜ‘𝐵)) ∈
ℝ) | 
| 116 | 115, 113 | remulcld 11292 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ((𝑀↑𝑐(ℜ‘𝐵)) ·
(exp‘((ℑ‘𝐵) · -(ℑ‘(log‘𝐴))))) ∈
ℝ) | 
| 117 | 51, 53, 54 | sylancl 586 | . . . . . . 7
⊢ (𝜑 → ((abs‘𝐵) · π) ∈
ℝ) | 
| 118 | 117 | reefcld 16125 | . . . . . 6
⊢ (𝜑 →
(exp‘((abs‘𝐵)
· π)) ∈ ℝ) | 
| 119 | 118 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (exp‘((abs‘𝐵) · π)) ∈
ℝ) | 
| 120 | 115, 119 | remulcld 11292 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ((𝑀↑𝑐(ℜ‘𝐵)) ·
(exp‘((abs‘𝐵)
· π))) ∈ ℝ) | 
| 121 | 81 | rpefcld 16142 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≠ 0) →
(exp‘((ℑ‘𝐵) · -(ℑ‘(log‘𝐴)))) ∈
ℝ+) | 
| 122 | 121 | rpge0d 13082 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → 0 ≤
(exp‘((ℑ‘𝐵) · -(ℑ‘(log‘𝐴))))) | 
| 123 | 16 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → 𝑀 ∈ ℝ) | 
| 124 |  | abscxpbnd.3 | . . . . . . 7
⊢ (𝜑 → 0 ≤ (ℜ‘𝐵)) | 
| 125 | 124 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → 0 ≤ (ℜ‘𝐵)) | 
| 126 | 46 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (abs‘𝐴) ≤ 𝑀) | 
| 127 | 110, 111,
123, 74, 125, 126 | cxple2ad 26768 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ((abs‘𝐴)↑𝑐(ℜ‘𝐵)) ≤ (𝑀↑𝑐(ℜ‘𝐵))) | 
| 128 | 112, 115,
113, 122, 127 | lemul1ad 12208 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (((abs‘𝐴)↑𝑐(ℜ‘𝐵)) ·
(exp‘((ℑ‘𝐵)
· -(ℑ‘(log‘𝐴))))) ≤ ((𝑀↑𝑐(ℜ‘𝐵)) ·
(exp‘((ℑ‘𝐵)
· -(ℑ‘(log‘𝐴)))))) | 
| 129 | 57 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → 0 ≤ (𝑀↑𝑐(ℜ‘𝐵))) | 
| 130 | 88 | abscld 15476 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ≠ 0) →
(abs‘(ℑ‘𝐵)) ∈ ℝ) | 
| 131 | 80 | recnd 11290 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ≠ 0) →
-(ℑ‘(log‘𝐴)) ∈ ℂ) | 
| 132 | 131 | abscld 15476 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ≠ 0) →
(abs‘-(ℑ‘(log‘𝐴))) ∈ ℝ) | 
| 133 | 130, 132 | remulcld 11292 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ≠ 0) →
((abs‘(ℑ‘𝐵)) ·
(abs‘-(ℑ‘(log‘𝐴)))) ∈ ℝ) | 
| 134 | 117 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ((abs‘𝐵) · π) ∈
ℝ) | 
| 135 | 81 | leabsd 15454 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ((ℑ‘𝐵) ·
-(ℑ‘(log‘𝐴))) ≤ (abs‘((ℑ‘𝐵) ·
-(ℑ‘(log‘𝐴))))) | 
| 136 | 88, 131 | absmuld 15494 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ≠ 0) →
(abs‘((ℑ‘𝐵) · -(ℑ‘(log‘𝐴)))) =
((abs‘(ℑ‘𝐵)) ·
(abs‘-(ℑ‘(log‘𝐴))))) | 
| 137 | 135, 136 | breqtrd 5168 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ((ℑ‘𝐵) ·
-(ℑ‘(log‘𝐴))) ≤ ((abs‘(ℑ‘𝐵)) ·
(abs‘-(ℑ‘(log‘𝐴))))) | 
| 138 | 66 | abscld 15476 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (abs‘𝐵) ∈ ℝ) | 
| 139 | 138, 132 | remulcld 11292 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ((abs‘𝐵) ·
(abs‘-(ℑ‘(log‘𝐴)))) ∈ ℝ) | 
| 140 | 131 | absge0d 15484 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → 0 ≤
(abs‘-(ℑ‘(log‘𝐴)))) | 
| 141 |  | absimle 15349 | . . . . . . . . . 10
⊢ (𝐵 ∈ ℂ →
(abs‘(ℑ‘𝐵)) ≤ (abs‘𝐵)) | 
| 142 | 66, 141 | syl 17 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ≠ 0) →
(abs‘(ℑ‘𝐵)) ≤ (abs‘𝐵)) | 
| 143 | 130, 138,
132, 140, 142 | lemul1ad 12208 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ≠ 0) →
((abs‘(ℑ‘𝐵)) ·
(abs‘-(ℑ‘(log‘𝐴)))) ≤ ((abs‘𝐵) ·
(abs‘-(ℑ‘(log‘𝐴))))) | 
| 144 | 53 | a1i 11 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → π ∈
ℝ) | 
| 145 | 66 | absge0d 15484 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → 0 ≤ (abs‘𝐵)) | 
| 146 | 89 | absnegd 15489 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 ≠ 0) →
(abs‘-(ℑ‘(log‘𝐴))) =
(abs‘(ℑ‘(log‘𝐴)))) | 
| 147 |  | logimcl 26612 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (-π <
(ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) ≤ π)) | 
| 148 | 43, 147 | sylan 580 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (-π <
(ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) ≤ π)) | 
| 149 | 148 | simpld 494 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → -π <
(ℑ‘(log‘𝐴))) | 
| 150 | 53 | renegcli 11571 | . . . . . . . . . . . . 13
⊢ -π
∈ ℝ | 
| 151 |  | ltle 11350 | . . . . . . . . . . . . 13
⊢ ((-π
∈ ℝ ∧ (ℑ‘(log‘𝐴)) ∈ ℝ) → (-π <
(ℑ‘(log‘𝐴)) → -π ≤
(ℑ‘(log‘𝐴)))) | 
| 152 | 150, 79, 151 | sylancr 587 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (-π <
(ℑ‘(log‘𝐴)) → -π ≤
(ℑ‘(log‘𝐴)))) | 
| 153 | 149, 152 | mpd 15 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → -π ≤
(ℑ‘(log‘𝐴))) | 
| 154 | 148 | simprd 495 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐴 ≠ 0) →
(ℑ‘(log‘𝐴)) ≤ π) | 
| 155 |  | absle 15355 | . . . . . . . . . . . 12
⊢
(((ℑ‘(log‘𝐴)) ∈ ℝ ∧ π ∈ ℝ)
→ ((abs‘(ℑ‘(log‘𝐴))) ≤ π ↔ (-π ≤
(ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) ≤ π))) | 
| 156 | 79, 53, 155 | sylancl 586 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐴 ≠ 0) →
((abs‘(ℑ‘(log‘𝐴))) ≤ π ↔ (-π ≤
(ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) ≤ π))) | 
| 157 | 153, 154,
156 | mpbir2and 713 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 ≠ 0) →
(abs‘(ℑ‘(log‘𝐴))) ≤ π) | 
| 158 | 146, 157 | eqbrtrd 5164 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ≠ 0) →
(abs‘-(ℑ‘(log‘𝐴))) ≤ π) | 
| 159 | 132, 144,
138, 145, 158 | lemul2ad 12209 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ((abs‘𝐵) ·
(abs‘-(ℑ‘(log‘𝐴)))) ≤ ((abs‘𝐵) · π)) | 
| 160 | 133, 139,
134, 143, 159 | letrd 11419 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ≠ 0) →
((abs‘(ℑ‘𝐵)) ·
(abs‘-(ℑ‘(log‘𝐴)))) ≤ ((abs‘𝐵) · π)) | 
| 161 | 81, 133, 134, 137, 160 | letrd 11419 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ((ℑ‘𝐵) ·
-(ℑ‘(log‘𝐴))) ≤ ((abs‘𝐵) · π)) | 
| 162 |  | efle 16155 | . . . . . . 7
⊢
((((ℑ‘𝐵)
· -(ℑ‘(log‘𝐴))) ∈ ℝ ∧ ((abs‘𝐵) · π) ∈ ℝ)
→ (((ℑ‘𝐵)
· -(ℑ‘(log‘𝐴))) ≤ ((abs‘𝐵) · π) ↔
(exp‘((ℑ‘𝐵) · -(ℑ‘(log‘𝐴)))) ≤
(exp‘((abs‘𝐵)
· π)))) | 
| 163 | 81, 134, 162 | syl2anc 584 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (((ℑ‘𝐵) ·
-(ℑ‘(log‘𝐴))) ≤ ((abs‘𝐵) · π) ↔
(exp‘((ℑ‘𝐵) · -(ℑ‘(log‘𝐴)))) ≤
(exp‘((abs‘𝐵)
· π)))) | 
| 164 | 161, 163 | mpbid 232 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ 0) →
(exp‘((ℑ‘𝐵) · -(ℑ‘(log‘𝐴)))) ≤
(exp‘((abs‘𝐵)
· π))) | 
| 165 | 113, 119,
115, 129, 164 | lemul2ad 12209 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ((𝑀↑𝑐(ℜ‘𝐵)) ·
(exp‘((ℑ‘𝐵) · -(ℑ‘(log‘𝐴))))) ≤ ((𝑀↑𝑐(ℜ‘𝐵)) ·
(exp‘((abs‘𝐵)
· π)))) | 
| 166 | 114, 116,
120, 128, 165 | letrd 11419 | . . 3
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (((abs‘𝐴)↑𝑐(ℜ‘𝐵)) ·
(exp‘((ℑ‘𝐵)
· -(ℑ‘(log‘𝐴))))) ≤ ((𝑀↑𝑐(ℜ‘𝐵)) ·
(exp‘((abs‘𝐵)
· π)))) | 
| 167 | 109, 166 | eqbrtrd 5164 | . 2
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (abs‘(𝐴↑𝑐𝐵)) ≤ ((𝑀↑𝑐(ℜ‘𝐵)) ·
(exp‘((abs‘𝐵)
· π)))) | 
| 168 | 63, 167 | pm2.61dane 3028 | 1
⊢ (𝜑 → (abs‘(𝐴↑𝑐𝐵)) ≤ ((𝑀↑𝑐(ℜ‘𝐵)) ·
(exp‘((abs‘𝐵)
· π)))) |