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 ( 𝑀 + 𝑁 ) = 𝐸 𝐹