Metamath Proof Explorer


Theorem sq9

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

Ref Expression
Assertion sq9
|- ( 9 ^ 2 ) = ; 8 1

Proof

Step Hyp Ref Expression
1 9cn
 |-  9 e. CC
2 1 sqvali
 |-  ( 9 ^ 2 ) = ( 9 x. 9 )
3 9t9e81
 |-  ( 9 x. 9 ) = ; 8 1
4 2 3 eqtri
 |-  ( 9 ^ 2 ) = ; 8 1