Metamath Proof Explorer
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 |