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 A0
decma.b B0
decma.c C0
decma.d D0
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 A0
2 decma.b B0
3 decma.c C0
4 decma.d D0
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 100
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=10A+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=10C+D
14 9 1 2 3 4 11 13 7 8 numadd M+N=10E+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 |-