Theorem numlti

Description: Comparing a digit to a decimal integer. (Contributed by Mario Carneiro, 18-Feb-2014)

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

Proof

Step	Hyp	Ref	Expression
1		numlti.1	|- T e. NN
2		numlti.2	|- A e. NN
3		numlti.3	|- B e. NN0
4		numlti.4	|- C e. NN0
5		numlti.5	|- C < T
6	1	nnnn0i	|- T e. NN0
7	6 4	num0h	|- C = ( ( T x. 0 ) + C )
8		0nn0	|- 0 e. NN0
9	2	nnnn0i	|- A e. NN0
10	2	nngt0i	|- 0 < A
11	1 8 9 4 3 5 10	numltc	|- ( ( T x. 0 ) + C ) < ( ( T x. A ) + B )
12	7 11	eqbrtri	|- C < ( ( T x. A ) + B )