Theorem sq4e2t8

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

	Ref	Expression
Assertion	sq4e2t8	⊢ ( 4 ↑ 2 ) = ( 2 · 8 )

Proof

Step	Hyp	Ref	Expression
1		2t2e4	⊢ ( 2 · 2 ) = 4
2	1	eqcomi	⊢ 4 = ( 2 · 2 )
3	2	oveq1i	⊢ ( 4 ↑ 2 ) = ( ( 2 · 2 ) ↑ 2 )
4		2cn	⊢ 2 ∈ ℂ
5	4 4	sqmuli	⊢ ( ( 2 · 2 ) ↑ 2 ) = ( ( 2 ↑ 2 ) · ( 2 ↑ 2 ) )
6	4	sqvali	⊢ ( 2 ↑ 2 ) = ( 2 · 2 )
7		sq2	⊢ ( 2 ↑ 2 ) = 4
8	6 7	oveq12i	⊢ ( ( 2 ↑ 2 ) · ( 2 ↑ 2 ) ) = ( ( 2 · 2 ) · 4 )
9		4cn	⊢ 4 ∈ ℂ
10	4 4 9	mulassi	⊢ ( ( 2 · 2 ) · 4 ) = ( 2 · ( 2 · 4 ) )
11		4t2e8	⊢ ( 4 · 2 ) = 8
12	9 4 11	mulcomli	⊢ ( 2 · 4 ) = 8
13	12	oveq2i	⊢ ( 2 · ( 2 · 4 ) ) = ( 2 · 8 )
14	8 10 13	3eqtri	⊢ ( ( 2 ↑ 2 ) · ( 2 ↑ 2 ) ) = ( 2 · 8 )
15	3 5 14	3eqtri	⊢ ( 4 ↑ 2 ) = ( 2 · 8 )