This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem abscxp

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

Ref Expression
Assertion abscxp ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ) → ( abs ‘ ( 𝐴 ↑𝑐 𝐵 ) ) = ( 𝐴 ↑𝑐 ( ℜ ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ) → 𝐵 ∈ ℂ )
2 relogcl ⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ 𝐴 ) ∈ ℝ )
3 2 recnd ⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ 𝐴 ) ∈ ℂ )
4 3 adantr ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ) → ( log ‘ 𝐴 ) ∈ ℂ )
5 1 4 mulcld ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ) → ( 𝐵 · ( log ‘ 𝐴 ) ) ∈ ℂ )
6 absef ⊢ ( ( 𝐵 · ( log ‘ 𝐴 ) ) ∈ ℂ → ( abs ‘ ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ) = ( exp ‘ ( ℜ ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ) )
7 5 6 syl ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ) → ( abs ‘ ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ) = ( exp ‘ ( ℜ ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ) )
8 remul2 ⊢ ( ( ( log ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ( ℜ ‘ ( ( log ‘ 𝐴 ) · 𝐵 ) ) = ( ( log ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) )
9 2 8 sylan ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ) → ( ℜ ‘ ( ( log ‘ 𝐴 ) · 𝐵 ) ) = ( ( log ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) )
10 1 4 mulcomd ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ) → ( 𝐵 · ( log ‘ 𝐴 ) ) = ( ( log ‘ 𝐴 ) · 𝐵 ) )
11 10 fveq2d ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ) → ( ℜ ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) = ( ℜ ‘ ( ( log ‘ 𝐴 ) · 𝐵 ) ) )
12 recl ⊢ ( 𝐵 ∈ ℂ → ( ℜ ‘ 𝐵 ) ∈ ℝ )
13 12 adantl ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ) → ( ℜ ‘ 𝐵 ) ∈ ℝ )
14 13 recnd ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ) → ( ℜ ‘ 𝐵 ) ∈ ℂ )
15 14 4 mulcomd ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ) → ( ( ℜ ‘ 𝐵 ) · ( log ‘ 𝐴 ) ) = ( ( log ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) )
16 9 11 15 3eqtr4d ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ) → ( ℜ ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) = ( ( ℜ ‘ 𝐵 ) · ( log ‘ 𝐴 ) ) )
17 16 fveq2d ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ) → ( exp ‘ ( ℜ ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ) = ( exp ‘ ( ( ℜ ‘ 𝐵 ) · ( log ‘ 𝐴 ) ) ) )
18 7 17 eqtrd ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ) → ( abs ‘ ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ) = ( exp ‘ ( ( ℜ ‘ 𝐵 ) · ( log ‘ 𝐴 ) ) ) )
19 rpcn ⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℂ )
20 19 adantr ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ) → 𝐴 ∈ ℂ )
21 rpne0 ⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ≠ 0 )
22 21 adantr ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ) → 𝐴 ≠ 0 )
23 cxpef ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐵 ) = ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) )
24 20 22 1 23 syl3anc ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐵 ) = ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) )
25 24 fveq2d ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ) → ( abs ‘ ( 𝐴 ↑𝑐 𝐵 ) ) = ( abs ‘ ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ) )
26 cxpef ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ ( ℜ ‘ 𝐵 ) ∈ ℂ ) → ( 𝐴 ↑𝑐 ( ℜ ‘ 𝐵 ) ) = ( exp ‘ ( ( ℜ ‘ 𝐵 ) · ( log ‘ 𝐴 ) ) ) )
27 20 22 14 26 syl3anc ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑𝑐 ( ℜ ‘ 𝐵 ) ) = ( exp ‘ ( ( ℜ ‘ 𝐵 ) · ( log ‘ 𝐴 ) ) ) )
28 18 25 27 3eqtr4d ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ) → ( abs ‘ ( 𝐴 ↑𝑐 𝐵 ) ) = ( 𝐴 ↑𝑐 ( ℜ ‘ 𝐵 ) ) )