Theorem 2nn0 11661

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

Syntax hints:   ∈ wcel 2107  2c2 11430  ℕ₀cn0 11642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-1cn 10330

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-reu 3097  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4672  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-ov 6925  df-om 7344  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-nn 11375  df-2 11438  df-n0 11643

This theorem is referenced by:  nn0n0n1ge2  11709  7p6e13  11925  8p3e11  11928  8p5e13  11930  9p3e12  11935  9p4e13  11936  4t3e12  11945  4t4e16  11946  5t3e15  11948  5t5e25  11950  6t3e18  11952  6t5e30  11954  7t3e21  11957  7t4e28  11958  7t5e35  11959  7t6e42  11960  7t7e49  11961  8t3e24  11963  8t4e32  11964  8t5e40  11965  9t3e27  11970  9t4e36  11971  9t8e72  11975  9t9e81  11976  decbin3  11989  2eluzge0  12039  xnn0le2is012  12388  fzo0to42pr  12874  nn0sqcl  13205  sqmul  13244  resqcl  13249  zsqcl  13253  cu2  13282  i3  13285  i4  13286  binom3  13304  expmulnbnd  13315  nn0opthlem1  13373  fac3  13385  faclbnd2  13396  faclbnd4lem1  13398  faclbnd4lem3  13400  hash2pr  13565  hashtplei  13580  s4fv2  14048  pfx2  14098  repsw3  14102  swrd2lsw  14103  2swrd2eqwrdeq  14104  2swrd2eqwrdeqOLD  14105  abssq  14453  sqabs  14454  iseraltlem2  14821  iseraltlem3  14822  bpoly2  15190  bpoly3  15191  bpoly4  15192  fsumcube  15193  ef4p  15245  efgt1p2  15246  efi4p  15269  ef01bndlem  15316  cos01bnd  15318  oexpneg  15473  oddge22np1  15477  bitsinv2  15571  bitsf1ocnv  15572  sadcaddlem  15585  sadadd2lem  15587  pythagtriplem4  15928  iserodd  15944  oddprmdvds  16011  prmreclem2  16025  prmreclem6  16029  vdwlem7  16095  vdwlem10  16098  vdwlem12  16100  dec2dvds  16171  dec5dvds  16172  decexp2  16183  2exp4  16193  2exp6  16194  2exp8  16195  2exp16  16196  3exp3  16197  2expltfac  16198  5prm  16214  7prm  16216  11prm  16220  13prm  16221  17prm  16222  19prm  16223  23prm  16224  prmlem2  16225  37prm  16226  43prm  16227  83prm  16228  139prm  16229  163prm  16230  317prm  16231  631prm  16232  1259lem1  16236  1259lem2  16237  1259lem3  16238  1259lem4  16239  1259lem5  16240  1259prm  16241  2503lem1  16242  2503lem2  16243  2503lem3  16244  2503prm  16245  4001lem1  16246  4001lem2  16247  4001lem3  16248  4001lem4  16249  4001prm  16250  ressds  16459  prdsvalstr  16499  pmtrprfval  18290  psgnunilem2  18299  efgredleme  18541  lt6abl  18682  mgpds  18886  srads  19583  cnfldstr  20144  cnfldfun  20154  setsmsds  22689  tmslem  22695  tnglem  22852  tngds  22860  sqcn  23085  ehl2eudis  23628  dveflem  24179  iaa  24517  tangtx  24695  efif1olem3  24728  efif1olem4  24729  root1id  24935  2logb9irr  24973  mcubic  25025  cubic2  25026  cubic  25027  binom4  25028  dquartlem2  25030  dquart  25031  quart1cl  25032  quart1lem  25033  quart1  25034  quartlem1  25035  quartlem2  25036  atandmcj  25087  bndatandm  25107  atansopn  25110  atantayl3  25117  leibpilem2  25120  leibpi  25121  leibpisum  25122  log2cnv  25123  log2tlbnd  25124  log2ublem2  25126  log2ublem3  25127  log2ub  25128  log2le1  25129  birthday  25133  basellem3  25261  basellem4  25262  basellem5  25263  basellem8  25266  issqf  25314  ppi3  25349  ppiublem2  25380  chtublem  25388  mersenne  25404  bcmax  25455  bcp1ctr  25456  bclbnd  25457  bpos1  25460  bposlem6  25466  bposlem8  25468  lgslem1  25474  lgsqrlem2  25524  gausslemma2dlem6  25549  lgseisenlem4  25555  2lgslem1c  25570  2lgslem3a  25573  2lgslem3b  25574  2lgslem3c  25575  2lgslem3d  25576  chebbnd1lem3  25612  rplogsumlem2  25626  dchrisumlem2  25631  dchrisum0flblem1  25649  dchrisum0flblem2  25650  dchrisum0flb  25651  selberglem2  25687  pntrmax  25705  pntlemo  25748  trkgstr  25795  ttgplusg  26227  ttgds  26230  eengstr  26329  usgrexmplef  26606  upgr2wlk  27015  usgr2pthlem  27115  usgr2pth  27116  wpthswwlks2on  27341  elwspths2spth  27347  upgr3v3e3cycl  27583  upgr4cycl4dv4e  27588  konigsbergiedgw  27654  konigsberglem1  27658  konigsberglem2  27659  konigsberglem3  27660  clwlknon2num  27796  1kp2ke3k  27878  ex-mod  27881  ex-exp  27882  ex-fac  27883  ipidsq  28137  strlem3a  29683  dpmul4  30184  madjusmdetlem4  30494  zlmds  30606  coinflippv  31144  prodfzo03  31283  hgt750lemd  31328  hgt750lem  31331  hgt750lem2  31332  hgt750leme  31338  tgoldbachgnn  31339  tgoldbachgtde  31340  tgoldbachgt  31343  kur14lem8  31794  sinccvglem  32163  dvtan  34085  sqn5i  38151  235t711  38157  ex-decpmul  38158  dffltz  38213  diophin  38296  irrapxlem5  38350  pellexlem2  38354  pell1qrge1  38394  jm2.22  38521  jm2.20nn  38523  jm2.27c  38533  rmydioph  38540  rmxdioph  38542  expdiophlem2  38548  frlmpwfi  38627  isnumbasgrplem3  38634  amgm2d  39457  dvdivbd  41066  itgsinexplem1  41097  itgsinexp  41098  stoweidlem1  41145  wallispilem4  41212  wallispilem5  41213  wallispi2lem2  41216  stirlinglem3  41220  stirlinglem5  41222  stirlinglem7  41224  stirlinglem8  41225  stirlinglem10  41227  stirlinglem11  41228  hoiqssbllem2  41764  fmtnoge3  42463  fmtnom1nn  42465  fmtnof1  42468  fmtnorec1  42470  sqrtpwpw2p  42471  fmtnosqrt  42472  fmtnorec2lem  42475  fmtnodvds  42477  fmtnorec3  42481  fmtnorec4  42482  fmtno2  42483  fmtno3  42484  fmtno5lem2  42487  fmtno5lem4  42489  fmtno5  42490  257prm  42494  odz2prm2pw  42496  fmtnoprmfac1lem  42497  fmtnoprmfac2lem1  42499  fmtnofac2lem  42501  fmtnofac2  42502  fmtnofac1  42503  fmtno4prmfac  42505  fmtno4nprmfac193  42507  fmtno4prm  42508  fmtno5faclem1  42512  fmtno5faclem2  42513  fmtno5faclem3  42514  fmtno5fac  42515  2exp5  42528  flsqrt  42529  139prmALT  42532  31prm  42533  m5prm  42534  2exp7  42535  127prm  42536  m7prm  42537  2exp11  42538  m11nprm  42539  sfprmdvdsmersenne  42541  lighneallem2  42544  lighneallem3  42545  lighneallem4a  42546  proththd  42552  3exp4mod41  42554  41prothprmlem1  42555  oexpnegALTV  42613  evengpoap3  42712  tgblthelfgott  42728  tgoldbachlt  42729  tgoldbach  42730  pgrple2abl  43161  pgrpgt2nabl  43162  ply1mulgsumlem2  43190  logbpw2m1  43376  blenpw2m1  43388  dignn0ehalf  43426  nn0sumshdiglemA  43428  nn0sumshdiglemB  43429  nn0mullong  43434  2sphere  43485  itscnhlinecirc02plem3  43520  inlinecirc02p  43523  onetansqsecsq  43610  cotsqcscsq  43611