Theorem 2nn0 11915

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

Syntax hints:   ∈ wcel 2114  2c2 11693  ℕ₀cn0 11898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-1cn 10595

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-ov 7159  df-om 7581  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-nn 11639  df-2 11701  df-n0 11899

This theorem is referenced by:  nn0n0n1ge2  11963  7p6e13  12177  8p3e11  12180  8p5e13  12182  9p3e12  12187  9p4e13  12188  4t3e12  12197  4t4e16  12198  5t3e15  12200  5t5e25  12202  6t3e18  12204  6t5e30  12206  7t3e21  12209  7t4e28  12210  7t5e35  12211  7t6e42  12212  7t7e49  12213  8t3e24  12215  8t4e32  12216  8t5e40  12217  9t3e27  12222  9t4e36  12223  9t8e72  12227  9t9e81  12228  decbin3  12241  2eluzge0  12294  xnn0le2is012  12640  fzo0to42pr  13125  nn0sqcl  13457  sqmul  13486  resqcl  13491  zsqcl  13495  cu2  13564  i3  13567  i4  13568  binom3  13586  expmulnbnd  13597  nn0opthlem1  13629  fac3  13641  faclbnd2  13652  faclbnd4lem1  13654  faclbnd4lem3  13656  hash2pr  13828  hashtplei  13843  s4fv2  14259  pfx2  14309  repsw3  14313  swrd2lsw  14314  2swrd2eqwrdeq  14315  abssq  14666  sqabs  14667  iseraltlem2  15039  iseraltlem3  15040  bpoly2  15411  bpoly3  15412  bpoly4  15413  fsumcube  15414  ef4p  15466  efgt1p2  15467  efi4p  15490  ef01bndlem  15537  cos01bnd  15539  oexpneg  15694  oddge22np1  15698  bitsinv2  15792  bitsf1ocnv  15793  sadcaddlem  15806  sadadd2lem  15808  pythagtriplem4  16156  iserodd  16172  oddprmdvds  16239  prmreclem2  16253  prmreclem6  16257  vdwlem7  16323  vdwlem10  16326  vdwlem12  16328  dec2dvds  16399  dec5dvds  16400  decexp2  16411  2exp4  16421  2exp6  16422  2exp8  16423  2exp16  16424  3exp3  16425  2expltfac  16426  5prm  16442  7prm  16444  11prm  16448  13prm  16449  17prm  16450  19prm  16451  23prm  16452  prmlem2  16453  37prm  16454  43prm  16455  83prm  16456  139prm  16457  163prm  16458  317prm  16459  631prm  16460  1259lem1  16464  1259lem2  16465  1259lem3  16466  1259lem4  16467  1259lem5  16468  1259prm  16469  2503lem1  16470  2503lem2  16471  2503lem3  16472  2503prm  16473  4001lem1  16474  4001lem2  16475  4001lem3  16476  4001lem4  16477  4001prm  16478  ressds  16686  prdsvalstr  16726  smndex2dbas  18079  smndex2dlinvh  18082  pmtrprfval  18615  psgnunilem2  18623  efgredleme  18869  lt6abl  19015  mgpds  19249  srads  19958  cnfldstr  20547  cnfldfun  20557  setsmsds  23086  tmslem  23092  tnglem  23249  tngds  23257  sqcn  23482  ehl2eudis  24025  dveflem  24576  iaa  24914  tangtx  25091  efif1olem3  25128  efif1olem4  25129  root1id  25335  2logb9irr  25373  mcubic  25425  cubic2  25426  cubic  25427  binom4  25428  dquartlem2  25430  dquart  25431  quart1cl  25432  quart1lem  25433  quart1  25434  quartlem1  25435  quartlem2  25436  atandmcj  25487  bndatandm  25507  atansopn  25510  atantayl3  25517  leibpilem2  25519  leibpi  25520  leibpisum  25521  log2cnv  25522  log2tlbnd  25523  log2ublem2  25525  log2ublem3  25526  log2ub  25527  log2le1  25528  birthday  25532  basellem3  25660  basellem4  25661  basellem5  25662  basellem8  25665  issqf  25713  ppi3  25748  ppiublem2  25779  chtublem  25787  mersenne  25803  bcmax  25854  bcp1ctr  25855  bclbnd  25856  bpos1  25859  bposlem6  25865  bposlem8  25867  lgslem1  25873  lgsqrlem2  25923  gausslemma2dlem6  25948  lgseisenlem4  25954  2lgslem1c  25969  2lgslem3a  25972  2lgslem3b  25973  2lgslem3c  25974  2lgslem3d  25975  2sq2  26009  2sqreultlem  26023  2sqreunnltlem  26026  chebbnd1lem3  26047  rplogsumlem2  26061  dchrisumlem2  26066  dchrisum0flblem1  26084  dchrisum0flblem2  26085  dchrisum0flb  26086  selberglem2  26122  pntrmax  26140  pntlemo  26183  trkgstr  26230  ttgplusg  26664  ttgds  26667  eengstr  26766  usgrexmplef  27041  upgr2wlk  27450  usgr2pthlem  27544  usgr2pth  27545  wpthswwlks2on  27740  elwspths2spth  27746  upgr3v3e3cycl  27959  upgr4cycl4dv4e  27964  konigsbergiedgw  28027  konigsberglem1  28031  konigsberglem2  28032  konigsberglem3  28033  clwlknon2num  28147  1kp2ke3k  28225  ex-mod  28228  ex-exp  28229  ex-fac  28230  9p10ne21  28249  ipidsq  28487  strlem3a  30029  xnn01gt  30495  dpmul4  30590  pfxlsw2ccat  30626  wrdt2ind  30627  madjusmdetlem4  31095  zlmds  31205  coinflippv  31741  prodfzo03  31874  hgt750lemd  31919  hgt750lem  31922  hgt750lem2  31923  hgt750leme  31929  tgoldbachgnn  31930  tgoldbachgtde  31931  tgoldbachgt  31934  cusgredgex  32368  kur14lem8  32460  sinccvglem  32915  dvtan  34957  420gcd8e4  39127  12lcm5e60  39129  60lcm7e420  39131  fac2xp3  39143  sqn5i  39220  235t711  39226  ex-decpmul  39227  dffltz  39320  3cubeslem2  39331  3cubeslem3l  39332  3cubeslem3r  39333  diophin  39418  irrapxlem5  39472  pellexlem2  39476  pell1qrge1  39516  jm2.22  39641  jm2.20nn  39643  jm2.27c  39653  rmydioph  39660  rmxdioph  39662  expdiophlem2  39668  frlmpwfi  39747  isnumbasgrplem3  39754  amgm2d  40600  dvdivbd  42257  itgsinexplem1  42288  itgsinexp  42289  stoweidlem1  42335  wallispilem4  42402  wallispilem5  42403  wallispi2lem2  42406  stirlinglem3  42410  stirlinglem5  42412  stirlinglem7  42414  stirlinglem8  42415  stirlinglem10  42417  stirlinglem11  42418  hoiqssbllem2  42954  fmtnoge3  43741  fmtnom1nn  43743  fmtnof1  43746  fmtnorec1  43748  sqrtpwpw2p  43749  fmtnosqrt  43750  fmtnorec2lem  43753  fmtnodvds  43755  fmtnorec3  43759  fmtnorec4  43760  fmtno2  43761  fmtno3  43762  fmtno5lem2  43765  fmtno5lem4  43767  fmtno5  43768  257prm  43772  odz2prm2pw  43774  fmtnoprmfac1lem  43775  fmtnoprmfac2lem1  43777  fmtnofac2lem  43779  fmtnofac2  43780  fmtnofac1  43781  fmtno4prmfac  43783  fmtno4nprmfac193  43785  fmtno4prm  43786  fmtno5faclem1  43790  fmtno5faclem2  43791  fmtno5faclem3  43792  fmtno5fac  43793  2exp5  43804  flsqrt  43805  139prmALT  43808  31prm  43809  m5prm  43810  2exp7  43811  127prm  43812  m7prm  43813  2exp11  43814  m11nprm  43815  sfprmdvdsmersenne  43817  lighneallem2  43820  lighneallem3  43821  lighneallem4a  43822  proththd  43828  3exp4mod41  43830  41prothprmlem1  43831  oexpnegALTV  43891  fppr2odd  43945  2exp340mod341  43947  341fppr2  43948  8exp8mod9  43950  nfermltl2rev  43957  evengpoap3  44013  tgblthelfgott  44029  tgoldbachlt  44030  tgoldbach  44031  pgrple2abl  44462  pgrpgt2nabl  44463  ply1mulgsumlem2  44490  logbpw2m1  44676  blenpw2m1  44688  dignn0ehalf  44726  nn0sumshdiglemA  44728  nn0sumshdiglemB  44729  nn0mullong  44734  2sphere  44785  itscnhlinecirc02plem3  44820  inlinecirc02p  44823  onetansqsecsq  44909  cotsqcscsq  44910