Theorem numlti

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

	Ref	Expression
Hypotheses	numlti.1	⊢ 𝑇 ∈ ℕ
	numlti.2	⊢ 𝐴 ∈ ℕ
	numlti.3	⊢ 𝐵 ∈ ℕ0
	numlti.4	⊢ 𝐶 ∈ ℕ0
	numlti.5	⊢ 𝐶 < 𝑇
Assertion	numlti	⊢ 𝐶 < ( ( 𝑇 · 𝐴 ) + 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		numlti.1	⊢ 𝑇 ∈ ℕ
2		numlti.2	⊢ 𝐴 ∈ ℕ
3		numlti.3	⊢ 𝐵 ∈ ℕ0
4		numlti.4	⊢ 𝐶 ∈ ℕ0
5		numlti.5	⊢ 𝐶 < 𝑇
6	1	nnnn0i	⊢ 𝑇 ∈ ℕ0
7	6 4	num0h	⊢ 𝐶 = ( ( 𝑇 · 0 ) + 𝐶 )
8		0nn0	⊢ 0 ∈ ℕ0
9	2	nnnn0i	⊢ 𝐴 ∈ ℕ0
10	2	nngt0i	⊢ 0 < 𝐴
11	1 8 9 4 3 5 10	numltc	⊢ ( ( 𝑇 · 0 ) + 𝐶 ) < ( ( 𝑇 · 𝐴 ) + 𝐵 )
12	7 11	eqbrtri	⊢ 𝐶 < ( ( 𝑇 · 𝐴 ) + 𝐵 )