Theorem 2nn0 12517

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

Syntax hints:   ∈ wcel 2149  2c2 12291  ℕ₀cn0 12500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-nul 5268  ax-pr 5402  ax-un 7730  ax-1cn 11154

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7411  df-om 7859  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-nn 12230  df-2 12299  df-n0 12501

This theorem is referenced by:  nn0n0n1ge2  12568  12nn0  12724  25nn0  12726  7p6e13  12790  8p3e11  12793  8p5e13  12795  9p3e12  12800  9p4e13  12801  4t3e12  12810  4t4e16  12811  5t3e15  12813  5t5e25  12815  6t3e18  12817  6t5e30  12819  7t3e21  12822  7t4e28  12823  7t5e35  12824  7t6e42  12825  7t7e49  12826  8t3e24  12828  8t4e32  12829  8t5e40  12830  9t3e27  12835  9t4e36  12836  9t8e72  12840  9t9e81  12841  2lt10  12851  decbin3  12856  2eluzge0  12901  xnn0le2is012  13268  fzo0to42pr  13778  fvf1tp  13818  nn0sqcl  14121  sqmul  14151  resqcl  14156  zsqcl  14161  cu2  14232  i3  14235  i4  14236  binom3  14256  expmulnbnd  14267  nn0opthlem1  14300  fac3  14312  faclbnd2  14323  faclbnd4lem1  14325  faclbnd4lem3  14327  hash2pr  14502  hashtplei  14517  tpf1ofv2  14531  tpfo  14533  s4fv2  14930  pfx2  14980  repsw3  14984  swrd2lsw  14985  2swrd2eqwrdeq  14986  abssq  15353  sqabs  15354  iseraltlem2  15730  iseraltlem3  15731  bpoly2  16107  bpoly3  16108  bpoly4  16109  fsumcube  16110  ef4p  16165  efgt1p2  16166  efi4p  16189  ef01bndlem  16236  cos01bnd  16238  oexpneg  16399  oddge22np1  16403  bitsinv2  16497  bitsf1ocnv  16498  sadcaddlem  16511  sadadd2lem  16513  pythagtriplem4  16875  iserodd  16891  oddprmdvds  16959  prmreclem2  16973  prmreclem6  16977  vdwlem7  17043  vdwlem10  17046  vdwlem12  17048  dec2dvds  17119  dec5dvds  17120  2exp4  17140  2exp5  17141  2exp6  17142  2exp7  17143  2exp8  17144  2exp11  17145  2exp16  17146  3exp3  17147  2expltfac  17148  5prm  17164  7prm  17166  11prm  17171  13prm  17172  17prm  17173  19prm  17174  23prm  17175  prmlem2  17176  37prm  17177  43prm  17178  83prm  17179  139prm  17180  163prm  17181  317prm  17182  631prm  17183  1259lem1  17187  1259lem2  17188  1259lem3  17189  1259lem4  17190  1259lem5  17191  1259prm  17192  2503lem1  17193  2503lem2  17194  2503lem3  17195  2503prm  17196  4001lem1  17197  4001lem2  17198  4001lem3  17199  4001lem4  17200  4001prm  17201  basendxltdsndx  17437  dsndxnplusgndx  17439  dsndxnmulrndx  17440  slotsdnscsi  17441  dsndxntsetndx  17442  slotsdifdsndx  17443  slotsdifunifndx  17450  prdsvalstr  17501  smndex2dbas  18972  smndex2dlinvh  18975  pmtrprfval  19553  psgnunilem2  19561  efgredleme  19809  lt6abl  19961  cnfldstr  21489  sqcn  24998  ehl2eudis  25546  dveflem  26103  iaa  26451  tangtx  26632  efif1olem3  26671  efif1olem4  26672  root1id  26881  2logb9irr  26922  mcubic  26974  cubic2  26975  cubic  26976  binom4  26977  dquartlem2  26979  dquart  26980  quart1lem  26982  quart1  26983  quartlem1  26984  quartlem2  26985  atandmcj  27036  bndatandm  27056  atansopn  27059  atantayl3  27066  leibpilem2  27068  leibpi  27069  leibpisum  27070  log2cnv  27071  log2tlbnd  27072  log2ublem2  27074  log2ublem3  27075  log2ub  27076  log2le1  27077  birthday  27081  basellem3  27209  basellem4  27210  basellem5  27211  basellem8  27214  issqf  27262  ppi3  27297  ppiublem2  27329  chtublem  27337  mersenne  27353  bcmax  27404  bcp1ctr  27405  bclbnd  27406  bpos1  27409  bposlem6  27415  bposlem8  27417  lgslem1  27423  lgsqrlem2  27473  gausslemma2dlem6  27498  lgseisenlem4  27504  2lgslem1c  27519  2lgslem3a  27522  2lgslem3b  27523  2lgslem3c  27524  2lgslem3d  27525  2sq2  27559  2sqreultlem  27573  2sqreunnltlem  27576  chebbnd1lem3  27597  rplogsumlem2  27611  dchrisumlem2  27616  dchrisum0flblem1  27634  dchrisum0flblem2  27635  dchrisum0flb  27636  selberglem2  27672  pntrmax  27690  pntlemo  27733  slotsinbpsd  28672  slotslnbpsd  28673  trkgstr  28675  eengstr  29267  usgrexmplef  29546  upgr2wlk  29953  usgr2pthlem  30049  usgr2pth  30050  wpthswwlks2on  30250  elwspths2spth  30256  upgr3v3e3cycl  30468  upgr4cycl4dv4e  30473  konigsbergiedgw  30536  konigsberglem1  30540  konigsberglem2  30541  konigsberglem3  30542  clwlknon2num  30656  1kp2ke3k  30734  ex-mod  30737  ex-exp  30738  ex-fac  30739  9p10ne21  30758  ipidsq  30999  strlem3a  32541  xnn01gt  33052  expevenpos  33116  dpmul4  33170  pfxlsw2ccat  33207  wrdt2ind  33210  eufndx  33550  eufid  33551  evl1deg2  33808  evl1deg3  33809  fldext2rspun  34013  rtelextdg2lem  34057  rtelextdg2  34058  constrelextdg2  34078  2sqr3minply  34111  cos9thpiminplylem1  34113  cos9thpiminplylem2  34114  cos9thpiminplylem4  34116  cos9thpiminplylem5  34117  cos9thpinconstrlem1  34120  madjusmdetlem4  34161  coinflippv  34815  prodfzo03  34931  hgt750lemd  34976  hgt750lem  34979  hgt750lem2  34980  hgt750leme  34986  tgoldbachgnn  34987  tgoldbachgtde  34988  tgoldbachgt  34991  cusgredgex  35509  kur14lem8  35600  sinccvglem  36059  dvtan  38204  420gcd8e4  42658  12lcm5e60  42660  60lcm7e420  42662  lcmineqlem17  42697  lcmineqlem18  42698  lcmineqlem20  42700  lcmineqlem21  42701  lcmineqlem22  42702  lcmineqlem  42704  3exp7  42705  3lexlogpow5ineq1  42706  3lexlogpow5ineq2  42707  3lexlogpow2ineq1  42710  3lexlogpow2ineq2  42711  3lexlogpow5ineq5  42712  aks4d1p1p2  42722  aks4d1p1p7  42726  aks4d1p1p5  42727  aks4d1p1  42728  2np3bcnp1  42796  2ap1caineq  42797  aks6d1c7lem1  42832  sqn5i  42929  235t711  42949  ex-decpmul  42950  nicomachus  42956  dffltz  43251  flt4lem  43262  flt4lem3  43265  flt4lem7  43276  nna4b4nsq  43277  sum9cubes  43289  3cubeslem2  43301  3cubeslem3l  43302  3cubeslem3r  43303  diophin  43388  irrapxlem5  43438  pellexlem2  43442  pell1qrge1  43482  jm2.22  43607  jm2.20nn  43609  jm2.27c  43619  rmydioph  43626  rmxdioph  43628  expdiophlem2  43634  frlmpwfi  43710  isnumbasgrplem3  43717  resqrtvalex  44256  imsqrtvalex  44257  amgm2d  44809  dvdivbd  46522  itgsinexplem1  46553  itgsinexp  46554  stoweidlem1  46600  wallispilem4  46667  wallispilem5  46668  wallispi2lem2  46671  stirlinglem3  46675  stirlinglem5  46677  stirlinglem7  46679  stirlinglem8  46680  stirlinglem10  46682  stirlinglem11  46683  hoiqssbllem2  47222  nthrucw  47487  sin3t  47490  cos3t  47491  sin5tlem1  47492  sin5tlem2  47493  sin5tlem4  47495  fmtnoge3  48164  fmtnom1nn  48166  fmtnof1  48169  fmtnorec1  48171  sqrtpwpw2p  48172  fmtnosqrt  48173  fmtnorec2lem  48176  fmtnodvds  48178  fmtnorec3  48182  fmtnorec4  48183  fmtno2  48184  fmtno3  48185  fmtno5lem2  48188  fmtno5lem4  48190  fmtno5  48191  257prm  48195  odz2prm2pw  48197  fmtnoprmfac1lem  48198  fmtnoprmfac2lem1  48200  fmtnofac2lem  48202  fmtnofac2  48203  fmtnofac1  48204  fmtno4prmfac  48206  fmtno4nprmfac193  48208  fmtno4prm  48209  fmtno5faclem1  48213  fmtno5faclem2  48214  fmtno5faclem3  48215  fmtno5fac  48216  flsqrt  48227  139prmALT  48230  31prm  48231  m5prm  48232  127prm  48233  m7prm  48234  m11nprm  48235  sfprmdvdsmersenne  48237  lighneallem2  48240  lighneallem3  48241  lighneallem4a  48242  proththd  48248  3exp4mod41  48250  41prothprmlem1  48251  oexpnegALTV  48324  fppr2odd  48378  2exp340mod341  48380  341fppr2  48381  8exp8mod9  48383  nfermltl2rev  48390  evengpoap3  48446  tgblthelfgott  48462  tgoldbachlt  48463  tgoldbach  48464  cycl3grtri  48594  usgrexmpl1lem  48668  usgrexmpl2lem  48673  gpg3nbgrvtx0  48723  gpgprismgr4cycllem7  48748  gpgprismgr4cycllem10  48751  gpg5edgnedg  48777  pgrple2abl  49023  pgrpgt2nabl  49024  ply1mulgsumlem2  49045  logbpw2m1  49225  blenpw2m1  49237  dignn0ehalf  49275  nn0sumshdiglemA  49277  nn0sumshdiglemB  49278  nn0mullong  49283  2aryfvalel  49305  itcoval2  49322  itcoval3  49323  itcovalt2lem2lem2  49332  itcovalt2lem1  49333  ackval2  49340  ackval3  49341  ackval0012  49347  ackval1012  49348  ackval2012  49349  ackval3012  49350  ackval42  49354  2sphere  49407  itscnhlinecirc02plem3  49442  inlinecirc02p  49445  onetansqsecsq  50417  cotsqcscsq  50418