Metamath Proof Explorer

Theorem cxpadd

Description: Sum of exponents law for complex exponentiation. Proposition 10-4.2(a) of Gleason p. 135. (Contributed by Mario Carneiro, 2-Aug-2014)

Ref Expression
Assertion cxpadd ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 ↑𝑐 ( 𝐵 + 𝐶 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) · ( 𝐴 ↑𝑐 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 simp2 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐵 ∈ ℂ )
2 simp3 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐶 ∈ ℂ )
3 logcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( log ‘ 𝐴 ) ∈ ℂ )
4 3 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( log ‘ 𝐴 ) ∈ ℂ )
5 1 2 4 adddird ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐵 + 𝐶 ) · ( log ‘ 𝐴 ) ) = ( ( 𝐵 · ( log ‘ 𝐴 ) ) + ( 𝐶 · ( log ‘ 𝐴 ) ) ) )
6 5 fveq2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( exp ‘ ( ( 𝐵 + 𝐶 ) · ( log ‘ 𝐴 ) ) ) = ( exp ‘ ( ( 𝐵 · ( log ‘ 𝐴 ) ) + ( 𝐶 · ( log ‘ 𝐴 ) ) ) ) )
7 1 4 mulcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 · ( log ‘ 𝐴 ) ) ∈ ℂ )
8 2 4 mulcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐶 · ( log ‘ 𝐴 ) ) ∈ ℂ )
9 efadd ⊢ ( ( ( 𝐵 · ( log ‘ 𝐴 ) ) ∈ ℂ ∧ ( 𝐶 · ( log ‘ 𝐴 ) ) ∈ ℂ ) → ( exp ‘ ( ( 𝐵 · ( log ‘ 𝐴 ) ) + ( 𝐶 · ( log ‘ 𝐴 ) ) ) ) = ( ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) · ( exp ‘ ( 𝐶 · ( log ‘ 𝐴 ) ) ) ) )
10 7 8 9 syl2anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( exp ‘ ( ( 𝐵 · ( log ‘ 𝐴 ) ) + ( 𝐶 · ( log ‘ 𝐴 ) ) ) ) = ( ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) · ( exp ‘ ( 𝐶 · ( log ‘ 𝐴 ) ) ) ) )
11 6 10 eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( exp ‘ ( ( 𝐵 + 𝐶 ) · ( log ‘ 𝐴 ) ) ) = ( ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) · ( exp ‘ ( 𝐶 · ( log ‘ 𝐴 ) ) ) ) )
12 simp1l ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐴 ∈ ℂ )
13 simp1r ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐴 ≠ 0 )
14 addcl ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 + 𝐶 ) ∈ ℂ )
15 14 3adant1 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 + 𝐶 ) ∈ ℂ )
16 cxpef ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ ( 𝐵 + 𝐶 ) ∈ ℂ ) → ( 𝐴 ↑𝑐 ( 𝐵 + 𝐶 ) ) = ( exp ‘ ( ( 𝐵 + 𝐶 ) · ( log ‘ 𝐴 ) ) ) )
17 12 13 15 16 syl3anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 ↑𝑐 ( 𝐵 + 𝐶 ) ) = ( exp ‘ ( ( 𝐵 + 𝐶 ) · ( log ‘ 𝐴 ) ) ) )
18 cxpef ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐵 ) = ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) )
19 12 13 1 18 syl3anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐵 ) = ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) )
20 cxpef ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐶 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐶 ) = ( exp ‘ ( 𝐶 · ( log ‘ 𝐴 ) ) ) )
21 12 13 2 20 syl3anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐶 ) = ( exp ‘ ( 𝐶 · ( log ‘ 𝐴 ) ) ) )
22 19 21 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 ↑𝑐 𝐵 ) · ( 𝐴 ↑𝑐 𝐶 ) ) = ( ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) · ( exp ‘ ( 𝐶 · ( log ‘ 𝐴 ) ) ) ) )
23 11 17 22 3eqtr4d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 ↑𝑐 ( 𝐵 + 𝐶 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) · ( 𝐴 ↑𝑐 𝐶 ) ) )