Metamath Proof Explorer


Theorem 3declth

Description: Comparing two decimal integers with three "digits" (unequal higher places). (Contributed by AV, 8-Sep-2021)

Ref Expression
Hypotheses 3decltc.a A 0
3decltc.b B 0
3decltc.c C 0
3decltc.d D 0
3decltc.e E 0
3decltc.f F 0
3decltc.3 A < B
3declth.1 C 9
3declth.2 E 9
Assertion 3declth Could not format assertion : No typesetting found for |- ; ; A C E < ; ; B D F with typecode |-

Proof

Step Hyp Ref Expression
1 3decltc.a A 0
2 3decltc.b B 0
3 3decltc.c C 0
4 3decltc.d D 0
5 3decltc.e E 0
6 3decltc.f F 0
7 3decltc.3 A < B
8 3declth.1 C 9
9 3declth.2 E 9
10 1 3 deccl Could not format ; A C e. NN0 : No typesetting found for |- ; A C e. NN0 with typecode |-
11 2 4 deccl Could not format ; B D e. NN0 : No typesetting found for |- ; B D e. NN0 with typecode |-
12 1 2 3 4 8 7 declth Could not format ; A C < ; B D : No typesetting found for |- ; A C < ; B D with typecode |-
13 10 11 5 6 9 12 declth Could not format ; ; A C E < ; ; B D F : No typesetting found for |- ; ; A C E < ; ; B D F with typecode |-