Theorem 2nn0 12466

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

Syntax hints:   ∈ wcel 2109  2c2 12248  ℕ₀cn0 12449

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714  ax-1cn 11133

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-ov 7393  df-om 7846  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-nn 12194  df-2 12256  df-n0 12450

This theorem is referenced by:  nn0n0n1ge2  12517  7p6e13  12734  8p3e11  12737  8p5e13  12739  9p3e12  12744  9p4e13  12745  4t3e12  12754  4t4e16  12755  5t3e15  12757  5t5e25  12759  6t3e18  12761  6t5e30  12763  7t3e21  12766  7t4e28  12767  7t5e35  12768  7t6e42  12769  7t7e49  12770  8t3e24  12772  8t4e32  12773  8t5e40  12774  9t3e27  12779  9t4e36  12780  9t8e72  12784  9t9e81  12785  decbin3  12798  2eluzge0  12847  xnn0le2is012  13213  fzo0to42pr  13721  fvf1tp  13758  nn0sqcl  14061  sqmul  14091  resqcl  14096  zsqcl  14101  cu2  14172  i3  14175  i4  14176  binom3  14196  expmulnbnd  14207  nn0opthlem1  14240  fac3  14252  faclbnd2  14263  faclbnd4lem1  14265  faclbnd4lem3  14267  hash2pr  14441  hashtplei  14456  tpf1ofv2  14470  tpfo  14472  s4fv2  14870  pfx2  14920  repsw3  14924  swrd2lsw  14925  2swrd2eqwrdeq  14926  abssq  15279  sqabs  15280  iseraltlem2  15656  iseraltlem3  15657  bpoly2  16030  bpoly3  16031  bpoly4  16032  fsumcube  16033  ef4p  16088  efgt1p2  16089  efi4p  16112  ef01bndlem  16159  cos01bnd  16161  oexpneg  16322  oddge22np1  16326  bitsinv2  16420  bitsf1ocnv  16421  sadcaddlem  16434  sadadd2lem  16436  pythagtriplem4  16797  iserodd  16813  oddprmdvds  16881  prmreclem2  16895  prmreclem6  16899  vdwlem7  16965  vdwlem10  16968  vdwlem12  16970  dec2dvds  17041  dec5dvds  17042  2exp4  17062  2exp5  17063  2exp6  17064  2exp7  17065  2exp8  17066  2exp11  17067  2exp16  17068  3exp3  17069  2expltfac  17070  5prm  17086  7prm  17088  11prm  17092  13prm  17093  17prm  17094  19prm  17095  23prm  17096  prmlem2  17097  37prm  17098  43prm  17099  83prm  17100  139prm  17101  163prm  17102  317prm  17103  631prm  17104  1259lem1  17108  1259lem2  17109  1259lem3  17110  1259lem4  17111  1259lem5  17112  1259prm  17113  2503lem1  17114  2503lem2  17115  2503lem3  17116  2503prm  17117  4001lem1  17118  4001lem2  17119  4001lem3  17120  4001lem4  17121  4001prm  17122  basendxltdsndx  17358  dsndxnplusgndx  17360  dsndxnmulrndx  17361  slotsdnscsi  17362  dsndxntsetndx  17363  slotsdifdsndx  17364  slotsdifunifndx  17371  prdsvalstr  17422  smndex2dbas  18848  smndex2dlinvh  18851  pmtrprfval  19424  psgnunilem2  19432  efgredleme  19680  lt6abl  19832  cnfldstr  21273  cnfldstrOLD  21288  sqcn  24774  ehl2eudis  25329  dveflem  25890  iaa  26240  tangtx  26421  efif1olem3  26460  efif1olem4  26461  root1id  26671  2logb9irr  26712  mcubic  26764  cubic2  26765  cubic  26766  binom4  26767  dquartlem2  26769  dquart  26770  quart1cl  26771  quart1lem  26772  quart1  26773  quartlem1  26774  quartlem2  26775  atandmcj  26826  bndatandm  26846  atansopn  26849  atantayl3  26856  leibpilem2  26858  leibpi  26859  leibpisum  26860  log2cnv  26861  log2tlbnd  26862  log2ublem2  26864  log2ublem3  26865  log2ub  26866  log2le1  26867  birthday  26871  basellem3  27000  basellem4  27001  basellem5  27002  basellem8  27005  issqf  27053  ppi3  27088  ppiublem2  27121  chtublem  27129  mersenne  27145  bcmax  27196  bcp1ctr  27197  bclbnd  27198  bpos1  27201  bposlem6  27207  bposlem8  27209  lgslem1  27215  lgsqrlem2  27265  gausslemma2dlem6  27290  lgseisenlem4  27296  2lgslem1c  27311  2lgslem3a  27314  2lgslem3b  27315  2lgslem3c  27316  2lgslem3d  27317  2sq2  27351  2sqreultlem  27365  2sqreunnltlem  27368  chebbnd1lem3  27389  rplogsumlem2  27403  dchrisumlem2  27408  dchrisum0flblem1  27426  dchrisum0flblem2  27427  dchrisum0flb  27428  selberglem2  27464  pntrmax  27482  pntlemo  27525  slotsinbpsd  28375  slotslnbpsd  28376  trkgstr  28378  eengstr  28914  usgrexmplef  29193  upgr2wlk  29603  usgr2pthlem  29700  usgr2pth  29701  wpthswwlks2on  29898  elwspths2spth  29904  upgr3v3e3cycl  30116  upgr4cycl4dv4e  30121  konigsbergiedgw  30184  konigsberglem1  30188  konigsberglem2  30189  konigsberglem3  30190  clwlknon2num  30304  1kp2ke3k  30382  ex-mod  30385  ex-exp  30386  ex-fac  30387  9p10ne21  30406  ipidsq  30646  strlem3a  32188  xnn01gt  32700  expevenpos  32778  dpmul4  32841  pfxlsw2ccat  32879  wrdt2ind  32882  eufndx  33247  eufid  33248  evl1deg2  33553  evl1deg3  33554  fldext2rspun  33684  rtelextdg2lem  33723  rtelextdg2  33724  constrelextdg2  33744  2sqr3minply  33777  cos9thpiminplylem1  33779  cos9thpiminplylem2  33780  cos9thpiminplylem4  33782  cos9thpiminplylem5  33783  cos9thpinconstrlem1  33786  madjusmdetlem4  33827  coinflippv  34482  prodfzo03  34601  hgt750lemd  34646  hgt750lem  34649  hgt750lem2  34650  hgt750leme  34656  tgoldbachgnn  34657  tgoldbachgtde  34658  tgoldbachgt  34661  cusgredgex  35116  kur14lem8  35207  sinccvglem  35666  dvtan  37671  420gcd8e4  42001  12lcm5e60  42003  60lcm7e420  42005  lcmineqlem17  42040  lcmineqlem18  42041  lcmineqlem20  42043  lcmineqlem21  42044  lcmineqlem22  42045  lcmineqlem  42047  3exp7  42048  3lexlogpow5ineq1  42049  3lexlogpow5ineq2  42050  3lexlogpow2ineq1  42053  3lexlogpow2ineq2  42054  3lexlogpow5ineq5  42055  aks4d1p1p2  42065  aks4d1p1p7  42069  aks4d1p1p5  42070  aks4d1p1  42071  2np3bcnp1  42139  2ap1caineq  42140  aks6d1c7lem1  42175  sqn5i  42280  235t711  42300  ex-decpmul  42301  nicomachus  42307  dffltz  42629  flt4lem  42640  flt4lem3  42643  flt4lem7  42654  nna4b4nsq  42655  sum9cubes  42667  3cubeslem2  42680  3cubeslem3l  42681  3cubeslem3r  42682  diophin  42767  irrapxlem5  42821  pellexlem2  42825  pell1qrge1  42865  jm2.22  42991  jm2.20nn  42993  jm2.27c  43003  rmydioph  43010  rmxdioph  43012  expdiophlem2  43018  frlmpwfi  43094  isnumbasgrplem3  43101  resqrtvalex  43641  imsqrtvalex  43642  amgm2d  44194  dvdivbd  45928  itgsinexplem1  45959  itgsinexp  45960  stoweidlem1  46006  wallispilem4  46073  wallispilem5  46074  wallispi2lem2  46077  stirlinglem3  46081  stirlinglem5  46083  stirlinglem7  46085  stirlinglem8  46086  stirlinglem10  46088  stirlinglem11  46089  hoiqssbllem2  46628  fmtnoge3  47535  fmtnom1nn  47537  fmtnof1  47540  fmtnorec1  47542  sqrtpwpw2p  47543  fmtnosqrt  47544  fmtnorec2lem  47547  fmtnodvds  47549  fmtnorec3  47553  fmtnorec4  47554  fmtno2  47555  fmtno3  47556  fmtno5lem2  47559  fmtno5lem4  47561  fmtno5  47562  257prm  47566  odz2prm2pw  47568  fmtnoprmfac1lem  47569  fmtnoprmfac2lem1  47571  fmtnofac2lem  47573  fmtnofac2  47574  fmtnofac1  47575  fmtno4prmfac  47577  fmtno4nprmfac193  47579  fmtno4prm  47580  fmtno5faclem1  47584  fmtno5faclem2  47585  fmtno5faclem3  47586  fmtno5fac  47587  flsqrt  47598  139prmALT  47601  31prm  47602  m5prm  47603  127prm  47604  m7prm  47605  m11nprm  47606  sfprmdvdsmersenne  47608  lighneallem2  47611  lighneallem3  47612  lighneallem4a  47613  proththd  47619  3exp4mod41  47621  41prothprmlem1  47622  oexpnegALTV  47682  fppr2odd  47736  2exp340mod341  47738  341fppr2  47739  8exp8mod9  47741  nfermltl2rev  47748  evengpoap3  47804  tgblthelfgott  47820  tgoldbachlt  47821  tgoldbach  47822  cycl3grtri  47950  usgrexmpl1lem  48016  usgrexmpl2lem  48021  gpg3nbgrvtx0  48071  gpgprismgr4cycllem7  48095  gpgprismgr4cycllem10  48098  pgrple2abl  48357  pgrpgt2nabl  48358  ply1mulgsumlem2  48380  logbpw2m1  48560  blenpw2m1  48572  dignn0ehalf  48610  nn0sumshdiglemA  48612  nn0sumshdiglemB  48613  nn0mullong  48618  2aryfvalel  48640  itcoval2  48657  itcoval3  48658  itcovalt2lem2lem2  48667  itcovalt2lem1  48668  ackval2  48675  ackval3  48676  ackval0012  48682  ackval1012  48683  ackval2012  48684  ackval3012  48685  ackval42  48689  2sphere  48742  itscnhlinecirc02plem3  48777  inlinecirc02p  48780  onetansqsecsq  49754  cotsqcscsq  49755