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 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
	3declth.1	|- C <_ 9
	3declth.2	|- E <_ 9
Assertion	3declth	|- ; ; 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		3declth.1	|- C <_ 9
9		3declth.2	|- E <_ 9
10	1 3	deccl	|- ; A C e. NN0
11	2 4	deccl	|- ; B D e. NN0
12	1 2 3 4 8 7	declth	|- ; A C < ; B D
13	10 11 5 6 9 12	declth	|- ; ; A C E < ; ; B D F