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

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 )