Theorem numltc

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

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

Proof

Step	Hyp	Ref	Expression
1		numlt.1	⊢ 𝑇 ∈ ℕ
2		numlt.2	⊢ 𝐴 ∈ ℕ0
3		numlt.3	⊢ 𝐵 ∈ ℕ0
4		numltc.3	⊢ 𝐶 ∈ ℕ0
5		numltc.4	⊢ 𝐷 ∈ ℕ0
6		numltc.5	⊢ 𝐶 < 𝑇
7		numltc.6	⊢ 𝐴 < 𝐵
8	1 2 4 1 6	numlt	⊢ ( ( 𝑇 · 𝐴 ) + 𝐶 ) < ( ( 𝑇 · 𝐴 ) + 𝑇 )
9	1	nnrei	⊢ 𝑇 ∈ ℝ
10	9	recni	⊢ 𝑇 ∈ ℂ
11	2	nn0rei	⊢ 𝐴 ∈ ℝ
12	11	recni	⊢ 𝐴 ∈ ℂ
13		ax-1cn	⊢ 1 ∈ ℂ
14	10 12 13	adddii	⊢ ( 𝑇 · ( 𝐴 + 1 ) ) = ( ( 𝑇 · 𝐴 ) + ( 𝑇 · 1 ) )
15	10	mulid1i	⊢ ( 𝑇 · 1 ) = 𝑇
16	15	oveq2i	⊢ ( ( 𝑇 · 𝐴 ) + ( 𝑇 · 1 ) ) = ( ( 𝑇 · 𝐴 ) + 𝑇 )
17	14 16	eqtri	⊢ ( 𝑇 · ( 𝐴 + 1 ) ) = ( ( 𝑇 · 𝐴 ) + 𝑇 )
18	8 17	breqtrri	⊢ ( ( 𝑇 · 𝐴 ) + 𝐶 ) < ( 𝑇 · ( 𝐴 + 1 ) )
19		nn0ltp1le	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( 𝐴 < 𝐵 ↔ ( 𝐴 + 1 ) ≤ 𝐵 ) )
20	2 3 19	mp2an	⊢ ( 𝐴 < 𝐵 ↔ ( 𝐴 + 1 ) ≤ 𝐵 )
21	7 20	mpbi	⊢ ( 𝐴 + 1 ) ≤ 𝐵
22	1	nngt0i	⊢ 0 < 𝑇
23		peano2re	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 + 1 ) ∈ ℝ )
24	11 23	ax-mp	⊢ ( 𝐴 + 1 ) ∈ ℝ
25	3	nn0rei	⊢ 𝐵 ∈ ℝ
26	24 25 9	lemul2i	⊢ ( 0 < 𝑇 → ( ( 𝐴 + 1 ) ≤ 𝐵 ↔ ( 𝑇 · ( 𝐴 + 1 ) ) ≤ ( 𝑇 · 𝐵 ) ) )
27	22 26	ax-mp	⊢ ( ( 𝐴 + 1 ) ≤ 𝐵 ↔ ( 𝑇 · ( 𝐴 + 1 ) ) ≤ ( 𝑇 · 𝐵 ) )
28	21 27	mpbi	⊢ ( 𝑇 · ( 𝐴 + 1 ) ) ≤ ( 𝑇 · 𝐵 )
29	9 11	remulcli	⊢ ( 𝑇 · 𝐴 ) ∈ ℝ
30	4	nn0rei	⊢ 𝐶 ∈ ℝ
31	29 30	readdcli	⊢ ( ( 𝑇 · 𝐴 ) + 𝐶 ) ∈ ℝ
32	9 24	remulcli	⊢ ( 𝑇 · ( 𝐴 + 1 ) ) ∈ ℝ
33	9 25	remulcli	⊢ ( 𝑇 · 𝐵 ) ∈ ℝ
34	31 32 33	ltletri	⊢ ( ( ( ( 𝑇 · 𝐴 ) + 𝐶 ) < ( 𝑇 · ( 𝐴 + 1 ) ) ∧ ( 𝑇 · ( 𝐴 + 1 ) ) ≤ ( 𝑇 · 𝐵 ) ) → ( ( 𝑇 · 𝐴 ) + 𝐶 ) < ( 𝑇 · 𝐵 ) )
35	18 28 34	mp2an	⊢ ( ( 𝑇 · 𝐴 ) + 𝐶 ) < ( 𝑇 · 𝐵 )
36	33 5	nn0addge1i	⊢ ( 𝑇 · 𝐵 ) ≤ ( ( 𝑇 · 𝐵 ) + 𝐷 )
37	5	nn0rei	⊢ 𝐷 ∈ ℝ
38	33 37	readdcli	⊢ ( ( 𝑇 · 𝐵 ) + 𝐷 ) ∈ ℝ
39	31 33 38	ltletri	⊢ ( ( ( ( 𝑇 · 𝐴 ) + 𝐶 ) < ( 𝑇 · 𝐵 ) ∧ ( 𝑇 · 𝐵 ) ≤ ( ( 𝑇 · 𝐵 ) + 𝐷 ) ) → ( ( 𝑇 · 𝐴 ) + 𝐶 ) < ( ( 𝑇 · 𝐵 ) + 𝐷 ) )
40	35 36 39	mp2an	⊢ ( ( 𝑇 · 𝐴 ) + 𝐶 ) < ( ( 𝑇 · 𝐵 ) + 𝐷 )