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

Metamath Proof Explorer

Theorem numsucc

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

Ref Expression
Hypotheses numsucc.1 ⊢ Y ∈ ℕ 0
numsucc.2 ⊢ T = Y + 1
numsucc.3 ⊢ A ∈ ℕ 0
numsucc.4 ⊢ A + 1 = B
numsucc.5 ⊢ N = T ⁢ A + Y
Assertion numsucc ⊢ N + 1 = T ⁢ B + 0

Proof

Step Hyp Ref Expression
1 numsucc.1 ⊢ Y ∈ ℕ 0
2 numsucc.2 ⊢ T = Y + 1
3 numsucc.3 ⊢ A ∈ ℕ 0
4 numsucc.4 ⊢ A + 1 = B
5 numsucc.5 ⊢ N = T ⁢ A + Y
6 1nn0 ⊢ 1 ∈ ℕ 0
7 1 6 nn0addcli ⊢ Y + 1 ∈ ℕ 0
8 2 7 eqeltri ⊢ T ∈ ℕ 0
9 8 nn0cni ⊢ T ∈ ℂ
10 9 mulridi ⊢ T ⋅ 1 = T
11 10 oveq2i ⊢ T ⁢ A + T ⋅ 1 = T ⁢ A + T
12 3 nn0cni ⊢ A ∈ ℂ
13 ax-1cn ⊢ 1 ∈ ℂ
14 9 12 13 adddii ⊢ T ⁢ A + 1 = T ⁢ A + T ⋅ 1
15 2 eqcomi ⊢ Y + 1 = T
16 8 3 1 15 5 numsuc ⊢ N + 1 = T ⁢ A + T
17 11 14 16 3eqtr4ri ⊢ N + 1 = T ⁢ A + 1
18 4 oveq2i ⊢ T ⁢ A + 1 = T ⁢ B
19 3 6 nn0addcli ⊢ A + 1 ∈ ℕ 0
20 4 19 eqeltrri ⊢ B ∈ ℕ 0
21 8 20 num0u ⊢ T ⁢ B = T ⁢ B + 0
22 17 18 21 3eqtri ⊢ N + 1 = T ⁢ B + 0