MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elnn0z Structured version   Visualization version   GIF version

Theorem elnn0z 11983
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
StepHypRef Expression
1 elnn0 11888 . 2 (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0))
2 elnnz 11980 . . 3 (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 0 < 𝑁))
3 eqcom 2828 . . 3 (𝑁 = 0 ↔ 0 = 𝑁)
42, 3orbi12i 908 . 2 ((𝑁 ∈ ℕ ∨ 𝑁 = 0) ↔ ((𝑁 ∈ ℤ ∧ 0 < 𝑁) ∨ 0 = 𝑁))
5 id 22 . . . . . 6 (𝑁 ∈ ℤ → 𝑁 ∈ ℤ)
6 0z 11981 . . . . . . 7 0 ∈ ℤ
7 eleq1 2900 . . . . . . 7 (0 = 𝑁 → (0 ∈ ℤ ↔ 𝑁 ∈ ℤ))
86, 7mpbii 234 . . . . . 6 (0 = 𝑁𝑁 ∈ ℤ)
95, 8jaoi 851 . . . . 5 ((𝑁 ∈ ℤ ∨ 0 = 𝑁) → 𝑁 ∈ ℤ)
10 orc 861 . . . . 5 (𝑁 ∈ ℤ → (𝑁 ∈ ℤ ∨ 0 = 𝑁))
119, 10impbii 210 . . . 4 ((𝑁 ∈ ℤ ∨ 0 = 𝑁) ↔ 𝑁 ∈ ℤ)
1211anbi1i 623 . . 3 (((𝑁 ∈ ℤ ∨ 0 = 𝑁) ∧ (0 < 𝑁 ∨ 0 = 𝑁)) ↔ (𝑁 ∈ ℤ ∧ (0 < 𝑁 ∨ 0 = 𝑁)))
13 ordir 1000 . . 3 (((𝑁 ∈ ℤ ∧ 0 < 𝑁) ∨ 0 = 𝑁) ↔ ((𝑁 ∈ ℤ ∨ 0 = 𝑁) ∧ (0 < 𝑁 ∨ 0 = 𝑁)))
14 0re 10632 . . . . 5 0 ∈ ℝ
15 zre 11974 . . . . 5 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
16 leloe 10716 . . . . 5 ((0 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁)))
1714, 15, 16sylancr 587 . . . 4 (𝑁 ∈ ℤ → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁)))
1817pm5.32i 575 . . 3 ((𝑁 ∈ ℤ ∧ 0 ≤ 𝑁) ↔ (𝑁 ∈ ℤ ∧ (0 < 𝑁 ∨ 0 = 𝑁)))
1912, 13, 183bitr4i 304 . 2 (((𝑁 ∈ ℤ ∧ 0 < 𝑁) ∨ 0 = 𝑁) ↔ (𝑁 ∈ ℤ ∧ 0 ≤ 𝑁))
201, 4, 193bitri 298 1 (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℤ ∧ 0 ≤ 𝑁))
Colors of variables: wff setvar class
Syntax hints:  wb 207  wa 396  wo 841   = wceq 1528  wcel 2105   class class class wbr 5058  cr 10525  0cc0 10526   < clt 10664  cle 10665  cn 11627  0cn0 11886  cz 11970
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4833  df-iun 4914  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7569  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-er 8279  df-en 8499  df-dom 8500  df-sdom 8501  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-nn 11628  df-n0 11887  df-z 11971
This theorem is referenced by:  zle0orge1  11987  nn0zrab  12000  znn0sub  12018  nn0ind  12066  fnn0ind  12070  fznn0  12989  elfz0ubfz0  13001  elfz0fzfz0  13002  fz0fzelfz0  13003  elfzmlbp  13008  difelfzle  13010  difelfznle  13011  elfzo0z  13069  fzofzim  13074  ubmelm1fzo  13123  flge0nn0  13180  zmodcl  13249  modmuladdnn0  13273  modsumfzodifsn  13302  zsqcl2  13492  swrdnnn0nd  14008  swrdswrdlem  14056  swrdswrd  14057  swrdccatin2  14081  pfxccatin12lem2  14083  pfxccatin12lem3  14084  repswswrd  14136  cshwidxmod  14155  nn0abscl  14662  iseralt  15031  binomrisefac  15386  oexpneg  15684  oddnn02np1  15687  evennn02n  15689  nn0ehalf  15719  nn0oddm1d2  15726  divalglem2  15736  divalglem8  15741  divalglem10  15743  divalgb  15745  bitsinv1lem  15780  dfgcd2  15884  algcvga  15913  hashgcdlem  16115  iserodd  16162  pockthlem  16231  4sqlem14  16284  cshwshashlem2  16420  chfacfscmul0  21396  chfacfpmmul0  21400  taylfvallem1  24874  tayl0  24879  leibpilem1OLD  25446  basellem3  25588  bcmono  25781  gausslemma2dlem0h  25867  2sqnn0  25942  crctcshwlkn0lem7  27522  crctcshwlkn0  27527  clwlkclwwlklem2a1  27698  clwlkclwwlklem2fv2  27702  clwlkclwwlklem2a  27704  wwlksubclwwlk  27765  0nn0m1nnn0  32249  knoppndvlem2  33750  irrapxlem1  39299  rmynn0  39434  rmyabs  39435  jm2.22  39472  jm2.23  39473  jm2.27a  39482  jm2.27c  39484  dvnprodlem1  42111  wallispilem4  42234  stirlinglem5  42244  elaa2lem  42399  etransclem3  42403  etransclem7  42407  etransclem10  42410  etransclem19  42419  etransclem20  42420  etransclem21  42421  etransclem22  42422  etransclem24  42424  etransclem27  42427  zm1nn  43383  eluzge0nn0  43393  elfz2z  43396  2elfz2melfz  43399  subsubelfzo0  43407  oexpnegALTV  43689  nn0oALTV  43708  nn0e  43709  nn0eo  44486  dig1  44566
  Copyright terms: Public domain W3C validator