Theorem 2nn0 12250

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

Syntax hints:   ∈ wcel 2106  2c2 12028  ℕ₀cn0 12233

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352  ax-un 7588  ax-1cn 10929

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-ov 7278  df-om 7713  df-2nd 7832  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-nn 11974  df-2 12036  df-n0 12234

This theorem is referenced by:  nn0n0n1ge2  12300  7p6e13  12515  8p3e11  12518  8p5e13  12520  9p3e12  12525  9p4e13  12526  4t3e12  12535  4t4e16  12536  5t3e15  12538  5t5e25  12540  6t3e18  12542  6t5e30  12544  7t3e21  12547  7t4e28  12548  7t5e35  12549  7t6e42  12550  7t7e49  12551  8t3e24  12553  8t4e32  12554  8t5e40  12555  9t3e27  12560  9t4e36  12561  9t8e72  12565  9t9e81  12566  decbin3  12579  2eluzge0  12633  xnn0le2is012  12980  fzo0to42pr  13474  nn0sqcl  13810  sqmul  13839  resqcl  13844  zsqcl  13848  cu2  13917  i3  13920  i4  13921  binom3  13939  expmulnbnd  13950  nn0opthlem1  13982  fac3  13994  faclbnd2  14005  faclbnd4lem1  14007  faclbnd4lem3  14009  hash2pr  14183  hashtplei  14198  s4fv2  14610  pfx2  14660  repsw3  14664  swrd2lsw  14665  2swrd2eqwrdeq  14666  abssq  15018  sqabs  15019  iseraltlem2  15394  iseraltlem3  15395  bpoly2  15767  bpoly3  15768  bpoly4  15769  fsumcube  15770  ef4p  15822  efgt1p2  15823  efi4p  15846  ef01bndlem  15893  cos01bnd  15895  oexpneg  16054  oddge22np1  16058  bitsinv2  16150  bitsf1ocnv  16151  sadcaddlem  16164  sadadd2lem  16166  pythagtriplem4  16520  iserodd  16536  oddprmdvds  16604  prmreclem2  16618  prmreclem6  16622  vdwlem7  16688  vdwlem10  16691  vdwlem12  16693  dec2dvds  16764  dec5dvds  16765  decexp2  16776  2exp4  16786  2exp5  16787  2exp6  16788  2exp7  16789  2exp8  16790  2exp11  16791  2exp16  16792  3exp3  16793  2expltfac  16794  5prm  16810  7prm  16812  11prm  16816  13prm  16817  17prm  16818  19prm  16819  23prm  16820  prmlem2  16821  37prm  16822  43prm  16823  83prm  16824  139prm  16825  163prm  16826  317prm  16827  631prm  16828  1259lem1  16832  1259lem2  16833  1259lem3  16834  1259lem4  16835  1259lem5  16836  1259prm  16837  2503lem1  16838  2503lem2  16839  2503lem3  16840  2503prm  16841  4001lem1  16842  4001lem2  16843  4001lem3  16844  4001lem4  16845  4001prm  16846  basendxltdsndx  17098  dsndxnplusgndx  17100  dsndxnmulrndx  17101  slotsdnscsi  17102  dsndxntsetndx  17103  slotsdifdsndx  17104  slotsdifunifndx  17111  prdsvalstr  17163  smndex2dbas  18553  smndex2dlinvh  18556  pmtrprfval  19095  psgnunilem2  19103  efgredleme  19349  lt6abl  19496  mgpdsOLD  19734  sradsOLD  20456  cnfldstr  20599  cnfldfunALTOLD  20611  setsmsdsOLD  23631  tmslemOLD  23638  tnglemOLD  23797  tngdsOLD  23812  sqcn  24037  ehl2eudis  24586  dveflem  25143  iaa  25485  tangtx  25662  efif1olem3  25700  efif1olem4  25701  root1id  25907  2logb9irr  25945  mcubic  25997  cubic2  25998  cubic  25999  binom4  26000  dquartlem2  26002  dquart  26003  quart1cl  26004  quart1lem  26005  quart1  26006  quartlem1  26007  quartlem2  26008  atandmcj  26059  bndatandm  26079  atansopn  26082  atantayl3  26089  leibpilem2  26091  leibpi  26092  leibpisum  26093  log2cnv  26094  log2tlbnd  26095  log2ublem2  26097  log2ublem3  26098  log2ub  26099  log2le1  26100  birthday  26104  basellem3  26232  basellem4  26233  basellem5  26234  basellem8  26237  issqf  26285  ppi3  26320  ppiublem2  26351  chtublem  26359  mersenne  26375  bcmax  26426  bcp1ctr  26427  bclbnd  26428  bpos1  26431  bposlem6  26437  bposlem8  26439  lgslem1  26445  lgsqrlem2  26495  gausslemma2dlem6  26520  lgseisenlem4  26526  2lgslem1c  26541  2lgslem3a  26544  2lgslem3b  26545  2lgslem3c  26546  2lgslem3d  26547  2sq2  26581  2sqreultlem  26595  2sqreunnltlem  26598  chebbnd1lem3  26619  rplogsumlem2  26633  dchrisumlem2  26638  dchrisum0flblem1  26656  dchrisum0flblem2  26657  dchrisum0flb  26658  selberglem2  26694  pntrmax  26712  pntlemo  26755  slotsinbpsd  26802  slotslnbpsd  26803  trkgstr  26805  ttgplusgOLD  27243  ttgdsOLD  27248  eengstr  27348  usgrexmplef  27626  upgr2wlk  28036  usgr2pthlem  28131  usgr2pth  28132  wpthswwlks2on  28326  elwspths2spth  28332  upgr3v3e3cycl  28544  upgr4cycl4dv4e  28549  konigsbergiedgw  28612  konigsberglem1  28616  konigsberglem2  28617  konigsberglem3  28618  clwlknon2num  28732  1kp2ke3k  28810  ex-mod  28813  ex-exp  28814  ex-fac  28815  9p10ne21  28834  ipidsq  29072  strlem3a  30614  xnn01gt  31093  dpmul4  31188  pfxlsw2ccat  31224  wrdt2ind  31225  madjusmdetlem4  31780  zlmdsOLD  31913  coinflippv  32450  prodfzo03  32583  hgt750lemd  32628  hgt750lem  32631  hgt750lem2  32632  hgt750leme  32638  tgoldbachgnn  32639  tgoldbachgtde  32640  tgoldbachgt  32643  cusgredgex  33083  kur14lem8  33175  sinccvglem  33630  dvtan  35827  420gcd8e4  40014  12lcm5e60  40016  60lcm7e420  40018  lcmineqlem17  40053  lcmineqlem18  40054  lcmineqlem20  40056  lcmineqlem21  40057  lcmineqlem22  40058  lcmineqlem  40060  3exp7  40061  3lexlogpow5ineq1  40062  3lexlogpow5ineq2  40063  3lexlogpow2ineq1  40066  3lexlogpow2ineq2  40067  3lexlogpow5ineq5  40068  aks4d1p1p2  40078  aks4d1p1p7  40082  aks4d1p1p5  40083  aks4d1p1  40084  2np3bcnp1  40100  2ap1caineq  40101  fac2xp3  40160  sqn5i  40313  235t711  40319  ex-decpmul  40320  dffltz  40471  flt4lem  40482  flt4lem3  40485  flt4lem7  40496  nna4b4nsq  40497  3cubeslem2  40507  3cubeslem3l  40508  3cubeslem3r  40509  diophin  40594  irrapxlem5  40648  pellexlem2  40652  pell1qrge1  40692  jm2.22  40817  jm2.20nn  40819  jm2.27c  40829  rmydioph  40836  rmxdioph  40838  expdiophlem2  40844  frlmpwfi  40923  isnumbasgrplem3  40930  resqrtvalex  41253  imsqrtvalex  41254  amgm2d  41809  dvdivbd  43464  itgsinexplem1  43495  itgsinexp  43496  stoweidlem1  43542  wallispilem4  43609  wallispilem5  43610  wallispi2lem2  43613  stirlinglem3  43617  stirlinglem5  43619  stirlinglem7  43621  stirlinglem8  43622  stirlinglem10  43624  stirlinglem11  43625  hoiqssbllem2  44161  fmtnoge3  44982  fmtnom1nn  44984  fmtnof1  44987  fmtnorec1  44989  sqrtpwpw2p  44990  fmtnosqrt  44991  fmtnorec2lem  44994  fmtnodvds  44996  fmtnorec3  45000  fmtnorec4  45001  fmtno2  45002  fmtno3  45003  fmtno5lem2  45006  fmtno5lem4  45008  fmtno5  45009  257prm  45013  odz2prm2pw  45015  fmtnoprmfac1lem  45016  fmtnoprmfac2lem1  45018  fmtnofac2lem  45020  fmtnofac2  45021  fmtnofac1  45022  fmtno4prmfac  45024  fmtno4nprmfac193  45026  fmtno4prm  45027  fmtno5faclem1  45031  fmtno5faclem2  45032  fmtno5faclem3  45033  fmtno5fac  45034  flsqrt  45045  139prmALT  45048  31prm  45049  m5prm  45050  127prm  45051  m7prm  45052  m11nprm  45053  sfprmdvdsmersenne  45055  lighneallem2  45058  lighneallem3  45059  lighneallem4a  45060  proththd  45066  3exp4mod41  45068  41prothprmlem1  45069  oexpnegALTV  45129  fppr2odd  45183  2exp340mod341  45185  341fppr2  45186  8exp8mod9  45188  nfermltl2rev  45195  evengpoap3  45251  tgblthelfgott  45267  tgoldbachlt  45268  tgoldbach  45269  pgrple2abl  45701  pgrpgt2nabl  45702  ply1mulgsumlem2  45728  logbpw2m1  45913  blenpw2m1  45925  dignn0ehalf  45963  nn0sumshdiglemA  45965  nn0sumshdiglemB  45966  nn0mullong  45971  2aryfvalel  45993  itcoval2  46010  itcoval3  46011  itcovalt2lem2lem2  46020  itcovalt2lem1  46021  ackval2  46028  ackval3  46029  ackval0012  46035  ackval1012  46036  ackval2012  46037  ackval3012  46038  ackval42  46042  2sphere  46095  itscnhlinecirc02plem3  46130  inlinecirc02p  46133  onetansqsecsq  46463  cotsqcscsq  46464