Theorem 1cxp

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

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

Proof

Step	Hyp	Ref	Expression
1		ax-1cn	⊢ 1 ∈ ℂ
2		ax-1ne0	⊢ 1 ≠ 0
3		cxpef	⊢ ( ( 1 ∈ ℂ ∧ 1 ≠ 0 ∧ 𝐴 ∈ ℂ ) → ( 1 ↑𝑐 𝐴 ) = ( exp ‘ ( 𝐴 · ( log ‘ 1 ) ) ) )
4	1 2 3	mp3an12	⊢ ( 𝐴 ∈ ℂ → ( 1 ↑𝑐 𝐴 ) = ( exp ‘ ( 𝐴 · ( log ‘ 1 ) ) ) )
5		log1	⊢ ( log ‘ 1 ) = 0
6	5	oveq2i	⊢ ( 𝐴 · ( log ‘ 1 ) ) = ( 𝐴 · 0 )
7		mul01	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · 0 ) = 0 )
8	6 7	syl5eq	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · ( log ‘ 1 ) ) = 0 )
9	8	fveq2d	⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( 𝐴 · ( log ‘ 1 ) ) ) = ( exp ‘ 0 ) )
10		ef0	⊢ ( exp ‘ 0 ) = 1
11	9 10	eqtrdi	⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( 𝐴 · ( log ‘ 1 ) ) ) = 1 )
12	4 11	eqtrd	⊢ ( 𝐴 ∈ ℂ → ( 1 ↑𝑐 𝐴 ) = 1 )