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 ∈ ℂ
2 1 sqvali ( 9 ↑ 2 ) = ( 9 · 9 )
3 9t9e81 ( 9 · 9 ) = 8 1
4 2 3 eqtri ( 9 ↑ 2 ) = 8 1