Theorem sq4e2t8

Description: The square of 4 is 2 times 8. (Contributed by AV, 20-Jul-2021)

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

Proof

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=22\cdot 4$$
11		4t2e8	$$⊢4\cdot 2=8$$
12	9 4 11	mulcomli	$$⊢2\cdot 4=8$$
13	12	oveq2i	$$⊢22\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$$