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	⊢ 𝐶 < ; 𝐴 𝐵