Theorem 3decltc

Description: Comparing two decimal integers with three "digits" (unequal higher places). (Contributed by AV, 15-Jun-2021) (Revised by AV, 6-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$$
	3decltc.1	$$⊢C<10$$
	3decltc.2	$$⊢E<10$$
Assertion	3decltc	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		3decltc.1	$$⊢C<10$$
9		3decltc.2	$$⊢E<10$$
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	decltc	Could not format ; A C < ; B D : No typesetting found for |- ; A C < ; B D with typecode |-
13	10 11 5 6 9 12	decltc	Could not format ; ; A C E < ; ; B D F : No typesetting found for |- ; ; A C E < ; ; B D F with typecode |-