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 
|- ( ph -> A e. CC )
abscxpbnd.2 
|- ( ph -> B e. CC )
abscxpbnd.3 
|- ( ph -> 0 <_ ( Re ` B ) )
abscxpbnd.4 
|- ( ph -> M e. RR )
abscxpbnd.5 
|- ( ph -> ( abs ` A ) <_ M )
Assertion abscxpbnd 
|- ( ph -> ( abs ` ( A ^c B ) ) <_ ( ( M ^c ( Re ` B ) ) x. ( exp ` ( ( abs ` B ) x. _pi ) ) ) )

Proof

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