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 ⊢ 10 2 = 100

Proof

Step Hyp Ref Expression
1 10nn0 ⊢ 10 ∈ ℕ 0
2 1 nn0cni ⊢ 10 ∈ ℂ
3 2 sqvali ⊢ 10 2 = 10 ⋅ 10
4 1 dec0u ⊢ 10 ⋅ 10 = 100
5 3 4 eqtri ⊢ 10 2 = 100