This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem declth

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

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

Step	Hyp	Ref	Expression
1		declt.a	$⊢ A \in ℕ_{0}$
2		declt.b	$⊢ B \in ℕ_{0}$
3		declth.c	$⊢ C \in ℕ_{0}$
4		declth.d	$⊢ D \in ℕ_{0}$
5		declth.e	$⊢ C \leq 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 \|-