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

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	$⊢ A \in ℂ \to A^{2} = A A$

Step	Hyp	Ref	Expression
1		df-2	$⊢ 2 = 1 + 1$
2	1	oveq2i	$⊢ A^{2} = A^{1 + 1}$
3		1nn0	$⊢ 1 \in ℕ_{0}$
4		expp1	$⊢ (A \in ℂ \land 1 \in ℕ_{0}) \to A^{1 + 1} = A^{1} A$
5	3 4	mpan2	$⊢ A \in ℂ \to A^{1 + 1} = A^{1} A$
6	2 5	eqtrid	$⊢ A \in ℂ \to A^{2} = A^{1} A$
7		exp1	$⊢ A \in ℂ \to A^{1} = A$
8	7	oveq1d	$⊢ A \in ℂ \to A^{1} A = A A$
9	6 8	eqtrd	$⊢ A \in ℂ \to A^{2} = A A$