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

Theorem 3nn0 11903
Description: 3 is a nonnegative integer. (Contributed by Mario Carneiro, 18-Feb-2014.)
Assertion
Ref Expression
3nn0 3 ∈ ℕ0

Proof of Theorem 3nn0
StepHypRef Expression
1 3nn 11704 . 2 3 ∈ ℕ
21nnnn0i 11893 1 3 ∈ ℕ0
Colors of variables: wff setvar class
Syntax hints:  wcel 2105  3c3 11681  0cn0 11885
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-1cn 10583
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-reu 3142  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-ov 7148  df-om 7570  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-nn 11627  df-2 11688  df-3 11689  df-n0 11886
This theorem is referenced by:  7p4e11  12162  7p7e14  12165  8p4e12  12168  8p6e14  12170  9p4e13  12175  9p5e14  12176  4t4e16  12185  5t4e20  12188  6t4e24  12192  6t6e36  12194  7t4e28  12197  7t6e42  12199  8t4e32  12203  8t5e40  12204  9t4e36  12210  9t5e45  12211  9t7e63  12213  9t8e72  12214  fz0to3un2pr  12997  4fvwrd4  13015  fldiv4p1lem1div2  13193  expnass  13558  binom3  13573  fac4  13629  4bc2eq6  13677  hash3tr  13836  bpoly3  15400  bpoly4  15401  fsumcube  15402  ef4p  15454  efi4p  15478  resin4p  15479  recos4p  15480  ef01bndlem  15525  sin01bnd  15526  sin01gt0  15531  2exp6  16410  2exp8  16411  2exp16  16412  3exp3  16413  7prm  16432  11prm  16436  13prm  16437  17prm  16438  23prm  16440  prmlem2  16441  37prm  16442  43prm  16443  83prm  16444  139prm  16445  163prm  16446  317prm  16447  631prm  16448  1259lem1  16452  1259lem2  16453  1259lem3  16454  1259lem4  16455  1259lem5  16456  1259prm  16457  2503lem1  16458  2503lem2  16459  2503lem3  16460  2503prm  16461  4001lem1  16462  4001lem2  16463  4001lem3  16464  4001lem4  16465  4001prm  16466  cnfldfun  20485  ressunif  22798  tuslem  22803  tangtx  25018  1cubrlem  25346  dcubic1lem  25348  dcubic2  25349  dcubic1  25350  dcubic  25351  mcubic  25352  cubic2  25353  cubic  25354  binom4  25355  dquartlem2  25357  quart1cl  25359  quart1lem  25360  quart1  25361  quartlem1  25362  quartlem2  25363  quart  25366  log2ublem1  25451  log2ublem3  25453  log2ub  25454  log2le1  25455  birthday  25459  ppiublem2  25706  bclbnd  25783  bpos1  25786  bposlem8  25794  gausslemma2dlem4  25872  2lgslem3b  25900  2lgslem3d  25902  pntlemd  26097  pntlema  26099  pntlemb  26100  pntlemf  26108  pntlemo  26110  pntlem3  26112  tgcgr4  26244  iscgra  26522  isinag  26551  isleag  26560  iseqlg  26580  usgrexmplef  26968  upgr3v3e3cycl  27886  upgr4cycl4dv4e  27891  konigsbergiedgw  27954  konigsberglem1  27958  konigsberglem2  27959  konigsberglem3  27960  konigsberglem4  27961  ex-prmo  28165  threehalves  30518  circlemethhgt  31813  hgt750lemd  31818  hgt750lem  31821  hgt750lem2  31822  hgt750lemb  31826  hgt750lema  31827  hgt750leme  31828  tgoldbachgtde  31830  tgoldbachgtda  31831  tgoldbachgt  31833  cusgracyclt3v  32300  kur14lem8  32357  235t711  39055  ex-decpmul  39056  3cubeslem3l  39161  3cubeslem3r  39162  3cubeslem4  39164  3cubes  39165  jm2.23  39471  jm2.20nn  39472  rmydioph  39489  rmxdioph  39491  expdiophlem2  39497  expdioph  39498  amgm3d  40430  lhe4.4ex1a  40538  fmtno3  43590  fmtno4  43591  fmtno5lem1  43592  fmtno5lem2  43593  fmtno5lem3  43594  fmtno5lem4  43595  fmtno5  43596  257prm  43600  fmtnoprmfac2lem1  43605  fmtno4prmfac  43611  fmtno4prmfac193  43612  fmtno4nprmfac193  43613  fmtno5faclem2  43619  2exp5  43632  139prmALT  43636  31prm  43637  m5prm  43638  127prm  43640  2exp11  43642  m11nprm  43643  mod42tp1mod8  43644  11t31e341  43774  2exp340mod341  43775  341fppr2  43776  8exp8mod9  43778  nfermltl2rev  43785  tgoldbachlt  43858  tgoldbach  43859  zlmodzxzldeplem1  44483
  Copyright terms: Public domain W3C validator