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