declei

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

	Ref	Expression
Hypotheses	declei.1	$⊢ A \in ℕ$
	declei.2	$⊢ B \in ℕ_{0}$
	declei.3	$⊢ C \in ℕ_{0}$
	declei.4	$⊢ C \leq 9$
Assertion	declei	Could not format assertion : No typesetting found for \|- C <_ ; A B with typecode \|-

Step	Hyp	Ref	Expression
1		declei.1	$⊢ A \in ℕ$
2		declei.2	$⊢ B \in ℕ_{0}$
3		declei.3	$⊢ C \in ℕ_{0}$
4		declei.4	$⊢ C \leq 9$
5	3	dec0h	Could not format C = ; 0 C : No typesetting found for \|- C = ; 0 C with typecode \|-
6		0nn0	$⊢ 0 \in ℕ_{0}$
7	1	nnnn0i	$⊢ A \in ℕ_{0}$
8	1	nngt0i	$⊢ 0 < A$
9	6 7 3 2 4 8	decleh	Could not format ; 0 C <_ ; A B : No typesetting found for \|- ; 0 C <_ ; A B with typecode \|-
10	5 9	eqbrtri	Could not format C <_ ; A B : No typesetting found for \|- C <_ ; A B with typecode \|-

Metamath Proof Explorer