Theorem 2nn0 11902

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

Syntax hints:   ∈ wcel 2111  2c2 11680  ℕ₀cn0 11885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-1cn 10584

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-ov 7138  df-om 7561  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-nn 11626  df-2 11688  df-n0 11886

This theorem is referenced by:  nn0n0n1ge2  11950  7p6e13  12164  8p3e11  12167  8p5e13  12169  9p3e12  12174  9p4e13  12175  4t3e12  12184  4t4e16  12185  5t3e15  12187  5t5e25  12189  6t3e18  12191  6t5e30  12193  7t3e21  12196  7t4e28  12197  7t5e35  12198  7t6e42  12199  7t7e49  12200  8t3e24  12202  8t4e32  12203  8t5e40  12204  9t3e27  12209  9t4e36  12210  9t8e72  12214  9t9e81  12215  decbin3  12228  2eluzge0  12281  xnn0le2is012  12627  fzo0to42pr  13119  nn0sqcl  13452  sqmul  13481  resqcl  13486  zsqcl  13490  cu2  13559  i3  13562  i4  13563  binom3  13581  expmulnbnd  13592  nn0opthlem1  13624  fac3  13636  faclbnd2  13647  faclbnd4lem1  13649  faclbnd4lem3  13651  hash2pr  13823  hashtplei  13838  s4fv2  14250  pfx2  14300  repsw3  14304  swrd2lsw  14305  2swrd2eqwrdeq  14306  abssq  14658  sqabs  14659  iseraltlem2  15031  iseraltlem3  15032  bpoly2  15403  bpoly3  15404  bpoly4  15405  fsumcube  15406  ef4p  15458  efgt1p2  15459  efi4p  15482  ef01bndlem  15529  cos01bnd  15531  oexpneg  15686  oddge22np1  15690  bitsinv2  15782  bitsf1ocnv  15783  sadcaddlem  15796  sadadd2lem  15798  pythagtriplem4  16146  iserodd  16162  oddprmdvds  16229  prmreclem2  16243  prmreclem6  16247  vdwlem7  16313  vdwlem10  16316  vdwlem12  16318  dec2dvds  16389  dec5dvds  16390  decexp2  16401  2exp4  16411  2exp5  16412  2exp6  16413  2exp7  16414  2exp8  16415  2exp16  16416  3exp3  16417  2expltfac  16418  5prm  16434  7prm  16436  11prm  16440  13prm  16441  17prm  16442  19prm  16443  23prm  16444  prmlem2  16445  37prm  16446  43prm  16447  83prm  16448  139prm  16449  163prm  16450  317prm  16451  631prm  16452  1259lem1  16456  1259lem2  16457  1259lem3  16458  1259lem4  16459  1259lem5  16460  1259prm  16461  2503lem1  16462  2503lem2  16463  2503lem3  16464  2503prm  16465  4001lem1  16466  4001lem2  16467  4001lem3  16468  4001lem4  16469  4001prm  16470  ressds  16678  prdsvalstr  16718  smndex2dbas  18071  smndex2dlinvh  18074  pmtrprfval  18607  psgnunilem2  18615  efgredleme  18861  lt6abl  19008  mgpds  19242  srads  19951  cnfldstr  20093  cnfldfun  20103  setsmsds  23083  tmslem  23089  tnglem  23246  tngds  23254  sqcn  23479  ehl2eudis  24026  dveflem  24582  iaa  24921  tangtx  25098  efif1olem3  25136  efif1olem4  25137  root1id  25343  2logb9irr  25381  mcubic  25433  cubic2  25434  cubic  25435  binom4  25436  dquartlem2  25438  dquart  25439  quart1cl  25440  quart1lem  25441  quart1  25442  quartlem1  25443  quartlem2  25444  atandmcj  25495  bndatandm  25515  atansopn  25518  atantayl3  25525  leibpilem2  25527  leibpi  25528  leibpisum  25529  log2cnv  25530  log2tlbnd  25531  log2ublem2  25533  log2ublem3  25534  log2ub  25535  log2le1  25536  birthday  25540  basellem3  25668  basellem4  25669  basellem5  25670  basellem8  25673  issqf  25721  ppi3  25756  ppiublem2  25787  chtublem  25795  mersenne  25811  bcmax  25862  bcp1ctr  25863  bclbnd  25864  bpos1  25867  bposlem6  25873  bposlem8  25875  lgslem1  25881  lgsqrlem2  25931  gausslemma2dlem6  25956  lgseisenlem4  25962  2lgslem1c  25977  2lgslem3a  25980  2lgslem3b  25981  2lgslem3c  25982  2lgslem3d  25983  2sq2  26017  2sqreultlem  26031  2sqreunnltlem  26034  chebbnd1lem3  26055  rplogsumlem2  26069  dchrisumlem2  26074  dchrisum0flblem1  26092  dchrisum0flblem2  26093  dchrisum0flb  26094  selberglem2  26130  pntrmax  26148  pntlemo  26191  trkgstr  26238  ttgplusg  26672  ttgds  26675  eengstr  26774  usgrexmplef  27049  upgr2wlk  27458  usgr2pthlem  27552  usgr2pth  27553  wpthswwlks2on  27747  elwspths2spth  27753  upgr3v3e3cycl  27965  upgr4cycl4dv4e  27970  konigsbergiedgw  28033  konigsberglem1  28037  konigsberglem2  28038  konigsberglem3  28039  clwlknon2num  28153  1kp2ke3k  28231  ex-mod  28234  ex-exp  28235  ex-fac  28236  9p10ne21  28255  ipidsq  28493  strlem3a  30035  xnn01gt  30521  dpmul4  30616  pfxlsw2ccat  30652  wrdt2ind  30653  madjusmdetlem4  31183  zlmds  31315  coinflippv  31851  prodfzo03  31984  hgt750lemd  32029  hgt750lem  32032  hgt750lem2  32033  hgt750leme  32039  tgoldbachgnn  32040  tgoldbachgtde  32041  tgoldbachgt  32044  cusgredgex  32481  kur14lem8  32573  sinccvglem  33028  dvtan  35107  420gcd8e4  39294  12lcm5e60  39296  60lcm7e420  39298  lcmineqlem17  39333  lcmineqlem18  39334  lcmineqlem20  39336  lcmineqlem21  39337  lcmineqlem22  39338  lcmineqlem  39340  3lexlogpow5ineq1  39341  2np3bcnp1  39348  2ap1caineq  39349  fac2xp3  39385  sqn5i  39479  235t711  39485  ex-decpmul  39486  dffltz  39615  3cubeslem2  39626  3cubeslem3l  39627  3cubeslem3r  39628  diophin  39713  irrapxlem5  39767  pellexlem2  39771  pell1qrge1  39811  jm2.22  39936  jm2.20nn  39938  jm2.27c  39948  rmydioph  39955  rmxdioph  39957  expdiophlem2  39963  frlmpwfi  40042  isnumbasgrplem3  40049  resqrtvalex  40345  imsqrtvalex  40346  amgm2d  40904  dvdivbd  42565  itgsinexplem1  42596  itgsinexp  42597  stoweidlem1  42643  wallispilem4  42710  wallispilem5  42711  wallispi2lem2  42714  stirlinglem3  42718  stirlinglem5  42720  stirlinglem7  42722  stirlinglem8  42723  stirlinglem10  42725  stirlinglem11  42726  hoiqssbllem2  43262  fmtnoge3  44047  fmtnom1nn  44049  fmtnof1  44052  fmtnorec1  44054  sqrtpwpw2p  44055  fmtnosqrt  44056  fmtnorec2lem  44059  fmtnodvds  44061  fmtnorec3  44065  fmtnorec4  44066  fmtno2  44067  fmtno3  44068  fmtno5lem2  44071  fmtno5lem4  44073  fmtno5  44074  257prm  44078  odz2prm2pw  44080  fmtnoprmfac1lem  44081  fmtnoprmfac2lem1  44083  fmtnofac2lem  44085  fmtnofac2  44086  fmtnofac1  44087  fmtno4prmfac  44089  fmtno4nprmfac193  44091  fmtno4prm  44092  fmtno5faclem1  44096  fmtno5faclem2  44097  fmtno5faclem3  44098  fmtno5fac  44099  flsqrt  44110  139prmALT  44113  31prm  44114  m5prm  44115  127prm  44116  m7prm  44117  2exp11  44118  m11nprm  44119  sfprmdvdsmersenne  44121  lighneallem2  44124  lighneallem3  44125  lighneallem4a  44126  proththd  44132  3exp4mod41  44134  41prothprmlem1  44135  oexpnegALTV  44195  fppr2odd  44249  2exp340mod341  44251  341fppr2  44252  8exp8mod9  44254  nfermltl2rev  44261  evengpoap3  44317  tgblthelfgott  44333  tgoldbachlt  44334  tgoldbach  44335  pgrple2abl  44767  pgrpgt2nabl  44768  ply1mulgsumlem2  44795  logbpw2m1  44981  blenpw2m1  44993  dignn0ehalf  45031  nn0sumshdiglemA  45033  nn0sumshdiglemB  45034  nn0mullong  45039  2aryfvalel  45061  itcoval2  45078  itcoval3  45079  itcovalt2lem2lem2  45088  itcovalt2lem1  45089  ackval2  45096  ackval3  45097  ackval0012  45103  ackval1012  45104  ackval2012  45105  ackval3012  45106  ackval42  45110  2sphere  45163  itscnhlinecirc02plem3  45198  inlinecirc02p  45201  onetansqsecsq  45287  cotsqcscsq  45288