Theorem decle

Description: Comparing two decimal integers (equal 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
	decle.4	|- B <_ C
Assertion	decle	|- ; A B <_ ; A C

Proof

Step	Hyp	Ref	Expression
1		decle.1	|- A e. NN0
2		decle.2	|- B e. NN0
3		decle.3	|- C e. NN0
4		decle.4	|- B <_ C
5	2	nn0rei	|- B e. RR
6	3	nn0rei	|- C e. RR
7		10nn0	|- ; 1 0 e. NN0
8	7 1	nn0mulcli	|- ( ; 1 0 x. A ) e. NN0
9	8	nn0rei	|- ( ; 1 0 x. A ) e. RR
10	5 6 9	leadd2i	|- ( B <_ C <-> ( ( ; 1 0 x. A ) + B ) <_ ( ( ; 1 0 x. A ) + C ) )
11	4 10	mpbi	|- ( ( ; 1 0 x. A ) + B ) <_ ( ( ; 1 0 x. A ) + C )
12		dfdec10	|- ; A B = ( ( ; 1 0 x. A ) + B )
13		dfdec10	|- ; A C = ( ( ; 1 0 x. A ) + C )
14	11 12 13	3brtr4i	|- ; A B <_ ; A C