Metamath Proof Explorer

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 ) = 𝐴 𝐶