Metamath Proof Explorer


Theorem sqval

Description: Value of the square of a complex number. (Contributed by Raph Levien, 10-Apr-2004)

Ref Expression
Assertion sqval ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 ) )

Proof

Step Hyp Ref Expression
1 df-2 2 = ( 1 + 1 )
2 1 oveq2i ( 𝐴 ↑ 2 ) = ( 𝐴 ↑ ( 1 + 1 ) )
3 1nn0 1 ∈ ℕ0
4 expp1 ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℕ0 ) → ( 𝐴 ↑ ( 1 + 1 ) ) = ( ( 𝐴 ↑ 1 ) · 𝐴 ) )
5 3 4 mpan2 ( 𝐴 ∈ ℂ → ( 𝐴 ↑ ( 1 + 1 ) ) = ( ( 𝐴 ↑ 1 ) · 𝐴 ) )
6 2 5 eqtrid ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 2 ) = ( ( 𝐴 ↑ 1 ) · 𝐴 ) )
7 exp1 ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 1 ) = 𝐴 )
8 7 oveq1d ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 1 ) · 𝐴 ) = ( 𝐴 · 𝐴 ) )
9 6 8 eqtrd ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 ) )