abscxp

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

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

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (A \in ℝ^{+} \land B \in ℂ) \to B \in ℂ$
2		relogcl	$⊢ A \in ℝ^{+} \to \log A \in ℝ$
3	2	recnd	$⊢ A \in ℝ^{+} \to \log A \in ℂ$
4	3	adantr	$⊢ (A \in ℝ^{+} \land B \in ℂ) \to \log A \in ℂ$
5	1 4	mulcld	$⊢ (A \in ℝ^{+} \land B \in ℂ) \to B \log A \in ℂ$
6		absef	$⊢ B \log A \in ℂ \to \|e^{B \log A}\| = e^{ℜ (B \log A)}$
7	5 6	syl	$⊢ (A \in ℝ^{+} \land B \in ℂ) \to \|e^{B \log A}\| = e^{ℜ (B \log A)}$
8		remul2	$⊢ (\log A \in ℝ \land B \in ℂ) \to ℜ (\log A B) = \log A ℜ (B)$
9	2 8	sylan	$⊢ (A \in ℝ^{+} \land B \in ℂ) \to ℜ (\log A B) = \log A ℜ (B)$
10	1 4	mulcomd	$⊢ (A \in ℝ^{+} \land B \in ℂ) \to B \log A = \log A B$
11	10	fveq2d	$⊢ (A \in ℝ^{+} \land B \in ℂ) \to ℜ (B \log A) = ℜ (\log A B)$
12		recl	$⊢ B \in ℂ \to ℜ (B) \in ℝ$
13	12	adantl	$⊢ (A \in ℝ^{+} \land B \in ℂ) \to ℜ (B) \in ℝ$
14	13	recnd	$⊢ (A \in ℝ^{+} \land B \in ℂ) \to ℜ (B) \in ℂ$
15	14 4	mulcomd	$⊢ (A \in ℝ^{+} \land B \in ℂ) \to ℜ (B) \log A = \log A ℜ (B)$
16	9 11 15	3eqtr4d	$⊢ (A \in ℝ^{+} \land B \in ℂ) \to ℜ (B \log A) = ℜ (B) \log A$
17	16	fveq2d	$⊢ (A \in ℝ^{+} \land B \in ℂ) \to e^{ℜ (B \log A)} = e^{ℜ (B) \log A}$
18	7 17	eqtrd	$⊢ (A \in ℝ^{+} \land B \in ℂ) \to \|e^{B \log A}\| = e^{ℜ (B) \log A}$
19		rpcn	$⊢ A \in ℝ^{+} \to A \in ℂ$
20	19	adantr	$⊢ (A \in ℝ^{+} \land B \in ℂ) \to A \in ℂ$
21		rpne0	$⊢ A \in ℝ^{+} \to A \neq 0$
22	21	adantr	$⊢ (A \in ℝ^{+} \land B \in ℂ) \to A \neq 0$
23		cxpef	$⊢ (A \in ℂ \land A \neq 0 \land B \in ℂ) \to A^{B} = e^{B \log A}$
24	20 22 1 23	syl3anc	$⊢ (A \in ℝ^{+} \land B \in ℂ) \to A^{B} = e^{B \log A}$
25	24	fveq2d	$⊢ (A \in ℝ^{+} \land B \in ℂ) \to \|A^{B}\| = \|e^{B \log A}\|$
26		cxpef	$⊢ (A \in ℂ \land A \neq 0 \land ℜ (B) \in ℂ) \to A^{ℜ (B)} = e^{ℜ (B) \log A}$
27	20 22 14 26	syl3anc	$⊢ (A \in ℝ^{+} \land B \in ℂ) \to A^{ℜ (B)} = e^{ℜ (B) \log A}$
28	18 25 27	3eqtr4d	$⊢ (A \in ℝ^{+} \land B \in ℂ) \to \|A^{B}\| = A^{ℜ (B)}$

Metamath Proof Explorer

Theorem abscxp

Proof