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 ) = ( 𝐴 · 𝐴 ) )