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

Metamath Proof Explorer

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