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 𝑌 ∈ ℕ0
numsucc.2 𝑇 = ( 𝑌 + 1 )
numsucc.3 𝐴 ∈ ℕ0
numsucc.4 ( 𝐴 + 1 ) = 𝐵
numsucc.5 𝑁 = ( ( 𝑇 · 𝐴 ) + 𝑌 )
Assertion numsucc ( 𝑁 + 1 ) = ( ( 𝑇 · 𝐵 ) + 0 )

Proof

Step Hyp Ref Expression
1 numsucc.1 𝑌 ∈ ℕ0
2 numsucc.2 𝑇 = ( 𝑌 + 1 )
3 numsucc.3 𝐴 ∈ ℕ0
4 numsucc.4 ( 𝐴 + 1 ) = 𝐵
5 numsucc.5 𝑁 = ( ( 𝑇 · 𝐴 ) + 𝑌 )
6 1nn0 1 ∈ ℕ0
7 1 6 nn0addcli ( 𝑌 + 1 ) ∈ ℕ0
8 2 7 eqeltri 𝑇 ∈ ℕ0
9 8 nn0cni 𝑇 ∈ ℂ
10 9 mulid1i ( 𝑇 · 1 ) = 𝑇
11 10 oveq2i ( ( 𝑇 · 𝐴 ) + ( 𝑇 · 1 ) ) = ( ( 𝑇 · 𝐴 ) + 𝑇 )
12 3 nn0cni 𝐴 ∈ ℂ
13 ax-1cn 1 ∈ ℂ
14 9 12 13 adddii ( 𝑇 · ( 𝐴 + 1 ) ) = ( ( 𝑇 · 𝐴 ) + ( 𝑇 · 1 ) )
15 2 eqcomi ( 𝑌 + 1 ) = 𝑇
16 8 3 1 15 5 numsuc ( 𝑁 + 1 ) = ( ( 𝑇 · 𝐴 ) + 𝑇 )
17 11 14 16 3eqtr4ri ( 𝑁 + 1 ) = ( 𝑇 · ( 𝐴 + 1 ) )
18 4 oveq2i ( 𝑇 · ( 𝐴 + 1 ) ) = ( 𝑇 · 𝐵 )
19 3 6 nn0addcli ( 𝐴 + 1 ) ∈ ℕ0
20 4 19 eqeltrri 𝐵 ∈ ℕ0
21 8 20 num0u ( 𝑇 · 𝐵 ) = ( ( 𝑇 · 𝐵 ) + 0 )
22 17 18 21 3eqtri ( 𝑁 + 1 ) = ( ( 𝑇 · 𝐵 ) + 0 )