Theorem 2nn0 12522

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

Syntax hints:   ∈ wcel 2143  2c2 12296  ℕ₀cn0 12505

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pr 5406  ax-un 7734  ax-1cn 11159

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  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 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7415  df-om 7864  df-2nd 7988  df-frecs 8279  df-wrecs 8310  df-recs 8359  df-rdg 8398  df-nn 12235  df-2 12304  df-n0 12506

This theorem is referenced by:  nn0n0n1ge2  12573  12nn0  12729  25nn0  12731  7p6e13  12795  8p3e11  12798  8p5e13  12800  9p3e12  12805  9p4e13  12806  4t3e12  12815  4t4e16  12816  5t3e15  12818  5t5e25  12820  6t3e18  12822  6t5e30  12824  7t3e21  12827  7t4e28  12828  7t5e35  12829  7t6e42  12830  7t7e49  12831  8t3e24  12833  8t4e32  12834  8t5e40  12835  9t3e27  12840  9t4e36  12841  9t8e72  12845  9t9e81  12846  2lt10  12856  decbin3  12861  2eluzge0  12906  xnn0le2is012  13273  fzo0to42pr  13784  fvf1tp  13824  nn0sqcl  14127  sqmul  14157  resqcl  14162  zsqcl  14167  cu2  14238  i3  14241  i4  14242  binom3  14262  expmulnbnd  14273  nn0opthlem1  14306  fac3  14318  faclbnd2  14329  faclbnd4lem1  14331  faclbnd4lem3  14333  hash2pr  14508  hashtplei  14523  tpf1ofv2  14537  tpfo  14539  s4fv2  14936  pfx2  14986  repsw3  14990  swrd2lsw  14991  2swrd2eqwrdeq  14992  abssq  15359  sqabs  15360  iseraltlem2  15736  iseraltlem3  15737  bpoly2  16112  bpoly3  16113  bpoly4  16114  fsumcube  16115  ef4p  16170  efgt1p2  16171  efi4p  16194  ef01bndlem  16241  cos01bnd  16243  oexpneg  16404  oddge22np1  16408  bitsinv2  16502  bitsf1ocnv  16503  sadcaddlem  16516  sadadd2lem  16518  pythagtriplem4  16880  iserodd  16896  oddprmdvds  16964  prmreclem2  16978  prmreclem6  16982  vdwlem7  17048  vdwlem10  17051  vdwlem12  17053  dec2dvds  17124  dec5dvds  17125  2exp4  17145  2exp5  17146  2exp6  17147  2exp7  17148  2exp8  17149  2exp11  17150  2exp16  17151  3exp3  17152  2expltfac  17153  5prm  17169  7prm  17171  11prm  17176  13prm  17177  17prm  17178  19prm  17179  23prm  17180  prmlem2  17181  37prm  17182  43prm  17183  83prm  17184  139prm  17185  163prm  17186  317prm  17187  631prm  17188  1259lem1  17192  1259lem2  17193  1259lem3  17194  1259lem4  17195  1259lem5  17196  1259prm  17197  2503lem1  17198  2503lem2  17199  2503lem3  17200  2503prm  17201  4001lem1  17202  4001lem2  17203  4001lem3  17204  4001lem4  17205  4001prm  17206  basendxltdsndx  17442  dsndxnplusgndx  17444  dsndxnmulrndx  17445  slotsdnscsi  17446  dsndxntsetndx  17447  slotsdifdsndx  17448  slotsdifunifndx  17455  prdsvalstr  17506  smndex2dbas  18977  smndex2dlinvh  18980  pmtrprfval  19558  psgnunilem2  19566  efgredleme  19814  lt6abl  19966  cnfldstr  21505  sqcn  25014  ehl2eudis  25562  dveflem  26119  iaa  26469  tangtx  26651  efif1olem3  26690  efif1olem4  26691  root1id  26900  2logb9irr  26941  mcubic  26993  cubic2  26994  cubic  26995  binom4  26996  dquartlem2  26998  dquart  26999  quart1lem  27001  quart1  27002  quartlem1  27003  quartlem2  27004  atandmcj  27055  bndatandm  27075  atansopn  27078  atantayl3  27085  leibpilem2  27087  leibpi  27088  leibpisum  27089  log2cnv  27090  log2tlbnd  27091  log2ublem2  27093  log2ublem3  27094  log2ub  27095  log2le1  27096  birthday  27100  basellem3  27228  basellem4  27229  basellem5  27230  basellem8  27233  issqf  27281  ppi3  27316  ppiublem2  27348  chtublem  27356  mersenne  27372  bcmax  27423  bcp1ctr  27424  bclbnd  27425  bpos1  27428  bposlem6  27434  bposlem8  27436  lgslem1  27442  lgsqrlem2  27492  gausslemma2dlem6  27517  lgseisenlem4  27523  2lgslem1c  27538  2lgslem3a  27541  2lgslem3b  27542  2lgslem3c  27543  2lgslem3d  27544  2sq2  27578  2sqreultlem  27592  2sqreunnltlem  27595  chebbnd1lem3  27616  rplogsumlem2  27630  dchrisumlem2  27635  dchrisum0flblem1  27653  dchrisum0flblem2  27654  dchrisum0flb  27655  selberglem2  27691  pntrmax  27709  pntlemo  27752  slotsinbpsd  28691  slotslnbpsd  28692  trkgstr  28694  eengstr  29311  usgrexmplef  29590  upgr2wlk  29997  usgr2pthlem  30093  usgr2pth  30094  wpthswwlks2on  30294  elwspths2spth  30300  upgr3v3e3cycl  30512  upgr4cycl4dv4e  30517  konigsbergiedgw  30580  konigsberglem1  30584  konigsberglem2  30585  konigsberglem3  30586  clwlknon2num  30700  1kp2ke3k  30778  ex-mod  30781  ex-exp  30782  ex-fac  30783  9p10ne21  30802  ipidsq  31043  strlem3a  32585  xnn01gt  33096  expevenpos  33160  dpmul4  33214  pfxlsw2ccat  33251  wrdt2ind  33254  eufndx  33594  eufid  33595  evl1deg2  33848  evl1deg3  33849  fldext2rspun  34053  rtelextdg2lem  34097  rtelextdg2  34098  constrelextdg2  34118  2sqr3minply  34151  cos9thpiminplylem1  34153  cos9thpiminplylem2  34154  cos9thpiminplylem4  34156  cos9thpiminplylem5  34157  cos9thpinconstrlem1  34160  madjusmdetlem4  34201  coinflippv  34855  prodfzo03  34971  hgt750lemd  35016  hgt750lem  35019  hgt750lem2  35020  hgt750leme  35026  tgoldbachgnn  35027  tgoldbachgtde  35028  tgoldbachgt  35031  cusgredgex  35595  kur14lem8  35686  sinccvglem  36145  dvtan  38302  420gcd8e4  42754  12lcm5e60  42756  60lcm7e420  42758  lcmineqlem17  42793  lcmineqlem18  42794  lcmineqlem20  42796  lcmineqlem21  42797  lcmineqlem22  42798  lcmineqlem  42800  3exp7  42801  3lexlogpow5ineq1  42802  3lexlogpow5ineq2  42803  3lexlogpow2ineq1  42806  3lexlogpow2ineq2  42807  3lexlogpow5ineq5  42808  aks4d1p1p2  42818  aks4d1p1p7  42822  aks4d1p1p5  42823  aks4d1p1  42824  2np3bcnp1  42892  2ap1caineq  42893  aks6d1c7lem1  42928  25or6to4  42954  sqn5i  43027  235t711  43047  ex-decpmul  43048  nicomachus  43054  dffltz  43349  flt4lem  43360  flt4lem3  43363  flt4lem7  43374  nna4b4nsq  43375  sum9cubes  43387  3cubeslem2  43399  3cubeslem3l  43400  3cubeslem3r  43401  diophin  43486  irrapxlem5  43536  pellexlem2  43540  pell1qrge1  43580  jm2.22  43705  jm2.20nn  43707  jm2.27c  43717  rmydioph  43724  rmxdioph  43726  expdiophlem2  43732  frlmpwfi  43808  isnumbasgrplem3  43815  resqrtvalex  44354  imsqrtvalex  44355  amgm2d  44907  dvdivbd  46620  itgsinexplem1  46651  itgsinexp  46652  stoweidlem1  46698  wallispilem4  46765  wallispilem5  46766  wallispi2lem2  46769  stirlinglem3  46773  stirlinglem5  46775  stirlinglem7  46777  stirlinglem8  46778  stirlinglem10  46780  stirlinglem11  46781  hoiqssbllem2  47320  sqrtnnaa  47587  sqrtnzqaa  47588  sin3t  47591  cos3t  47592  sin5tlem1  47593  sin5tlem2  47594  sin5tlem4  47596  fmtnoge3  48265  fmtnom1nn  48267  fmtnof1  48270  fmtnorec1  48272  sqrtpwpw2p  48273  fmtnosqrt  48274  fmtnorec2lem  48277  fmtnodvds  48279  fmtnorec3  48283  fmtnorec4  48284  fmtno2  48285  fmtno3  48286  fmtno5lem2  48289  fmtno5lem4  48291  fmtno5  48292  257prm  48296  odz2prm2pw  48298  fmtnoprmfac1lem  48299  fmtnoprmfac2lem1  48301  fmtnofac2lem  48303  fmtnofac2  48304  fmtnofac1  48305  fmtno4prmfac  48307  fmtno4nprmfac193  48309  fmtno4prm  48310  fmtno5faclem1  48314  fmtno5faclem2  48315  fmtno5faclem3  48316  fmtno5fac  48317  flsqrt  48328  139prmALT  48331  31prm  48332  m5prm  48333  127prm  48334  m7prm  48335  m11nprm  48336  sfprmdvdsmersenne  48338  lighneallem2  48341  lighneallem3  48342  lighneallem4a  48343  proththd  48349  3exp4mod41  48351  41prothprmlem1  48352  oexpnegALTV  48425  fppr2odd  48479  2exp340mod341  48481  341fppr2  48482  8exp8mod9  48484  nfermltl2rev  48491  evengpoap3  48547  tgblthelfgott  48563  tgoldbachlt  48564  tgoldbach  48565  cycl3grtri  48695  usgrexmpl1lem  48769  usgrexmpl2lem  48774  gpg3nbgrvtx0  48824  gpgprismgr4cycllem7  48849  gpgprismgr4cycllem10  48852  gpg5edgnedg  48878  pgrple2abl  49128  pgrpgt2nabl  49129  ply1mulgsumlem2  49150  logbpw2m1  49330  blenpw2m1  49342  dignn0ehalf  49380  nn0sumshdiglemA  49382  nn0sumshdiglemB  49383  nn0mullong  49388  2aryfvalel  49410  itcoval2  49427  itcoval3  49428  itcovalt2lem2lem2  49437  itcovalt2lem1  49438  ackval2  49445  ackval3  49446  ackval0012  49452  ackval1012  49453  ackval2012  49454  ackval3012  49455  ackval42  49459  2sphere  49512  itscnhlinecirc02plem3  49547  inlinecirc02p  49550  onetansqsecsq  50522  cotsqcscsq  50523