Theorem decltdi

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

	Ref	Expression
Hypotheses	declti.a	$$⊢A\in \mathbb{N}$$
	declti.b	$$⊢B\in {\mathbb{N}}_0$$
	declti.c	$$⊢C\in {\mathbb{N}}_0$$
	decltdi.4	$$⊢C\le 9$$
Assertion	decltdi	Could not format assertion : No typesetting found for |- C < ; A B with typecode |-

Proof

Step	Hyp	Ref	Expression
1		declti.a	$$⊢A\in \mathbb{N}$$
2		declti.b	$$⊢B\in {\mathbb{N}}_0$$
3		declti.c	$$⊢C\in {\mathbb{N}}_0$$
4		decltdi.4	$$⊢C\le 9$$
5	3 4	le9lt10	$$⊢C<10$$
6	1 2 3 5	declti	Could not format C < ; A B : No typesetting found for |- C < ; A B with typecode |-