Metamath Proof Explorer


Theorem decaddci2

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 decaddi.1 𝐴 ∈ ℕ0
decaddi.2 𝐵 ∈ ℕ0
decaddi.3 𝑁 ∈ ℕ0
decaddi.4 𝑀 = 𝐴 𝐵
decaddci.5 ( 𝐴 + 1 ) = 𝐷
decaddci2.6 ( 𝐵 + 𝑁 ) = 1 0
Assertion decaddci2 ( 𝑀 + 𝑁 ) = 𝐷 0

Proof

Step Hyp Ref Expression
1 decaddi.1 𝐴 ∈ ℕ0
2 decaddi.2 𝐵 ∈ ℕ0
3 decaddi.3 𝑁 ∈ ℕ0
4 decaddi.4 𝑀 = 𝐴 𝐵
5 decaddci.5 ( 𝐴 + 1 ) = 𝐷
6 decaddci2.6 ( 𝐵 + 𝑁 ) = 1 0
7 0nn0 0 ∈ ℕ0
8 1 2 3 4 5 7 6 decaddci ( 𝑀 + 𝑁 ) = 𝐷 0