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

Proof

Step Hyp Ref Expression
1 df-dec 10 = 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 = 10