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

Metamath Proof Explorer

Theorem decadd

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

Ref Expression
Hypotheses decma.a 
|- A e. NN0
decma.b 
|- B e. NN0
decma.c 
|- C e. NN0
decma.d 
|- D e. NN0
decma.m 
|- M = ; A B
decma.n 
|- N = ; C D
decadd.e 
|- ( A + C ) = E
decadd.f 
|- ( B + D ) = F
Assertion decadd 
|- ( M + N ) = ; E F

Proof

Step Hyp Ref Expression
1 decma.a 
 |-  A e. NN0
2 decma.b 
 |-  B e. NN0
3 decma.c 
 |-  C e. NN0
4 decma.d 
 |-  D e. NN0
5 decma.m 
 |-  M = ; A B
6 decma.n 
 |-  N = ; C D
7 decadd.e 
 |-  ( A + C ) = E
8 decadd.f 
 |-  ( B + D ) = F
9 10nn0 
 |-  ; 1 0 e. NN0
10 dfdec10 
 |-  ; A B = ( ( ; 1 0 x. A ) + B )
11 5 10 eqtri 
 |-  M = ( ( ; 1 0 x. A ) + B )
12 dfdec10 
 |-  ; C D = ( ( ; 1 0 x. C ) + D )
13 6 12 eqtri 
 |-  N = ( ( ; 1 0 x. C ) + D )
14 9 1 2 3 4 11 13 7 8 numadd 
 |-  ( M + N ) = ( ( ; 1 0 x. E ) + F )
15 dfdec10 
 |-  ; E F = ( ( ; 1 0 x. E ) + F )
16 14 15 eqtr4i 
 |-  ( M + N ) = ; E F