Metamath Proof Explorer


Theorem sq9

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

Ref Expression
Assertion sq9 92=81

Proof

Step Hyp Ref Expression
1 9cn 9
2 1 sqvali 92=99
3 9t9e81 99=81
4 2 3 eqtri 92=81