Metamath Proof Explorer


Theorem sq8

Description: The square of 8 is 64. (Contributed by SN, 26-Aug-2025)

Ref Expression
Assertion sq8 ( 8 ↑ 2 ) = 6 4

Proof

Step Hyp Ref Expression
1 8cn 8 ∈ ℂ
2 1 sqvali ( 8 ↑ 2 ) = ( 8 · 8 )
3 8t8e64 ( 8 · 8 ) = 6 4
4 2 3 eqtri ( 8 ↑ 2 ) = 6 4