Metamath Proof Explorer


Theorem sq8

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

Ref Expression
Assertion sq8 ⊢ 8 2 = 64

Proof

Step Hyp Ref Expression
1 8cn ⊢ 8 ∈ ℂ
2 1 sqvali ⊢ 8 2 = 8 ⋅ 8
3 8t8e64 ⊢ 8 ⋅ 8 = 64
4 2 3 eqtri ⊢ 8 2 = 64