Proof of Theorem rpabscxpbnd
Step | Hyp | Ref
| Expression |
1 | | rpabscxpbnd.1 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈
ℝ+) |
2 | | abscxpbnd.2 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ ℂ) |
3 | | rpcxpef 13154 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ)
→ (𝐴↑𝑐𝐵) = (exp‘(𝐵 · (log‘𝐴)))) |
4 | 1, 2, 3 | syl2anc 409 |
. . . 4
⊢ (𝜑 → (𝐴↑𝑐𝐵) = (exp‘(𝐵 · (log‘𝐴)))) |
5 | 4 | fveq2d 5465 |
. . 3
⊢ (𝜑 → (abs‘(𝐴↑𝑐𝐵)) =
(abs‘(exp‘(𝐵
· (log‘𝐴))))) |
6 | 1 | relogcld 13142 |
. . . . . 6
⊢ (𝜑 → (log‘𝐴) ∈
ℝ) |
7 | 6 | recnd 7885 |
. . . . 5
⊢ (𝜑 → (log‘𝐴) ∈
ℂ) |
8 | 2, 7 | mulcld 7877 |
. . . 4
⊢ (𝜑 → (𝐵 · (log‘𝐴)) ∈ ℂ) |
9 | | absef 11643 |
. . . 4
⊢ ((𝐵 · (log‘𝐴)) ∈ ℂ →
(abs‘(exp‘(𝐵
· (log‘𝐴)))) =
(exp‘(ℜ‘(𝐵
· (log‘𝐴))))) |
10 | 8, 9 | syl 14 |
. . 3
⊢ (𝜑 →
(abs‘(exp‘(𝐵
· (log‘𝐴)))) =
(exp‘(ℜ‘(𝐵
· (log‘𝐴))))) |
11 | 2 | recld 10815 |
. . . . . . 7
⊢ (𝜑 → (ℜ‘𝐵) ∈
ℝ) |
12 | 7 | recld 10815 |
. . . . . . 7
⊢ (𝜑 →
(ℜ‘(log‘𝐴)) ∈ ℝ) |
13 | 11, 12 | remulcld 7887 |
. . . . . 6
⊢ (𝜑 → ((ℜ‘𝐵) ·
(ℜ‘(log‘𝐴))) ∈ ℝ) |
14 | 13 | recnd 7885 |
. . . . 5
⊢ (𝜑 → ((ℜ‘𝐵) ·
(ℜ‘(log‘𝐴))) ∈ ℂ) |
15 | 2 | imcld 10816 |
. . . . . . 7
⊢ (𝜑 → (ℑ‘𝐵) ∈
ℝ) |
16 | 7 | imcld 10816 |
. . . . . . . 8
⊢ (𝜑 →
(ℑ‘(log‘𝐴)) ∈ ℝ) |
17 | 16 | renegcld 8234 |
. . . . . . 7
⊢ (𝜑 →
-(ℑ‘(log‘𝐴)) ∈ ℝ) |
18 | 15, 17 | remulcld 7887 |
. . . . . 6
⊢ (𝜑 → ((ℑ‘𝐵) ·
-(ℑ‘(log‘𝐴))) ∈ ℝ) |
19 | 18 | recnd 7885 |
. . . . 5
⊢ (𝜑 → ((ℑ‘𝐵) ·
-(ℑ‘(log‘𝐴))) ∈ ℂ) |
20 | | efadd 11549 |
. . . . 5
⊢
((((ℜ‘𝐵)
· (ℜ‘(log‘𝐴))) ∈ ℂ ∧
((ℑ‘𝐵) ·
-(ℑ‘(log‘𝐴))) ∈ ℂ) →
(exp‘(((ℜ‘𝐵) · (ℜ‘(log‘𝐴))) + ((ℑ‘𝐵) ·
-(ℑ‘(log‘𝐴))))) = ((exp‘((ℜ‘𝐵) ·
(ℜ‘(log‘𝐴)))) ·
(exp‘((ℑ‘𝐵) · -(ℑ‘(log‘𝐴)))))) |
21 | 14, 19, 20 | syl2anc 409 |
. . . 4
⊢ (𝜑 →
(exp‘(((ℜ‘𝐵) · (ℜ‘(log‘𝐴))) + ((ℑ‘𝐵) ·
-(ℑ‘(log‘𝐴))))) = ((exp‘((ℜ‘𝐵) ·
(ℜ‘(log‘𝐴)))) ·
(exp‘((ℑ‘𝐵) · -(ℑ‘(log‘𝐴)))))) |
22 | 15, 16 | remulcld 7887 |
. . . . . . . 8
⊢ (𝜑 → ((ℑ‘𝐵) ·
(ℑ‘(log‘𝐴))) ∈ ℝ) |
23 | 22 | recnd 7885 |
. . . . . . 7
⊢ (𝜑 → ((ℑ‘𝐵) ·
(ℑ‘(log‘𝐴))) ∈ ℂ) |
24 | 14, 23 | negsubd 8171 |
. . . . . 6
⊢ (𝜑 → (((ℜ‘𝐵) ·
(ℜ‘(log‘𝐴))) + -((ℑ‘𝐵) · (ℑ‘(log‘𝐴)))) = (((ℜ‘𝐵) ·
(ℜ‘(log‘𝐴))) − ((ℑ‘𝐵) ·
(ℑ‘(log‘𝐴))))) |
25 | 15 | recnd 7885 |
. . . . . . . 8
⊢ (𝜑 → (ℑ‘𝐵) ∈
ℂ) |
26 | 16 | recnd 7885 |
. . . . . . . 8
⊢ (𝜑 →
(ℑ‘(log‘𝐴)) ∈ ℂ) |
27 | 25, 26 | mulneg2d 8266 |
. . . . . . 7
⊢ (𝜑 → ((ℑ‘𝐵) ·
-(ℑ‘(log‘𝐴))) = -((ℑ‘𝐵) · (ℑ‘(log‘𝐴)))) |
28 | 27 | oveq2d 5830 |
. . . . . 6
⊢ (𝜑 → (((ℜ‘𝐵) ·
(ℜ‘(log‘𝐴))) + ((ℑ‘𝐵) · -(ℑ‘(log‘𝐴)))) = (((ℜ‘𝐵) ·
(ℜ‘(log‘𝐴))) + -((ℑ‘𝐵) · (ℑ‘(log‘𝐴))))) |
29 | 2, 7 | remuld 10840 |
. . . . . 6
⊢ (𝜑 → (ℜ‘(𝐵 · (log‘𝐴))) = (((ℜ‘𝐵) ·
(ℜ‘(log‘𝐴))) − ((ℑ‘𝐵) ·
(ℑ‘(log‘𝐴))))) |
30 | 24, 28, 29 | 3eqtr4d 2197 |
. . . . 5
⊢ (𝜑 → (((ℜ‘𝐵) ·
(ℜ‘(log‘𝐴))) + ((ℑ‘𝐵) · -(ℑ‘(log‘𝐴)))) = (ℜ‘(𝐵 · (log‘𝐴)))) |
31 | 30 | fveq2d 5465 |
. . . 4
⊢ (𝜑 →
(exp‘(((ℜ‘𝐵) · (ℜ‘(log‘𝐴))) + ((ℑ‘𝐵) ·
-(ℑ‘(log‘𝐴))))) = (exp‘(ℜ‘(𝐵 · (log‘𝐴))))) |
32 | 6 | rered 10846 |
. . . . . . . . 9
⊢ (𝜑 →
(ℜ‘(log‘𝐴)) = (log‘𝐴)) |
33 | 1 | rpred 9581 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℝ) |
34 | 1 | rpge0d 9585 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≤ 𝐴) |
35 | 33, 34 | absidd 11044 |
. . . . . . . . . 10
⊢ (𝜑 → (abs‘𝐴) = 𝐴) |
36 | 35 | fveq2d 5465 |
. . . . . . . . 9
⊢ (𝜑 →
(log‘(abs‘𝐴)) =
(log‘𝐴)) |
37 | 32, 36 | eqtr4d 2190 |
. . . . . . . 8
⊢ (𝜑 →
(ℜ‘(log‘𝐴)) = (log‘(abs‘𝐴))) |
38 | 37 | oveq2d 5830 |
. . . . . . 7
⊢ (𝜑 → ((ℜ‘𝐵) ·
(ℜ‘(log‘𝐴))) = ((ℜ‘𝐵) · (log‘(abs‘𝐴)))) |
39 | 38 | fveq2d 5465 |
. . . . . 6
⊢ (𝜑 →
(exp‘((ℜ‘𝐵) · (ℜ‘(log‘𝐴)))) =
(exp‘((ℜ‘𝐵) · (log‘(abs‘𝐴))))) |
40 | 35, 1 | eqeltrd 2231 |
. . . . . . 7
⊢ (𝜑 → (abs‘𝐴) ∈
ℝ+) |
41 | 11 | recnd 7885 |
. . . . . . 7
⊢ (𝜑 → (ℜ‘𝐵) ∈
ℂ) |
42 | | rpcxpef 13154 |
. . . . . . 7
⊢
(((abs‘𝐴)
∈ ℝ+ ∧ (ℜ‘𝐵) ∈ ℂ) → ((abs‘𝐴)↑𝑐(ℜ‘𝐵)) =
(exp‘((ℜ‘𝐵)
· (log‘(abs‘𝐴))))) |
43 | 40, 41, 42 | syl2anc 409 |
. . . . . 6
⊢ (𝜑 → ((abs‘𝐴)↑𝑐(ℜ‘𝐵)) =
(exp‘((ℜ‘𝐵)
· (log‘(abs‘𝐴))))) |
44 | 39, 43 | eqtr4d 2190 |
. . . . 5
⊢ (𝜑 →
(exp‘((ℜ‘𝐵) · (ℜ‘(log‘𝐴)))) = ((abs‘𝐴)↑𝑐(ℜ‘𝐵))) |
45 | 44 | oveq1d 5829 |
. . . 4
⊢ (𝜑 →
((exp‘((ℜ‘𝐵) · (ℜ‘(log‘𝐴)))) ·
(exp‘((ℑ‘𝐵) · -(ℑ‘(log‘𝐴))))) = (((abs‘𝐴)↑𝑐(ℜ‘𝐵)) ·
(exp‘((ℑ‘𝐵)
· -(ℑ‘(log‘𝐴)))))) |
46 | 21, 31, 45 | 3eqtr3d 2195 |
. . 3
⊢ (𝜑 →
(exp‘(ℜ‘(𝐵
· (log‘𝐴)))) =
(((abs‘𝐴)↑𝑐(ℜ‘𝐵)) ·
(exp‘((ℑ‘𝐵)
· -(ℑ‘(log‘𝐴)))))) |
47 | 5, 10, 46 | 3eqtrd 2191 |
. 2
⊢ (𝜑 → (abs‘(𝐴↑𝑐𝐵)) = (((abs‘𝐴)↑𝑐(ℜ‘𝐵)) ·
(exp‘((ℑ‘𝐵)
· -(ℑ‘(log‘𝐴)))))) |
48 | 40, 11 | rpcxpcld 13191 |
. . . . 5
⊢ (𝜑 → ((abs‘𝐴)↑𝑐(ℜ‘𝐵)) ∈
ℝ+) |
49 | 48 | rpred 9581 |
. . . 4
⊢ (𝜑 → ((abs‘𝐴)↑𝑐(ℜ‘𝐵)) ∈
ℝ) |
50 | 18 | reefcld 11543 |
. . . 4
⊢ (𝜑 →
(exp‘((ℑ‘𝐵) · -(ℑ‘(log‘𝐴)))) ∈
ℝ) |
51 | 49, 50 | remulcld 7887 |
. . 3
⊢ (𝜑 → (((abs‘𝐴)↑𝑐(ℜ‘𝐵)) ·
(exp‘((ℑ‘𝐵)
· -(ℑ‘(log‘𝐴))))) ∈ ℝ) |
52 | | abscxpbnd.4 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℝ) |
53 | | abscxpbnd.5 |
. . . . . . 7
⊢ (𝜑 → (abs‘𝐴) ≤ 𝑀) |
54 | 52, 40, 53 | rpgecld 9621 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈
ℝ+) |
55 | 54, 11 | rpcxpcld 13191 |
. . . . 5
⊢ (𝜑 → (𝑀↑𝑐(ℜ‘𝐵)) ∈
ℝ+) |
56 | 55 | rpred 9581 |
. . . 4
⊢ (𝜑 → (𝑀↑𝑐(ℜ‘𝐵)) ∈
ℝ) |
57 | 56, 50 | remulcld 7887 |
. . 3
⊢ (𝜑 → ((𝑀↑𝑐(ℜ‘𝐵)) ·
(exp‘((ℑ‘𝐵) · -(ℑ‘(log‘𝐴))))) ∈
ℝ) |
58 | 2 | abscld 11058 |
. . . . . 6
⊢ (𝜑 → (abs‘𝐵) ∈
ℝ) |
59 | | pire 13046 |
. . . . . 6
⊢ π
∈ ℝ |
60 | | remulcl 7839 |
. . . . . 6
⊢
(((abs‘𝐵)
∈ ℝ ∧ π ∈ ℝ) → ((abs‘𝐵) · π) ∈
ℝ) |
61 | 58, 59, 60 | sylancl 410 |
. . . . 5
⊢ (𝜑 → ((abs‘𝐵) · π) ∈
ℝ) |
62 | 61 | reefcld 11543 |
. . . 4
⊢ (𝜑 →
(exp‘((abs‘𝐵)
· π)) ∈ ℝ) |
63 | 56, 62 | remulcld 7887 |
. . 3
⊢ (𝜑 → ((𝑀↑𝑐(ℜ‘𝐵)) ·
(exp‘((abs‘𝐵)
· π))) ∈ ℝ) |
64 | 18 | rpefcld 11560 |
. . . . 5
⊢ (𝜑 →
(exp‘((ℑ‘𝐵) · -(ℑ‘(log‘𝐴)))) ∈
ℝ+) |
65 | 64 | rpge0d 9585 |
. . . 4
⊢ (𝜑 → 0 ≤
(exp‘((ℑ‘𝐵) · -(ℑ‘(log‘𝐴))))) |
66 | 1 | rpcnd 9583 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℂ) |
67 | 1 | rpap0d 9587 |
. . . . . . 7
⊢ (𝜑 → 𝐴 # 0) |
68 | 66, 67 | absrpclapd 11065 |
. . . . . 6
⊢ (𝜑 → (abs‘𝐴) ∈
ℝ+) |
69 | 52, 68, 53 | rpgecld 9621 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈
ℝ+) |
70 | | rpabscxpbnd.3 |
. . . . . . 7
⊢ (𝜑 → 0 < (ℜ‘𝐵)) |
71 | 11, 70 | elrpd 9578 |
. . . . . 6
⊢ (𝜑 → (ℜ‘𝐵) ∈
ℝ+) |
72 | | rpcxple2 13177 |
. . . . . 6
⊢
(((abs‘𝐴)
∈ ℝ+ ∧ 𝑀 ∈ ℝ+ ∧
(ℜ‘𝐵) ∈
ℝ+) → ((abs‘𝐴) ≤ 𝑀 ↔ ((abs‘𝐴)↑𝑐(ℜ‘𝐵)) ≤ (𝑀↑𝑐(ℜ‘𝐵)))) |
73 | 68, 69, 71, 72 | syl3anc 1217 |
. . . . 5
⊢ (𝜑 → ((abs‘𝐴) ≤ 𝑀 ↔ ((abs‘𝐴)↑𝑐(ℜ‘𝐵)) ≤ (𝑀↑𝑐(ℜ‘𝐵)))) |
74 | 53, 73 | mpbid 146 |
. . . 4
⊢ (𝜑 → ((abs‘𝐴)↑𝑐(ℜ‘𝐵)) ≤ (𝑀↑𝑐(ℜ‘𝐵))) |
75 | 49, 56, 50, 65, 74 | lemul1ad 8789 |
. . 3
⊢ (𝜑 → (((abs‘𝐴)↑𝑐(ℜ‘𝐵)) ·
(exp‘((ℑ‘𝐵)
· -(ℑ‘(log‘𝐴))))) ≤ ((𝑀↑𝑐(ℜ‘𝐵)) ·
(exp‘((ℑ‘𝐵)
· -(ℑ‘(log‘𝐴)))))) |
76 | 55 | rpge0d 9585 |
. . . 4
⊢ (𝜑 → 0 ≤ (𝑀↑𝑐(ℜ‘𝐵))) |
77 | 25 | abscld 11058 |
. . . . . . 7
⊢ (𝜑 →
(abs‘(ℑ‘𝐵)) ∈ ℝ) |
78 | 17 | recnd 7885 |
. . . . . . . 8
⊢ (𝜑 →
-(ℑ‘(log‘𝐴)) ∈ ℂ) |
79 | 78 | abscld 11058 |
. . . . . . 7
⊢ (𝜑 →
(abs‘-(ℑ‘(log‘𝐴))) ∈ ℝ) |
80 | 77, 79 | remulcld 7887 |
. . . . . 6
⊢ (𝜑 →
((abs‘(ℑ‘𝐵)) ·
(abs‘-(ℑ‘(log‘𝐴)))) ∈ ℝ) |
81 | 18 | leabsd 11038 |
. . . . . . 7
⊢ (𝜑 → ((ℑ‘𝐵) ·
-(ℑ‘(log‘𝐴))) ≤ (abs‘((ℑ‘𝐵) ·
-(ℑ‘(log‘𝐴))))) |
82 | 25, 78 | absmuld 11071 |
. . . . . . 7
⊢ (𝜑 →
(abs‘((ℑ‘𝐵) · -(ℑ‘(log‘𝐴)))) =
((abs‘(ℑ‘𝐵)) ·
(abs‘-(ℑ‘(log‘𝐴))))) |
83 | 81, 82 | breqtrd 3986 |
. . . . . 6
⊢ (𝜑 → ((ℑ‘𝐵) ·
-(ℑ‘(log‘𝐴))) ≤ ((abs‘(ℑ‘𝐵)) ·
(abs‘-(ℑ‘(log‘𝐴))))) |
84 | 58, 79 | remulcld 7887 |
. . . . . . 7
⊢ (𝜑 → ((abs‘𝐵) ·
(abs‘-(ℑ‘(log‘𝐴)))) ∈ ℝ) |
85 | 78 | absge0d 11061 |
. . . . . . . 8
⊢ (𝜑 → 0 ≤
(abs‘-(ℑ‘(log‘𝐴)))) |
86 | | absimle 10961 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℂ →
(abs‘(ℑ‘𝐵)) ≤ (abs‘𝐵)) |
87 | 2, 86 | syl 14 |
. . . . . . . 8
⊢ (𝜑 →
(abs‘(ℑ‘𝐵)) ≤ (abs‘𝐵)) |
88 | 77, 58, 79, 85, 87 | lemul1ad 8789 |
. . . . . . 7
⊢ (𝜑 →
((abs‘(ℑ‘𝐵)) ·
(abs‘-(ℑ‘(log‘𝐴)))) ≤ ((abs‘𝐵) ·
(abs‘-(ℑ‘(log‘𝐴))))) |
89 | 59 | a1i 9 |
. . . . . . . 8
⊢ (𝜑 → π ∈
ℝ) |
90 | 2 | absge0d 11061 |
. . . . . . . 8
⊢ (𝜑 → 0 ≤ (abs‘𝐵)) |
91 | 26 | absnegd 11066 |
. . . . . . . . 9
⊢ (𝜑 →
(abs‘-(ℑ‘(log‘𝐴))) =
(abs‘(ℑ‘(log‘𝐴)))) |
92 | 59 | renegcli 8116 |
. . . . . . . . . . . 12
⊢ -π
∈ ℝ |
93 | | 0re 7857 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℝ |
94 | | pipos 13048 |
. . . . . . . . . . . . 13
⊢ 0 <
π |
95 | | lt0neg2 8323 |
. . . . . . . . . . . . . 14
⊢ (π
∈ ℝ → (0 < π ↔ -π < 0)) |
96 | 59, 95 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (0 <
π ↔ -π < 0) |
97 | 94, 96 | mpbi 144 |
. . . . . . . . . . . 12
⊢ -π
< 0 |
98 | 92, 93, 97 | ltleii 7958 |
. . . . . . . . . . 11
⊢ -π
≤ 0 |
99 | 6 | reim0d 10847 |
. . . . . . . . . . 11
⊢ (𝜑 →
(ℑ‘(log‘𝐴)) = 0) |
100 | 98, 99 | breqtrrid 3998 |
. . . . . . . . . 10
⊢ (𝜑 → -π ≤
(ℑ‘(log‘𝐴))) |
101 | 93, 59, 94 | ltleii 7958 |
. . . . . . . . . . 11
⊢ 0 ≤
π |
102 | 99, 101 | eqbrtrdi 3999 |
. . . . . . . . . 10
⊢ (𝜑 →
(ℑ‘(log‘𝐴)) ≤ π) |
103 | | absle 10966 |
. . . . . . . . . . 11
⊢
(((ℑ‘(log‘𝐴)) ∈ ℝ ∧ π ∈ ℝ)
→ ((abs‘(ℑ‘(log‘𝐴))) ≤ π ↔ (-π ≤
(ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) ≤ π))) |
104 | 16, 59, 103 | sylancl 410 |
. . . . . . . . . 10
⊢ (𝜑 →
((abs‘(ℑ‘(log‘𝐴))) ≤ π ↔ (-π ≤
(ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) ≤ π))) |
105 | 100, 102,
104 | mpbir2and 929 |
. . . . . . . . 9
⊢ (𝜑 →
(abs‘(ℑ‘(log‘𝐴))) ≤ π) |
106 | 91, 105 | eqbrtrd 3982 |
. . . . . . . 8
⊢ (𝜑 →
(abs‘-(ℑ‘(log‘𝐴))) ≤ π) |
107 | 79, 89, 58, 90, 106 | lemul2ad 8790 |
. . . . . . 7
⊢ (𝜑 → ((abs‘𝐵) ·
(abs‘-(ℑ‘(log‘𝐴)))) ≤ ((abs‘𝐵) · π)) |
108 | 80, 84, 61, 88, 107 | letrd 7978 |
. . . . . 6
⊢ (𝜑 →
((abs‘(ℑ‘𝐵)) ·
(abs‘-(ℑ‘(log‘𝐴)))) ≤ ((abs‘𝐵) · π)) |
109 | 18, 80, 61, 83, 108 | letrd 7978 |
. . . . 5
⊢ (𝜑 → ((ℑ‘𝐵) ·
-(ℑ‘(log‘𝐴))) ≤ ((abs‘𝐵) · π)) |
110 | | efle 13036 |
. . . . . 6
⊢
((((ℑ‘𝐵)
· -(ℑ‘(log‘𝐴))) ∈ ℝ ∧ ((abs‘𝐵) · π) ∈ ℝ)
→ (((ℑ‘𝐵)
· -(ℑ‘(log‘𝐴))) ≤ ((abs‘𝐵) · π) ↔
(exp‘((ℑ‘𝐵) · -(ℑ‘(log‘𝐴)))) ≤
(exp‘((abs‘𝐵)
· π)))) |
111 | 18, 61, 110 | syl2anc 409 |
. . . . 5
⊢ (𝜑 → (((ℑ‘𝐵) ·
-(ℑ‘(log‘𝐴))) ≤ ((abs‘𝐵) · π) ↔
(exp‘((ℑ‘𝐵) · -(ℑ‘(log‘𝐴)))) ≤
(exp‘((abs‘𝐵)
· π)))) |
112 | 109, 111 | mpbid 146 |
. . . 4
⊢ (𝜑 →
(exp‘((ℑ‘𝐵) · -(ℑ‘(log‘𝐴)))) ≤
(exp‘((abs‘𝐵)
· π))) |
113 | 50, 62, 56, 76, 112 | lemul2ad 8790 |
. . 3
⊢ (𝜑 → ((𝑀↑𝑐(ℜ‘𝐵)) ·
(exp‘((ℑ‘𝐵) · -(ℑ‘(log‘𝐴))))) ≤ ((𝑀↑𝑐(ℜ‘𝐵)) ·
(exp‘((abs‘𝐵)
· π)))) |
114 | 51, 57, 63, 75, 113 | letrd 7978 |
. 2
⊢ (𝜑 → (((abs‘𝐴)↑𝑐(ℜ‘𝐵)) ·
(exp‘((ℑ‘𝐵)
· -(ℑ‘(log‘𝐴))))) ≤ ((𝑀↑𝑐(ℜ‘𝐵)) ·
(exp‘((abs‘𝐵)
· π)))) |
115 | 47, 114 | eqbrtrd 3982 |
1
⊢ (𝜑 → (abs‘(𝐴↑𝑐𝐵)) ≤ ((𝑀↑𝑐(ℜ‘𝐵)) ·
(exp‘((abs‘𝐵)
· π)))) |