Metamath Proof Explorer


Theorem sq4

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

Ref Expression
Assertion sq4 4 2 = 16

Proof

Step Hyp Ref Expression
1 4cn 4
2 1 sqvali 4 2 = 4 4
3 4t4e16 4 4 = 16
4 2 3 eqtri 4 2 = 16