Metamath Proof Explorer


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 )