Theorem 0nn0 12443

Description: 0 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)

Assertion

Ref	Expression
0nn0	⊢ 0 ∈ ℕ0

Proof of Theorem 0nn0

Step	Hyp	Ref	Expression
1		eqid 2737	. 2 ⊢ 0 = 0
2		elnn0 12430	. . . 4 ⊢ (0 ∈ ℕ0 ↔ (0 ∈ ℕ ∨ 0 = 0))
3	2	biimpri 228	. . 3 ⊢ ((0 ∈ ℕ ∨ 0 = 0) → 0 ∈ ℕ0)
4	3	olcs 877	. 2 ⊢ (0 = 0 → 0 ∈ ℕ0)
5	1, 4	ax-mp 5	1 ⊢ 0 ∈ ℕ0

Syntax hints:   ∨ wo 848   = wceq 1542   ∈ wcel 2114  0cc0 11029  ℕcn 12165  ℕ₀cn0 12428

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-mulcl 11091  ax-i2m1 11097

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-sn 4569  df-n0 12429

This theorem is referenced by:  0xnn0  12507  nn0ind-raph  12620  10nn0  12653  declei  12671  numlti  12672  nummul1c  12684  decaddc2  12691  decrmanc  12692  decrmac  12693  decaddm10  12694  decaddi  12695  decaddci  12696  decaddci2  12697  decmul1  12699  decmulnc  12702  6p5e11  12708  7p4e11  12711  8p3e11  12716  9p2e11  12722  10p10e20  12730  xnn0n0n1ge2b  13074  0elfz  13569  4fvwrd4  13593  fvinim0ffz  13735  ssnn0fi  13938  fsuppmapnn0fiubex  13945  exple1  14130  nn0opth2  14225  faclbnd4lem3  14248  bc0k  14264  bcn1  14266  bccl  14275  hasheq0  14316  hashrabrsn  14325  hashbc  14406  fi1uzind  14460  brfi1ind  14462  opfi1ind  14465  iswrdi  14470  wrdnfi  14501  s1fv  14564  ccat2s1fst  14593  splfv2a  14709  repsw0  14730  0csh0  14746  cshw1  14775  s2fv0  14840  s3fv0  14844  s4fv0  14848  pfx2  14900  ofs1  14923  relexp0g  14975  relexpaddg  15006  rtrclreclem2  15012  fsumnn0cl  15689  binom  15786  bcxmas  15791  isumnn0nn  15798  climcndslem1  15805  geoser  15823  geomulcvg  15832  risefac0  15983  fallfac0  15984  risefac1  15989  fallfac1  15990  binomfallfaclem2  15996  binomfallfac  15997  bpoly0  16006  bpoly2  16013  bpoly3  16014  bpoly4  16015  fsumcube  16016  ef0lem  16034  ege2le3  16046  ef4p  16071  efgt1p2  16072  efgt1p  16073  ruclem11  16198  nthruz  16211  nn0o  16343  ndvdssub  16369  5ndvds3  16373  bits0  16388  0bits  16399  sadcf  16413  sadc0  16414  sadcaddlem  16417  sadcadd  16418  sadadd2lem  16419  sadadd2  16420  smupf  16438  smup0  16439  smumullem  16452  gcdcl  16466  nn0seqcvgd  16530  algcvg  16536  eucalg  16547  lcmcl  16561  lcmfval  16581  lcmfcl  16588  pclem  16800  pcfac  16861  vdwap0  16938  vdwap1  16939  vdwlem6  16948  hashbc0  16967  0ram  16982  0ramcl  16985  ramz2  16986  ramz  16987  ramcl  16991  prmo0  16998  dec5dvds2  17027  2exp11  17051  2exp16  17052  11prm  17076  37prm  17082  43prm  17083  83prm  17084  139prm  17085  163prm  17086  317prm  17087  631prm  17088  1259lem1  17092  1259lem2  17093  1259lem3  17094  1259lem4  17095  1259lem5  17096  2503lem1  17098  2503lem2  17099  2503lem3  17100  2503prm  17101  4001lem1  17102  4001lem2  17103  4001lem3  17104  4001lem4  17105  4001prm  17106  plendxnocndx  17338  slotsdifdsndx  17348  slotsdifunifndx  17355  odrngstr  17357  slotsdifplendx2  17370  imasvalstr  17405  ipostr  18486  gsumws1  18797  cycsubm  19168  psgnunilem2  19461  psgnunilem3  19462  odfval  19498  oddvdsnn0  19510  pgp0  19562  sylow1lem1  19564  cyggex2  19863  telgsums  19959  srgbinomlem3  20200  srgbinomlem4  20201  srgbinom  20203  cnfldstr  21346  cnfldstrOLD  21361  nn0subm  21412  expmhm  21426  nn0srg  21427  znf1o  21541  zzngim  21542  cygznlem1  21556  cygznlem2a  21557  cygznlem3  21559  cygth  21561  freshmansdream  21564  snifpsrbag  21910  fczpsrbag  21911  psrbagaddcl  21914  psrlidm  21950  mvrf1  21974  mplcoe3  22026  mplcoe5  22028  ltbwe  22032  psrbag0  22050  psrbagsn  22051  evlslem1  22070  mhpsclcl  22123  mhpmulcl  22125  psdmul  22142  psdmvr  22145  00ply1bas  22213  ply1plusgfvi  22215  coe1sclmul  22257  coe1sclmul2  22259  coe1scl  22262  ply1sclid  22263  ply1idvr1OLD  22270  cply1coe0bi  22277  ply1scleq  22280  cpm2mf  22727  m2cpminvid2lem  22729  m2cpminvid2  22730  m2cpmfo  22731  decpmatid  22745  pmatcollpw3  22759  pmatcollpw3fi1lem1  22761  pmatcollpwscmatlem1  22764  pmatcollpwscmatlem2  22765  idpm2idmp  22776  chfacfscmulgsum  22835  chfacfpmmulgsum  22839  cpmadugsumlemF  22851  dscmet  24547  ehl0base  25393  ehl0  25394  itgcnlem  25767  dvn0  25901  dvn1  25903  cpncn  25913  dveflem  25956  c1lip2  25975  deg1le0  26086  ply1divex  26112  mon1pid  26129  ply1rem  26141  fta1g  26145  plyconst  26181  plypf1  26187  plyco  26216  0dgr  26220  0dgrb  26221  coefv0  26223  dgreq0  26240  vieta1lem2  26288  vieta1  26289  aareccl  26303  aannenlem2  26306  taylthlem1  26350  radcnv0  26394  abelthlem6  26414  abelthlem9  26418  logtayl  26637  cxp0  26647  cxpeq  26734  leibpilem2  26918  leibpi  26919  log2ublem3  26925  log2ub  26926  log2le1  26927  divsqrtsumlem  26957  dmgmn0  27003  lgambdd  27014  sqff1o  27159  ppiublem2  27180  chtublem  27188  bclbnd  27257  bposlem8  27268  lgsval  27278  dchrisum0flblem1  27485  dchrisum0flb  27487  ostth2lem2  27611  usgrexmplef  29342  usgr0edg0rusgr  29659  usgr2pthlem  29846  wwlksn0s  29944  rusgrnumwwlkb0  30057  erclwwlkref  30105  clwwlkf1  30134  0wlkonlem1  30203  upgr4cycl4dv4e  30270  1kp2ke3k  30531  ex-fac  30536  ex-prmo  30544  nn0min  32909  dpmul1000  32973  dp0h  32976  dpexpp1  32982  dpmul4  32988  threehalves  32989  1mhdrd  32990  s1f1  33018  s2f1  33020  cshw1s2  33035  cycpm2tr  33195  deg1le0eq0  33648  ply1unit  33650  evl1deg1  33651  evl1deg2  33652  evl1deg3  33653  ply1dg1rt  33655  m1pmeq  33660  psrbasfsupp  33687  mplmulmvr  33698  evlextv  33701  mplvrpmlem  33702  mplvrpmfgalem  33703  mplvrpmga  33704  mplvrpmmhm  33705  mplvrpmrhm  33706  psrmonprod  33711  esplyfval0  33723  esplylem  33725  esplyfv1  33728  esplyfval1  33732  esplyfvaln  33733  esplyind  33734  vietalem  33738  vieta  33739  minplyirredlem  33870  rtelextdg2lem  33886  fldext2chn  33888  constraddcl  33922  constrnegcl  33923  constrdircl  33925  constrremulcl  33927  2sqr3minply  33940  lmatcl  33976  lmat22e12  33979  lmat22e21  33980  fsumcvg4  34110  oddpwdc  34514  eulerpartlems  34520  eulerpartlemb  34528  eulerpartlemt  34531  eulerpartgbij  34532  eulerpartlemmf  34535  eulerpartlemgf  34539  eulerpartlemgs2  34540  eulerpartlemn  34541  fib0  34559  fib1  34560  fibp1  34561  ofcs1  34704  signsply0  34711  signsvvf  34739  prodfzo03  34763  repr0  34771  breprexp  34793  hgt750lemd  34808  hgt750lem  34811  hgt750lem2  34812  hgt750leme  34818  tgoldbachgtde  34820  0nn0m1nnn0  35311  f1resfz0f1d  35312  usgrgt2cycl  35328  subfac0  35375  subfacval2  35385  subfaclim  35386  cvmliftlem7  35489  cvmliftlem13  35494  bccolsum  35937  fwddifn0  36362  heiborlem4  38149  heiborlem10  38155  12gcd5e1  42456  60gcd6e6  42457  60gcd7e1  42458  420gcd8e4  42459  12lcm5e60  42461  60lcm7e420  42463  420lcm8e840  42464  lcmineqlem  42505  3exp7  42506  3lexlogpow5ineq1  42507  3lexlogpow5ineq2  42508  3lexlogpow5ineq5  42513  aks4d1p1  42529  aks6d1c2lem4  42580  aks6d1c2  42583  sticksstones11  42609  sticksstones22  42621  aks6d1c7lem1  42633  sqn5i  42731  decpmul  42734  sqdeccom12  42735  sq3deccom12  42736  235t711  42751  ex-decpmul  42752  mhphflem  43043  0prjspn  43075  sum9cubes  43119  nacsfix  43158  diophrw  43205  pell1qr1  43317  monotoddzzfi  43388  jm2.23  43442  hbtlem5  43574  mncn0  43585  aaitgo  43608  brfvrcld  44136  corclrcl  44152  dfrtrcl3  44178  fvrtrcllb0d  44180  fvrtrcllb0da  44181  corcltrcl  44184  cotrclrcl  44187  k0004val0  44599  bccn0  44788  bccn1  44789  binomcxplemradcnv  44797  binomcxplemnotnn0  44801  rexanuz2nf  45938  dvnmul  46389  dvnprodlem3  46394  wallispilem2  46512  wallispi2lem2  46518  stirlinglem5  46524  stirlinglem7  46526  fourierdlem83  46635  fourierdlem112  46664  fouriersw  46677  elaa2lem  46679  elaa2  46680  etransclem48  46728  etransc  46729  iccelpart  47905  fmtno0  48015  fmtnorec2  48018  fmtno5lem1  48028  fmtno5lem2  48029  fmtno5lem4  48031  257prm  48036  fmtnofac2  48044  fmtnofac1  48045  fmtno4prmfac  48047  fmtno4nprmfac193  48049  fmtno5faclem1  48054  fmtno5faclem2  48055  fmtno5faclem3  48056  fmtno5fac  48057  fmtno5nprm  48058  139prmALT  48071  31prm  48072  127prm  48074  m11nprm  48076  bits0ALTV  48167  2exp340mod341  48221  nfermltl2rev  48231  evengpoap3  48287  tgoldbachlt  48304  tgoldbach  48305  stgr0  48448  usgrexmpl1lem  48509  usgrexmpl2lem  48514  gpgprismgr4cycllem6  48588  gpgprismgr4cycllem7  48589  gpgprismgr4cycllem10  48592  nn0mnd  48667  ssnn0ssfz  48837  dig1  49096  0dig2nn0e  49100  0dig2nn0o  49101  0aryfvalel  49122  itcoval0  49150  itcoval1  49151  ackval0  49168  ackval1  49169  ackvalsuc0val  49175  ackval0012  49177  ackval1012  49178  ackval2012  49179  ackval3012  49180  ackval41a  49182