Theorem declei

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

	Ref	Expression
Hypotheses	declei.1	⊢ 𝐴 ∈ ℕ
	declei.2	⊢ 𝐵 ∈ ℕ0
	declei.3	⊢ 𝐶 ∈ ℕ0
	declei.4	⊢ 𝐶 ≤ 9
Assertion	declei	⊢ 𝐶 ≤ ; 𝐴 𝐵

Proof

Step	Hyp	Ref	Expression
1		declei.1	⊢ 𝐴 ∈ ℕ
2		declei.2	⊢ 𝐵 ∈ ℕ0
3		declei.3	⊢ 𝐶 ∈ ℕ0
4		declei.4	⊢ 𝐶 ≤ 9
5	3	dec0h	⊢ 𝐶 = ; 0 𝐶
6		0nn0	⊢ 0 ∈ ℕ0
7	1	nnnn0i	⊢ 𝐴 ∈ ℕ0
8	1	nngt0i	⊢ 0 < 𝐴
9	6 7 3 2 4 8	decleh	⊢ ; 0 𝐶 ≤ ; 𝐴 𝐵
10	5 9	eqbrtri	⊢ 𝐶 ≤ ; 𝐴 𝐵