Metamath Proof Explorer


Theorem numsucc

Description: The successor of a decimal integer (with carry). (Contributed by Mario Carneiro, 18-Feb-2014)

Ref Expression
Hypotheses numsucc.1 Y0
numsucc.2 T=Y+1
numsucc.3 A0
numsucc.4 A+1=B
numsucc.5 N=TA+Y
Assertion numsucc N+1=TB+0

Proof

Step Hyp Ref Expression
1 numsucc.1 Y0
2 numsucc.2 T=Y+1
3 numsucc.3 A0
4 numsucc.4 A+1=B
5 numsucc.5 N=TA+Y
6 1nn0 10
7 1 6 nn0addcli Y+10
8 2 7 eqeltri T0
9 8 nn0cni T
10 9 mulid1i T1=T
11 10 oveq2i TA+T1=TA+T
12 3 nn0cni A
13 ax-1cn 1
14 9 12 13 adddii TA+1=TA+T1
15 2 eqcomi Y+1=T
16 8 3 1 15 5 numsuc N+1=TA+T
17 11 14 16 3eqtr4ri N+1=TA+1
18 4 oveq2i TA+1=TB
19 3 6 nn0addcli A+10
20 4 19 eqeltrri B0
21 8 20 num0u TB=TB+0
22 17 18 21 3eqtri N+1=TB+0