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

Step	Hyp	Ref	Expression
1		sq10	$⊢ 10^{2} = 100$
2		9nn0	$⊢ 9 \in ℕ_{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$