Theorem cxpval

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

	Ref	Expression
Assertion	cxpval	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐵 ) = if ( 𝐴 = 0 , if ( 𝐵 = 0 , 1 , 0 ) , ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝑥 = 𝐴 )
2	1	eqeq1d	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑥 = 0 ↔ 𝐴 = 0 ) )
3		simpr	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝑦 = 𝐵 )
4	3	eqeq1d	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑦 = 0 ↔ 𝐵 = 0 ) )
5	4	ifbid	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → if ( 𝑦 = 0 , 1 , 0 ) = if ( 𝐵 = 0 , 1 , 0 ) )
6	1	fveq2d	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( log ‘ 𝑥 ) = ( log ‘ 𝐴 ) )
7	3 6	oveq12d	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑦 · ( log ‘ 𝑥 ) ) = ( 𝐵 · ( log ‘ 𝐴 ) ) )
8	7	fveq2d	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( exp ‘ ( 𝑦 · ( log ‘ 𝑥 ) ) ) = ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) )
9	2 5 8	ifbieq12d	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → if ( 𝑥 = 0 , if ( 𝑦 = 0 , 1 , 0 ) , ( exp ‘ ( 𝑦 · ( log ‘ 𝑥 ) ) ) ) = if ( 𝐴 = 0 , if ( 𝐵 = 0 , 1 , 0 ) , ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ) )
10		df-cxp	⊢ ↑𝑐 = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ if ( 𝑥 = 0 , if ( 𝑦 = 0 , 1 , 0 ) , ( exp ‘ ( 𝑦 · ( log ‘ 𝑥 ) ) ) ) )
11		ax-1cn	⊢ 1 ∈ ℂ
12		0cn	⊢ 0 ∈ ℂ
13	11 12	ifcli	⊢ if ( 𝐵 = 0 , 1 , 0 ) ∈ ℂ
14	13	elexi	⊢ if ( 𝐵 = 0 , 1 , 0 ) ∈ V
15		fvex	⊢ ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ∈ V
16	14 15	ifex	⊢ if ( 𝐴 = 0 , if ( 𝐵 = 0 , 1 , 0 ) , ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ) ∈ V
17	9 10 16	ovmpoa	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐵 ) = if ( 𝐴 = 0 , if ( 𝐵 = 0 , 1 , 0 ) , ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ) )