Metamath Proof Explorer

Theorem decaddc2

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 ) = 𝐸
decaddc2.t ⊢ ( 𝐵 + 𝐷 ) = 1 0
Assertion decaddc2 ( 𝑀 + 𝑁 ) = 𝐸 0

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 decaddc2.t ⊢ ( 𝐵 + 𝐷 ) = 1 0
9 0nn0 ⊢ 0 ∈ ℕ0
10 1 2 3 4 5 6 7 9 8 decaddc ⊢ ( 𝑀 + 𝑁 ) = 𝐸 0