This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · ( 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 )