MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2nn0 Structured version   Visualization version   GIF version

Theorem 2nn0 11306
Description: 2 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)
Assertion
Ref Expression
2nn0 2 ∈ ℕ0

Proof of Theorem 2nn0
StepHypRef Expression
1 2nn 11182 . 2 2 ∈ ℕ
21nnnn0i 11297 1 2 ∈ ℕ0
Colors of variables: wff setvar class
Syntax hints:  wcel 1989  2c2 11067  0cn0 11289
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-8 1991  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-sep 4779  ax-nul 4787  ax-pow 4841  ax-pr 4904  ax-un 6946  ax-1cn 9991
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ne 2794  df-ral 2916  df-rex 2917  df-reu 2918  df-rab 2920  df-v 3200  df-sbc 3434  df-csb 3532  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-pss 3588  df-nul 3914  df-if 4085  df-pw 4158  df-sn 4176  df-pr 4178  df-tp 4180  df-op 4182  df-uni 4435  df-iun 4520  df-br 4652  df-opab 4711  df-mpt 4728  df-tr 4751  df-id 5022  df-eprel 5027  df-po 5033  df-so 5034  df-fr 5071  df-we 5073  df-xp 5118  df-rel 5119  df-cnv 5120  df-co 5121  df-dm 5122  df-rn 5123  df-res 5124  df-ima 5125  df-pred 5678  df-ord 5724  df-on 5725  df-lim 5726  df-suc 5727  df-iota 5849  df-fun 5888  df-fn 5889  df-f 5890  df-f1 5891  df-fo 5892  df-f1o 5893  df-fv 5894  df-ov 6650  df-om 7063  df-wrecs 7404  df-recs 7465  df-rdg 7503  df-nn 11018  df-2 11076  df-n0 11290
This theorem is referenced by:  nn0n0n1ge2  11355  7p6e13  11605  8p3e11  11609  8p3e11OLD  11610  8p5e13  11612  9p3e12  11618  9p4e13  11619  4t3e12  11629  4t4e16  11630  5t3e15  11632  5t3e15OLD  11633  5t5e25  11636  5t5e25OLD  11637  6t3e18  11639  6t5e30  11641  6t5e30OLD  11642  7t3e21  11646  7t4e28  11647  7t5e35  11648  7t6e42  11649  7t7e49  11650  8t3e24  11652  8t4e32  11653  8t5e40  11654  8t5e40OLD  11655  9t3e27  11661  9t4e36  11662  9t8e72  11666  9t9e81  11667  decbin3  11681  2eluzge0  11730  xnn0le2is012  12073  fzo0to42pr  12551  nn0sqcl  12882  sqmul  12921  resqcl  12926  zsqcl  12929  cu2  12958  i3  12961  i4  12962  binom3  12980  expmulnbnd  12991  nn0opthlem1  13050  fac3  13062  faclbnd2  13073  faclbnd4lem1  13075  faclbnd4lem3  13077  hash2pr  13246  hashtplei  13261  s4fv2  13636  repsw3  13688  swrd2lsw  13689  2swrd2eqwrdeq  13690  abssq  14040  sqabs  14041  iseraltlem2  14407  iseraltlem3  14408  bpoly2  14782  bpoly3  14783  bpoly4  14784  fsumcube  14785  ef4p  14837  efgt1p2  14838  efi4p  14861  ef01bndlem  14908  cos01bnd  14910  oexpneg  15063  oddge22np1  15067  bitsinv2  15159  bitsf1ocnv  15160  sadcaddlem  15173  sadadd2lem  15175  pythagtriplem4  15518  iserodd  15534  oddprmdvds  15601  prmreclem2  15615  prmreclem6  15619  vdwlem7  15685  vdwlem10  15688  vdwlem12  15690  dec2dvds  15761  dec5dvds  15762  decexp2  15773  2exp4  15788  2exp6  15789  2exp8  15790  2exp16  15791  3exp3  15792  2expltfac  15793  5prm  15809  7prm  15811  11prm  15816  13prm  15817  17prm  15818  19prm  15819  23prm  15820  prmlem2  15821  37prm  15822  43prm  15823  83prm  15824  139prm  15825  163prm  15826  317prm  15827  631prm  15828  1259lem1  15832  1259lem2  15833  1259lem3  15834  1259lem4  15835  1259lem5  15836  1259prm  15837  2503lem1  15838  2503lem2  15839  2503lem3  15840  2503prm  15841  4001lem1  15842  4001lem2  15843  4001lem3  15844  4001lem4  15845  4001prm  15846  ressds  16067  prdsvalstr  16107  pmtrprfval  17901  psgnunilem2  17909  efgredleme  18150  lt6abl  18290  mgpds  18493  srads  19180  cnfldstr  19742  cnfldfun  19752  setsmsds  22275  tmslem  22281  tnglem  22438  tngds  22446  sqcn  22671  dveflem  23736  iaa  24074  tangtx  24251  efif1olem3  24284  efif1olem4  24285  root1id  24489  mcubic  24568  cubic2  24569  cubic  24570  binom4  24571  dquartlem2  24573  dquart  24574  quart1cl  24575  quart1lem  24576  quart1  24577  quartlem1  24578  quartlem2  24579  atandmcj  24630  bndatandm  24650  atansopn  24653  atantayl3  24660  leibpilem2  24662  leibpi  24663  leibpisum  24664  log2cnv  24665  log2tlbnd  24666  log2ublem2  24668  log2ublem3  24669  log2ub  24670  log2le1  24671  birthday  24675  basellem3  24803  basellem4  24804  basellem5  24805  basellem8  24808  issqf  24856  ppi3  24891  ppiublem2  24922  chtublem  24930  mersenne  24946  bcmax  24997  bcp1ctr  24998  bclbnd  24999  bpos1  25002  bposlem6  25008  bposlem8  25010  lgslem1  25016  lgsqrlem2  25066  gausslemma2dlem6  25091  lgseisenlem4  25097  2lgslem1c  25112  2lgslem3a  25115  2lgslem3b  25116  2lgslem3c  25117  2lgslem3d  25118  chebbnd1lem3  25154  rplogsumlem2  25168  dchrisumlem2  25173  dchrisum0flblem1  25191  dchrisum0flblem2  25192  dchrisum0flb  25193  selberglem2  25229  pntrmax  25247  pntlemo  25290  trkgstr  25337  ttgplusg  25752  ttgds  25755  eengstr  25854  usgrexmplef  26145  upgr2wlk  26558  usgr2pthlem  26653  usgr2pth  26654  wwlks2onv  26841  elwwlks2  26855  elwspths2spth  26856  upgr3v3e3cycl  27033  upgr4cycl4dv4e  27038  konigsbergiedgw  27101  konigsbergiedgwOLD  27102  konigsberglem1  27107  konigsberglem2  27108  konigsberglem3  27109  fusgr2wsp2nb  27185  extwwlkfablem2lem  27194  1kp2ke3k  27287  ex-mod  27290  ex-exp  27291  ex-fac  27292  ipidsq  27549  strlem3a  29095  dpmul4  29607  madjusmdetlem4  29881  zlmds  29993  coinflippv  30530  prodfzo03  30666  hgt750lemd  30711  hgt750lem  30714  hgt750lem2  30715  hgt750leme  30721  tgoldbachgnn  30722  tgoldbachgtde  30723  tgoldbachgt  30726  kur14lem8  31180  sinccvglem  31551  dvtan  33440  diophin  37162  irrapxlem5  37216  pellexlem2  37220  pell1qrge1  37260  jm2.22  37388  jm2.20nn  37390  jm2.27c  37400  rmydioph  37407  rmxdioph  37409  expdiophlem2  37415  frlmpwfi  37494  isnumbasgrplem3  37501  amgm2d  38327  dvdivbd  39907  itgsinexplem1  39938  itgsinexp  39939  stoweidlem1  39987  wallispilem4  40054  wallispilem5  40055  wallispi2lem2  40058  stirlinglem3  40062  stirlinglem5  40064  stirlinglem7  40066  stirlinglem8  40067  stirlinglem10  40069  stirlinglem11  40070  hoiqssbllem2  40606  pfx2  41183  fmtnoge3  41213  fmtnom1nn  41215  fmtnof1  41218  fmtnorec1  41220  sqrtpwpw2p  41221  fmtnosqrt  41222  fmtnorec2lem  41225  fmtnodvds  41227  fmtnorec3  41231  fmtnorec4  41232  fmtno2  41233  fmtno3  41234  fmtno5lem2  41237  fmtno5lem4  41239  fmtno5  41240  257prm  41244  odz2prm2pw  41246  fmtnoprmfac1lem  41247  fmtnoprmfac2lem1  41249  fmtnofac2lem  41251  fmtnofac2  41252  fmtnofac1  41253  fmtno4prmfac  41255  fmtno4nprmfac193  41257  fmtno4prm  41258  fmtno5faclem1  41262  fmtno5faclem2  41263  fmtno5faclem3  41264  fmtno5fac  41265  2exp5  41278  flsqrt  41279  139prmALT  41282  31prm  41283  m5prm  41284  2exp7  41285  127prm  41286  m7prm  41287  2exp11  41288  m11nprm  41289  sfprmdvdsmersenne  41291  lighneallem2  41294  lighneallem3  41295  lighneallem4a  41296  proththd  41302  3exp4mod41  41304  41prothprmlem1  41305  oexpnegALTV  41359  evengpoap3  41458  tgblthelfgott  41474  tgoldbachlt  41475  tgoldbach  41476  tgblthelfgottOLD  41480  tgoldbachltOLD  41481  tgoldbachOLD  41483  pgrple2abl  41917  pgrpgt2nabl  41918  ply1mulgsumlem2  41946  logbpw2m1  42132  blenpw2m1  42144  dignn0ehalf  42182  nn0sumshdiglemA  42184  nn0sumshdiglemB  42185  nn0mullong  42190  onetansqsecsq  42273  cotsqcscsq  42274
  Copyright terms: Public domain W3C validator