Metamath Proof Explorer


Theorem sq9

Description: The square of 9 is 81. (Contributed by SN, 30-Mar-2025)

Ref Expression
Assertion sq9 ⊢ 9 2 = 81

Proof

Step Hyp Ref Expression
1 9cn ⊢ 9 ∈ ℂ
2 1 sqvali ⊢ 9 2 = 9 ⋅ 9
3 9t9e81 ⊢ 9 ⋅ 9 = 81
4 2 3 eqtri ⊢ 9 2 = 81