Theorem cxp1

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

	Ref	Expression
Assertion	cxp1	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑𝑐 1 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		1nn0	⊢ 1 ∈ ℕ0
2		cxpexp	⊢ ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℕ0 ) → ( 𝐴 ↑𝑐 1 ) = ( 𝐴 ↑ 1 ) )
3	1 2	mpan2	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑𝑐 1 ) = ( 𝐴 ↑ 1 ) )
4		exp1	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 1 ) = 𝐴 )
5	3 4	eqtrd	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑𝑐 1 ) = 𝐴 )