Metamath Proof Explorer


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