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 ℕ_{0}$
	decle.2	$⊢ B \in ℕ_{0}$
	decle.3	$⊢ C \in ℕ_{0}$
	decleh.4	$⊢ D \in ℕ_{0}$
	decleh.5	$⊢ C \leq 9$
	decleh.6	$⊢ A < B$
Assertion	decleh	Could not format assertion : No typesetting found for \|- ; A C <_ ; B D with typecode \|-

Step	Hyp	Ref	Expression
1		decle.1	$⊢ A \in ℕ_{0}$
2		decle.2	$⊢ B \in ℕ_{0}$
3		decle.3	$⊢ C \in ℕ_{0}$
4		decleh.4	$⊢ D \in ℕ_{0}$
5		decleh.5	$⊢ C \leq 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 \|-

Metamath Proof Explorer