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