Theorem 3declth

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

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

Proof

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