Theorem 2nn0 12449

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

Syntax hints:   ∈ wcel 2121  2c2 12231  ℕ₀cn0 12432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5220  ax-nul 5230  ax-pr 5364  ax-un 7681  ax-1cn 11092

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3or 1094  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-ral 3056  df-rex 3066  df-reu 3347  df-rab 3394  df-v 3435  df-sbc 3725  df-csb 3833  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3904  df-nul 4264  df-if 4457  df-pw 4533  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-iun 4925  df-br 5075  df-opab 5137  df-mpt 5156  df-tr 5182  df-id 5515  df-eprel 5520  df-po 5528  df-so 5529  df-fr 5573  df-we 5575  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-pred 6255  df-ord 6316  df-on 6317  df-lim 6318  df-suc 6319  df-iota 6444  df-fun 6490  df-fn 6491  df-f 6492  df-f1 6493  df-fo 6494  df-f1o 6495  df-fv 6496  df-ov 7362  df-om 7810  df-2nd 7934  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8343  df-nn 12170  df-2 12239  df-n0 12433

This theorem is referenced by:  nn0n0n1ge2  12500  7p6e13  12717  8p3e11  12720  8p5e13  12722  9p3e12  12727  9p4e13  12728  4t3e12  12737  4t4e16  12738  5t3e15  12740  5t5e25  12742  6t3e18  12744  6t5e30  12746  7t3e21  12749  7t4e28  12750  7t5e35  12751  7t6e42  12752  7t7e49  12753  8t3e24  12755  8t4e32  12756  8t5e40  12757  9t3e27  12762  9t4e36  12763  9t8e72  12767  9t9e81  12768  decbin3  12781  2eluzge0  12826  xnn0le2is012  13193  fzo0to42pr  13703  fvf1tp  13743  nn0sqcl  14046  sqmul  14076  resqcl  14081  zsqcl  14086  cu2  14157  i3  14160  i4  14161  binom3  14181  expmulnbnd  14192  nn0opthlem1  14225  fac3  14237  faclbnd2  14248  faclbnd4lem1  14250  faclbnd4lem3  14252  hash2pr  14426  hashtplei  14441  tpf1ofv2  14455  tpfo  14457  s4fv2  14854  pfx2  14904  repsw3  14908  swrd2lsw  14909  2swrd2eqwrdeq  14910  abssq  15263  sqabs  15264  iseraltlem2  15640  iseraltlem3  15641  bpoly2  16017  bpoly3  16018  bpoly4  16019  fsumcube  16020  ef4p  16075  efgt1p2  16076  efi4p  16099  ef01bndlem  16146  cos01bnd  16148  oexpneg  16309  oddge22np1  16313  bitsinv2  16407  bitsf1ocnv  16408  sadcaddlem  16421  sadadd2lem  16423  pythagtriplem4  16785  iserodd  16801  oddprmdvds  16869  prmreclem2  16883  prmreclem6  16887  vdwlem7  16953  vdwlem10  16956  vdwlem12  16958  dec2dvds  17029  dec5dvds  17030  2exp4  17050  2exp5  17051  2exp6  17052  2exp7  17053  2exp8  17054  2exp11  17055  2exp16  17056  3exp3  17057  2expltfac  17058  5prm  17074  7prm  17076  11prm  17080  13prm  17081  17prm  17082  19prm  17083  23prm  17084  prmlem2  17085  37prm  17086  43prm  17087  83prm  17088  139prm  17089  163prm  17090  317prm  17091  631prm  17092  1259lem1  17096  1259lem2  17097  1259lem3  17098  1259lem4  17099  1259lem5  17100  1259prm  17101  2503lem1  17102  2503lem2  17103  2503lem3  17104  2503prm  17105  4001lem1  17106  4001lem2  17107  4001lem3  17108  4001lem4  17109  4001prm  17110  basendxltdsndx  17346  dsndxnplusgndx  17348  dsndxnmulrndx  17349  slotsdnscsi  17350  dsndxntsetndx  17351  slotsdifdsndx  17352  slotsdifunifndx  17359  prdsvalstr  17410  smndex2dbas  18880  smndex2dlinvh  18883  pmtrprfval  19456  psgnunilem2  19464  efgredleme  19712  lt6abl  19864  cnfldstr  21352  sqcn  24862  ehl2eudis  25410  dveflem  25967  iaa  26312  tangtx  26490  efif1olem3  26529  efif1olem4  26530  root1id  26739  2logb9irr  26780  mcubic  26832  cubic2  26833  cubic  26834  binom4  26835  dquartlem2  26837  dquart  26838  quart1cl  26839  quart1lem  26840  quart1  26841  quartlem1  26842  quartlem2  26843  atandmcj  26894  bndatandm  26914  atansopn  26917  atantayl3  26924  leibpilem2  26926  leibpi  26927  leibpisum  26928  log2cnv  26929  log2tlbnd  26930  log2ublem2  26932  log2ublem3  26933  log2ub  26934  log2le1  26935  birthday  26939  basellem3  27067  basellem4  27068  basellem5  27069  basellem8  27072  issqf  27120  ppi3  27155  ppiublem2  27187  chtublem  27195  mersenne  27211  bcmax  27262  bcp1ctr  27263  bclbnd  27264  bpos1  27267  bposlem6  27273  bposlem8  27275  lgslem1  27281  lgsqrlem2  27331  gausslemma2dlem6  27356  lgseisenlem4  27362  2lgslem1c  27377  2lgslem3a  27380  2lgslem3b  27381  2lgslem3c  27382  2lgslem3d  27383  2sq2  27417  2sqreultlem  27431  2sqreunnltlem  27434  chebbnd1lem3  27455  rplogsumlem2  27469  dchrisumlem2  27474  dchrisum0flblem1  27492  dchrisum0flblem2  27493  dchrisum0flb  27494  selberglem2  27530  pntrmax  27548  pntlemo  27591  slotsinbpsd  28529  slotslnbpsd  28530  trkgstr  28532  eengstr  29069  usgrexmplef  29348  upgr2wlk  29755  usgr2pthlem  29851  usgr2pth  29852  wpthswwlks2on  30052  elwspths2spth  30058  upgr3v3e3cycl  30270  upgr4cycl4dv4e  30275  konigsbergiedgw  30338  konigsberglem1  30342  konigsberglem2  30343  konigsberglem3  30344  clwlknon2num  30458  1kp2ke3k  30536  ex-mod  30539  ex-exp  30540  ex-fac  30541  9p10ne21  30560  ipidsq  30801  strlem3a  32343  xnn01gt  32864  expevenpos  32940  dpmul4  32994  pfxlsw2ccat  33031  wrdt2ind  33034  eufndx  33376  eufid  33377  evl1deg2  33670  evl1deg3  33671  fldext2rspun  33876  rtelextdg2lem  33920  rtelextdg2  33921  constrelextdg2  33941  2sqr3minply  33974  cos9thpiminplylem1  33976  cos9thpiminplylem2  33977  cos9thpiminplylem4  33979  cos9thpiminplylem5  33980  cos9thpinconstrlem1  33983  madjusmdetlem4  34024  coinflippv  34678  prodfzo03  34797  hgt750lemd  34842  hgt750lem  34845  hgt750lem2  34846  hgt750leme  34852  tgoldbachgnn  34853  tgoldbachgtde  34854  tgoldbachgt  34857  cusgredgex  35363  kur14lem8  35454  sinccvglem  35913  dvtan  38050  420gcd8e4  42504  12lcm5e60  42506  60lcm7e420  42508  lcmineqlem17  42543  lcmineqlem18  42544  lcmineqlem20  42546  lcmineqlem21  42547  lcmineqlem22  42548  lcmineqlem  42550  3exp7  42551  3lexlogpow5ineq1  42552  3lexlogpow5ineq2  42553  3lexlogpow2ineq1  42556  3lexlogpow2ineq2  42557  3lexlogpow5ineq5  42558  aks4d1p1p2  42568  aks4d1p1p7  42572  aks4d1p1p5  42573  aks4d1p1  42574  2np3bcnp1  42642  2ap1caineq  42643  aks6d1c7lem1  42678  sqn5i  42775  235t711  42795  ex-decpmul  42796  nicomachus  42802  dffltz  43097  flt4lem  43108  flt4lem3  43111  flt4lem7  43122  nna4b4nsq  43123  sum9cubes  43135  3cubeslem2  43147  3cubeslem3l  43148  3cubeslem3r  43149  diophin  43234  irrapxlem5  43284  pellexlem2  43288  pell1qrge1  43328  jm2.22  43453  jm2.20nn  43455  jm2.27c  43465  rmydioph  43472  rmxdioph  43474  expdiophlem2  43480  frlmpwfi  43556  isnumbasgrplem3  43563  resqrtvalex  44102  imsqrtvalex  44103  amgm2d  44655  dvdivbd  46378  itgsinexplem1  46409  itgsinexp  46410  stoweidlem1  46456  wallispilem4  46523  wallispilem5  46524  wallispi2lem2  46527  stirlinglem3  46531  stirlinglem5  46533  stirlinglem7  46535  stirlinglem8  46536  stirlinglem10  46538  stirlinglem11  46539  hoiqssbllem2  47078  nthrucw  47343  sin3t  47346  cos3t  47347  sin5tlem1  47348  sin5tlem2  47349  sin5tlem4  47351  fmtnoge3  48020  fmtnom1nn  48022  fmtnof1  48025  fmtnorec1  48027  sqrtpwpw2p  48028  fmtnosqrt  48029  fmtnorec2lem  48032  fmtnodvds  48034  fmtnorec3  48038  fmtnorec4  48039  fmtno2  48040  fmtno3  48041  fmtno5lem2  48044  fmtno5lem4  48046  fmtno5  48047  257prm  48051  odz2prm2pw  48053  fmtnoprmfac1lem  48054  fmtnoprmfac2lem1  48056  fmtnofac2lem  48058  fmtnofac2  48059  fmtnofac1  48060  fmtno4prmfac  48062  fmtno4nprmfac193  48064  fmtno4prm  48065  fmtno5faclem1  48069  fmtno5faclem2  48070  fmtno5faclem3  48071  fmtno5fac  48072  flsqrt  48083  139prmALT  48086  31prm  48087  m5prm  48088  127prm  48089  m7prm  48090  m11nprm  48091  sfprmdvdsmersenne  48093  lighneallem2  48096  lighneallem3  48097  lighneallem4a  48098  proththd  48104  3exp4mod41  48106  41prothprmlem1  48107  oexpnegALTV  48180  fppr2odd  48234  2exp340mod341  48236  341fppr2  48237  8exp8mod9  48239  nfermltl2rev  48246  evengpoap3  48302  tgblthelfgott  48318  tgoldbachlt  48319  tgoldbach  48320  cycl3grtri  48450  usgrexmpl1lem  48524  usgrexmpl2lem  48529  gpg3nbgrvtx0  48579  gpgprismgr4cycllem7  48604  gpgprismgr4cycllem10  48607  gpg5edgnedg  48633  pgrple2abl  48868  pgrpgt2nabl  48869  ply1mulgsumlem2  48890  logbpw2m1  49070  blenpw2m1  49082  dignn0ehalf  49120  nn0sumshdiglemA  49122  nn0sumshdiglemB  49123  nn0mullong  49128  2aryfvalel  49150  itcoval2  49167  itcoval3  49168  itcovalt2lem2lem2  49177  itcovalt2lem1  49178  ackval2  49185  ackval3  49186  ackval0012  49192  ackval1012  49193  ackval2012  49194  ackval3012  49195  ackval42  49199  2sphere  49252  itscnhlinecirc02plem3  49287  inlinecirc02p  49290  onetansqsecsq  50263  cotsqcscsq  50264