Theorem 2nn0 12445

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

Syntax hints:   ∈ wcel 2114  2c2 12227  ℕ₀cn0 12428

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370  ax-un 7682  ax-1cn 11087

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7363  df-om 7811  df-2nd 7936  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-nn 12166  df-2 12235  df-n0 12429

This theorem is referenced by:  nn0n0n1ge2  12496  7p6e13  12713  8p3e11  12716  8p5e13  12718  9p3e12  12723  9p4e13  12724  4t3e12  12733  4t4e16  12734  5t3e15  12736  5t5e25  12738  6t3e18  12740  6t5e30  12742  7t3e21  12745  7t4e28  12746  7t5e35  12747  7t6e42  12748  7t7e49  12749  8t3e24  12751  8t4e32  12752  8t5e40  12753  9t3e27  12758  9t4e36  12759  9t8e72  12763  9t9e81  12764  decbin3  12777  2eluzge0  12822  xnn0le2is012  13189  fzo0to42pr  13699  fvf1tp  13739  nn0sqcl  14042  sqmul  14072  resqcl  14077  zsqcl  14082  cu2  14153  i3  14156  i4  14157  binom3  14177  expmulnbnd  14188  nn0opthlem1  14221  fac3  14233  faclbnd2  14244  faclbnd4lem1  14246  faclbnd4lem3  14248  hash2pr  14422  hashtplei  14437  tpf1ofv2  14451  tpfo  14453  s4fv2  14850  pfx2  14900  repsw3  14904  swrd2lsw  14905  2swrd2eqwrdeq  14906  abssq  15259  sqabs  15260  iseraltlem2  15636  iseraltlem3  15637  bpoly2  16013  bpoly3  16014  bpoly4  16015  fsumcube  16016  ef4p  16071  efgt1p2  16072  efi4p  16095  ef01bndlem  16142  cos01bnd  16144  oexpneg  16305  oddge22np1  16309  bitsinv2  16403  bitsf1ocnv  16404  sadcaddlem  16417  sadadd2lem  16419  pythagtriplem4  16781  iserodd  16797  oddprmdvds  16865  prmreclem2  16879  prmreclem6  16883  vdwlem7  16949  vdwlem10  16952  vdwlem12  16954  dec2dvds  17025  dec5dvds  17026  2exp4  17046  2exp5  17047  2exp6  17048  2exp7  17049  2exp8  17050  2exp11  17051  2exp16  17052  3exp3  17053  2expltfac  17054  5prm  17070  7prm  17072  11prm  17076  13prm  17077  17prm  17078  19prm  17079  23prm  17080  prmlem2  17081  37prm  17082  43prm  17083  83prm  17084  139prm  17085  163prm  17086  317prm  17087  631prm  17088  1259lem1  17092  1259lem2  17093  1259lem3  17094  1259lem4  17095  1259lem5  17096  1259prm  17097  2503lem1  17098  2503lem2  17099  2503lem3  17100  2503prm  17101  4001lem1  17102  4001lem2  17103  4001lem3  17104  4001lem4  17105  4001prm  17106  basendxltdsndx  17342  dsndxnplusgndx  17344  dsndxnmulrndx  17345  slotsdnscsi  17346  dsndxntsetndx  17347  slotsdifdsndx  17348  slotsdifunifndx  17355  prdsvalstr  17406  smndex2dbas  18876  smndex2dlinvh  18879  pmtrprfval  19453  psgnunilem2  19461  efgredleme  19709  lt6abl  19861  cnfldstr  21346  cnfldstrOLD  21361  sqcn  24851  ehl2eudis  25399  dveflem  25956  iaa  26302  tangtx  26482  efif1olem3  26521  efif1olem4  26522  root1id  26731  2logb9irr  26772  mcubic  26824  cubic2  26825  cubic  26826  binom4  26827  dquartlem2  26829  dquart  26830  quart1cl  26831  quart1lem  26832  quart1  26833  quartlem1  26834  quartlem2  26835  atandmcj  26886  bndatandm  26906  atansopn  26909  atantayl3  26916  leibpilem2  26918  leibpi  26919  leibpisum  26920  log2cnv  26921  log2tlbnd  26922  log2ublem2  26924  log2ublem3  26925  log2ub  26926  log2le1  26927  birthday  26931  basellem3  27060  basellem4  27061  basellem5  27062  basellem8  27065  issqf  27113  ppi3  27148  ppiublem2  27180  chtublem  27188  mersenne  27204  bcmax  27255  bcp1ctr  27256  bclbnd  27257  bpos1  27260  bposlem6  27266  bposlem8  27268  lgslem1  27274  lgsqrlem2  27324  gausslemma2dlem6  27349  lgseisenlem4  27355  2lgslem1c  27370  2lgslem3a  27373  2lgslem3b  27374  2lgslem3c  27375  2lgslem3d  27376  2sq2  27410  2sqreultlem  27424  2sqreunnltlem  27427  chebbnd1lem3  27448  rplogsumlem2  27462  dchrisumlem2  27467  dchrisum0flblem1  27485  dchrisum0flblem2  27486  dchrisum0flb  27487  selberglem2  27523  pntrmax  27541  pntlemo  27584  slotsinbpsd  28523  slotslnbpsd  28524  trkgstr  28526  eengstr  29063  usgrexmplef  29342  upgr2wlk  29750  usgr2pthlem  29846  usgr2pth  29847  wpthswwlks2on  30047  elwspths2spth  30053  upgr3v3e3cycl  30265  upgr4cycl4dv4e  30270  konigsbergiedgw  30333  konigsberglem1  30337  konigsberglem2  30338  konigsberglem3  30339  clwlknon2num  30453  1kp2ke3k  30531  ex-mod  30534  ex-exp  30535  ex-fac  30536  9p10ne21  30555  ipidsq  30796  strlem3a  32338  xnn01gt  32858  expevenpos  32934  dpmul4  32988  pfxlsw2ccat  33025  wrdt2ind  33028  eufndx  33366  eufid  33367  evl1deg2  33652  evl1deg3  33653  fldext2rspun  33842  rtelextdg2lem  33886  rtelextdg2  33887  constrelextdg2  33907  2sqr3minply  33940  cos9thpiminplylem1  33942  cos9thpiminplylem2  33943  cos9thpiminplylem4  33945  cos9thpiminplylem5  33946  cos9thpinconstrlem1  33949  madjusmdetlem4  33990  coinflippv  34644  prodfzo03  34763  hgt750lemd  34808  hgt750lem  34811  hgt750lem2  34812  hgt750leme  34818  tgoldbachgnn  34819  tgoldbachgtde  34820  tgoldbachgt  34823  cusgredgex  35320  kur14lem8  35411  sinccvglem  35870  dvtan  38005  420gcd8e4  42459  12lcm5e60  42461  60lcm7e420  42463  lcmineqlem17  42498  lcmineqlem18  42499  lcmineqlem20  42501  lcmineqlem21  42502  lcmineqlem22  42503  lcmineqlem  42505  3exp7  42506  3lexlogpow5ineq1  42507  3lexlogpow5ineq2  42508  3lexlogpow2ineq1  42511  3lexlogpow2ineq2  42512  3lexlogpow5ineq5  42513  aks4d1p1p2  42523  aks4d1p1p7  42527  aks4d1p1p5  42528  aks4d1p1  42529  2np3bcnp1  42597  2ap1caineq  42598  aks6d1c7lem1  42633  sqn5i  42731  235t711  42751  ex-decpmul  42752  nicomachus  42758  dffltz  43081  flt4lem  43092  flt4lem3  43095  flt4lem7  43106  nna4b4nsq  43107  sum9cubes  43119  3cubeslem2  43131  3cubeslem3l  43132  3cubeslem3r  43133  diophin  43218  irrapxlem5  43272  pellexlem2  43276  pell1qrge1  43316  jm2.22  43441  jm2.20nn  43443  jm2.27c  43453  rmydioph  43460  rmxdioph  43462  expdiophlem2  43468  frlmpwfi  43544  isnumbasgrplem3  43551  resqrtvalex  44090  imsqrtvalex  44091  amgm2d  44643  dvdivbd  46369  itgsinexplem1  46400  itgsinexp  46401  stoweidlem1  46447  wallispilem4  46514  wallispilem5  46515  wallispi2lem2  46518  stirlinglem3  46522  stirlinglem5  46524  stirlinglem7  46526  stirlinglem8  46527  stirlinglem10  46529  stirlinglem11  46530  hoiqssbllem2  47069  nthrucw  47332  sin3t  47335  cos3t  47336  sin5tlem1  47337  sin5tlem2  47338  sin5tlem4  47340  fmtnoge3  48005  fmtnom1nn  48007  fmtnof1  48010  fmtnorec1  48012  sqrtpwpw2p  48013  fmtnosqrt  48014  fmtnorec2lem  48017  fmtnodvds  48019  fmtnorec3  48023  fmtnorec4  48024  fmtno2  48025  fmtno3  48026  fmtno5lem2  48029  fmtno5lem4  48031  fmtno5  48032  257prm  48036  odz2prm2pw  48038  fmtnoprmfac1lem  48039  fmtnoprmfac2lem1  48041  fmtnofac2lem  48043  fmtnofac2  48044  fmtnofac1  48045  fmtno4prmfac  48047  fmtno4nprmfac193  48049  fmtno4prm  48050  fmtno5faclem1  48054  fmtno5faclem2  48055  fmtno5faclem3  48056  fmtno5fac  48057  flsqrt  48068  139prmALT  48071  31prm  48072  m5prm  48073  127prm  48074  m7prm  48075  m11nprm  48076  sfprmdvdsmersenne  48078  lighneallem2  48081  lighneallem3  48082  lighneallem4a  48083  proththd  48089  3exp4mod41  48091  41prothprmlem1  48092  oexpnegALTV  48165  fppr2odd  48219  2exp340mod341  48221  341fppr2  48222  8exp8mod9  48224  nfermltl2rev  48231  evengpoap3  48287  tgblthelfgott  48303  tgoldbachlt  48304  tgoldbach  48305  cycl3grtri  48435  usgrexmpl1lem  48509  usgrexmpl2lem  48514  gpg3nbgrvtx0  48564  gpgprismgr4cycllem7  48589  gpgprismgr4cycllem10  48592  gpg5edgnedg  48618  pgrple2abl  48853  pgrpgt2nabl  48854  ply1mulgsumlem2  48875  logbpw2m1  49055  blenpw2m1  49067  dignn0ehalf  49105  nn0sumshdiglemA  49107  nn0sumshdiglemB  49108  nn0mullong  49113  2aryfvalel  49135  itcoval2  49152  itcoval3  49153  itcovalt2lem2lem2  49162  itcovalt2lem1  49163  ackval2  49170  ackval3  49171  ackval0012  49177  ackval1012  49178  ackval2012  49179  ackval3012  49180  ackval42  49184  2sphere  49237  itscnhlinecirc02plem3  49272  inlinecirc02p  49275  onetansqsecsq  50248  cotsqcscsq  50249