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

Metamath Proof Explorer

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$

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