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 ) = ; 1 0

Proof

Step	Hyp	Ref	Expression
1		df-dec	⊢ ; 1 0 = ( ( ( 9 + 1 ) · 1 ) + 0 )
2		9nn	⊢ 9 ∈ ℕ
3		1nn	⊢ 1 ∈ ℕ
4		nnaddcl	⊢ ( ( 9 ∈ ℕ ∧ 1 ∈ ℕ ) → ( 9 + 1 ) ∈ ℕ )
5	2 3 4	mp2an	⊢ ( 9 + 1 ) ∈ ℕ
6	5	nncni	⊢ ( 9 + 1 ) ∈ ℂ
7	6	mulid1i	⊢ ( ( 9 + 1 ) · 1 ) = ( 9 + 1 )
8	7	oveq1i	⊢ ( ( ( 9 + 1 ) · 1 ) + 0 ) = ( ( 9 + 1 ) + 0 )
9	6	addid1i	⊢ ( ( 9 + 1 ) + 0 ) = ( 9 + 1 )
10	1 8 9	3eqtrri	⊢ ( 9 + 1 ) = ; 1 0