Theorem nn0lt10b

Description: A nonnegative integer less than 1 is 0 . (Contributed by Paul Chapman, 22-Jun-2011) (Proof shortened by OpenAI, 25-Mar-2020)

	Ref	Expression
Assertion	nn0lt10b	$$⊢N\in {\mathbb{N}}_0\to \left(N<1\leftrightarrow N=0\right)$$

Proof

Step	Hyp	Ref	Expression
1		elnn0	$$⊢N\in {\mathbb{N}}_0\leftrightarrow \left(N\in \mathbb{N}\vee N=0\right)$$
2		nnnlt1	$$⊢N\in \mathbb{N}\to \neg N<1$$
3	2	pm2.21d	$$⊢N\in \mathbb{N}\to \left(N<1\to N=0\right)$$
4		ax-1	$$⊢N=0\to \left(N<1\to N=0\right)$$
5	3 4	jaoi	$$⊢\left(N\in \mathbb{N}\vee N=0\right)\to \left(N<1\to N=0\right)$$
6	1 5	sylbi	$$⊢N\in {\mathbb{N}}_0\to \left(N<1\to N=0\right)$$
7		0lt1	$$⊢0<1$$
8		breq1	$$⊢N=0\to \left(N<1\leftrightarrow 0<1\right)$$
9	7 8	mpbiri	$$⊢N=0\to N<1$$
10	6 9	impbid1	$$⊢N\in {\mathbb{N}}_0\to \left(N<1\leftrightarrow N=0\right)$$