Theorem 0nn0m1nnn0

Description: A number is zero if and only if it's a nonnegative integer that becomes negative after subtracting 1. (Contributed by BTernaryTau, 30-Sep-2023)

	Ref	Expression
Assertion	0nn0m1nnn0	$$⊢N=0\leftrightarrow \left(N\in {\mathbb{N}}_0\wedge \neg N-1\in {\mathbb{N}}_0\right)$$

Proof

Step	Hyp	Ref	Expression
1		0nn0	$$⊢0\in {\mathbb{N}}_0$$
2		eleq1	$$⊢N=0\to \left(N\in {\mathbb{N}}_0\leftrightarrow 0\in {\mathbb{N}}_0\right)$$
3	1 2	mpbiri	$$⊢N=0\to N\in {\mathbb{N}}_0$$
4		1nn	$$⊢1\in \mathbb{N}$$
5		0mnnnnn0	$$⊢1\in \mathbb{N}\to \left(0-1\right)\notin {\mathbb{N}}_0$$
6	4 5	ax-mp	$$⊢\left(0-1\right)\notin {\mathbb{N}}_0$$
7		oveq1	$$⊢N=0\to N-1=0-1$$
8		neleq1	$$⊢N-1=0-1\to \left(\left(N-1\right)\notin {\mathbb{N}}_0\leftrightarrow \left(0-1\right)\notin {\mathbb{N}}_0\right)$$
9	7 8	syl	$$⊢N=0\to \left(\left(N-1\right)\notin {\mathbb{N}}_0\leftrightarrow \left(0-1\right)\notin {\mathbb{N}}_0\right)$$
10	6 9	mpbiri	$$⊢N=0\to \left(N-1\right)\notin {\mathbb{N}}_0$$
11		df-nel	$$⊢\left(N-1\right)\notin {\mathbb{N}}_0\leftrightarrow \neg N-1\in {\mathbb{N}}_0$$
12	10 11	sylib	$$⊢N=0\to \neg N-1\in {\mathbb{N}}_0$$
13	3 12	jca	$$⊢N=0\to \left(N\in {\mathbb{N}}_0\wedge \neg N-1\in {\mathbb{N}}_0\right)$$
14		nn0z	$$⊢N\in {\mathbb{N}}_0\to N\in \mathbb{Z}$$
15		peano2zm	$$⊢N\in \mathbb{Z}\to N-1\in \mathbb{Z}$$
16	14 15	syl	$$⊢N\in {\mathbb{N}}_0\to N-1\in \mathbb{Z}$$
17		elnn0z	$$⊢N-1\in {\mathbb{N}}_0\leftrightarrow \left(N-1\in \mathbb{Z}\wedge 0\le N-1\right)$$
18	17	notbii	$$⊢\neg N-1\in {\mathbb{N}}_0\leftrightarrow \neg \left(N-1\in \mathbb{Z}\wedge 0\le N-1\right)$$
19	18	biimpi	$$⊢\neg N-1\in {\mathbb{N}}_0\to \neg \left(N-1\in \mathbb{Z}\wedge 0\le N-1\right)$$
20		annotanannot	$$⊢\left(N-1\in \mathbb{Z}\wedge \neg \left(N-1\in \mathbb{Z}\wedge 0\le N-1\right)\right)\leftrightarrow \left(N-1\in \mathbb{Z}\wedge \neg 0\le N-1\right)$$
21	20	simprbi	$$⊢\left(N-1\in \mathbb{Z}\wedge \neg \left(N-1\in \mathbb{Z}\wedge 0\le N-1\right)\right)\to \neg 0\le N-1$$
22	16 19 21	syl2an	$$⊢\left(N\in {\mathbb{N}}_0\wedge \neg N-1\in {\mathbb{N}}_0\right)\to \neg 0\le N-1$$
23		zre	$$⊢N-1\in \mathbb{Z}\to N-1\in ℝ$$
24	14 15 23	3syl	$$⊢N\in {\mathbb{N}}_0\to N-1\in ℝ$$
25		0red	$$⊢N\in {\mathbb{N}}_0\to 0\in ℝ$$
26	24 25	ltnled	$$⊢N\in {\mathbb{N}}_0\to \left(N-1<0\leftrightarrow \neg 0\le N-1\right)$$
27	26	biimprd	$$⊢N\in {\mathbb{N}}_0\to \left(\neg 0\le N-1\to N-1<0\right)$$
28	27	adantr	$$⊢\left(N\in {\mathbb{N}}_0\wedge \neg N-1\in {\mathbb{N}}_0\right)\to \left(\neg 0\le N-1\to N-1<0\right)$$
29	22 28	mpd	$$⊢\left(N\in {\mathbb{N}}_0\wedge \neg N-1\in {\mathbb{N}}_0\right)\to N-1<0$$
30		0z	$$⊢0\in \mathbb{Z}$$
31		zlem1lt	$$⊢\left(N\in \mathbb{Z}\wedge 0\in \mathbb{Z}\right)\to \left(N\le 0\leftrightarrow N-1<0\right)$$
32	14 30 31	sylancl	$$⊢N\in {\mathbb{N}}_0\to \left(N\le 0\leftrightarrow N-1<0\right)$$
33	32	biimprd	$$⊢N\in {\mathbb{N}}_0\to \left(N-1<0\to N\le 0\right)$$
34	33	adantr	$$⊢\left(N\in {\mathbb{N}}_0\wedge \neg N-1\in {\mathbb{N}}_0\right)\to \left(N-1<0\to N\le 0\right)$$
35	29 34	mpd	$$⊢\left(N\in {\mathbb{N}}_0\wedge \neg N-1\in {\mathbb{N}}_0\right)\to N\le 0$$
36		nn0ge0	$$⊢N\in {\mathbb{N}}_0\to 0\le N$$
37	36	adantr	$$⊢\left(N\in {\mathbb{N}}_0\wedge \neg N-1\in {\mathbb{N}}_0\right)\to 0\le N$$
38		nn0re	$$⊢N\in {\mathbb{N}}_0\to N\in ℝ$$
39	38 25	letri3d	$$⊢N\in {\mathbb{N}}_0\to \left(N=0\leftrightarrow \left(N\le 0\wedge 0\le N\right)\right)$$
40	39	biimprd	$$⊢N\in {\mathbb{N}}_0\to \left(\left(N\le 0\wedge 0\le N\right)\to N=0\right)$$
41	40	adantr	$$⊢\left(N\in {\mathbb{N}}_0\wedge \neg N-1\in {\mathbb{N}}_0\right)\to \left(\left(N\le 0\wedge 0\le N\right)\to N=0\right)$$
42	35 37 41	mp2and	$$⊢\left(N\in {\mathbb{N}}_0\wedge \neg N-1\in {\mathbb{N}}_0\right)\to N=0$$
43	13 42	impbii	$$⊢N=0\leftrightarrow \left(N\in {\mathbb{N}}_0\wedge \neg N-1\in {\mathbb{N}}_0\right)$$