This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem decaddc2

Description: Add two numerals M and N (with carry). (Contributed by Mario Carneiro, 18-Feb-2014) (Revised by AV, 6-Sep-2021)

Ref Expression
Hypotheses decma.a ⊢ A ∈ ℕ 0
decma.b ⊢ B ∈ ℕ 0
decma.c ⊢ C ∈ ℕ 0
decma.d ⊢ D ∈ ℕ 0
decma.m No typesetting found for |- M = ; A B with typecode |-
decma.n No typesetting found for |- N = ; C D with typecode |-
decaddc.e ⊢ A + C + 1 = E
decaddc2.t ⊢ B + D = 10
Assertion decaddc2 Could not format assertion : No typesetting found for |- ( M + N ) = ; E 0 with typecode |-

Proof

Step Hyp Ref Expression
1 decma.a ⊢ A ∈ ℕ 0
2 decma.b ⊢ B ∈ ℕ 0
3 decma.c ⊢ C ∈ ℕ 0
4 decma.d ⊢ D ∈ ℕ 0
5 decma.m Could not format M = ; A B : No typesetting found for |- M = ; A B with typecode |-
6 decma.n Could not format N = ; C D : No typesetting found for |- N = ; C D with typecode |-
7 decaddc.e ⊢ A + C + 1 = E
8 decaddc2.t ⊢ B + D = 10
9 0nn0 ⊢ 0 ∈ ℕ 0
10 1 2 3 4 5 6 7 9 8 decaddc Could not format ( M + N ) = ; E 0 : No typesetting found for |- ( M + N ) = ; E 0 with typecode |-