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