Theorem numlti

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

	Ref	Expression
Hypotheses	numlti.1	$$⊢T\in \mathbb{N}$$
	numlti.2	$$⊢A\in \mathbb{N}$$
	numlti.3	$$⊢B\in {\mathbb{N}}_0$$
	numlti.4	$$⊢C\in {\mathbb{N}}_0$$
	numlti.5	$$⊢C<T$$
Assertion	numlti	$$⊢C<TA+B$$

Proof

Step	Hyp	Ref	Expression
1		numlti.1	$$⊢T\in \mathbb{N}$$
2		numlti.2	$$⊢A\in \mathbb{N}$$
3		numlti.3	$$⊢B\in {\mathbb{N}}_0$$
4		numlti.4	$$⊢C\in {\mathbb{N}}_0$$
5		numlti.5	$$⊢C<T$$
6	1	nnnn0i	$$⊢T\in {\mathbb{N}}_0$$
7	6 4	num0h	$$⊢C=T\cdot 0+C$$
8		0nn0	$$⊢0\in {\mathbb{N}}_0$$
9	2	nnnn0i	$$⊢A\in {\mathbb{N}}_0$$
10	2	nngt0i	$$⊢0<A$$
11	1 8 9 4 3 5 10	numltc	$$⊢T\cdot 0+C<TA+B$$
12	7 11	eqbrtri	$$⊢C<TA+B$$