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 0
decma.b B 0
decma.c C 0
decma.d D 0
decma.m No typesetting found for |- M = ; A B with typecode |-
decma.n No typesetting found for |- N = ; C D with typecode |-
decadd.e A + C = E
decadd.f B + D = F
Assertion decadd Could not format assertion : No typesetting found for |- ( M + N ) = ; E F with typecode |-

Proof

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