abscxp2

Description: Absolute value of a power, when the exponent is real. (Contributed by Mario Carneiro, 15-Sep-2014)

		Ref	Expression
	Assertion	abscxp2	$⊢ (A \in ℂ \land B \in ℝ) \to \|A^{B}\| = {\|A\|}^{B}$

Proof

Step	Hyp	Ref	Expression
1		0red	$⊢ ((A \in ℂ \land B \in ℝ) \land A = 0) \to 0 \in ℝ$
2		0le0	$⊢ 0 \leq 0$
3	2	a1i	$⊢ ((A \in ℂ \land B \in ℝ) \land A = 0) \to 0 \leq 0$
4		simplr	$⊢ ((A \in ℂ \land B \in ℝ) \land A = 0) \to B \in ℝ$
5		recxpcl	$⊢ (0 \in ℝ \land 0 \leq 0 \land B \in ℝ) \to 0^{B} \in ℝ$
6	1 3 4 5	syl3anc	$⊢ ((A \in ℂ \land B \in ℝ) \land A = 0) \to 0^{B} \in ℝ$
7		cxpge0	$⊢ (0 \in ℝ \land 0 \leq 0 \land B \in ℝ) \to 0 \leq 0^{B}$
8	1 3 4 7	syl3anc	$⊢ ((A \in ℂ \land B \in ℝ) \land A = 0) \to 0 \leq 0^{B}$
9	6 8	absidd	$⊢ ((A \in ℂ \land B \in ℝ) \land A = 0) \to \|0^{B}\| = 0^{B}$
10		simpr	$⊢ ((A \in ℂ \land B \in ℝ) \land A = 0) \to A = 0$
11	10	oveq1d	$⊢ ((A \in ℂ \land B \in ℝ) \land A = 0) \to A^{B} = 0^{B}$
12	11	fveq2d	$⊢ ((A \in ℂ \land B \in ℝ) \land A = 0) \to \|A^{B}\| = \|0^{B}\|$
13	10	abs00bd	$⊢ ((A \in ℂ \land B \in ℝ) \land A = 0) \to \|A\| = 0$
14	13	oveq1d	$⊢ ((A \in ℂ \land B \in ℝ) \land A = 0) \to {\|A\|}^{B} = 0^{B}$
15	9 12 14	3eqtr4d	$⊢ ((A \in ℂ \land B \in ℝ) \land A = 0) \to \|A^{B}\| = {\|A\|}^{B}$
16		simplr	$⊢ ((A \in ℂ \land B \in ℝ) \land A \neq 0) \to B \in ℝ$
17	16	recnd	$⊢ ((A \in ℂ \land B \in ℝ) \land A \neq 0) \to B \in ℂ$
18		logcl	$⊢ (A \in ℂ \land A \neq 0) \to \log A \in ℂ$
19	18	adantlr	$⊢ ((A \in ℂ \land B \in ℝ) \land A \neq 0) \to \log A \in ℂ$
20	17 19	mulcld	$⊢ ((A \in ℂ \land B \in ℝ) \land A \neq 0) \to B \log A \in ℂ$
21		absef	$⊢ B \log A \in ℂ \to \|e^{B \log A}\| = e^{ℜ (B \log A)}$
22	20 21	syl	$⊢ ((A \in ℂ \land B \in ℝ) \land A \neq 0) \to \|e^{B \log A}\| = e^{ℜ (B \log A)}$
23	16 19	remul2d	$⊢ ((A \in ℂ \land B \in ℝ) \land A \neq 0) \to ℜ (B \log A) = B ℜ (\log A)$
24		relog	$⊢ (A \in ℂ \land A \neq 0) \to ℜ (\log A) = \log \|A\|$
25	24	adantlr	$⊢ ((A \in ℂ \land B \in ℝ) \land A \neq 0) \to ℜ (\log A) = \log \|A\|$
26	25	oveq2d	$⊢ ((A \in ℂ \land B \in ℝ) \land A \neq 0) \to B ℜ (\log A) = B \log \|A\|$
27	23 26	eqtrd	$⊢ ((A \in ℂ \land B \in ℝ) \land A \neq 0) \to ℜ (B \log A) = B \log \|A\|$
28	27	fveq2d	$⊢ ((A \in ℂ \land B \in ℝ) \land A \neq 0) \to e^{ℜ (B \log A)} = e^{B \log \|A\|}$
29	22 28	eqtrd	$⊢ ((A \in ℂ \land B \in ℝ) \land A \neq 0) \to \|e^{B \log A}\| = e^{B \log \|A\|}$
30		simpll	$⊢ ((A \in ℂ \land B \in ℝ) \land A \neq 0) \to A \in ℂ$
31		simpr	$⊢ ((A \in ℂ \land B \in ℝ) \land A \neq 0) \to A \neq 0$
32		cxpef	$⊢ (A \in ℂ \land A \neq 0 \land B \in ℂ) \to A^{B} = e^{B \log A}$
33	30 31 17 32	syl3anc	$⊢ ((A \in ℂ \land B \in ℝ) \land A \neq 0) \to A^{B} = e^{B \log A}$
34	33	fveq2d	$⊢ ((A \in ℂ \land B \in ℝ) \land A \neq 0) \to \|A^{B}\| = \|e^{B \log A}\|$
35	30	abscld	$⊢ ((A \in ℂ \land B \in ℝ) \land A \neq 0) \to \|A\| \in ℝ$
36	35	recnd	$⊢ ((A \in ℂ \land B \in ℝ) \land A \neq 0) \to \|A\| \in ℂ$
37		abs00	$⊢ A \in ℂ \to (\|A\| = 0 \leftrightarrow A = 0)$
38	37	adantr	$⊢ (A \in ℂ \land B \in ℝ) \to (\|A\| = 0 \leftrightarrow A = 0)$
39	38	necon3bid	$⊢ (A \in ℂ \land B \in ℝ) \to (\|A\| \neq 0 \leftrightarrow A \neq 0)$
40	39	biimpar	$⊢ ((A \in ℂ \land B \in ℝ) \land A \neq 0) \to \|A\| \neq 0$
41		cxpef	$⊢ (\|A\| \in ℂ \land \|A\| \neq 0 \land B \in ℂ) \to {\|A\|}^{B} = e^{B \log \|A\|}$
42	36 40 17 41	syl3anc	$⊢ ((A \in ℂ \land B \in ℝ) \land A \neq 0) \to {\|A\|}^{B} = e^{B \log \|A\|}$
43	29 34 42	3eqtr4d	$⊢ ((A \in ℂ \land B \in ℝ) \land A \neq 0) \to \|A^{B}\| = {\|A\|}^{B}$
44	15 43	pm2.61dane	$⊢ (A \in ℂ \land B \in ℝ) \to \|A^{B}\| = {\|A\|}^{B}$

Metamath Proof Explorer

Theorem abscxp2

Proof