Theorem 2nn0 12616

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

This proof depends on syntax axioms:   ∈ wcel 2145  2c2 12390  ℕ₀cn0 12599

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-un 7749  ax-1cn 11251

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7421  df-om 7876  df-2nd 8000  df-frecs 8292  df-wrecs 8323  df-recs 8372  df-rdg 8411  df-nn 12329  df-2 12398  df-n0 12600

This theorem is used by:  nn0n0n1ge2  12667  12nn0  12824  25nn0  12826  7p6e13  12890  8p3e11  12893  8p5e13  12895  9p3e12  12900  9p4e13  12901  4t3e12  12910  4t4e16  12911  5t3e15  12913  5t5e25  12915  6t3e18  12917  6t5e30  12919  7t3e21  12922  7t4e28  12923  7t5e35  12924  7t6e42  12925  7t7e49  12926  8t3e24  12928  8t4e32  12929  8t5e40  12930  9t3e27  12935  9t4e36  12936  9t8e72  12940  9t9e81  12941  2lt10  12951  decbin3  12956  2eluzge0  13001  xnn0le2is012  13369  fzo0to42pr  13881  fvf1tp  13922  nn0sqcl  14225  sqmul  14255  resqcl  14260  zsqcl  14265  cu2  14336  exp4sqsq  14337  i3  14340  i4  14341  binom3  14361  expmulnbnd  14372  nn0opthlem1  14405  fac3  14417  faclbnd2  14428  faclbnd4lem1  14430  faclbnd4lem3  14432  hash2pr  14607  hashtplei  14622  tpf1ofv2  14636  tpfo  14638  s4fv2  15041  pfx2  15091  repsw3  15097  swrd2lsw  15098  2swrd2eqwrdeq  15099  abssq  15466  sqabs  15467  iseraltlem2  15843  iseraltlem3  15844  bpoly2  16216  bpoly3  16217  bpoly4  16218  fsumcube  16219  ef4p  16274  efgt1p2  16275  efi4p  16298  ef01bndlem  16345  cos01bnd  16347  oexpneg  16508  oddge22np1  16512  bitsinv2  16606  bitsf1ocnv  16607  sadcaddlem  16620  sadadd2lem  16622  pythagtriplem4  16990  iserodd  17006  oddprmdvds  17074  prmreclem2  17088  prmreclem6  17092  vdwlem7  17158  vdwlem10  17161  vdwlem12  17163  dec2dvds  17234  dec5dvds  17235  2exp4  17255  2exp5  17256  2exp6  17257  2exp7  17258  2exp8  17259  2exp11  17260  2exp16  17261  3exp3  17262  2expltfac  17263  5prm  17279  7prm  17281  11prm  17286  13prm  17287  17prm  17288  19prm  17289  23prm  17290  prmlem2  17291  37prm  17292  43prm  17293  83prm  17294  139prm  17295  163prm  17296  317prm  17297  631prm  17298  1259lem1  17302  1259lem2  17303  1259lem3  17304  1259lem4  17305  1259lem5  17306  1259prm  17307  2503lem1  17308  2503lem2  17309  2503lem3  17310  2503prm  17311  4001lem1  17312  4001lem2  17313  4001lem3  17314  4001lem4  17315  4001prm  17316  basendxltdsndx  17552  dsndxnplusgndx  17554  dsndxnmulrndx  17555  slotsdnscsi  17556  dsndxntsetndx  17557  slotsdifdsndx  17558  slotsdifunifndx  17565  prdsvalstr  17616  smndex2dbas  19106  smndex2dlinvh  19109  pmtrprfval  19694  psgnunilem2  19702  efgredleme  19950  lt6abl  20102  cnfldstr  21673  sqcn  25188  ehl2eudis  25736  dveflem  26292  iaa  26644  iaaOLD  26645  tangtx  26827  efif1olem3  26865  efif1olem4  26866  root1id  27075  2logb9irr  27116  mcubic  27168  cubic2  27169  cubic  27170  binom4  27171  dquartlem2  27173  dquart  27174  quart1lem  27176  quart1  27177  quartlem1  27178  quartlem2  27179  atandmcj  27230  bndatandm  27250  atansopn  27253  atantayl3  27260  leibpilem2  27262  leibpi  27263  leibpisum  27264  log2cnv  27265  log2tlbnd  27266  log2ublem2  27268  log2ublem3  27269  log2ub  27270  log2le1  27271  birthday  27275  basellem3  27403  basellem4  27404  basellem5  27405  basellem8  27408  issqf  27456  ppi3  27491  ppiublem2  27523  chtublem  27531  mersenne  27547  bcmax  27598  bcp1ctr  27599  bclbnd  27600  bpos1  27603  bposlem6  27609  bposlem8  27611  lgslem1  27617  lgsqrlem2  27667  gausslemma2dlem6  27692  lgseisenlem4  27698  2lgslem1c  27713  2lgslem3a  27716  2lgslem3b  27717  2lgslem3c  27718  2lgslem3d  27719  2sq2  27753  2sqreultlem  27767  2sqreunnltlem  27770  chebbnd1lem3  27791  rplogsumlem2  27805  dchrisumlem2  27810  dchrisum0flblem1  27828  dchrisum0flblem2  27829  dchrisum0flb  27830  selberglem2  27866  pntrmax  27884  pntlemo  27927  flt4lem3  27971  flt4lem7  27982  nna4b4nsq  27983  fltoprmlem2  27987  slotsinbpsd  28896  slotslnbpsd  28897  trkgstr  28899  eengstr  29551  usgrexmplef  29833  upgr2wlk  30240  usgr2pthlem  30342  usgr2pth  30343  wpthswwlks2on  30546  elwspths2spth  30552  upgr3v3e3cycl  30774  upgr4cycl4dv4e  30779  konigsbergiedgw  30842  konigsberglem1  30846  konigsberglem2  30847  konigsberglem3  30848  clwlknon2num  30962  1kp2ke3k  31040  ex-mod  31043  ex-exp  31044  ex-fac  31045  9p10ne21  31064  ipidsq  31305  strlem3a  32847  xnn01gt  33355  expevenpos  33419  dpmul4  33473  pfxlsw2ccat  33506  wrdt2ind  33509  eufndx  33847  eufid  33848  evl1deg2  34102  evl1deg3  34103  fldext2rspun  34307  rtelextdg2lem  34351  rtelextdg2  34352  constrelextdg2  34372  2sqr3minply  34405  cos9thpiminplylem1  34407  cos9thpiminplylem2  34408  cos9thpiminplylem4  34410  cos9thpiminplylem5  34411  cos9thpinconstrlem1  34414  madjusmdetlem4  34455  coinflippv  35109  prodfzo03  35225  hgt750lemd  35270  hgt750lem  35273  hgt750lem2  35274  hgt750leme  35280  tgoldbachgnn  35281  tgoldbachgtde  35282  tgoldbachgt  35285  cusgredgex  35885  kur14lem8  35957  sinccvglem  36416  dvtan  38568  420gcd8e4  43036  12lcm5e60  43038  60lcm7e420  43040  lcmineqlem17  43075  lcmineqlem18  43076  lcmineqlem20  43078  lcmineqlem21  43079  lcmineqlem22  43080  lcmineqlem  43082  3exp7  43083  3lexlogpow5ineq1  43084  3lexlogpow5ineq2  43085  3lexlogpow2ineq1  43088  3lexlogpow2ineq2  43089  3lexlogpow5ineq5  43090  aks4d1p1p2  43100  aks4d1p1p7  43104  aks4d1p1p5  43105  aks4d1p1  43106  2np3bcnp1  43174  2ap1caineq  43175  aks6d1c7lem1  43210  25or6to4  43236  sqn5i  43322  235t711  43342  ex-decpmul  43343  nicomachus  43349  dffltz  43650  sum9cubes  43663  3cubeslem2  43675  3cubeslem3l  43676  3cubeslem3r  43677  diophin  43762  irrapxlem5  43812  pellexlem2  43816  pell1qrge1  43856  jm2.22  43981  jm2.20nn  43983  jm2.27c  43993  rmydioph  44000  rmxdioph  44002  expdiophlem2  44008  frlmpwfi  44084  isnumbasgrplem3  44091  resqrtvalex  44630  imsqrtvalex  44631  amgm2d  45183  dvdivbd  46902  itgsinexplem1  46933  itgsinexp  46934  stoweidlem1  46980  wallispilem4  47047  wallispilem5  47048  wallispi2lem2  47051  stirlinglem3  47055  stirlinglem5  47057  stirlinglem7  47059  stirlinglem8  47060  stirlinglem10  47062  stirlinglem11  47063  hoiqssbllem2  47602  sqrtnnaa  47882  sqrtnzqaa  47883  sin3t  47886  cos3t  47887  sin5tlem1  47888  sin5tlem2  47889  sin5tlem4  47891  goldpolyfactor  47896  sqrtnpoly  47912  fmtnoge3  48584  fmtnom1nn  48586  fmtnof1  48589  fmtnorec1  48591  sqrtpwpw2p  48592  fmtnosqrt  48593  fmtnorec2lem  48596  fmtnodvds  48598  fmtnorec3  48602  fmtnorec4  48603  fmtno2  48604  fmtno3  48605  fmtno5lem2  48608  fmtno5lem4  48610  fmtno5  48611  257prm  48615  odz2prm2pw  48617  fmtnoprmfac1lem  48618  fmtnoprmfac2lem1  48620  fmtnofac2lem  48622  fmtnofac2  48623  fmtnofac1  48624  fmtno4prmfac  48626  fmtno4nprmfac193  48628  fmtno4prm  48629  fmtno5faclem1  48633  fmtno5faclem2  48634  fmtno5faclem3  48635  fmtno5fac  48636  flsqrt  48647  139prmALT  48650  31prm  48651  m5prm  48652  127prm  48653  m7prm  48654  m11nprm  48655  sfprmdvdsmersenne  48657  lighneallem2  48660  lighneallem3  48661  lighneallem4a  48662  proththd  48668  3exp4mod41  48670  41prothprmlem1  48671  oexpnegALTV  48744  fppr2odd  48798  2exp340mod341  48800  341fppr2  48801  8exp8mod9  48803  nfermltl2rev  48810  evengpoap3  48866  tgblthelfgott  48882  tgoldbachlt  48883  tgoldbach  48884  cycl3grtri  49014  usgrexmpl1lem  49088  usgrexmpl2lem  49093  gpg3nbgrvtx0  49143  gpgprismgr4cycllem7  49168  gpgprismgr4cycllem10  49171  gpg5edgnedg  49197  pgrple2abl  49446  pgrpgt2nabl  49447  ply1mulgsumlem2  49468  logbpw2m1  49648  blenpw2m1  49660  dignn0ehalf  49698  nn0sumshdiglemA  49700  nn0sumshdiglemB  49701  nn0mullong  49706  2aryfvalel  49728  itcoval2  49745  itcoval3  49746  itcovalt2lem2lem2  49755  itcovalt2lem1  49756  ackval2  49763  ackval3  49764  ackval0012  49770  ackval1012  49771  ackval2012  49772  ackval3012  49773  ackval42  49777  2sphere  49830  itscnhlinecirc02plem3  49865  inlinecirc02p  49868  onetansqsecsq  50823  cotsqcscsq  50824