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 e. CC
2 1 sqvali
 |-  ( 8 ^ 2 ) = ( 8 x. 8 )
3 8t8e64
 |-  ( 8 x. 8 ) = ; 6 4
4 2 3 eqtri
 |-  ( 8 ^ 2 ) = ; 6 4