Theorem decltdi

Description: Comparing a digit to a decimal integer. (Contributed by AV, 8-Sep-2021)

	Ref	Expression
Hypotheses	declti.a	⊢ 𝐴 ∈ ℕ
	declti.b	⊢ 𝐵 ∈ ℕ0
	declti.c	⊢ 𝐶 ∈ ℕ0
	decltdi.4	⊢ 𝐶 ≤ 9
Assertion	decltdi	⊢ 𝐶 < ; 𝐴 𝐵

Proof

Step	Hyp	Ref	Expression
1		declti.a	⊢ 𝐴 ∈ ℕ
2		declti.b	⊢ 𝐵 ∈ ℕ0
3		declti.c	⊢ 𝐶 ∈ ℕ0
4		decltdi.4	⊢ 𝐶 ≤ 9
5	3 4	le9lt10	⊢ 𝐶 < ; 1 0
6	1 2 3 5	declti	⊢ 𝐶 < ; 𝐴 𝐵