Theorem 9p1e10

Description: 9 + 1 = 10. (Contributed by Mario Carneiro, 18-Apr-2015) (Revised by Stanislas Polu, 7-Apr-2020) (Revised by AV, 1-Aug-2021)

	Ref	Expression
Assertion	9p1e10	$$⊢9+1=10$$

Proof

Step	Hyp	Ref	Expression
1		df-dec	$$⊢10=\left(9+1\right)\cdot 1+0$$
2		9nn	$$⊢9\in \mathbb{N}$$
3		1nn	$$⊢1\in \mathbb{N}$$
4		nnaddcl	$$⊢\left(9\in \mathbb{N}\wedge 1\in \mathbb{N}\right)\to 9+1\in \mathbb{N}$$
5	2 3 4	mp2an	$$⊢9+1\in \mathbb{N}$$
6	5	nncni	$$⊢9+1\in ℂ$$
7	6	mulridi	$$⊢\left(9+1\right)\cdot 1=9+1$$
8	7	oveq1i	$$⊢\left(9+1\right)\cdot 1+0=9+1+0$$
9	6	addridi	$$⊢9+1+0=9+1$$
10	1 8 9	3eqtrri	$$⊢9+1=10$$