Description: The successor of a decimal integer (with carry). (Contributed by Mario Carneiro, 18-Feb-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | numsucc.1 | |
|
numsucc.2 | |
||
numsucc.3 | |
||
numsucc.4 | |
||
numsucc.5 | |
||
Assertion | numsucc | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | numsucc.1 | |
|
2 | numsucc.2 | |
|
3 | numsucc.3 | |
|
4 | numsucc.4 | |
|
5 | numsucc.5 | |
|
6 | 1nn0 | |
|
7 | 1 6 | nn0addcli | |
8 | 2 7 | eqeltri | |
9 | 8 | nn0cni | |
10 | 9 | mulid1i | |
11 | 10 | oveq2i | |
12 | 3 | nn0cni | |
13 | ax-1cn | |
|
14 | 9 12 13 | adddii | |
15 | 2 | eqcomi | |
16 | 8 3 1 15 5 | numsuc | |
17 | 11 14 16 | 3eqtr4ri | |
18 | 4 | oveq2i | |
19 | 3 6 | nn0addcli | |
20 | 4 19 | eqeltrri | |
21 | 8 20 | num0u | |
22 | 17 18 21 | 3eqtri | |