Theorem elnn0z 12599

Description: Nonnegative integer property expressed in terms of integers. (Contributed by NM, 9-May-2004.)

Assertion

Ref	Expression
elnn0z	⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℤ ∧ 0 ≤ 𝑁))

Proof of Theorem elnn0z

Step	Hyp	Ref	Expression
1		elnn0 12501	. 2 ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0))
2		elnnz 12596	. . 3 ⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 0 < 𝑁))
3		eqcom 2770	. . 3 ⊢ (𝑁 = 0 ↔ 0 = 𝑁)
4	2, 3	orbi12i 927	. 2 ⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) ↔ ((𝑁 ∈ ℤ ∧ 0 < 𝑁) ∨ 0 = 𝑁))
5		id 23	. . . . . 6 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℤ)
6		0z 12597	. . . . . . 7 ⊢ 0 ∈ ℤ
7		eleq1 2851	. . . . . . 7 ⊢ (0 = 𝑁 → (0 ∈ ℤ ↔ 𝑁 ∈ ℤ))
8	6, 7	mpbii 236	. . . . . 6 ⊢ (0 = 𝑁 → 𝑁 ∈ ℤ)
9	5, 8	jaoi 870	. . . . 5 ⊢ ((𝑁 ∈ ℤ ∨ 0 = 𝑁) → 𝑁 ∈ ℤ)
10		orc 880	. . . . 5 ⊢ (𝑁 ∈ ℤ → (𝑁 ∈ ℤ ∨ 0 = 𝑁))
11	9, 10	impbii 212	. . . 4 ⊢ ((𝑁 ∈ ℤ ∨ 0 = 𝑁) ↔ 𝑁 ∈ ℤ)
12	11	anbi1i 635	. . 3 ⊢ (((𝑁 ∈ ℤ ∨ 0 = 𝑁) ∧ (0 < 𝑁 ∨ 0 = 𝑁)) ↔ (𝑁 ∈ ℤ ∧ (0 < 𝑁 ∨ 0 = 𝑁)))
13		ordir 1024	. . 3 ⊢ (((𝑁 ∈ ℤ ∧ 0 < 𝑁) ∨ 0 = 𝑁) ↔ ((𝑁 ∈ ℤ ∨ 0 = 𝑁) ∧ (0 < 𝑁 ∨ 0 = 𝑁)))
14		0re 11205	. . . . 5 ⊢ 0 ∈ ℝ
15		zre 12590	. . . . 5 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
16		leloe 11291	. . . . 5 ⊢ ((0 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁)))
17	14, 15, 16	sylancr 598	. . . 4 ⊢ (𝑁 ∈ ℤ → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁)))
18	17	pm5.32i 584	. . 3 ⊢ ((𝑁 ∈ ℤ ∧ 0 ≤ 𝑁) ↔ (𝑁 ∈ ℤ ∧ (0 < 𝑁 ∨ 0 = 𝑁)))
19	12, 13, 18	3bitr4i 306	. 2 ⊢ (((𝑁 ∈ ℤ ∧ 0 < 𝑁) ∨ 0 = 𝑁) ↔ (𝑁 ∈ ℤ ∧ 0 ≤ 𝑁))
20	1, 4, 19	3bitri 300	1 ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℤ ∧ 0 ≤ 𝑁))

Syntax hints:   ↔ wb 209   ∧ wa 400   ∨ wo 860   = wceq 1570   ∈ wcel 2143   class class class wbr 5109  ℝcr 11094  0cc0 11095   < clt 11238   ≤ cle 11239  ℕcn 12228  ℕ₀cn0 12499  ℤcz 12586

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-mulcom 11159  ax-addass 11160  ax-mulass 11161  ax-distr 11162  ax-i2m1 11163  ax-1ne0 11164  ax-1rid 11165  ax-rnegex 11166  ax-rrecex 11167  ax-cnre 11168  ax-pre-lttri 11169  ax-pre-lttrn 11170  ax-pre-ltadd 11171  ax-pre-mulgt0 11172

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7859  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11240  df-mnf 11241  df-xr 11242  df-ltxr 11243  df-le 11244  df-sub 11438  df-neg 11439  df-nn 12229  df-n0 12500  df-z 12587

This theorem is referenced by:  zle0orge1  12603  nn0zrab  12618  znn0sub  12636  nn0ind  12686  fnn0ind  12690  fznn0  13643  elfz0ubfz0  13656  elfz0fzfz0  13657  fz0fzelfz0  13658  elfzmlbp  13663  difelfzle  13665  difelfznle  13666  elfzo0z  13726  fzofzim  13734  ubmelm1fzo  13788  flge0nn0  13849  zmodcl  13920  modmuladdnn0  13947  modsumfzodifsn  13976  zsqcl2  14170  swrdnnn0nd  14690  swrdswrdlem  14737  swrdswrd  14738  swrdccatin2  14762  pfxccatin12lem2  14764  pfxccatin12lem3  14765  repswswrd  14817  cshwidxmod  14836  nn0abscl  15359  iseralt  15732  binomrisefac  16091  oexpneg  16398  oddnn02np1  16401  evennn02n  16403  nn0ehalf  16431  nn0oddm1d2  16438  divalglem2  16448  divalglem8  16453  divalglem10  16455  divalgb  16457  bitsinv1lem  16494  dfgcd2  16599  algcvga  16632  hashgcdlem  16842  iserodd  16890  pockthlem  16960  4sqlem14  17013  cshwshashlem2  17151  chfacfscmul0  23015  chfacfpmmul0  23019  taylfvallem1  26520  tayl0  26525  basellem3  27247  bcmono  27441  gausslemma2dlem0h  27527  2sqnn0  27602  crctcshwlkn0lem7  30165  crctcshwlkn0  30170  clwlkclwwlklem2a1  30343  clwlkclwwlklem2fv2  30347  clwlkclwwlklem2a  30349  wwlksubclwwlk  30409  0nn0m1nnn0  35604  knoppndvlem2  37102  aks4d1p1p2  42837  aks4d1p1p4  42838  aks4d1p3  42845  aks4d1p7  42850  aks4d1p8  42854  aks4d1p9  42855  aks6d1c1  42883  hashscontpow1  42888  aks6d1c2lem4  42894  aks6d1c2  42897  aks6d1c5lem3  42904  aks6d1c5lem2  42905  sticksstones10  42922  sticksstones12a  42924  aks6d1c6lem3  42939  aks6d1c6lem4  42940  bcled  42945  bcle2d  42946  aks6d1c7lem1  42947  aks6d1c7lem2  42948  unitscyglem5  42966  irrapxlem1  43549  rmynn0  43684  rmyabs  43685  jm2.22  43722  jm2.23  43723  jm2.27a  43732  jm2.27c  43734  dvnprodlem1  46660  wallispilem4  46782  stirlinglem5  46792  elaa2lem  46947  etransclem3  46951  etransclem7  46955  etransclem10  46958  etransclem19  46967  etransclem20  46968  etransclem21  46969  etransclem22  46970  etransclem24  46972  etransclem27  46975  ormkglobd  47591  zm1nn  48039  eluzge0nn0  48049  elfz2z  48052  2elfz2melfz  48055  subsubelfzo0  48064  oexpnegALTV  48442  nn0oALTV  48461  nn0e  48462  gpgusgralem  48821  nn0eo  49308  dig1  49388