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

Metamath Proof Explorer

Theorem decltdi

Description: Comparing a digit to a decimal integer. (Contributed by AV, 8-Sep-2021)

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

Step	Hyp	Ref	Expression
1		declti.a	$⊢ A \in ℕ$
2		declti.b	$⊢ B \in ℕ_{0}$
3		declti.c	$⊢ C \in ℕ_{0}$
4		decltdi.4	$⊢ C \leq 9$
5	3 4	le9lt10	$⊢ C < 10$
6	1 2 3 5	declti	Could not format C < ; A B : No typesetting found for \|- C < ; A B with typecode \|-