Theorem 2nn0 11186

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

Assertion

Ref	Expression
2nn0	⊢ 2 ∈ ℕ0

Proof of Theorem 2nn0

Step	Hyp	Ref	Expression
1		2nn 11062	. 2 ⊢ 2 ∈ ℕ
2	1	nnnn0i 11177	1 ⊢ 2 ∈ ℕ0

Syntax hints:   ∈ wcel 1977  2c2 10947  ℕ₀cn0 11169

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-1cn 9873

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-om 6958  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-nn 10898  df-2 10956  df-n0 11170

This theorem is referenced by:  nn0n0n1ge2  11235  7p6e13  11484  8p3e11  11488  8p3e11OLD  11489  8p5e13  11491  9p3e12  11497  9p4e13  11498  4t3e12  11508  4t4e16  11509  5t3e15  11511  5t3e15OLD  11512  5t5e25  11515  5t5e25OLD  11516  6t3e18  11518  6t5e30  11520  6t5e30OLD  11521  7t3e21  11525  7t4e28  11526  7t5e35  11527  7t6e42  11528  7t7e49  11529  8t3e24  11531  8t4e32  11532  8t5e40  11533  8t5e40OLD  11534  9t3e27  11540  9t4e36  11541  9t8e72  11545  9t9e81  11546  decbin3  11560  2eluzge0  11609  fzo0to42pr  12422  nn0sqcl  12749  sqmul  12788  resqcl  12793  zsqcl  12796  cu2  12825  i3  12828  i4  12829  binom3  12847  expmulnbnd  12858  nn0opthlem1  12917  fac3  12929  faclbnd2  12940  faclbnd4lem1  12942  faclbnd4lem3  12944  hash2pr  13108  hashtplei  13120  s4fv2  13492  repsw3  13542  swrd2lsw  13543  2swrd2eqwrdeq  13544  abssq  13894  sqabs  13895  iseraltlem2  14261  iseraltlem3  14262  bpoly2  14627  bpoly3  14628  bpoly4  14629  fsumcube  14630  ef4p  14682  efgt1p2  14683  efi4p  14706  ef01bndlem  14753  cos01bnd  14755  oexpneg  14907  oddge22np1  14911  bitsinv2  15003  bitsf1ocnv  15004  sadcaddlem  15017  sadadd2lem  15019  pythagtriplem4  15362  iserodd  15378  oddprmdvds  15445  prmreclem2  15459  prmreclem6  15463  vdwlem7  15529  vdwlem10  15532  vdwlem12  15534  dec2dvds  15605  dec5dvds  15606  decexp2  15617  2exp4  15632  2exp6  15633  2exp8  15634  2exp16  15635  3exp3  15636  2expltfac  15637  5prm  15653  7prm  15655  11prm  15660  13prm  15661  17prm  15662  19prm  15663  23prm  15664  prmlem2  15665  37prm  15666  43prm  15667  83prm  15668  139prm  15669  163prm  15670  317prm  15671  631prm  15672  1259lem1  15676  1259lem2  15677  1259lem3  15678  1259lem4  15679  1259lem5  15680  1259prm  15681  2503lem1  15682  2503lem2  15683  2503lem3  15684  2503prm  15685  4001lem1  15686  4001lem2  15687  4001lem3  15688  4001lem4  15689  4001prm  15690  ressds  15896  prdsvalstr  15936  pmtrprfval  17730  psgnunilem2  17738  efgredleme  17979  lt6abl  18119  mgpds  18322  srads  19007  cnfldstr  19569  setsmsds  22091  tmslem  22097  tnglem  22254  tngds  22262  sqcn  22485  dveflem  23546  iaa  23884  tangtx  24061  efif1olem3  24094  efif1olem4  24095  root1id  24295  mcubic  24374  cubic2  24375  cubic  24376  binom4  24377  dquartlem2  24379  dquart  24380  quart1cl  24381  quart1lem  24382  quart1  24383  quartlem1  24384  quartlem2  24385  atandmcj  24436  bndatandm  24456  atansopn  24459  atantayl3  24466  leibpilem2  24468  leibpi  24469  leibpisum  24470  log2cnv  24471  log2tlbnd  24472  log2ublem2  24474  log2ublem3  24475  log2ub  24476  log2le1  24477  birthday  24481  basellem3  24609  basellem4  24610  basellem5  24611  basellem8  24614  issqf  24662  ppi3  24697  ppiublem2  24728  chtublem  24736  mersenne  24752  bcmax  24803  bcp1ctr  24804  bclbnd  24805  bpos1  24808  bposlem6  24814  bposlem8  24816  lgslem1  24822  lgsqrlem2  24872  gausslemma2dlem6  24897  lgseisenlem4  24903  2lgslem1c  24918  2lgslem3a  24921  2lgslem3b  24922  2lgslem3c  24923  2lgslem3d  24924  chebbnd1lem3  24960  rplogsumlem2  24974  dchrisumlem2  24979  dchrisum0flblem1  24997  dchrisum0flblem2  24998  dchrisum0flb  24999  selberglem2  25035  pntrmax  25053  pntlemo  25096  trkgstr  25143  ttgplusg  25558  ttgds  25561  eengstr  25660  upgredg  25811  usgraex2elv  25926  is2wlk  26095  3v3e3cycl1  26172  constr3trllem3  26180  4cycl4v4e  26194  4cycl4dv  26195  clwwlkn2  26303  wwlkext2clwwlk  26331  extwwlkfablem2lem  26602  numclwwlkovf2  26611  numclwwlk2lem1  26629  numclwlk2lem2f  26630  numclwlk2lem2f1o  26632  1kp2ke3k  26695  ex-mod  26698  ex-exp  26699  ex-fac  26700  ipidsq  26949  strlem3a  28495  madjusmdetlem4  29224  zlmds  29336  coinflippv  29872  kur14lem8  30449  sinccvglem  30820  dvtan  32630  diophin  36354  irrapxlem5  36408  pellexlem2  36412  pell1qrge1  36452  jm2.22  36580  jm2.20nn  36582  jm2.27c  36592  rmydioph  36599  rmxdioph  36601  expdiophlem2  36607  frlmpwfi  36686  isnumbasgrplem3  36694  amgm2d  37523  dvdivbd  38813  itgsinexplem1  38845  itgsinexp  38846  stoweidlem1  38894  wallispilem4  38961  wallispilem5  38962  wallispi2lem2  38965  stirlinglem3  38969  stirlinglem5  38971  stirlinglem7  38973  stirlinglem8  38974  stirlinglem10  38976  stirlinglem11  38977  hoiqssbllem2  39513  fmtnoge3  39980  fmtnom1nn  39982  fmtnof1  39985  fmtnorec1  39987  sqrtpwpw2p  39988  fmtnosqrt  39989  fmtnorec2lem  39992  fmtnodvds  39994  fmtnorec3  39998  fmtnorec4  39999  fmtno2  40000  fmtno3  40001  fmtno5lem2  40004  fmtno5lem4  40006  fmtno5  40007  257prm  40011  odz2prm2pw  40013  fmtnoprmfac1lem  40014  fmtnoprmfac2lem1  40016  fmtnofac2lem  40018  fmtnofac2  40019  fmtnofac1  40020  fmtno4prmfac  40022  fmtno4nprmfac193  40024  fmtno4prm  40025  fmtno5faclem1  40029  fmtno5faclem2  40030  fmtno5faclem3  40031  fmtno5fac  40032  2exp5  40045  flsqrt  40046  139prmALT  40049  31prm  40050  m5prm  40051  2exp7  40052  127prm  40053  m7prm  40054  2exp11  40055  m11nprm  40056  sfprmdvdsmersenne  40058  lighneallem2  40061  lighneallem3  40062  lighneallem4a  40063  proththd  40069  3exp4mod41  40071  41prothprmlem1  40072  oexpnegALTV  40126  evengpoap3  40215  tgblthelfgott  40229  tgoldbachlt  40230  tgoldbach  40232  tgblthelfgottOLD  40236  tgoldbachltOLD  40237  tgoldbachOLD  40239  pfx2  40275  upgr2wlk  40876  usgr2pthlem  40969  usgr2pth  40970  wwlks2onv  41158  elwwlks2  41170  elwspths2spth  41171  upgr3v3e3cycl  41347  upgr4cycl4dv4e  41352  konigsbergiedgw  41416  konigsbergiedgwOLD  41417  konigsberglem1  41422  konigsberglem2  41423  konigsberglem3  41424  fusgr2wsp2nb  41498  av-extwwlkfablem2lem  41507  pgrple2abl  41940  pgrpgt2nabl  41941  ply1mulgsumlem2  41969  logbpw2m1  42159  blenpw2m1  42171  dignn0ehalf  42209  nn0sumshdiglemA  42211  nn0sumshdiglemB  42212  nn0mullong  42217  onetansqsecsq  42301  cotsqcscsq  42302