This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ A ∈ ℕ 0
declt.b ⊢ B ∈ ℕ 0
decsuc.c ⊢ B + 1 = C
decsuc.n No typesetting found for |- N = ; A B with typecode |-
Assertion decsuc Could not format assertion : No typesetting found for |- ( N + 1 ) = ; A C with typecode |-

Proof

Step Hyp Ref Expression
1 declt.a ⊢ A ∈ ℕ 0
2 declt.b ⊢ B ∈ ℕ 0
3 decsuc.c ⊢ B + 1 = C
4 decsuc.n Could not format N = ; A B : No typesetting found for |- N = ; A B with typecode |-
5 10nn0 ⊢ 10 ∈ ℕ 0
6 dfdec10 Could not format ; A B = ( ( ; 1 0 x. A ) + B ) : No typesetting found for |- ; A B = ( ( ; 1 0 x. A ) + B ) with typecode |-
7 4 6 eqtri ⊢ N = 10 ⁢ A + B
8 5 1 2 3 7 numsuc ⊢ N + 1 = 10 ⁢ A + C
9 dfdec10 Could not format ; A C = ( ( ; 1 0 x. A ) + C ) : No typesetting found for |- ; A C = ( ( ; 1 0 x. A ) + C ) with typecode |-
10 8 9 eqtr4i Could not format ( N + 1 ) = ; A C : No typesetting found for |- ( N + 1 ) = ; A C with typecode |-