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	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐵 ) ∈ ℂ )