Theorem 2nn0 12435

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

Syntax hints:   ∈ wcel 2109  2c2 12217  ℕ₀cn0 12418

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 5246  ax-nul 5256  ax-pr 5382  ax-un 7691  ax-1cn 11102

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 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-ov 7372  df-om 7823  df-2nd 7948  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-nn 12163  df-2 12225  df-n0 12419

This theorem is referenced by:  nn0n0n1ge2  12486  7p6e13  12703  8p3e11  12706  8p5e13  12708  9p3e12  12713  9p4e13  12714  4t3e12  12723  4t4e16  12724  5t3e15  12726  5t5e25  12728  6t3e18  12730  6t5e30  12732  7t3e21  12735  7t4e28  12736  7t5e35  12737  7t6e42  12738  7t7e49  12739  8t3e24  12741  8t4e32  12742  8t5e40  12743  9t3e27  12748  9t4e36  12749  9t8e72  12753  9t9e81  12754  decbin3  12767  2eluzge0  12816  xnn0le2is012  13182  fzo0to42pr  13690  fvf1tp  13727  nn0sqcl  14030  sqmul  14060  resqcl  14065  zsqcl  14070  cu2  14141  i3  14144  i4  14145  binom3  14165  expmulnbnd  14176  nn0opthlem1  14209  fac3  14221  faclbnd2  14232  faclbnd4lem1  14234  faclbnd4lem3  14236  hash2pr  14410  hashtplei  14425  tpf1ofv2  14439  tpfo  14441  s4fv2  14839  pfx2  14889  repsw3  14893  swrd2lsw  14894  2swrd2eqwrdeq  14895  abssq  15248  sqabs  15249  iseraltlem2  15625  iseraltlem3  15626  bpoly2  15999  bpoly3  16000  bpoly4  16001  fsumcube  16002  ef4p  16057  efgt1p2  16058  efi4p  16081  ef01bndlem  16128  cos01bnd  16130  oexpneg  16291  oddge22np1  16295  bitsinv2  16389  bitsf1ocnv  16390  sadcaddlem  16403  sadadd2lem  16405  pythagtriplem4  16766  iserodd  16782  oddprmdvds  16850  prmreclem2  16864  prmreclem6  16868  vdwlem7  16934  vdwlem10  16937  vdwlem12  16939  dec2dvds  17010  dec5dvds  17011  2exp4  17031  2exp5  17032  2exp6  17033  2exp7  17034  2exp8  17035  2exp11  17036  2exp16  17037  3exp3  17038  2expltfac  17039  5prm  17055  7prm  17057  11prm  17061  13prm  17062  17prm  17063  19prm  17064  23prm  17065  prmlem2  17066  37prm  17067  43prm  17068  83prm  17069  139prm  17070  163prm  17071  317prm  17072  631prm  17073  1259lem1  17077  1259lem2  17078  1259lem3  17079  1259lem4  17080  1259lem5  17081  1259prm  17082  2503lem1  17083  2503lem2  17084  2503lem3  17085  2503prm  17086  4001lem1  17087  4001lem2  17088  4001lem3  17089  4001lem4  17090  4001prm  17091  basendxltdsndx  17327  dsndxnplusgndx  17329  dsndxnmulrndx  17330  slotsdnscsi  17331  dsndxntsetndx  17332  slotsdifdsndx  17333  slotsdifunifndx  17340  prdsvalstr  17391  smndex2dbas  18817  smndex2dlinvh  18820  pmtrprfval  19393  psgnunilem2  19401  efgredleme  19649  lt6abl  19801  cnfldstr  21242  cnfldstrOLD  21257  sqcn  24743  ehl2eudis  25298  dveflem  25859  iaa  26209  tangtx  26390  efif1olem3  26429  efif1olem4  26430  root1id  26640  2logb9irr  26681  mcubic  26733  cubic2  26734  cubic  26735  binom4  26736  dquartlem2  26738  dquart  26739  quart1cl  26740  quart1lem  26741  quart1  26742  quartlem1  26743  quartlem2  26744  atandmcj  26795  bndatandm  26815  atansopn  26818  atantayl3  26825  leibpilem2  26827  leibpi  26828  leibpisum  26829  log2cnv  26830  log2tlbnd  26831  log2ublem2  26833  log2ublem3  26834  log2ub  26835  log2le1  26836  birthday  26840  basellem3  26969  basellem4  26970  basellem5  26971  basellem8  26974  issqf  27022  ppi3  27057  ppiublem2  27090  chtublem  27098  mersenne  27114  bcmax  27165  bcp1ctr  27166  bclbnd  27167  bpos1  27170  bposlem6  27176  bposlem8  27178  lgslem1  27184  lgsqrlem2  27234  gausslemma2dlem6  27259  lgseisenlem4  27265  2lgslem1c  27280  2lgslem3a  27283  2lgslem3b  27284  2lgslem3c  27285  2lgslem3d  27286  2sq2  27320  2sqreultlem  27334  2sqreunnltlem  27337  chebbnd1lem3  27358  rplogsumlem2  27372  dchrisumlem2  27377  dchrisum0flblem1  27395  dchrisum0flblem2  27396  dchrisum0flb  27397  selberglem2  27433  pntrmax  27451  pntlemo  27494  slotsinbpsd  28344  slotslnbpsd  28345  trkgstr  28347  eengstr  28883  usgrexmplef  29162  upgr2wlk  29570  usgr2pthlem  29666  usgr2pth  29667  wpthswwlks2on  29864  elwspths2spth  29870  upgr3v3e3cycl  30082  upgr4cycl4dv4e  30087  konigsbergiedgw  30150  konigsberglem1  30154  konigsberglem2  30155  konigsberglem3  30156  clwlknon2num  30270  1kp2ke3k  30348  ex-mod  30351  ex-exp  30352  ex-fac  30353  9p10ne21  30372  ipidsq  30612  strlem3a  32154  xnn01gt  32666  expevenpos  32744  dpmul4  32807  pfxlsw2ccat  32845  wrdt2ind  32848  eufndx  33213  eufid  33214  evl1deg2  33519  evl1deg3  33520  fldext2rspun  33650  rtelextdg2lem  33689  rtelextdg2  33690  constrelextdg2  33710  2sqr3minply  33743  cos9thpiminplylem1  33745  cos9thpiminplylem2  33746  cos9thpiminplylem4  33748  cos9thpiminplylem5  33749  cos9thpinconstrlem1  33752  madjusmdetlem4  33793  coinflippv  34448  prodfzo03  34567  hgt750lemd  34612  hgt750lem  34615  hgt750lem2  34616  hgt750leme  34622  tgoldbachgnn  34623  tgoldbachgtde  34624  tgoldbachgt  34627  cusgredgex  35082  kur14lem8  35173  sinccvglem  35632  dvtan  37637  420gcd8e4  41967  12lcm5e60  41969  60lcm7e420  41971  lcmineqlem17  42006  lcmineqlem18  42007  lcmineqlem20  42009  lcmineqlem21  42010  lcmineqlem22  42011  lcmineqlem  42013  3exp7  42014  3lexlogpow5ineq1  42015  3lexlogpow5ineq2  42016  3lexlogpow2ineq1  42019  3lexlogpow2ineq2  42020  3lexlogpow5ineq5  42021  aks4d1p1p2  42031  aks4d1p1p7  42035  aks4d1p1p5  42036  aks4d1p1  42037  2np3bcnp1  42105  2ap1caineq  42106  aks6d1c7lem1  42141  sqn5i  42246  235t711  42266  ex-decpmul  42267  nicomachus  42273  dffltz  42595  flt4lem  42606  flt4lem3  42609  flt4lem7  42620  nna4b4nsq  42621  sum9cubes  42633  3cubeslem2  42646  3cubeslem3l  42647  3cubeslem3r  42648  diophin  42733  irrapxlem5  42787  pellexlem2  42791  pell1qrge1  42831  jm2.22  42957  jm2.20nn  42959  jm2.27c  42969  rmydioph  42976  rmxdioph  42978  expdiophlem2  42984  frlmpwfi  43060  isnumbasgrplem3  43067  resqrtvalex  43607  imsqrtvalex  43608  amgm2d  44160  dvdivbd  45894  itgsinexplem1  45925  itgsinexp  45926  stoweidlem1  45972  wallispilem4  46039  wallispilem5  46040  wallispi2lem2  46043  stirlinglem3  46047  stirlinglem5  46049  stirlinglem7  46051  stirlinglem8  46052  stirlinglem10  46054  stirlinglem11  46055  hoiqssbllem2  46594  fmtnoge3  47504  fmtnom1nn  47506  fmtnof1  47509  fmtnorec1  47511  sqrtpwpw2p  47512  fmtnosqrt  47513  fmtnorec2lem  47516  fmtnodvds  47518  fmtnorec3  47522  fmtnorec4  47523  fmtno2  47524  fmtno3  47525  fmtno5lem2  47528  fmtno5lem4  47530  fmtno5  47531  257prm  47535  odz2prm2pw  47537  fmtnoprmfac1lem  47538  fmtnoprmfac2lem1  47540  fmtnofac2lem  47542  fmtnofac2  47543  fmtnofac1  47544  fmtno4prmfac  47546  fmtno4nprmfac193  47548  fmtno4prm  47549  fmtno5faclem1  47553  fmtno5faclem2  47554  fmtno5faclem3  47555  fmtno5fac  47556  flsqrt  47567  139prmALT  47570  31prm  47571  m5prm  47572  127prm  47573  m7prm  47574  m11nprm  47575  sfprmdvdsmersenne  47577  lighneallem2  47580  lighneallem3  47581  lighneallem4a  47582  proththd  47588  3exp4mod41  47590  41prothprmlem1  47591  oexpnegALTV  47651  fppr2odd  47705  2exp340mod341  47707  341fppr2  47708  8exp8mod9  47710  nfermltl2rev  47717  evengpoap3  47773  tgblthelfgott  47789  tgoldbachlt  47790  tgoldbach  47791  cycl3grtri  47919  usgrexmpl1lem  47985  usgrexmpl2lem  47990  gpg3nbgrvtx0  48040  gpgprismgr4cycllem7  48064  gpgprismgr4cycllem10  48067  pgrple2abl  48326  pgrpgt2nabl  48327  ply1mulgsumlem2  48349  logbpw2m1  48529  blenpw2m1  48541  dignn0ehalf  48579  nn0sumshdiglemA  48581  nn0sumshdiglemB  48582  nn0mullong  48587  2aryfvalel  48609  itcoval2  48626  itcoval3  48627  itcovalt2lem2lem2  48636  itcovalt2lem1  48637  ackval2  48644  ackval3  48645  ackval0012  48651  ackval1012  48652  ackval2012  48653  ackval3012  48654  ackval42  48658  2sphere  48711  itscnhlinecirc02plem3  48746  inlinecirc02p  48749  onetansqsecsq  49723  cotsqcscsq  49724