Theorem le9lt10

Description: A "decimal digit" (i.e. a nonnegative integer less than or equal to 9) is less than 10. (Contributed by AV, 8-Sep-2021)

	Ref	Expression
Hypotheses	le9lt10.c	$$⊢A\in {\mathbb{N}}_0$$
	le9lt10.e	$$⊢A\le 9$$
Assertion	le9lt10	$$⊢A<10$$

Proof

Step	Hyp	Ref	Expression
1		le9lt10.c	$$⊢A\in {\mathbb{N}}_0$$
2		le9lt10.e	$$⊢A\le 9$$
3	1	nn0zi	$$⊢A\in \mathbb{Z}$$
4		9nn0	$$⊢9\in {\mathbb{N}}_0$$
5	4	nn0zi	$$⊢9\in \mathbb{Z}$$
6		zleltp1	$$⊢\left(A\in \mathbb{Z}\wedge 9\in \mathbb{Z}\right)\to \left(A\le 9\leftrightarrow A<9+1\right)$$
7	3 5 6	mp2an	$$⊢A\le 9\leftrightarrow A<9+1$$
8	2 7	mpbi	$$⊢A<9+1$$
9		9p1e10	$$⊢9+1=10$$
10	8 9	breqtri	$$⊢A<10$$