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

Metamath Proof Explorer

Theorem decltc

Description: Comparing two decimal integers (unequal higher places). (Contributed by Mario Carneiro, 18-Feb-2014) (Revised by AV, 6-Sep-2021)

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

Proof

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