Metamath Proof Explorer

Theorem cxpcl

Description: Closure of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014)

Ref Expression
Assertion cxpcl ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐵 ) ∈ ℂ )

Proof

Step Hyp Ref Expression
1 cxpval ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐵 ) = if ( 𝐴 = 0 , if ( 𝐵 = 0 , 1 , 0 ) , ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ) )
2 ax-1cn ⊢ 1 ∈ ℂ
3 0cn ⊢ 0 ∈ ℂ
4 2 3 ifcli ⊢ if ( 𝐵 = 0 , 1 , 0 ) ∈ ℂ
5 4 a1i ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐴 = 0 ) → if ( 𝐵 = 0 , 1 , 0 ) ∈ ℂ )
6 df-ne ⊢ ( 𝐴 ≠ 0 ↔ ¬ 𝐴 = 0 )
7 id ⊢ ( 𝐵 ∈ ℂ → 𝐵 ∈ ℂ )
8 logcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( log ‘ 𝐴 ) ∈ ℂ )
9 mulcl ⊢ ( ( 𝐵 ∈ ℂ ∧ ( log ‘ 𝐴 ) ∈ ℂ ) → ( 𝐵 · ( log ‘ 𝐴 ) ) ∈ ℂ )
10 7 8 9 syl2anr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) → ( 𝐵 · ( log ‘ 𝐴 ) ) ∈ ℂ )
11 10 an32s ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐴 ≠ 0 ) → ( 𝐵 · ( log ‘ 𝐴 ) ) ∈ ℂ )
12 efcl ⊢ ( ( 𝐵 · ( log ‘ 𝐴 ) ) ∈ ℂ → ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ∈ ℂ )
13 11 12 syl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ∈ ℂ )
14 6 13 sylan2br ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ¬ 𝐴 = 0 ) → ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ∈ ℂ )
15 5 14 ifclda ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → if ( 𝐴 = 0 , if ( 𝐵 = 0 , 1 , 0 ) , ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ) ∈ ℂ )
16 1 15 eqeltrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐵 ) ∈ ℂ )