abscxpbnd

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

	Ref	Expression
Hypotheses	abscxpbnd.1	$⊢ φ \to A \in ℂ$
	abscxpbnd.2	$⊢ φ \to B \in ℂ$
	abscxpbnd.3	$⊢ φ \to 0 \leq ℜ (B)$
	abscxpbnd.4	$⊢ φ \to M \in ℝ$
	abscxpbnd.5	$⊢ φ \to \|A\| \leq M$
Assertion	abscxpbnd	$⊢ φ \to \|A^{B}\| \leq M^{ℜ (B)} e^{\|B\| π}$

Proof

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

Metamath Proof Explorer

Theorem abscxpbnd

Proof