Theorem abscxp2

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

	Ref	Expression
Assertion	abscxp2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ) → ( abs ‘ ( 𝐴 ↑𝑐 𝐵 ) ) = ( ( abs ‘ 𝐴 ) ↑𝑐 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		0red	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 = 0 ) → 0 ∈ ℝ )
2		0le0	⊢ 0 ≤ 0
3	2	a1i	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 = 0 ) → 0 ≤ 0 )
4		simplr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 = 0 ) → 𝐵 ∈ ℝ )
5		recxpcl	⊢ ( ( 0 ∈ ℝ ∧ 0 ≤ 0 ∧ 𝐵 ∈ ℝ ) → ( 0 ↑𝑐 𝐵 ) ∈ ℝ )
6	1 3 4 5	syl3anc	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 = 0 ) → ( 0 ↑𝑐 𝐵 ) ∈ ℝ )
7		cxpge0	⊢ ( ( 0 ∈ ℝ ∧ 0 ≤ 0 ∧ 𝐵 ∈ ℝ ) → 0 ≤ ( 0 ↑𝑐 𝐵 ) )
8	1 3 4 7	syl3anc	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 = 0 ) → 0 ≤ ( 0 ↑𝑐 𝐵 ) )
9	6 8	absidd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 = 0 ) → ( abs ‘ ( 0 ↑𝑐 𝐵 ) ) = ( 0 ↑𝑐 𝐵 ) )
10		simpr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 = 0 ) → 𝐴 = 0 )
11	10	oveq1d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 = 0 ) → ( 𝐴 ↑𝑐 𝐵 ) = ( 0 ↑𝑐 𝐵 ) )
12	11	fveq2d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 = 0 ) → ( abs ‘ ( 𝐴 ↑𝑐 𝐵 ) ) = ( abs ‘ ( 0 ↑𝑐 𝐵 ) ) )
13	10	abs00bd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 = 0 ) → ( abs ‘ 𝐴 ) = 0 )
14	13	oveq1d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 = 0 ) → ( ( abs ‘ 𝐴 ) ↑𝑐 𝐵 ) = ( 0 ↑𝑐 𝐵 ) )
15	9 12 14	3eqtr4d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 = 0 ) → ( abs ‘ ( 𝐴 ↑𝑐 𝐵 ) ) = ( ( abs ‘ 𝐴 ) ↑𝑐 𝐵 ) )
16		simplr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ 0 ) → 𝐵 ∈ ℝ )
17	16	recnd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ 0 ) → 𝐵 ∈ ℂ )
18		logcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( log ‘ 𝐴 ) ∈ ℂ )
19	18	adantlr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ 0 ) → ( log ‘ 𝐴 ) ∈ ℂ )
20	17 19	mulcld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ 0 ) → ( 𝐵 · ( log ‘ 𝐴 ) ) ∈ ℂ )
21		absef	⊢ ( ( 𝐵 · ( log ‘ 𝐴 ) ) ∈ ℂ → ( abs ‘ ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ) = ( exp ‘ ( ℜ ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ) )
22	20 21	syl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ 0 ) → ( abs ‘ ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ) = ( exp ‘ ( ℜ ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ) )
23	16 19	remul2d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ 0 ) → ( ℜ ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) = ( 𝐵 · ( ℜ ‘ ( log ‘ 𝐴 ) ) ) )
24		relog	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℜ ‘ ( log ‘ 𝐴 ) ) = ( log ‘ ( abs ‘ 𝐴 ) ) )
25	24	adantlr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ 0 ) → ( ℜ ‘ ( log ‘ 𝐴 ) ) = ( log ‘ ( abs ‘ 𝐴 ) ) )
26	25	oveq2d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ 0 ) → ( 𝐵 · ( ℜ ‘ ( log ‘ 𝐴 ) ) ) = ( 𝐵 · ( log ‘ ( abs ‘ 𝐴 ) ) ) )
27	23 26	eqtrd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ 0 ) → ( ℜ ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) = ( 𝐵 · ( log ‘ ( abs ‘ 𝐴 ) ) ) )
28	27	fveq2d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( ℜ ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ) = ( exp ‘ ( 𝐵 · ( log ‘ ( abs ‘ 𝐴 ) ) ) ) )
29	22 28	eqtrd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ 0 ) → ( abs ‘ ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ) = ( exp ‘ ( 𝐵 · ( log ‘ ( abs ‘ 𝐴 ) ) ) ) )
30		simpll	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ ℂ )
31		simpr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ 0 ) → 𝐴 ≠ 0 )
32		cxpef	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐵 ) = ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) )
33	30 31 17 32	syl3anc	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ 0 ) → ( 𝐴 ↑𝑐 𝐵 ) = ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) )
34	33	fveq2d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ 0 ) → ( abs ‘ ( 𝐴 ↑𝑐 𝐵 ) ) = ( abs ‘ ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ) )
35	30	abscld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ∈ ℝ )
36	35	recnd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ∈ ℂ )
37		abs00	⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) = 0 ↔ 𝐴 = 0 ) )
38	37	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ) → ( ( abs ‘ 𝐴 ) = 0 ↔ 𝐴 = 0 ) )
39	38	necon3bid	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ) → ( ( abs ‘ 𝐴 ) ≠ 0 ↔ 𝐴 ≠ 0 ) )
40	39	biimpar	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ≠ 0 )
41		cxpef	⊢ ( ( ( abs ‘ 𝐴 ) ∈ ℂ ∧ ( abs ‘ 𝐴 ) ≠ 0 ∧ 𝐵 ∈ ℂ ) → ( ( abs ‘ 𝐴 ) ↑𝑐 𝐵 ) = ( exp ‘ ( 𝐵 · ( log ‘ ( abs ‘ 𝐴 ) ) ) ) )
42	36 40 17 41	syl3anc	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ 0 ) → ( ( abs ‘ 𝐴 ) ↑𝑐 𝐵 ) = ( exp ‘ ( 𝐵 · ( log ‘ ( abs ‘ 𝐴 ) ) ) ) )
43	29 34 42	3eqtr4d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ 0 ) → ( abs ‘ ( 𝐴 ↑𝑐 𝐵 ) ) = ( ( abs ‘ 𝐴 ) ↑𝑐 𝐵 ) )
44	15 43	pm2.61dane	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ) → ( abs ‘ ( 𝐴 ↑𝑐 𝐵 ) ) = ( ( abs ‘ 𝐴 ) ↑𝑐 𝐵 ) )