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

Metamath Proof Explorer

Theorem numlt

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

Ref Expression
Hypotheses numlt.1 ⊢ T ∈ ℕ
numlt.2 ⊢ A ∈ ℕ 0
numlt.3 ⊢ B ∈ ℕ 0
numlt.4 ⊢ C ∈ ℕ
numlt.5 ⊢ B < C
Assertion numlt ⊢ T ⁢ A + B < T ⁢ A + C

Proof

Step Hyp Ref Expression
1 numlt.1 ⊢ T ∈ ℕ
2 numlt.2 ⊢ A ∈ ℕ 0
3 numlt.3 ⊢ B ∈ ℕ 0
4 numlt.4 ⊢ C ∈ ℕ
5 numlt.5 ⊢ B < C
6 3 nn0rei ⊢ B ∈ ℝ
7 4 nnrei ⊢ C ∈ ℝ
8 1 nnnn0i ⊢ T ∈ ℕ 0
9 8 2 nn0mulcli ⊢ T ⁢ A ∈ ℕ 0
10 9 nn0rei ⊢ T ⁢ A ∈ ℝ
11 6 7 10 ltadd2i ⊢ B < C ↔ T ⁢ A + B < T ⁢ A + C
12 5 11 mpbi ⊢ T ⁢ A + B < T ⁢ A + C