sq4e2t8

		Ref	Expression
	Assertion	sq4e2t8	$⊢ 4^{2} = 2 \cdot 8$

Step	Hyp	Ref	Expression
1		2t2e4	$⊢ 2 \cdot 2 = 4$
2	1	eqcomi	$⊢ 4 = 2 \cdot 2$
3	2	oveq1i	$⊢ 4^{2} = {2 \cdot 2}^{2}$
4		2cn	$⊢ 2 \in ℂ$
5	4 4	sqmuli	$⊢ {2 \cdot 2}^{2} = 2^{2} 2^{2}$
6	4	sqvali	$⊢ 2^{2} = 2 \cdot 2$
7		sq2	$⊢ 2^{2} = 4$
8	6 7	oveq12i	$⊢ 2^{2} 2^{2} = 2 \cdot 2 \cdot 4$
9		4cn	$⊢ 4 \in ℂ$
10	4 4 9	mulassi	$⊢ 2 \cdot 2 \cdot 4 = 2 2 \cdot 4$
11		4t2e8	$⊢ 4 \cdot 2 = 8$
12	9 4 11	mulcomli	$⊢ 2 \cdot 4 = 8$
13	12	oveq2i	$⊢ 2 2 \cdot 4 = 2 \cdot 8$
14	8 10 13	3eqtri	$⊢ 2^{2} 2^{2} = 2 \cdot 8$
15	3 5 14	3eqtri	$⊢ 4^{2} = 2 \cdot 8$

Metamath Proof Explorer