Theorem numlt

Description: Comparing two decimal integers (equal higher places). (Contributed by Mario Carneiro, 18-Feb-2014)

	Ref	Expression
Hypotheses	numlt.1	|- T e. NN
	numlt.2	|- A e. NN0
	numlt.3	|- B e. NN0
	numlt.4	|- C e. NN
	numlt.5	|- B < C
Assertion	numlt	|- ( ( T x. A ) + B ) < ( ( T x. A ) + C )

Proof

Step	Hyp	Ref	Expression
1		numlt.1	|- T e. NN
2		numlt.2	|- A e. NN0
3		numlt.3	|- B e. NN0
4		numlt.4	|- C e. NN
5		numlt.5	|- B < C
6	3	nn0rei	|- B e. RR
7	4	nnrei	|- C e. RR
8	1	nnnn0i	|- T e. NN0
9	8 2	nn0mulcli	|- ( T x. A ) e. NN0
10	9	nn0rei	|- ( T x. A ) e. RR
11	6 7 10	ltadd2i	|- ( B < C <-> ( ( T x. A ) + B ) < ( ( T x. A ) + C ) )
12	5 11	mpbi	|- ( ( T x. A ) + B ) < ( ( T x. A ) + C )