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 ‘ 𝐵 ) · π ) ) ) )