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

Metamath Proof Explorer

Theorem declt

Description: Comparing two decimal integers (equal higher places). (Contributed by Mario Carneiro, 17-Apr-2015) (Revised by AV, 6-Sep-2021)

Ref Expression
Hypotheses declt.a ⊢ A ∈ ℕ 0
declt.b ⊢ B ∈ ℕ 0
declt.c ⊢ C ∈ ℕ
declt.l ⊢ B < C
Assertion declt Could not format assertion : No typesetting found for |- ; A B < ; A C with typecode |-

Proof

Step Hyp Ref Expression
1 declt.a ⊢ A ∈ ℕ 0
2 declt.b ⊢ B ∈ ℕ 0
3 declt.c ⊢ C ∈ ℕ
4 declt.l ⊢ B < C
5 10nn ⊢ 10 ∈ ℕ
6 5 1 2 3 4 numlt ⊢ 10 ⁢ A + B < 10 ⁢ A + C
7 dfdec10 Could not format ; A B = ( ( ; 1 0 x. A ) + B ) : No typesetting found for |- ; A B = ( ( ; 1 0 x. A ) + B ) with typecode |-
8 dfdec10 Could not format ; A C = ( ( ; 1 0 x. A ) + C ) : No typesetting found for |- ; A C = ( ( ; 1 0 x. A ) + C ) with typecode |-
9 6 7 8 3brtr4i Could not format ; A B < ; A C : No typesetting found for |- ; A B < ; A C with typecode |-