Theorem declth

Description: Comparing two decimal integers (unequal higher places). (Contributed by AV, 8-Sep-2021)

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

Proof

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