Theorem decleh

Description: Comparing two decimal integers (unequal higher places). (Contributed by AV, 17-Aug-2021) (Revised by AV, 8-Sep-2021)

	Ref	Expression
Hypotheses	decle.1	|- A e. NN0
	decle.2	|- B e. NN0
	decle.3	|- C e. NN0
	decleh.4	|- D e. NN0
	decleh.5	|- C <_ 9
	decleh.6	|- A < B
Assertion	decleh	|- ; A C <_ ; B D

Proof

Step	Hyp	Ref	Expression
1		decle.1	|- A e. NN0
2		decle.2	|- B e. NN0
3		decle.3	|- C e. NN0
4		decleh.4	|- D e. NN0
5		decleh.5	|- C <_ 9
6		decleh.6	|- A < B
7	1 3	deccl	|- ; A C e. NN0
8	7	nn0rei	|- ; A C e. RR
9	2 4	deccl	|- ; B D e. NN0
10	9	nn0rei	|- ; B D e. RR
11	1 2 3 4 5 6	declth	|- ; A C < ; B D
12	8 10 11	ltleii	|- ; A C <_ ; B D