Description: The square of 10 is 100. (Contributed by AV, 14-Jun-2021) (Revised by AV, 1-Aug-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | sq10 | ⊢ ( ; 1 0 ↑ 2 ) = ; ; 1 0 0 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 10nn0 | ⊢ ; 1 0 ∈ ℕ0 | |
| 2 | 1 | nn0cni | ⊢ ; 1 0 ∈ ℂ |
| 3 | 2 | sqvali | ⊢ ( ; 1 0 ↑ 2 ) = ( ; 1 0 · ; 1 0 ) |
| 4 | 1 | dec0u | ⊢ ( ; 1 0 · ; 1 0 ) = ; ; 1 0 0 |
| 5 | 3 4 | eqtri | ⊢ ( ; 1 0 ↑ 2 ) = ; ; 1 0 0 |