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	|- A e. NN
	declti.b	|- B e. NN0
	declti.c	|- C e. NN0
	declti.l	|- C < ; 1 0
Assertion	declti	|- C < ; A B

Proof

Step	Hyp	Ref	Expression
1		declti.a	|- A e. NN
2		declti.b	|- B e. NN0
3		declti.c	|- C e. NN0
4		declti.l	|- C < ; 1 0
5		10nn	|- ; 1 0 e. NN
6	5 1 2 3 4	numlti	|- C < ( ( ; 1 0 x. A ) + B )
7		dfdec10	|- ; A B = ( ( ; 1 0 x. A ) + B )
8	6 7	breqtrri	|- C < ; A B