Metamath Proof Explorer

Theorem decaddi

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 ⊢ 𝑀 = 𝐴 𝐵
decaddi.5 ⊢ ( 𝐵 + 𝑁 ) = 𝐶
Assertion decaddi ( 𝑀 + 𝑁 ) = 𝐴 𝐶

Proof

Step Hyp Ref Expression
1 decaddi.1 ⊢ 𝐴 ∈ ℕ0
2 decaddi.2 ⊢ 𝐵 ∈ ℕ0
3 decaddi.3 ⊢ 𝑁 ∈ ℕ0
4 decaddi.4 ⊢ 𝑀 = 𝐴 𝐵
5 decaddi.5 ⊢ ( 𝐵 + 𝑁 ) = 𝐶
6 0nn0 ⊢ 0 ∈ ℕ0
7 3 dec0h ⊢ 𝑁 = 0 𝑁
8 1 nn0cni ⊢ 𝐴 ∈ ℂ
9 8 addridi ⊢ ( 𝐴 + 0 ) = 𝐴
10 1 2 6 3 4 7 9 5 decadd ⊢ ( 𝑀 + 𝑁 ) = 𝐴 𝐶