Theorem declei

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

	Ref	Expression
Hypotheses	declei.1	$$⊢A\in \mathbb{N}$$
	declei.2	$$⊢B\in {\mathbb{N}}_0$$
	declei.3	$$⊢C\in {\mathbb{N}}_0$$
	declei.4	$$⊢C\le 9$$
Assertion	declei	Could not format assertion : No typesetting found for |- C <_ ; A B with typecode |-

Proof

Step	Hyp	Ref	Expression
1		declei.1	$$⊢A\in \mathbb{N}$$
2		declei.2	$$⊢B\in {\mathbb{N}}_0$$
3		declei.3	$$⊢C\in {\mathbb{N}}_0$$
4		declei.4	$$⊢C\le 9$$
5	3	dec0h	Could not format C = ; 0 C : No typesetting found for |- C = ; 0 C with typecode |-
6		0nn0	$$⊢0\in {\mathbb{N}}_0$$
7	1	nnnn0i	$$⊢A\in {\mathbb{N}}_0$$
8	1	nngt0i	$$⊢0<A$$
9	6 7 3 2 4 8	decleh	Could not format ; 0 C <_ ; A B : No typesetting found for |- ; 0 C <_ ; A B with typecode |-
10	5 9	eqbrtri	Could not format C <_ ; A B : No typesetting found for |- C <_ ; A B with typecode |-