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

Metamath Proof Explorer

Theorem numsuc

Description: The successor of a decimal integer (no carry). (Contributed by Mario Carneiro, 18-Feb-2014)

Ref Expression
Hypotheses numnncl.1 ⊢ T ∈ ℕ 0
numnncl.2 ⊢ A ∈ ℕ 0
numcl.2 ⊢ B ∈ ℕ 0
numsuc.4 ⊢ B + 1 = C
numsuc.5 ⊢ N = T ⁢ A + B
Assertion numsuc ⊢ N + 1 = T ⁢ A + C

Proof

Step Hyp Ref Expression
1 numnncl.1 ⊢ T ∈ ℕ 0
2 numnncl.2 ⊢ A ∈ ℕ 0
3 numcl.2 ⊢ B ∈ ℕ 0
4 numsuc.4 ⊢ B + 1 = C
5 numsuc.5 ⊢ N = T ⁢ A + B
6 5 oveq1i ⊢ N + 1 = T ⁢ A + B + 1
7 1 2 nn0mulcli ⊢ T ⁢ A ∈ ℕ 0
8 7 nn0cni ⊢ T ⁢ A ∈ ℂ
9 3 nn0cni ⊢ B ∈ ℂ
10 ax-1cn ⊢ 1 ∈ ℂ
11 8 9 10 addassi ⊢ T ⁢ A + B + 1 = T ⁢ A + B + 1
12 4 oveq2i ⊢ T ⁢ A + B + 1 = T ⁢ A + C
13 6 11 12 3eqtri ⊢ N + 1 = T ⁢ A + C