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 โŠข ๐ด โˆˆ โ„•0
decma.b โŠข ๐ต โˆˆ โ„•0
decma.c โŠข ๐ถ โˆˆ โ„•0
decma.d โŠข ๐ท โˆˆ โ„•0
decma.m โŠข ๐‘€ = ๐ด ๐ต
decma.n โŠข ๐‘ = ๐ถ ๐ท
decaddc.e โŠข ( ( ๐ด + ๐ถ ) + 1 ) = ๐ธ
decaddc.f โŠข ๐น โˆˆ โ„•0
decaddc.2 โŠข ( ๐ต + ๐ท ) = 1 ๐น
Assertion decaddc ( ๐‘€ + ๐‘ ) = ๐ธ ๐น

Proof

Step Hyp Ref Expression
1 decma.a โŠข ๐ด โˆˆ โ„•0
2 decma.b โŠข ๐ต โˆˆ โ„•0
3 decma.c โŠข ๐ถ โˆˆ โ„•0
4 decma.d โŠข ๐ท โˆˆ โ„•0
5 decma.m โŠข ๐‘€ = ๐ด ๐ต
6 decma.n โŠข ๐‘ = ๐ถ ๐ท
7 decaddc.e โŠข ( ( ๐ด + ๐ถ ) + 1 ) = ๐ธ
8 decaddc.f โŠข ๐น โˆˆ โ„•0
9 decaddc.2 โŠข ( ๐ต + ๐ท ) = 1 ๐น
10 10nn0 โŠข 1 0 โˆˆ โ„•0
11 dfdec10 โŠข ๐ด ๐ต = ( ( 1 0 ยท ๐ด ) + ๐ต )
12 5 11 eqtri โŠข ๐‘€ = ( ( 1 0 ยท ๐ด ) + ๐ต )
13 dfdec10 โŠข ๐ถ ๐ท = ( ( 1 0 ยท ๐ถ ) + ๐ท )
14 6 13 eqtri โŠข ๐‘ = ( ( 1 0 ยท ๐ถ ) + ๐ท )
15 dfdec10 โŠข 1 ๐น = ( ( 1 0 ยท 1 ) + ๐น )
16 9 15 eqtri โŠข ( ๐ต + ๐ท ) = ( ( 1 0 ยท 1 ) + ๐น )
17 10 1 2 3 4 12 14 8 7 16 numaddc โŠข ( ๐‘€ + ๐‘ ) = ( ( 1 0 ยท ๐ธ ) + ๐น )
18 dfdec10 โŠข ๐ธ ๐น = ( ( 1 0 ยท ๐ธ ) + ๐น )
19 17 18 eqtr4i โŠข ( ๐‘€ + ๐‘ ) = ๐ธ ๐น