This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem decaddi

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
decaddi.5 
|- ( B + N ) = C
Assertion decaddi 
|- ( M + N ) = ; A 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 decaddi.5 
 |-  ( B + N ) = C
6 0nn0 
 |-  0 e. NN0
7 3 dec0h 
 |-  N = ; 0 N
8 1 nn0cni 
 |-  A e. CC
9 8 addridi 
 |-  ( A + 0 ) = A
10 1 2 6 3 4 7 9 5 decadd 
 |-  ( M + N ) = ; A C