Metamath Proof Explorer


Theorem sq7

Description: The square of 7 is 49. (Contributed by SN, 26-Aug-2025)

Ref Expression
Assertion sq7 ( 7 ↑ 2 ) = 4 9

Proof

Step Hyp Ref Expression
1 7cn 7 ∈ ℂ
2 1 sqvali ( 7 ↑ 2 ) = ( 7 · 7 )
3 7t7e49 ( 7 · 7 ) = 4 9
4 2 3 eqtri ( 7 ↑ 2 ) = 4 9