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

Metamath Proof Explorer

Theorem declti

Description: Comparing a digit to a decimal integer. (Contributed by Mario Carneiro, 18-Feb-2014) (Revised by AV, 6-Sep-2021)

	Ref	Expression
Hypotheses	declti.a	$⊢ A \in ℕ$
	declti.b	$⊢ B \in ℕ_{0}$
	declti.c	$⊢ C \in ℕ_{0}$
	declti.l	$⊢ C < 10$
Assertion	declti	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		declti.l	$⊢ C < 10$
5		10nn	$⊢ 10 \in ℕ$
6	5 1 2 3 4	numlti	$⊢ C < 10 A + B$
7		dfdec10	Could not format ; A B = ( ( ; 1 0 x. A ) + B ) : No typesetting found for \|- ; A B = ( ( ; 1 0 x. A ) + B ) with typecode \|-
8	6 7	breqtrri	Could not format C < ; A B : No typesetting found for \|- C < ; A B with typecode \|-