Metamath Proof Explorer

Theorem decaddci

Description: Add two numerals M and N (no carry). (Contributed by Mario Carneiro, 18-Feb-2014)

Ref Expression
Hypotheses decaddi.1 ⊢ 𝐴 ∈ ℕ0
decaddi.2 ⊢ 𝐵 ∈ ℕ0
decaddi.3 ⊢ 𝑁 ∈ ℕ0
decaddi.4 ⊢ 𝑀 = 𝐴 𝐵
decaddci.5 ⊢ ( 𝐴 + 1 ) = 𝐷
decaddci.6 ⊢ 𝐶 ∈ ℕ0
decaddci.7 ⊢ ( 𝐵 + 𝑁 ) = 1 𝐶
Assertion decaddci ( 𝑀 + 𝑁 ) = 𝐷 𝐶

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 decaddci.6 ⊢ 𝐶 ∈ ℕ0
7 decaddci.7 ⊢ ( 𝐵 + 𝑁 ) = 1 𝐶
8 0nn0 ⊢ 0 ∈ ℕ0
9 3 dec0h ⊢ 𝑁 = 0 𝑁
10 1 nn0cni ⊢ 𝐴 ∈ ℂ
11 10 addridi ⊢ ( 𝐴 + 0 ) = 𝐴
12 11 oveq1i ⊢ ( ( 𝐴 + 0 ) + 1 ) = ( 𝐴 + 1 )
13 12 5 eqtri ⊢ ( ( 𝐴 + 0 ) + 1 ) = 𝐷
14 1 2 8 3 4 9 13 6 7 decaddc ⊢ ( 𝑀 + 𝑁 ) = 𝐷 𝐶