Theorem numlt

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

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

Proof

Step	Hyp	Ref	Expression
1		numlt.1	⊢ 𝑇 ∈ ℕ
2		numlt.2	⊢ 𝐴 ∈ ℕ0
3		numlt.3	⊢ 𝐵 ∈ ℕ0
4		numlt.4	⊢ 𝐶 ∈ ℕ
5		numlt.5	⊢ 𝐵 < 𝐶
6	3	nn0rei	⊢ 𝐵 ∈ ℝ
7	4	nnrei	⊢ 𝐶 ∈ ℝ
8	1	nnnn0i	⊢ 𝑇 ∈ ℕ0
9	8 2	nn0mulcli	⊢ ( 𝑇 · 𝐴 ) ∈ ℕ0
10	9	nn0rei	⊢ ( 𝑇 · 𝐴 ) ∈ ℝ
11	6 7 10	ltadd2i	⊢ ( 𝐵 < 𝐶 ↔ ( ( 𝑇 · 𝐴 ) + 𝐵 ) < ( ( 𝑇 · 𝐴 ) + 𝐶 ) )
12	5 11	mpbi	⊢ ( ( 𝑇 · 𝐴 ) + 𝐵 ) < ( ( 𝑇 · 𝐴 ) + 𝐶 )