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