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

Theorem 3nn0 11907
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 11708 . 2 3 ∈ ℕ
21nnnn0i 11897 1 3 ∈ ℕ0
Colors of variables: wff setvar class
Syntax hints:  wcel 2112  3c3 11685  0cn0 11889
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 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-1cn 10588
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 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-reu 3116  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-ov 7142  df-om 7565  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-nn 11630  df-2 11692  df-3 11693  df-n0 11890
This theorem is referenced by:  7p4e11  12166  7p7e14  12169  8p4e12  12172  8p6e14  12174  9p4e13  12179  9p5e14  12180  4t4e16  12189  5t4e20  12192  6t4e24  12196  6t6e36  12198  7t4e28  12201  7t6e42  12203  8t4e32  12207  8t5e40  12208  9t4e36  12214  9t5e45  12215  9t7e63  12217  9t8e72  12218  fz0to3un2pr  13008  4fvwrd4  13026  fldiv4p1lem1div2  13204  expnass  13570  binom3  13585  fac4  13641  4bc2eq6  13689  hash3tr  13848  bpoly3  15408  bpoly4  15409  fsumcube  15410  ef4p  15462  efi4p  15486  resin4p  15487  recos4p  15488  ef01bndlem  15533  sin01bnd  15534  sin01gt0  15539  2exp5  16416  2exp6  16417  2exp8  16419  2exp16  16420  3exp3  16421  7prm  16440  11prm  16444  13prm  16445  17prm  16446  23prm  16448  prmlem2  16449  37prm  16450  43prm  16451  83prm  16452  139prm  16453  163prm  16454  317prm  16455  631prm  16456  1259lem1  16460  1259lem2  16461  1259lem3  16462  1259lem4  16463  1259lem5  16464  1259prm  16465  2503lem1  16466  2503lem2  16467  2503lem3  16468  2503prm  16469  4001lem1  16470  4001lem2  16471  4001lem3  16472  4001lem4  16473  4001prm  16474  cnfldfun  20107  ressunif  22872  tuslem  22877  tangtx  25102  1cubrlem  25431  dcubic1lem  25433  dcubic2  25434  dcubic1  25435  dcubic  25436  mcubic  25437  cubic2  25438  cubic  25439  binom4  25440  dquartlem2  25442  quart1cl  25444  quart1lem  25445  quart1  25446  quartlem1  25447  quartlem2  25448  quart  25451  log2ublem1  25536  log2ublem3  25538  log2ub  25539  log2le1  25540  birthday  25544  ppiublem2  25791  bclbnd  25868  bpos1  25871  bposlem8  25879  gausslemma2dlem4  25957  2lgslem3b  25985  2lgslem3d  25987  pntlemd  26182  pntlema  26184  pntlemb  26185  pntlemf  26193  pntlemo  26195  pntlem3  26197  tgcgr4  26329  iscgra  26607  isinag  26636  isleag  26645  iseqlg  26665  usgrexmplef  27053  upgr3v3e3cycl  27969  upgr4cycl4dv4e  27974  konigsbergiedgw  28037  konigsberglem1  28041  konigsberglem2  28042  konigsberglem3  28043  konigsberglem4  28044  ex-prmo  28248  threehalves  30621  circlemethhgt  32028  hgt750lemd  32033  hgt750lem  32036  hgt750lem2  32037  hgt750lemb  32041  hgt750lema  32042  hgt750leme  32043  tgoldbachgtde  32045  tgoldbachgtda  32046  tgoldbachgt  32048  cusgracyclt3v  32517  kur14lem8  32574  3lexlogpow5ineq1  39340  3lexlogpow5ineq2  39341  235t711  39478  ex-decpmul  39479  3cubeslem3l  39620  3cubeslem3r  39621  3cubeslem4  39623  3cubes  39624  jm2.23  39930  jm2.20nn  39931  rmydioph  39948  rmxdioph  39950  expdiophlem2  39956  expdioph  39957  resqrtvalex  40338  amgm3d  40898  lhe4.4ex1a  41026  fmtno3  44061  fmtno4  44062  fmtno5lem1  44063  fmtno5lem2  44064  fmtno5lem3  44065  fmtno5lem4  44066  fmtno5  44067  257prm  44071  fmtnoprmfac2lem1  44076  fmtno4prmfac  44082  fmtno4prmfac193  44083  fmtno4nprmfac193  44084  fmtno5faclem2  44090  139prmALT  44106  31prm  44107  m5prm  44108  127prm  44109  2exp11  44111  m11nprm  44112  mod42tp1mod8  44113  11t31e341  44243  2exp340mod341  44244  341fppr2  44245  8exp8mod9  44247  nfermltl2rev  44254  tgoldbachlt  44327  tgoldbach  44328  zlmodzxzldeplem1  44902  itcoval3  45072  ackval3  45090  ackval0012  45096  ackval1012  45097  ackval2012  45098  ackval3012  45099  ackval40  45100  ackval41a  45101  ackval41  45102  ackval42  45103
  Copyright terms: Public domain W3C validator