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	$$⊢{10}^2=99+1$$

Proof

Step	Hyp	Ref	Expression
1		sq10	$$⊢{10}^2=100$$
2		9nn0	$$⊢9\in {\mathbb{N}}_0$$
3		9p1e10	$$⊢9+1=10$$
4		eqid	$$⊢99=99$$
5	2 3 4	decsucc	$$⊢99+1=100$$
6	1 5	eqtr4i	$$⊢{10}^2=99+1$$