This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sq10e99m1

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

Ref Expression
Assertion sq10e99m1 ( 1 0 ↑ 2 ) = ( 9 9 + 1 )

Proof

Step Hyp Ref Expression
1 sq10 ⊢ ( 1 0 ↑ 2 ) = 1 0 0
2 9nn0 ⊢ 9 ∈ ℕ0
3 9p1e10 ⊢ ( 9 + 1 ) = 1 0
4 eqid ⊢ 9 9 = 9 9
5 2 3 4 decsucc ⊢ ( 9 9 + 1 ) = 1 0 0
6 1 5 eqtr4i ⊢ ( 1 0 ↑ 2 ) = ( 9 9 + 1 )