Description: Value of the square of a complex number. (Contributed by Raph Levien, 10-Apr-2004)
Ref | Expression | ||
---|---|---|---|
Assertion | sqval | ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 ) ) |
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 ) = ( 𝐴 · 𝐴 ) ) |