Theorem 2nn0 12532

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

This proof depends on syntax axioms:   ∈ wcel 2146  2c2 12306  ℕ₀cn0 12515

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406  ax-un 7738  ax-1cn 11169

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7419  df-om 7865  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-nn 12245  df-2 12314  df-n0 12516

This theorem is used by:  nn0n0n1ge2  12583  12nn0  12739  25nn0  12741  7p6e13  12805  8p3e11  12808  8p5e13  12810  9p3e12  12815  9p4e13  12816  4t3e12  12825  4t4e16  12826  5t3e15  12828  5t5e25  12830  6t3e18  12832  6t5e30  12834  7t3e21  12837  7t4e28  12838  7t5e35  12839  7t6e42  12840  7t7e49  12841  8t3e24  12843  8t4e32  12844  8t5e40  12845  9t3e27  12850  9t4e36  12851  9t8e72  12855  9t9e81  12856  2lt10  12866  decbin3  12871  2eluzge0  12916  xnn0le2is012  13283  fzo0to42pr  13794  fvf1tp  13835  nn0sqcl  14138  sqmul  14168  resqcl  14173  zsqcl  14178  cu2  14249  i3  14252  i4  14253  binom3  14273  expmulnbnd  14284  nn0opthlem1  14317  fac3  14329  faclbnd2  14340  faclbnd4lem1  14342  faclbnd4lem3  14344  hash2pr  14519  hashtplei  14534  tpf1ofv2  14548  tpfo  14550  s4fv2  14953  pfx2  15003  repsw3  15007  swrd2lsw  15008  2swrd2eqwrdeq  15009  abssq  15376  sqabs  15377  iseraltlem2  15753  iseraltlem3  15754  bpoly2  16128  bpoly3  16129  bpoly4  16130  fsumcube  16131  ef4p  16186  efgt1p2  16187  efi4p  16210  ef01bndlem  16257  cos01bnd  16259  oexpneg  16420  oddge22np1  16424  bitsinv2  16518  bitsf1ocnv  16519  sadcaddlem  16532  sadadd2lem  16534  pythagtriplem4  16896  iserodd  16912  oddprmdvds  16980  prmreclem2  16994  prmreclem6  16998  vdwlem7  17064  vdwlem10  17067  vdwlem12  17069  dec2dvds  17140  dec5dvds  17141  2exp4  17161  2exp5  17162  2exp6  17163  2exp7  17164  2exp8  17165  2exp11  17166  2exp16  17167  3exp3  17168  2expltfac  17169  5prm  17185  7prm  17187  11prm  17192  13prm  17193  17prm  17194  19prm  17195  23prm  17196  prmlem2  17197  37prm  17198  43prm  17199  83prm  17200  139prm  17201  163prm  17202  317prm  17203  631prm  17204  1259lem1  17208  1259lem2  17209  1259lem3  17210  1259lem4  17211  1259lem5  17212  1259prm  17213  2503lem1  17214  2503lem2  17215  2503lem3  17216  2503prm  17217  4001lem1  17218  4001lem2  17219  4001lem3  17220  4001lem4  17221  4001prm  17222  basendxltdsndx  17458  dsndxnplusgndx  17460  dsndxnmulrndx  17461  slotsdnscsi  17462  dsndxntsetndx  17463  slotsdifdsndx  17464  slotsdifunifndx  17471  prdsvalstr  17522  smndex2dbas  18999  smndex2dlinvh  19002  pmtrprfval  19580  psgnunilem2  19588  efgredleme  19836  lt6abl  19988  cnfldstr  21553  sqcn  25062  ehl2eudis  25610  dveflem  26167  iaa  26517  tangtx  26699  efif1olem3  26738  efif1olem4  26739  root1id  26948  2logb9irr  26989  mcubic  27041  cubic2  27042  cubic  27043  binom4  27044  dquartlem2  27046  dquart  27047  quart1lem  27049  quart1  27050  quartlem1  27051  quartlem2  27052  atandmcj  27103  bndatandm  27123  atansopn  27126  atantayl3  27133  leibpilem2  27135  leibpi  27136  leibpisum  27137  log2cnv  27138  log2tlbnd  27139  log2ublem2  27141  log2ublem3  27142  log2ub  27143  log2le1  27144  birthday  27148  basellem3  27276  basellem4  27277  basellem5  27278  basellem8  27281  issqf  27329  ppi3  27364  ppiublem2  27396  chtublem  27404  mersenne  27420  bcmax  27471  bcp1ctr  27472  bclbnd  27473  bpos1  27476  bposlem6  27482  bposlem8  27484  lgslem1  27490  lgsqrlem2  27540  gausslemma2dlem6  27565  lgseisenlem4  27571  2lgslem1c  27586  2lgslem3a  27589  2lgslem3b  27590  2lgslem3c  27591  2lgslem3d  27592  2sq2  27626  2sqreultlem  27640  2sqreunnltlem  27643  chebbnd1lem3  27664  rplogsumlem2  27678  dchrisumlem2  27683  dchrisum0flblem1  27701  dchrisum0flblem2  27702  dchrisum0flb  27703  selberglem2  27739  pntrmax  27757  pntlemo  27800  slotsinbpsd  28739  slotslnbpsd  28740  trkgstr  28742  eengstr  29359  usgrexmplef  29638  upgr2wlk  30045  usgr2pthlem  30141  usgr2pth  30142  wpthswwlks2on  30342  elwspths2spth  30348  upgr3v3e3cycl  30560  upgr4cycl4dv4e  30565  konigsbergiedgw  30628  konigsberglem1  30632  konigsberglem2  30633  konigsberglem3  30634  clwlknon2num  30748  1kp2ke3k  30826  ex-mod  30829  ex-exp  30830  ex-fac  30831  9p10ne21  30850  ipidsq  31091  strlem3a  32633  xnn01gt  33144  expevenpos  33208  dpmul4  33262  pfxlsw2ccat  33295  wrdt2ind  33298  eufndx  33636  eufid  33637  evl1deg2  33890  evl1deg3  33891  fldext2rspun  34095  rtelextdg2lem  34139  rtelextdg2  34140  constrelextdg2  34160  2sqr3minply  34193  cos9thpiminplylem1  34195  cos9thpiminplylem2  34196  cos9thpiminplylem4  34198  cos9thpiminplylem5  34199  cos9thpinconstrlem1  34202  madjusmdetlem4  34243  coinflippv  34898  prodfzo03  35014  hgt750lemd  35059  hgt750lem  35062  hgt750lem2  35063  hgt750leme  35069  tgoldbachgnn  35070  tgoldbachgtde  35071  tgoldbachgt  35074  cusgredgex  35627  kur14lem8  35718  sinccvglem  36177  dvtan  38354  420gcd8e4  42806  12lcm5e60  42808  60lcm7e420  42810  lcmineqlem17  42845  lcmineqlem18  42846  lcmineqlem20  42848  lcmineqlem21  42849  lcmineqlem22  42850  lcmineqlem  42852  3exp7  42853  3lexlogpow5ineq1  42854  3lexlogpow5ineq2  42855  3lexlogpow2ineq1  42858  3lexlogpow2ineq2  42859  3lexlogpow5ineq5  42860  aks4d1p1p2  42870  aks4d1p1p7  42874  aks4d1p1p5  42875  aks4d1p1  42876  2np3bcnp1  42944  2ap1caineq  42945  aks6d1c7lem1  42980  25or6to4  43006  sqn5i  43079  235t711  43099  ex-decpmul  43100  nicomachus  43106  dffltz  43399  flt4lem  43410  flt4lem3  43413  flt4lem7  43424  nna4b4nsq  43425  sum9cubes  43437  3cubeslem2  43449  3cubeslem3l  43450  3cubeslem3r  43451  diophin  43536  irrapxlem5  43586  pellexlem2  43590  pell1qrge1  43630  jm2.22  43755  jm2.20nn  43757  jm2.27c  43767  rmydioph  43774  rmxdioph  43776  expdiophlem2  43782  frlmpwfi  43858  isnumbasgrplem3  43865  resqrtvalex  44404  imsqrtvalex  44405  amgm2d  44957  dvdivbd  46670  itgsinexplem1  46701  itgsinexp  46702  stoweidlem1  46748  wallispilem4  46815  wallispilem5  46816  wallispi2lem2  46819  stirlinglem3  46823  stirlinglem5  46825  stirlinglem7  46827  stirlinglem8  46828  stirlinglem10  46830  stirlinglem11  46831  hoiqssbllem2  47370  sqrtnnaa  47637  sqrtnzqaa  47638  sin3t  47641  cos3t  47642  sin5tlem1  47643  sin5tlem2  47644  sin5tlem4  47646  fmtnoge3  48315  fmtnom1nn  48317  fmtnof1  48320  fmtnorec1  48322  sqrtpwpw2p  48323  fmtnosqrt  48324  fmtnorec2lem  48327  fmtnodvds  48329  fmtnorec3  48333  fmtnorec4  48334  fmtno2  48335  fmtno3  48336  fmtno5lem2  48339  fmtno5lem4  48341  fmtno5  48342  257prm  48346  odz2prm2pw  48348  fmtnoprmfac1lem  48349  fmtnoprmfac2lem1  48351  fmtnofac2lem  48353  fmtnofac2  48354  fmtnofac1  48355  fmtno4prmfac  48357  fmtno4nprmfac193  48359  fmtno4prm  48360  fmtno5faclem1  48364  fmtno5faclem2  48365  fmtno5faclem3  48366  fmtno5fac  48367  flsqrt  48378  139prmALT  48381  31prm  48382  m5prm  48383  127prm  48384  m7prm  48385  m11nprm  48386  sfprmdvdsmersenne  48388  lighneallem2  48391  lighneallem3  48392  lighneallem4a  48393  proththd  48399  3exp4mod41  48401  41prothprmlem1  48402  oexpnegALTV  48475  fppr2odd  48529  2exp340mod341  48531  341fppr2  48532  8exp8mod9  48534  nfermltl2rev  48541  evengpoap3  48597  tgblthelfgott  48613  tgoldbachlt  48614  tgoldbach  48615  cycl3grtri  48745  usgrexmpl1lem  48819  usgrexmpl2lem  48824  gpg3nbgrvtx0  48874  gpgprismgr4cycllem7  48899  gpgprismgr4cycllem10  48902  gpg5edgnedg  48928  pgrple2abl  49178  pgrpgt2nabl  49179  ply1mulgsumlem2  49200  logbpw2m1  49380  blenpw2m1  49392  dignn0ehalf  49430  nn0sumshdiglemA  49432  nn0sumshdiglemB  49433  nn0mullong  49438  2aryfvalel  49460  itcoval2  49477  itcoval3  49478  itcovalt2lem2lem2  49487  itcovalt2lem1  49488  ackval2  49495  ackval3  49496  ackval0012  49502  ackval1012  49503  ackval2012  49504  ackval3012  49505  ackval42  49509  2sphere  49562  itscnhlinecirc02plem3  49597  inlinecirc02p  49600  onetansqsecsq  50572  cotsqcscsq  50573