Metamath Proof Explorer


Theorem sq10

Description: The square of 10 is 100. (Contributed by AV, 14-Jun-2021) (Revised by AV, 1-Aug-2021)

Ref Expression
Assertion sq10 102=100

Proof

Step Hyp Ref Expression
1 10nn0 100
2 1 nn0cni 10
3 2 sqvali 102=1010
4 1 dec0u 1010=100
5 3 4 eqtri 102=100