Theorem 2nn0 12419

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

Syntax hints:   ∈ wcel 2109  2c2 12201  ℕ₀cn0 12402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7675  ax-1cn 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-iun 4946  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5518  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-we 5578  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-ov 7356  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-nn 12147  df-2 12209  df-n0 12403

This theorem is referenced by:  nn0n0n1ge2  12470  7p6e13  12687  8p3e11  12690  8p5e13  12692  9p3e12  12697  9p4e13  12698  4t3e12  12707  4t4e16  12708  5t3e15  12710  5t5e25  12712  6t3e18  12714  6t5e30  12716  7t3e21  12719  7t4e28  12720  7t5e35  12721  7t6e42  12722  7t7e49  12723  8t3e24  12725  8t4e32  12726  8t5e40  12727  9t3e27  12732  9t4e36  12733  9t8e72  12737  9t9e81  12738  decbin3  12751  2eluzge0  12800  xnn0le2is012  13166  fzo0to42pr  13674  fvf1tp  13711  nn0sqcl  14014  sqmul  14044  resqcl  14049  zsqcl  14054  cu2  14125  i3  14128  i4  14129  binom3  14149  expmulnbnd  14160  nn0opthlem1  14193  fac3  14205  faclbnd2  14216  faclbnd4lem1  14218  faclbnd4lem3  14220  hash2pr  14394  hashtplei  14409  tpf1ofv2  14423  tpfo  14425  s4fv2  14822  pfx2  14872  repsw3  14876  swrd2lsw  14877  2swrd2eqwrdeq  14878  abssq  15231  sqabs  15232  iseraltlem2  15608  iseraltlem3  15609  bpoly2  15982  bpoly3  15983  bpoly4  15984  fsumcube  15985  ef4p  16040  efgt1p2  16041  efi4p  16064  ef01bndlem  16111  cos01bnd  16113  oexpneg  16274  oddge22np1  16278  bitsinv2  16372  bitsf1ocnv  16373  sadcaddlem  16386  sadadd2lem  16388  pythagtriplem4  16749  iserodd  16765  oddprmdvds  16833  prmreclem2  16847  prmreclem6  16851  vdwlem7  16917  vdwlem10  16920  vdwlem12  16922  dec2dvds  16993  dec5dvds  16994  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  17310  dsndxnplusgndx  17312  dsndxnmulrndx  17313  slotsdnscsi  17314  dsndxntsetndx  17315  slotsdifdsndx  17316  slotsdifunifndx  17323  prdsvalstr  17374  smndex2dbas  18806  smndex2dlinvh  18809  pmtrprfval  19384  psgnunilem2  19392  efgredleme  19640  lt6abl  19792  cnfldstr  21281  cnfldstrOLD  21296  sqcn  24783  ehl2eudis  25338  dveflem  25899  iaa  26249  tangtx  26430  efif1olem3  26469  efif1olem4  26470  root1id  26680  2logb9irr  26721  mcubic  26773  cubic2  26774  cubic  26775  binom4  26776  dquartlem2  26778  dquart  26779  quart1cl  26780  quart1lem  26781  quart1  26782  quartlem1  26783  quartlem2  26784  atandmcj  26835  bndatandm  26855  atansopn  26858  atantayl3  26865  leibpilem2  26867  leibpi  26868  leibpisum  26869  log2cnv  26870  log2tlbnd  26871  log2ublem2  26873  log2ublem3  26874  log2ub  26875  log2le1  26876  birthday  26880  basellem3  27009  basellem4  27010  basellem5  27011  basellem8  27014  issqf  27062  ppi3  27097  ppiublem2  27130  chtublem  27138  mersenne  27154  bcmax  27205  bcp1ctr  27206  bclbnd  27207  bpos1  27210  bposlem6  27216  bposlem8  27218  lgslem1  27224  lgsqrlem2  27274  gausslemma2dlem6  27299  lgseisenlem4  27305  2lgslem1c  27320  2lgslem3a  27323  2lgslem3b  27324  2lgslem3c  27325  2lgslem3d  27326  2sq2  27360  2sqreultlem  27374  2sqreunnltlem  27377  chebbnd1lem3  27398  rplogsumlem2  27412  dchrisumlem2  27417  dchrisum0flblem1  27435  dchrisum0flblem2  27436  dchrisum0flb  27437  selberglem2  27473  pntrmax  27491  pntlemo  27534  slotsinbpsd  28404  slotslnbpsd  28405  trkgstr  28407  eengstr  28943  usgrexmplef  29222  upgr2wlk  29630  usgr2pthlem  29726  usgr2pth  29727  wpthswwlks2on  29924  elwspths2spth  29930  upgr3v3e3cycl  30142  upgr4cycl4dv4e  30147  konigsbergiedgw  30210  konigsberglem1  30214  konigsberglem2  30215  konigsberglem3  30216  clwlknon2num  30330  1kp2ke3k  30408  ex-mod  30411  ex-exp  30412  ex-fac  30413  9p10ne21  30432  ipidsq  30672  strlem3a  32214  xnn01gt  32726  expevenpos  32804  dpmul4  32867  pfxlsw2ccat  32905  wrdt2ind  32908  eufndx  33242  eufid  33243  evl1deg2  33525  evl1deg3  33526  fldext2rspun  33656  rtelextdg2lem  33695  rtelextdg2  33696  constrelextdg2  33716  2sqr3minply  33749  cos9thpiminplylem1  33751  cos9thpiminplylem2  33752  cos9thpiminplylem4  33754  cos9thpiminplylem5  33755  cos9thpinconstrlem1  33758  madjusmdetlem4  33799  coinflippv  34454  prodfzo03  34573  hgt750lemd  34618  hgt750lem  34621  hgt750lem2  34622  hgt750leme  34628  tgoldbachgnn  34629  tgoldbachgtde  34630  tgoldbachgt  34633  cusgredgex  35097  kur14lem8  35188  sinccvglem  35647  dvtan  37652  420gcd8e4  41982  12lcm5e60  41984  60lcm7e420  41986  lcmineqlem17  42021  lcmineqlem18  42022  lcmineqlem20  42024  lcmineqlem21  42025  lcmineqlem22  42026  lcmineqlem  42028  3exp7  42029  3lexlogpow5ineq1  42030  3lexlogpow5ineq2  42031  3lexlogpow2ineq1  42034  3lexlogpow2ineq2  42035  3lexlogpow5ineq5  42036  aks4d1p1p2  42046  aks4d1p1p7  42050  aks4d1p1p5  42051  aks4d1p1  42052  2np3bcnp1  42120  2ap1caineq  42121  aks6d1c7lem1  42156  sqn5i  42261  235t711  42281  ex-decpmul  42282  nicomachus  42288  dffltz  42610  flt4lem  42621  flt4lem3  42624  flt4lem7  42635  nna4b4nsq  42636  sum9cubes  42648  3cubeslem2  42661  3cubeslem3l  42662  3cubeslem3r  42663  diophin  42748  irrapxlem5  42802  pellexlem2  42806  pell1qrge1  42846  jm2.22  42971  jm2.20nn  42973  jm2.27c  42983  rmydioph  42990  rmxdioph  42992  expdiophlem2  42998  frlmpwfi  43074  isnumbasgrplem3  43081  resqrtvalex  43621  imsqrtvalex  43622  amgm2d  44174  dvdivbd  45908  itgsinexplem1  45939  itgsinexp  45940  stoweidlem1  45986  wallispilem4  46053  wallispilem5  46054  wallispi2lem2  46057  stirlinglem3  46061  stirlinglem5  46063  stirlinglem7  46065  stirlinglem8  46066  stirlinglem10  46068  stirlinglem11  46069  hoiqssbllem2  46608  fmtnoge3  47518  fmtnom1nn  47520  fmtnof1  47523  fmtnorec1  47525  sqrtpwpw2p  47526  fmtnosqrt  47527  fmtnorec2lem  47530  fmtnodvds  47532  fmtnorec3  47536  fmtnorec4  47537  fmtno2  47538  fmtno3  47539  fmtno5lem2  47542  fmtno5lem4  47544  fmtno5  47545  257prm  47549  odz2prm2pw  47551  fmtnoprmfac1lem  47552  fmtnoprmfac2lem1  47554  fmtnofac2lem  47556  fmtnofac2  47557  fmtnofac1  47558  fmtno4prmfac  47560  fmtno4nprmfac193  47562  fmtno4prm  47563  fmtno5faclem1  47567  fmtno5faclem2  47568  fmtno5faclem3  47569  fmtno5fac  47570  flsqrt  47581  139prmALT  47584  31prm  47585  m5prm  47586  127prm  47587  m7prm  47588  m11nprm  47589  sfprmdvdsmersenne  47591  lighneallem2  47594  lighneallem3  47595  lighneallem4a  47596  proththd  47602  3exp4mod41  47604  41prothprmlem1  47605  oexpnegALTV  47665  fppr2odd  47719  2exp340mod341  47721  341fppr2  47722  8exp8mod9  47724  nfermltl2rev  47731  evengpoap3  47787  tgblthelfgott  47803  tgoldbachlt  47804  tgoldbach  47805  cycl3grtri  47935  usgrexmpl1lem  48009  usgrexmpl2lem  48014  gpg3nbgrvtx0  48064  gpgprismgr4cycllem7  48089  gpgprismgr4cycllem10  48092  gpg5edgnedg  48118  pgrple2abl  48353  pgrpgt2nabl  48354  ply1mulgsumlem2  48376  logbpw2m1  48556  blenpw2m1  48568  dignn0ehalf  48606  nn0sumshdiglemA  48608  nn0sumshdiglemB  48609  nn0mullong  48614  2aryfvalel  48636  itcoval2  48653  itcoval3  48654  itcovalt2lem2lem2  48663  itcovalt2lem1  48664  ackval2  48671  ackval3  48672  ackval0012  48678  ackval1012  48679  ackval2012  48680  ackval3012  48681  ackval42  48685  2sphere  48738  itscnhlinecirc02plem3  48773  inlinecirc02p  48776  onetansqsecsq  49750  cotsqcscsq  49751