This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 mulridi ⊢ ( 𝑇 · 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 ⊢ ( ( 𝑇 · 𝐴 ) + 𝐶 ) < ( ( 𝑇 · 𝐵 ) + 𝐷 )