Theorem decsucc

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

	Ref	Expression
Hypotheses	decsucc.1	⊢ 𝐴 ∈ ℕ0
	decsucc.2	⊢ ( 𝐴 + 1 ) = 𝐵
	decsucc.3	⊢ 𝑁 = ; 𝐴 9
Assertion	decsucc	⊢ ( 𝑁 + 1 ) = ; 𝐵 0

Proof

Step	Hyp	Ref	Expression
1		decsucc.1	⊢ 𝐴 ∈ ℕ0
2		decsucc.2	⊢ ( 𝐴 + 1 ) = 𝐵
3		decsucc.3	⊢ 𝑁 = ; 𝐴 9
4		9nn0	⊢ 9 ∈ ℕ0
5		9p1e10	⊢ ( 9 + 1 ) = ; 1 0
6	5	eqcomi	⊢ ; 1 0 = ( 9 + 1 )
7		dfdec10	⊢ ; 𝐴 9 = ( ( ; 1 0 · 𝐴 ) + 9 )
8	3 7	eqtri	⊢ 𝑁 = ( ( ; 1 0 · 𝐴 ) + 9 )
9	4 6 1 2 8	numsucc	⊢ ( 𝑁 + 1 ) = ( ( ; 1 0 · 𝐵 ) + 0 )
10		dfdec10	⊢ ; 𝐵 0 = ( ( ; 1 0 · 𝐵 ) + 0 )
11	9 10	eqtr4i	⊢ ( 𝑁 + 1 ) = ; 𝐵 0