This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem abscxpbnd

Description: Bound on the absolute value of a complex power. (Contributed by Mario Carneiro, 15-Sep-2014)

Ref Expression
Hypotheses abscxpbnd.1 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
abscxpbnd.2 ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
abscxpbnd.3 ⊢ ( 𝜑 → 0 ≤ ( ℜ ‘ 𝐵 ) )
abscxpbnd.4 ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
abscxpbnd.5 ⊢ ( 𝜑 → ( abs ‘ 𝐴 ) ≤ 𝑀 )
Assertion abscxpbnd ( 𝜑 → ( abs ‘ ( 𝐴 ↑𝑐 𝐵 ) ) ≤ ( ( 𝑀 ↑𝑐 ( ℜ ‘ 𝐵 ) ) · ( exp ‘ ( ( abs ‘ 𝐵 ) · π ) ) ) )

Proof

Step Hyp Ref Expression
1 abscxpbnd.1 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2 abscxpbnd.2 ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3 abscxpbnd.3 ⊢ ( 𝜑 → 0 ≤ ( ℜ ‘ 𝐵 ) )
4 abscxpbnd.4 ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
5 abscxpbnd.5 ⊢ ( 𝜑 → ( abs ‘ 𝐴 ) ≤ 𝑀 )
6 1le1 ⊢ 1 ≤ 1
7 6 a1i ⊢ ( ( ( 𝜑 ∧ 𝐴 = 0 ) ∧ 𝐵 = 0 ) → 1 ≤ 1 )
8 oveq12 ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) → ( 𝐴 ↑𝑐 𝐵 ) = ( 0 ↑𝑐 0 ) )
9 8 adantll ⊢ ( ( ( 𝜑 ∧ 𝐴 = 0 ) ∧ 𝐵 = 0 ) → ( 𝐴 ↑𝑐 𝐵 ) = ( 0 ↑𝑐 0 ) )
10 0cn ⊢ 0 ∈ ℂ
11 cxp0 ⊢ ( 0 ∈ ℂ → ( 0 ↑𝑐 0 ) = 1 )
12 10 11 ax-mp ⊢ ( 0 ↑𝑐 0 ) = 1
13 9 12 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝐴 = 0 ) ∧ 𝐵 = 0 ) → ( 𝐴 ↑𝑐 𝐵 ) = 1 )
14 13 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝐴 = 0 ) ∧ 𝐵 = 0 ) → ( abs ‘ ( 𝐴 ↑𝑐 𝐵 ) ) = ( abs ‘ 1 ) )
15 abs1 ⊢ ( abs ‘ 1 ) = 1
16 14 15 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝐴 = 0 ) ∧ 𝐵 = 0 ) → ( abs ‘ ( 𝐴 ↑𝑐 𝐵 ) ) = 1 )
17 fveq2 ⊢ ( 𝐵 = 0 → ( ℜ ‘ 𝐵 ) = ( ℜ ‘ 0 ) )
18 re0 ⊢ ( ℜ ‘ 0 ) = 0
19 17 18 eqtrdi ⊢ ( 𝐵 = 0 → ( ℜ ‘ 𝐵 ) = 0 )
20 19 oveq2d ⊢ ( 𝐵 = 0 → ( 𝑀 ↑𝑐 ( ℜ ‘ 𝐵 ) ) = ( 𝑀 ↑𝑐 0 ) )
21 4 recnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
22 21 cxp0d ⊢ ( 𝜑 → ( 𝑀 ↑𝑐 0 ) = 1 )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = 0 ) → ( 𝑀 ↑𝑐 0 ) = 1 )
24 20 23 sylan9eqr ⊢ ( ( ( 𝜑 ∧ 𝐴 = 0 ) ∧ 𝐵 = 0 ) → ( 𝑀 ↑𝑐 ( ℜ ‘ 𝐵 ) ) = 1 )
25 simpr ⊢ ( ( ( 𝜑 ∧ 𝐴 = 0 ) ∧ 𝐵 = 0 ) → 𝐵 = 0 )
26 25 abs00bd ⊢ ( ( ( 𝜑 ∧ 𝐴 = 0 ) ∧ 𝐵 = 0 ) → ( abs ‘ 𝐵 ) = 0 )
27 26 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝐴 = 0 ) ∧ 𝐵 = 0 ) → ( ( abs ‘ 𝐵 ) · π ) = ( 0 · π ) )
28 picn ⊢ π ∈ ℂ
29 28 mul02i ⊢ ( 0 · π ) = 0
30 27 29 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝐴 = 0 ) ∧ 𝐵 = 0 ) → ( ( abs ‘ 𝐵 ) · π ) = 0 )
31 30 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝐴 = 0 ) ∧ 𝐵 = 0 ) → ( exp ‘ ( ( abs ‘ 𝐵 ) · π ) ) = ( exp ‘ 0 ) )
32 ef0 ⊢ ( exp ‘ 0 ) = 1
33 31 32 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝐴 = 0 ) ∧ 𝐵 = 0 ) → ( exp ‘ ( ( abs ‘ 𝐵 ) · π ) ) = 1 )
34 24 33 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝐴 = 0 ) ∧ 𝐵 = 0 ) → ( ( 𝑀 ↑𝑐 ( ℜ ‘ 𝐵 ) ) · ( exp ‘ ( ( abs ‘ 𝐵 ) · π ) ) ) = ( 1 · 1 ) )
35 1t1e1 ⊢ ( 1 · 1 ) = 1
36 34 35 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝐴 = 0 ) ∧ 𝐵 = 0 ) → ( ( 𝑀 ↑𝑐 ( ℜ ‘ 𝐵 ) ) · ( exp ‘ ( ( abs ‘ 𝐵 ) · π ) ) ) = 1 )
37 7 16 36 3brtr4d ⊢ ( ( ( 𝜑 ∧ 𝐴 = 0 ) ∧ 𝐵 = 0 ) → ( abs ‘ ( 𝐴 ↑𝑐 𝐵 ) ) ≤ ( ( 𝑀 ↑𝑐 ( ℜ ‘ 𝐵 ) ) · ( exp ‘ ( ( abs ‘ 𝐵 ) · π ) ) ) )
38 simplr ⊢ ( ( ( 𝜑 ∧ 𝐴 = 0 ) ∧ 𝐵 ≠ 0 ) → 𝐴 = 0 )
39 38 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝐴 = 0 ) ∧ 𝐵 ≠ 0 ) → ( 𝐴 ↑𝑐 𝐵 ) = ( 0 ↑𝑐 𝐵 ) )
40 2 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = 0 ) → 𝐵 ∈ ℂ )
41 0cxp ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( 0 ↑𝑐 𝐵 ) = 0 )
42 40 41 sylan ⊢ ( ( ( 𝜑 ∧ 𝐴 = 0 ) ∧ 𝐵 ≠ 0 ) → ( 0 ↑𝑐 𝐵 ) = 0 )
43 39 42 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝐴 = 0 ) ∧ 𝐵 ≠ 0 ) → ( 𝐴 ↑𝑐 𝐵 ) = 0 )
44 43 abs00bd ⊢ ( ( ( 𝜑 ∧ 𝐴 = 0 ) ∧ 𝐵 ≠ 0 ) → ( abs ‘ ( 𝐴 ↑𝑐 𝐵 ) ) = 0 )
45 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
46 1 abscld ⊢ ( 𝜑 → ( abs ‘ 𝐴 ) ∈ ℝ )
47 1 absge0d ⊢ ( 𝜑 → 0 ≤ ( abs ‘ 𝐴 ) )
48 45 46 4 47 5 letrd ⊢ ( 𝜑 → 0 ≤ 𝑀 )
49 2 recld ⊢ ( 𝜑 → ( ℜ ‘ 𝐵 ) ∈ ℝ )
50 4 48 49 recxpcld ⊢ ( 𝜑 → ( 𝑀 ↑𝑐 ( ℜ ‘ 𝐵 ) ) ∈ ℝ )
51 50 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 = 0 ) ∧ 𝐵 ≠ 0 ) → ( 𝑀 ↑𝑐 ( ℜ ‘ 𝐵 ) ) ∈ ℝ )
52 2 abscld ⊢ ( 𝜑 → ( abs ‘ 𝐵 ) ∈ ℝ )
53 52 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 = 0 ) ∧ 𝐵 ≠ 0 ) → ( abs ‘ 𝐵 ) ∈ ℝ )
54 pire ⊢ π ∈ ℝ
55 remulcl ⊢ ( ( ( abs ‘ 𝐵 ) ∈ ℝ ∧ π ∈ ℝ ) → ( ( abs ‘ 𝐵 ) · π ) ∈ ℝ )
56 53 54 55 sylancl ⊢ ( ( ( 𝜑 ∧ 𝐴 = 0 ) ∧ 𝐵 ≠ 0 ) → ( ( abs ‘ 𝐵 ) · π ) ∈ ℝ )
57 56 reefcld ⊢ ( ( ( 𝜑 ∧ 𝐴 = 0 ) ∧ 𝐵 ≠ 0 ) → ( exp ‘ ( ( abs ‘ 𝐵 ) · π ) ) ∈ ℝ )
58 4 48 49 cxpge0d ⊢ ( 𝜑 → 0 ≤ ( 𝑀 ↑𝑐 ( ℜ ‘ 𝐵 ) ) )
59 58 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 = 0 ) ∧ 𝐵 ≠ 0 ) → 0 ≤ ( 𝑀 ↑𝑐 ( ℜ ‘ 𝐵 ) ) )
60 56 rpefcld ⊢ ( ( ( 𝜑 ∧ 𝐴 = 0 ) ∧ 𝐵 ≠ 0 ) → ( exp ‘ ( ( abs ‘ 𝐵 ) · π ) ) ∈ ℝ+ )
61 60 rpge0d ⊢ ( ( ( 𝜑 ∧ 𝐴 = 0 ) ∧ 𝐵 ≠ 0 ) → 0 ≤ ( exp ‘ ( ( abs ‘ 𝐵 ) · π ) ) )
62 51 57 59 61 mulge0d ⊢ ( ( ( 𝜑 ∧ 𝐴 = 0 ) ∧ 𝐵 ≠ 0 ) → 0 ≤ ( ( 𝑀 ↑𝑐 ( ℜ ‘ 𝐵 ) ) · ( exp ‘ ( ( abs ‘ 𝐵 ) · π ) ) ) )
63 44 62 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝐴 = 0 ) ∧ 𝐵 ≠ 0 ) → ( abs ‘ ( 𝐴 ↑𝑐 𝐵 ) ) ≤ ( ( 𝑀 ↑𝑐 ( ℜ ‘ 𝐵 ) ) · ( exp ‘ ( ( abs ‘ 𝐵 ) · π ) ) ) )
64 37 63 pm2.61dane ⊢ ( ( 𝜑 ∧ 𝐴 = 0 ) → ( abs ‘ ( 𝐴 ↑𝑐 𝐵 ) ) ≤ ( ( 𝑀 ↑𝑐 ( ℜ ‘ 𝐵 ) ) · ( exp ‘ ( ( abs ‘ 𝐵 ) · π ) ) ) )
65 1 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ ℂ )
66 simpr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → 𝐴 ≠ 0 )
67 2 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → 𝐵 ∈ ℂ )
68 65 66 67 cxpefd ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( 𝐴 ↑𝑐 𝐵 ) = ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) )
69 68 fveq2d ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( abs ‘ ( 𝐴 ↑𝑐 𝐵 ) ) = ( abs ‘ ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ) )
70 logcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( log ‘ 𝐴 ) ∈ ℂ )
71 1 70 sylan ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( log ‘ 𝐴 ) ∈ ℂ )
72 67 71 mulcld ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( 𝐵 · ( log ‘ 𝐴 ) ) ∈ ℂ )
73 absef ⊢ ( ( 𝐵 · ( log ‘ 𝐴 ) ) ∈ ℂ → ( abs ‘ ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ) = ( exp ‘ ( ℜ ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ) )
74 72 73 syl ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( abs ‘ ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ) = ( exp ‘ ( ℜ ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ) )
75 67 recld ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ℜ ‘ 𝐵 ) ∈ ℝ )
76 71 recld ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ℜ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ )
77 75 76 remulcld ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ( ℜ ‘ 𝐵 ) · ( ℜ ‘ ( log ‘ 𝐴 ) ) ) ∈ ℝ )
78 77 recnd ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ( ℜ ‘ 𝐵 ) · ( ℜ ‘ ( log ‘ 𝐴 ) ) ) ∈ ℂ )
79 67 imcld ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ℑ ‘ 𝐵 ) ∈ ℝ )
80 71 imcld ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ )
81 80 renegcld ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → - ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ )
82 79 81 remulcld ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ( ℑ ‘ 𝐵 ) · - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∈ ℝ )
83 82 recnd ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ( ℑ ‘ 𝐵 ) · - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∈ ℂ )
84 efadd ⊢ ( ( ( ( ℜ ‘ 𝐵 ) · ( ℜ ‘ ( log ‘ 𝐴 ) ) ) ∈ ℂ ∧ ( ( ℑ ‘ 𝐵 ) · - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∈ ℂ ) → ( exp ‘ ( ( ( ℜ ‘ 𝐵 ) · ( ℜ ‘ ( log ‘ 𝐴 ) ) ) + ( ( ℑ ‘ 𝐵 ) · - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) = ( ( exp ‘ ( ( ℜ ‘ 𝐵 ) · ( ℜ ‘ ( log ‘ 𝐴 ) ) ) ) · ( exp ‘ ( ( ℑ ‘ 𝐵 ) · - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) )
85 78 83 84 syl2anc ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( ( ( ℜ ‘ 𝐵 ) · ( ℜ ‘ ( log ‘ 𝐴 ) ) ) + ( ( ℑ ‘ 𝐵 ) · - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) = ( ( exp ‘ ( ( ℜ ‘ 𝐵 ) · ( ℜ ‘ ( log ‘ 𝐴 ) ) ) ) · ( exp ‘ ( ( ℑ ‘ 𝐵 ) · - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) )
86 79 80 remulcld ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ( ℑ ‘ 𝐵 ) · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∈ ℝ )
87 86 recnd ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ( ℑ ‘ 𝐵 ) · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∈ ℂ )
88 78 87 negsubd ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ( ( ℜ ‘ 𝐵 ) · ( ℜ ‘ ( log ‘ 𝐴 ) ) ) + - ( ( ℑ ‘ 𝐵 ) · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) = ( ( ( ℜ ‘ 𝐵 ) · ( ℜ ‘ ( log ‘ 𝐴 ) ) ) − ( ( ℑ ‘ 𝐵 ) · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) )
89 79 recnd ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ℑ ‘ 𝐵 ) ∈ ℂ )
90 80 recnd ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℂ )
91 89 90 mulneg2d ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ( ℑ ‘ 𝐵 ) · - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = - ( ( ℑ ‘ 𝐵 ) · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
92 91 oveq2d ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ( ( ℜ ‘ 𝐵 ) · ( ℜ ‘ ( log ‘ 𝐴 ) ) ) + ( ( ℑ ‘ 𝐵 ) · - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) = ( ( ( ℜ ‘ 𝐵 ) · ( ℜ ‘ ( log ‘ 𝐴 ) ) ) + - ( ( ℑ ‘ 𝐵 ) · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) )
93 67 71 remuld ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ℜ ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) = ( ( ( ℜ ‘ 𝐵 ) · ( ℜ ‘ ( log ‘ 𝐴 ) ) ) − ( ( ℑ ‘ 𝐵 ) · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) )
94 88 92 93 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ( ( ℜ ‘ 𝐵 ) · ( ℜ ‘ ( log ‘ 𝐴 ) ) ) + ( ( ℑ ‘ 𝐵 ) · - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) = ( ℜ ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) )
95 94 fveq2d ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( ( ( ℜ ‘ 𝐵 ) · ( ℜ ‘ ( log ‘ 𝐴 ) ) ) + ( ( ℑ ‘ 𝐵 ) · - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) = ( exp ‘ ( ℜ ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ) )
96 relog ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℜ ‘ ( log ‘ 𝐴 ) ) = ( log ‘ ( abs ‘ 𝐴 ) ) )
97 1 96 sylan ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ℜ ‘ ( log ‘ 𝐴 ) ) = ( log ‘ ( abs ‘ 𝐴 ) ) )
98 97 oveq2d ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ( ℜ ‘ 𝐵 ) · ( ℜ ‘ ( log ‘ 𝐴 ) ) ) = ( ( ℜ ‘ 𝐵 ) · ( log ‘ ( abs ‘ 𝐴 ) ) ) )
99 98 fveq2d ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( ( ℜ ‘ 𝐵 ) · ( ℜ ‘ ( log ‘ 𝐴 ) ) ) ) = ( exp ‘ ( ( ℜ ‘ 𝐵 ) · ( log ‘ ( abs ‘ 𝐴 ) ) ) ) )
100 46 recnd ⊢ ( 𝜑 → ( abs ‘ 𝐴 ) ∈ ℂ )
101 100 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ∈ ℂ )
102 1 abs00ad ⊢ ( 𝜑 → ( ( abs ‘ 𝐴 ) = 0 ↔ 𝐴 = 0 ) )
103 102 necon3bid ⊢ ( 𝜑 → ( ( abs ‘ 𝐴 ) ≠ 0 ↔ 𝐴 ≠ 0 ) )
104 103 biimpar ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ≠ 0 )
105 75 recnd ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ℜ ‘ 𝐵 ) ∈ ℂ )
106 101 104 105 cxpefd ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ( abs ‘ 𝐴 ) ↑𝑐 ( ℜ ‘ 𝐵 ) ) = ( exp ‘ ( ( ℜ ‘ 𝐵 ) · ( log ‘ ( abs ‘ 𝐴 ) ) ) ) )
107 99 106 eqtr4d ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( ( ℜ ‘ 𝐵 ) · ( ℜ ‘ ( log ‘ 𝐴 ) ) ) ) = ( ( abs ‘ 𝐴 ) ↑𝑐 ( ℜ ‘ 𝐵 ) ) )
108 107 oveq1d ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ( exp ‘ ( ( ℜ ‘ 𝐵 ) · ( ℜ ‘ ( log ‘ 𝐴 ) ) ) ) · ( exp ‘ ( ( ℑ ‘ 𝐵 ) · - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) = ( ( ( abs ‘ 𝐴 ) ↑𝑐 ( ℜ ‘ 𝐵 ) ) · ( exp ‘ ( ( ℑ ‘ 𝐵 ) · - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) )
109 85 95 108 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( ℜ ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ) = ( ( ( abs ‘ 𝐴 ) ↑𝑐 ( ℜ ‘ 𝐵 ) ) · ( exp ‘ ( ( ℑ ‘ 𝐵 ) · - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) )
110 69 74 109 3eqtrd ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( abs ‘ ( 𝐴 ↑𝑐 𝐵 ) ) = ( ( ( abs ‘ 𝐴 ) ↑𝑐 ( ℜ ‘ 𝐵 ) ) · ( exp ‘ ( ( ℑ ‘ 𝐵 ) · - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) )
111 65 abscld ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ∈ ℝ )
112 65 absge0d ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → 0 ≤ ( abs ‘ 𝐴 ) )
113 111 112 75 recxpcld ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ( abs ‘ 𝐴 ) ↑𝑐 ( ℜ ‘ 𝐵 ) ) ∈ ℝ )
114 82 reefcld ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( ( ℑ ‘ 𝐵 ) · - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ∈ ℝ )
115 113 114 remulcld ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ( ( abs ‘ 𝐴 ) ↑𝑐 ( ℜ ‘ 𝐵 ) ) · ( exp ‘ ( ( ℑ ‘ 𝐵 ) · - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) ∈ ℝ )
116 50 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( 𝑀 ↑𝑐 ( ℜ ‘ 𝐵 ) ) ∈ ℝ )
117 116 114 remulcld ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ( 𝑀 ↑𝑐 ( ℜ ‘ 𝐵 ) ) · ( exp ‘ ( ( ℑ ‘ 𝐵 ) · - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) ∈ ℝ )
118 52 54 55 sylancl ⊢ ( 𝜑 → ( ( abs ‘ 𝐵 ) · π ) ∈ ℝ )
119 118 reefcld ⊢ ( 𝜑 → ( exp ‘ ( ( abs ‘ 𝐵 ) · π ) ) ∈ ℝ )
120 119 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( ( abs ‘ 𝐵 ) · π ) ) ∈ ℝ )
121 116 120 remulcld ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ( 𝑀 ↑𝑐 ( ℜ ‘ 𝐵 ) ) · ( exp ‘ ( ( abs ‘ 𝐵 ) · π ) ) ) ∈ ℝ )
122 82 rpefcld ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( ( ℑ ‘ 𝐵 ) · - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ∈ ℝ+ )
123 122 rpge0d ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → 0 ≤ ( exp ‘ ( ( ℑ ‘ 𝐵 ) · - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) )
124 4 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → 𝑀 ∈ ℝ )
125 3 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → 0 ≤ ( ℜ ‘ 𝐵 ) )
126 5 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ≤ 𝑀 )
127 111 112 124 75 125 126 cxple2ad ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ( abs ‘ 𝐴 ) ↑𝑐 ( ℜ ‘ 𝐵 ) ) ≤ ( 𝑀 ↑𝑐 ( ℜ ‘ 𝐵 ) ) )
128 113 116 114 123 127 lemul1ad ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ( ( abs ‘ 𝐴 ) ↑𝑐 ( ℜ ‘ 𝐵 ) ) · ( exp ‘ ( ( ℑ ‘ 𝐵 ) · - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) ≤ ( ( 𝑀 ↑𝑐 ( ℜ ‘ 𝐵 ) ) · ( exp ‘ ( ( ℑ ‘ 𝐵 ) · - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) )
129 58 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → 0 ≤ ( 𝑀 ↑𝑐 ( ℜ ‘ 𝐵 ) ) )
130 89 abscld ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( abs ‘ ( ℑ ‘ 𝐵 ) ) ∈ ℝ )
131 81 recnd ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → - ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℂ )
132 131 abscld ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( abs ‘ - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∈ ℝ )
133 130 132 remulcld ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ( abs ‘ ( ℑ ‘ 𝐵 ) ) · ( abs ‘ - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ∈ ℝ )
134 118 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ( abs ‘ 𝐵 ) · π ) ∈ ℝ )
135 82 leabsd ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ( ℑ ‘ 𝐵 ) · - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ≤ ( abs ‘ ( ( ℑ ‘ 𝐵 ) · - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) )
136 89 131 absmuld ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( abs ‘ ( ( ℑ ‘ 𝐵 ) · - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) = ( ( abs ‘ ( ℑ ‘ 𝐵 ) ) · ( abs ‘ - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) )
137 135 136 breqtrd ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ( ℑ ‘ 𝐵 ) · - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ≤ ( ( abs ‘ ( ℑ ‘ 𝐵 ) ) · ( abs ‘ - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) )
138 67 abscld ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐵 ) ∈ ℝ )
139 138 132 remulcld ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ( abs ‘ 𝐵 ) · ( abs ‘ - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ∈ ℝ )
140 131 absge0d ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → 0 ≤ ( abs ‘ - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
141 absimle ⊢ ( 𝐵 ∈ ℂ → ( abs ‘ ( ℑ ‘ 𝐵 ) ) ≤ ( abs ‘ 𝐵 ) )
142 67 141 syl ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( abs ‘ ( ℑ ‘ 𝐵 ) ) ≤ ( abs ‘ 𝐵 ) )
143 130 138 132 140 142 lemul1ad ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ( abs ‘ ( ℑ ‘ 𝐵 ) ) · ( abs ‘ - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ≤ ( ( abs ‘ 𝐵 ) · ( abs ‘ - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) )
144 54 a1i ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → π ∈ ℝ )
145 67 absge0d ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → 0 ≤ ( abs ‘ 𝐵 ) )
146 90 absnegd ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( abs ‘ - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
147 logimcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π ) )
148 1 147 sylan ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π ) )
149 148 simpld ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) )
150 54 renegcli ⊢ - π ∈ ℝ
151 ltle ⊢ ( ( - π ∈ ℝ ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ ) → ( - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) → - π ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
152 150 80 151 sylancr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) → - π ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
153 149 152 mpd ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → - π ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) )
154 148 simprd ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π )
155 absle ⊢ ( ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ ∧ π ∈ ℝ ) → ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ≤ π ↔ ( - π ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π ) ) )
156 80 54 155 sylancl ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ≤ π ↔ ( - π ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π ) ) )
157 153 154 156 mpbir2and ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ≤ π )
158 146 157 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( abs ‘ - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ≤ π )
159 132 144 138 145 158 lemul2ad ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ( abs ‘ 𝐵 ) · ( abs ‘ - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ≤ ( ( abs ‘ 𝐵 ) · π ) )
160 133 139 134 143 159 letrd ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ( abs ‘ ( ℑ ‘ 𝐵 ) ) · ( abs ‘ - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ≤ ( ( abs ‘ 𝐵 ) · π ) )
161 82 133 134 137 160 letrd ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ( ℑ ‘ 𝐵 ) · - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ≤ ( ( abs ‘ 𝐵 ) · π ) )
162 efle ⊢ ( ( ( ( ℑ ‘ 𝐵 ) · - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∈ ℝ ∧ ( ( abs ‘ 𝐵 ) · π ) ∈ ℝ ) → ( ( ( ℑ ‘ 𝐵 ) · - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ≤ ( ( abs ‘ 𝐵 ) · π ) ↔ ( exp ‘ ( ( ℑ ‘ 𝐵 ) · - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ≤ ( exp ‘ ( ( abs ‘ 𝐵 ) · π ) ) ) )
163 82 134 162 syl2anc ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ( ( ℑ ‘ 𝐵 ) · - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ≤ ( ( abs ‘ 𝐵 ) · π ) ↔ ( exp ‘ ( ( ℑ ‘ 𝐵 ) · - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ≤ ( exp ‘ ( ( abs ‘ 𝐵 ) · π ) ) ) )
164 161 163 mpbid ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( ( ℑ ‘ 𝐵 ) · - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ≤ ( exp ‘ ( ( abs ‘ 𝐵 ) · π ) ) )
165 114 120 116 129 164 lemul2ad ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ( 𝑀 ↑𝑐 ( ℜ ‘ 𝐵 ) ) · ( exp ‘ ( ( ℑ ‘ 𝐵 ) · - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) ≤ ( ( 𝑀 ↑𝑐 ( ℜ ‘ 𝐵 ) ) · ( exp ‘ ( ( abs ‘ 𝐵 ) · π ) ) ) )
166 115 117 121 128 165 letrd ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ( ( abs ‘ 𝐴 ) ↑𝑐 ( ℜ ‘ 𝐵 ) ) · ( exp ‘ ( ( ℑ ‘ 𝐵 ) · - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) ≤ ( ( 𝑀 ↑𝑐 ( ℜ ‘ 𝐵 ) ) · ( exp ‘ ( ( abs ‘ 𝐵 ) · π ) ) ) )
167 110 166 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( abs ‘ ( 𝐴 ↑𝑐 𝐵 ) ) ≤ ( ( 𝑀 ↑𝑐 ( ℜ ‘ 𝐵 ) ) · ( exp ‘ ( ( abs ‘ 𝐵 ) · π ) ) ) )
168 64 167 pm2.61dane ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 ↑𝑐 𝐵 ) ) ≤ ( ( 𝑀 ↑𝑐 ( ℜ ‘ 𝐵 ) ) · ( exp ‘ ( ( abs ‘ 𝐵 ) · π ) ) ) )