Metamath Proof Explorer


Theorem decaddci

Description: Add two numerals M and N (no carry). (Contributed by Mario Carneiro, 18-Feb-2014)

Ref Expression
Hypotheses decaddi.1
|- A e. NN0
decaddi.2
|- B e. NN0
decaddi.3
|- N e. NN0
decaddi.4
|- M = ; A B
decaddci.5
|- ( A + 1 ) = D
decaddci.6
|- C e. NN0
decaddci.7
|- ( B + N ) = ; 1 C
Assertion decaddci
|- ( M + N ) = ; D C

Proof

Step Hyp Ref Expression
1 decaddi.1
 |-  A e. NN0
2 decaddi.2
 |-  B e. NN0
3 decaddi.3
 |-  N e. NN0
4 decaddi.4
 |-  M = ; A B
5 decaddci.5
 |-  ( A + 1 ) = D
6 decaddci.6
 |-  C e. NN0
7 decaddci.7
 |-  ( B + N ) = ; 1 C
8 0nn0
 |-  0 e. NN0
9 3 dec0h
 |-  N = ; 0 N
10 1 nn0cni
 |-  A e. CC
11 10 addid1i
 |-  ( A + 0 ) = A
12 11 oveq1i
 |-  ( ( A + 0 ) + 1 ) = ( A + 1 )
13 12 5 eqtri
 |-  ( ( A + 0 ) + 1 ) = D
14 1 2 8 3 4 9 13 6 7 decaddc
 |-  ( M + N ) = ; D C