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 ) x. 1 ) + 0 )
2		9nn	|- 9 e. NN
3		1nn	|- 1 e. NN
4		nnaddcl	|- ( ( 9 e. NN /\ 1 e. NN ) -> ( 9 + 1 ) e. NN )
5	2 3 4	mp2an	|- ( 9 + 1 ) e. NN
6	5	nncni	|- ( 9 + 1 ) e. CC
7	6	mulid1i	|- ( ( 9 + 1 ) x. 1 ) = ( 9 + 1 )
8	7	oveq1i	|- ( ( ( 9 + 1 ) x. 1 ) + 0 ) = ( ( 9 + 1 ) + 0 )
9	6	addid1i	|- ( ( 9 + 1 ) + 0 ) = ( 9 + 1 )
10	1 8 9	3eqtrri	|- ( 9 + 1 ) = ; 1 0