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 e. NN0
	declt.b	|- B e. NN0
	decltc.c	|- C e. NN0
	decltc.d	|- D e. NN0
	decltc.s	|- C < ; 1 0
	decltc.l	|- A < B
Assertion	decltc	|- ; A C < ; B D

Proof

Step	Hyp	Ref	Expression
1		declt.a	|- A e. NN0
2		declt.b	|- B e. NN0
3		decltc.c	|- C e. NN0
4		decltc.d	|- D e. NN0
5		decltc.s	|- C < ; 1 0
6		decltc.l	|- A < B
7		10nn	|- ; 1 0 e. NN
8	7 1 2 3 4 5 6	numltc	|- ( ( ; 1 0 x. A ) + C ) < ( ( ; 1 0 x. B ) + D )
9		dfdec10	|- ; A C = ( ( ; 1 0 x. A ) + C )
10		dfdec10	|- ; B D = ( ( ; 1 0 x. B ) + D )
11	8 9 10	3brtr4i	|- ; A C < ; B D