Theorem 2nn0 12485

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 12281	. 2 ⊢ 2 ∈ ℕ
2	1	nnnn0i 12476	1 ⊢ 2 ∈ ℕ0

Syntax hints:   ∈ wcel 2107  2c2 12263  ℕ₀cn0 12468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7720  ax-1cn 11164

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7407  df-om 7851  df-2nd 7971  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-nn 12209  df-2 12271  df-n0 12469

This theorem is referenced by:  nn0n0n1ge2  12535  7p6e13  12751  8p3e11  12754  8p5e13  12756  9p3e12  12761  9p4e13  12762  4t3e12  12771  4t4e16  12772  5t3e15  12774  5t5e25  12776  6t3e18  12778  6t5e30  12780  7t3e21  12783  7t4e28  12784  7t5e35  12785  7t6e42  12786  7t7e49  12787  8t3e24  12789  8t4e32  12790  8t5e40  12791  9t3e27  12796  9t4e36  12797  9t8e72  12801  9t9e81  12802  decbin3  12815  2eluzge0  12873  xnn0le2is012  13221  fzo0to42pr  13715  nn0sqcl  14051  sqmul  14080  resqcl  14085  zsqcl  14090  cu2  14160  i3  14163  i4  14164  binom3  14183  expmulnbnd  14194  nn0opthlem1  14224  fac3  14236  faclbnd2  14247  faclbnd4lem1  14249  faclbnd4lem3  14251  hash2pr  14426  hashtplei  14441  s4fv2  14844  pfx2  14894  repsw3  14898  swrd2lsw  14899  2swrd2eqwrdeq  14900  abssq  15249  sqabs  15250  iseraltlem2  15625  iseraltlem3  15626  bpoly2  15997  bpoly3  15998  bpoly4  15999  fsumcube  16000  ef4p  16052  efgt1p2  16053  efi4p  16076  ef01bndlem  16123  cos01bnd  16125  oexpneg  16284  oddge22np1  16288  bitsinv2  16380  bitsf1ocnv  16381  sadcaddlem  16394  sadadd2lem  16396  pythagtriplem4  16748  iserodd  16764  oddprmdvds  16832  prmreclem2  16846  prmreclem6  16850  vdwlem7  16916  vdwlem10  16919  vdwlem12  16921  dec2dvds  16992  dec5dvds  16993  decexp2  17004  2exp4  17014  2exp5  17015  2exp6  17016  2exp7  17017  2exp8  17018  2exp11  17019  2exp16  17020  3exp3  17021  2expltfac  17022  5prm  17038  7prm  17040  11prm  17044  13prm  17045  17prm  17046  19prm  17047  23prm  17048  prmlem2  17049  37prm  17050  43prm  17051  83prm  17052  139prm  17053  163prm  17054  317prm  17055  631prm  17056  1259lem1  17060  1259lem2  17061  1259lem3  17062  1259lem4  17063  1259lem5  17064  1259prm  17065  2503lem1  17066  2503lem2  17067  2503lem3  17068  2503prm  17069  4001lem1  17070  4001lem2  17071  4001lem3  17072  4001lem4  17073  4001prm  17074  basendxltdsndx  17329  dsndxnplusgndx  17331  dsndxnmulrndx  17332  slotsdnscsi  17333  dsndxntsetndx  17334  slotsdifdsndx  17335  slotsdifunifndx  17342  prdsvalstr  17394  smndex2dbas  18791  smndex2dlinvh  18794  pmtrprfval  19348  psgnunilem2  19356  efgredleme  19604  lt6abl  19755  mgpdsOLD  19993  sradsOLD  20795  cnfldstr  20931  cnfldfunALTOLD  20943  setsmsdsOLD  23966  tmslemOLD  23973  tnglemOLD  24132  tngdsOLD  24147  sqcn  24372  ehl2eudis  24921  dveflem  25478  iaa  25820  tangtx  25997  efif1olem3  26035  efif1olem4  26036  root1id  26242  2logb9irr  26280  mcubic  26332  cubic2  26333  cubic  26334  binom4  26335  dquartlem2  26337  dquart  26338  quart1cl  26339  quart1lem  26340  quart1  26341  quartlem1  26342  quartlem2  26343  atandmcj  26394  bndatandm  26414  atansopn  26417  atantayl3  26424  leibpilem2  26426  leibpi  26427  leibpisum  26428  log2cnv  26429  log2tlbnd  26430  log2ublem2  26432  log2ublem3  26433  log2ub  26434  log2le1  26435  birthday  26439  basellem3  26567  basellem4  26568  basellem5  26569  basellem8  26572  issqf  26620  ppi3  26655  ppiublem2  26686  chtublem  26694  mersenne  26710  bcmax  26761  bcp1ctr  26762  bclbnd  26763  bpos1  26766  bposlem6  26772  bposlem8  26774  lgslem1  26780  lgsqrlem2  26830  gausslemma2dlem6  26855  lgseisenlem4  26861  2lgslem1c  26876  2lgslem3a  26879  2lgslem3b  26880  2lgslem3c  26881  2lgslem3d  26882  2sq2  26916  2sqreultlem  26930  2sqreunnltlem  26933  chebbnd1lem3  26954  rplogsumlem2  26968  dchrisumlem2  26973  dchrisum0flblem1  26991  dchrisum0flblem2  26992  dchrisum0flb  26993  selberglem2  27029  pntrmax  27047  pntlemo  27090  slotsinbpsd  27672  slotslnbpsd  27673  trkgstr  27675  ttgplusgOLD  28113  ttgdsOLD  28118  eengstr  28218  usgrexmplef  28496  upgr2wlk  28905  usgr2pthlem  29000  usgr2pth  29001  wpthswwlks2on  29195  elwspths2spth  29201  upgr3v3e3cycl  29413  upgr4cycl4dv4e  29418  konigsbergiedgw  29481  konigsberglem1  29485  konigsberglem2  29486  konigsberglem3  29487  clwlknon2num  29601  1kp2ke3k  29679  ex-mod  29682  ex-exp  29683  ex-fac  29684  9p10ne21  29703  ipidsq  29941  strlem3a  31483  xnn01gt  31961  dpmul4  32058  pfxlsw2ccat  32094  wrdt2ind  32095  madjusmdetlem4  32748  zlmdsOLD  32881  coinflippv  33420  prodfzo03  33553  hgt750lemd  33598  hgt750lem  33601  hgt750lem2  33602  hgt750leme  33608  tgoldbachgnn  33609  tgoldbachgtde  33610  tgoldbachgt  33613  cusgredgex  34050  kur14lem8  34142  sinccvglem  34595  dvtan  36476  420gcd8e4  40809  12lcm5e60  40811  60lcm7e420  40813  lcmineqlem17  40848  lcmineqlem18  40849  lcmineqlem20  40851  lcmineqlem21  40852  lcmineqlem22  40853  lcmineqlem  40855  3exp7  40856  3lexlogpow5ineq1  40857  3lexlogpow5ineq2  40858  3lexlogpow2ineq1  40861  3lexlogpow2ineq2  40862  3lexlogpow5ineq5  40863  aks4d1p1p2  40873  aks4d1p1p7  40877  aks4d1p1p5  40878  aks4d1p1  40879  2np3bcnp1  40898  2ap1caineq  40899  fac2xp3  40958  sqn5i  41147  235t711  41153  ex-decpmul  41154  dffltz  41320  flt4lem  41331  flt4lem3  41334  flt4lem7  41345  nna4b4nsq  41346  3cubeslem2  41356  3cubeslem3l  41357  3cubeslem3r  41358  diophin  41443  irrapxlem5  41497  pellexlem2  41501  pell1qrge1  41541  jm2.22  41667  jm2.20nn  41669  jm2.27c  41679  rmydioph  41686  rmxdioph  41688  expdiophlem2  41694  frlmpwfi  41773  isnumbasgrplem3  41780  resqrtvalex  42329  imsqrtvalex  42330  amgm2d  42883  dvdivbd  44574  itgsinexplem1  44605  itgsinexp  44606  stoweidlem1  44652  wallispilem4  44719  wallispilem5  44720  wallispi2lem2  44723  stirlinglem3  44727  stirlinglem5  44729  stirlinglem7  44731  stirlinglem8  44732  stirlinglem10  44734  stirlinglem11  44735  hoiqssbllem2  45274  fmtnoge3  46133  fmtnom1nn  46135  fmtnof1  46138  fmtnorec1  46140  sqrtpwpw2p  46141  fmtnosqrt  46142  fmtnorec2lem  46145  fmtnodvds  46147  fmtnorec3  46151  fmtnorec4  46152  fmtno2  46153  fmtno3  46154  fmtno5lem2  46157  fmtno5lem4  46159  fmtno5  46160  257prm  46164  odz2prm2pw  46166  fmtnoprmfac1lem  46167  fmtnoprmfac2lem1  46169  fmtnofac2lem  46171  fmtnofac2  46172  fmtnofac1  46173  fmtno4prmfac  46175  fmtno4nprmfac193  46177  fmtno4prm  46178  fmtno5faclem1  46182  fmtno5faclem2  46183  fmtno5faclem3  46184  fmtno5fac  46185  flsqrt  46196  139prmALT  46199  31prm  46200  m5prm  46201  127prm  46202  m7prm  46203  m11nprm  46204  sfprmdvdsmersenne  46206  lighneallem2  46209  lighneallem3  46210  lighneallem4a  46211  proththd  46217  3exp4mod41  46219  41prothprmlem1  46220  oexpnegALTV  46280  fppr2odd  46334  2exp340mod341  46336  341fppr2  46337  8exp8mod9  46339  nfermltl2rev  46346  evengpoap3  46402  tgblthelfgott  46418  tgoldbachlt  46419  tgoldbach  46420  pgrple2abl  46943  pgrpgt2nabl  46944  ply1mulgsumlem2  46970  logbpw2m1  47155  blenpw2m1  47167  dignn0ehalf  47205  nn0sumshdiglemA  47207  nn0sumshdiglemB  47208  nn0mullong  47213  2aryfvalel  47235  itcoval2  47252  itcoval3  47253  itcovalt2lem2lem2  47262  itcovalt2lem1  47263  ackval2  47270  ackval3  47271  ackval0012  47277  ackval1012  47278  ackval2012  47279  ackval3012  47280  ackval42  47284  2sphere  47337  itscnhlinecirc02plem3  47372  inlinecirc02p  47375  onetansqsecsq  47708  cotsqcscsq  47709