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	mulridi	⊢ ( 𝑇 · 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 )