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

Metamath Proof Explorer

Theorem declti

Description: Comparing a digit to a decimal integer. (Contributed by Mario Carneiro, 18-Feb-2014) (Revised by AV, 6-Sep-2021)

Ref Expression
Hypotheses declti.a ⊢ 𝐴 ∈ ℕ
declti.b ⊢ 𝐵 ∈ ℕ0
declti.c ⊢ 𝐶 ∈ ℕ0
declti.l ⊢ 𝐶 < 1 0
Assertion declti 𝐶 < 𝐴 𝐵

Proof

Step Hyp Ref Expression
1 declti.a ⊢ 𝐴 ∈ ℕ
2 declti.b ⊢ 𝐵 ∈ ℕ0
3 declti.c ⊢ 𝐶 ∈ ℕ0
4 declti.l ⊢ 𝐶 < 1 0
5 10nn ⊢ 1 0 ∈ ℕ
6 5 1 2 3 4 numlti ⊢ 𝐶 < ( ( 1 0 · 𝐴 ) + 𝐵 )
7 dfdec10 ⊢ 𝐴 𝐵 = ( ( 1 0 · 𝐴 ) + 𝐵 )
8 6 7 breqtrri ⊢ 𝐶 < 𝐴 𝐵