Metamath Proof Explorer


Theorem decaddc

Description: Add two numerals M and N (with 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
decaddc.e
|- ( ( A + C ) + 1 ) = E
decaddc.f
|- F e. NN0
decaddc.2
|- ( B + D ) = ; 1 F
Assertion decaddc
|- ( 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 decaddc.e
 |-  ( ( A + C ) + 1 ) = E
8 decaddc.f
 |-  F e. NN0
9 decaddc.2
 |-  ( B + D ) = ; 1 F
10 10nn0
 |-  ; 1 0 e. NN0
11 dfdec10
 |-  ; A B = ( ( ; 1 0 x. A ) + B )
12 5 11 eqtri
 |-  M = ( ( ; 1 0 x. A ) + B )
13 dfdec10
 |-  ; C D = ( ( ; 1 0 x. C ) + D )
14 6 13 eqtri
 |-  N = ( ( ; 1 0 x. C ) + D )
15 dfdec10
 |-  ; 1 F = ( ( ; 1 0 x. 1 ) + F )
16 9 15 eqtri
 |-  ( B + D ) = ( ( ; 1 0 x. 1 ) + F )
17 10 1 2 3 4 12 14 8 7 16 numaddc
 |-  ( M + N ) = ( ( ; 1 0 x. E ) + F )
18 dfdec10
 |-  ; E F = ( ( ; 1 0 x. E ) + F )
19 17 18 eqtr4i
 |-  ( M + N ) = ; E F