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

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 ⊢ A ∈ ℕ 0
decsucc.2 ⊢ A + 1 = B
decsucc.3 No typesetting found for |- N = ; A 9 with typecode |-
Assertion decsucc Could not format assertion : No typesetting found for |- ( N + 1 ) = ; B 0 with typecode |-

Proof

Step Hyp Ref Expression
1 decsucc.1 ⊢ A ∈ ℕ 0
2 decsucc.2 ⊢ A + 1 = B
3 decsucc.3 Could not format N = ; A 9 : No typesetting found for |- N = ; A 9 with typecode |-
4 9nn0 ⊢ 9 ∈ ℕ 0
5 9p1e10 ⊢ 9 + 1 = 10
6 5 eqcomi ⊢ 10 = 9 + 1
7 dfdec10 Could not format ; A 9 = ( ( ; 1 0 x. A ) + 9 ) : No typesetting found for |- ; A 9 = ( ( ; 1 0 x. A ) + 9 ) with typecode |-
8 3 7 eqtri ⊢ N = 10 ⁢ A + 9
9 4 6 1 2 8 numsucc ⊢ N + 1 = 10 ⁢ B + 0
10 dfdec10 Could not format ; B 0 = ( ( ; 1 0 x. B ) + 0 ) : No typesetting found for |- ; B 0 = ( ( ; 1 0 x. B ) + 0 ) with typecode |-
11 9 10 eqtr4i Could not format ( N + 1 ) = ; B 0 : No typesetting found for |- ( N + 1 ) = ; B 0 with typecode |-