Theorem declei

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

	Ref	Expression
Hypotheses	declei.1	|- A e. NN
	declei.2	|- B e. NN0
	declei.3	|- C e. NN0
	declei.4	|- C <_ 9
Assertion	declei	|- C <_ ; A B

Proof

Step	Hyp	Ref	Expression
1		declei.1	|- A e. NN
2		declei.2	|- B e. NN0
3		declei.3	|- C e. NN0
4		declei.4	|- C <_ 9
5	3	dec0h	|- C = ; 0 C
6		0nn0	|- 0 e. NN0
7	1	nnnn0i	|- A e. NN0
8	1	nngt0i	|- 0 < A
9	6 7 3 2 4 8	decleh	|- ; 0 C <_ ; A B
10	5 9	eqbrtri	|- C <_ ; A B