Theorem decsuc

Description: The successor of a decimal integer (no carry). (Contributed by Mario Carneiro, 17-Apr-2015) (Revised by AV, 6-Sep-2021)

	Ref	Expression
Hypotheses	declt.a	⊢ 𝐴 ∈ ℕ0
	declt.b	⊢ 𝐵 ∈ ℕ0
	decsuc.c	⊢ ( 𝐵 + 1 ) = 𝐶
	decsuc.n	⊢ 𝑁 = ; 𝐴 𝐵
Assertion	decsuc	⊢ ( 𝑁 + 1 ) = ; 𝐴 𝐶

Proof

Step	Hyp	Ref	Expression
1		declt.a	⊢ 𝐴 ∈ ℕ0
2		declt.b	⊢ 𝐵 ∈ ℕ0
3		decsuc.c	⊢ ( 𝐵 + 1 ) = 𝐶
4		decsuc.n	⊢ 𝑁 = ; 𝐴 𝐵
5		10nn0	⊢ ; 1 0 ∈ ℕ0
6		dfdec10	⊢ ; 𝐴 𝐵 = ( ( ; 1 0 · 𝐴 ) + 𝐵 )
7	4 6	eqtri	⊢ 𝑁 = ( ( ; 1 0 · 𝐴 ) + 𝐵 )
8	5 1 2 3 7	numsuc	⊢ ( 𝑁 + 1 ) = ( ( ; 1 0 · 𝐴 ) + 𝐶 )
9		dfdec10	⊢ ; 𝐴 𝐶 = ( ( ; 1 0 · 𝐴 ) + 𝐶 )
10	8 9	eqtr4i	⊢ ( 𝑁 + 1 ) = ; 𝐴 𝐶