Metamath Proof Explorer


Theorem 3decltc

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

Ref Expression
Hypotheses 3decltc.a
|- A e. NN0
3decltc.b
|- B e. NN0
3decltc.c
|- C e. NN0
3decltc.d
|- D e. NN0
3decltc.e
|- E e. NN0
3decltc.f
|- F e. NN0
3decltc.3
|- A < B
3decltc.1
|- C < ; 1 0
3decltc.2
|- E < ; 1 0
Assertion 3decltc
|- ; ; A C E < ; ; B D F

Proof

Step Hyp Ref Expression
1 3decltc.a
 |-  A e. NN0
2 3decltc.b
 |-  B e. NN0
3 3decltc.c
 |-  C e. NN0
4 3decltc.d
 |-  D e. NN0
5 3decltc.e
 |-  E e. NN0
6 3decltc.f
 |-  F e. NN0
7 3decltc.3
 |-  A < B
8 3decltc.1
 |-  C < ; 1 0
9 3decltc.2
 |-  E < ; 1 0
10 1 3 deccl
 |-  ; A C e. NN0
11 2 4 deccl
 |-  ; B D e. NN0
12 1 2 3 4 8 7 decltc
 |-  ; A C < ; B D
13 10 11 5 6 9 12 decltc
 |-  ; ; A C E < ; ; B D F