Theorem decleh

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

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

Proof

Step	Hyp	Ref	Expression
1		decle.1	$$⊢A\in {\mathbb{N}}_0$$
2		decle.2	$$⊢B\in {\mathbb{N}}_0$$
3		decle.3	$$⊢C\in {\mathbb{N}}_0$$
4		decleh.4	$$⊢D\in {\mathbb{N}}_0$$
5		decleh.5	$$⊢C\le 9$$
6		decleh.6	$$⊢A<B$$
7	1 3	deccl	Could not format ; A C e. NN0 : No typesetting found for |- ; A C e. NN0 with typecode |-
8	7	nn0rei	Could not format ; A C e. RR : No typesetting found for |- ; A C e. RR with typecode |-
9	2 4	deccl	Could not format ; B D e. NN0 : No typesetting found for |- ; B D e. NN0 with typecode |-
10	9	nn0rei	Could not format ; B D e. RR : No typesetting found for |- ; B D e. RR with typecode |-
11	1 2 3 4 5 6	declth	Could not format ; A C < ; B D : No typesetting found for |- ; A C < ; B D with typecode |-
12	8 10 11	ltleii	Could not format ; A C <_ ; B D : No typesetting found for |- ; A C <_ ; B D with typecode |-