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

Theorem 3nn0 10894
Description: 3 is a nonnegative integer. (Contributed by Mario Carneiro, 18-Feb-2014.)
Assertion
Ref Expression
3nn0  |-  3  e.  NN0

Proof of Theorem 3nn0
StepHypRef Expression
1 3nn 10775 . 2  |-  3  e.  NN
21nnnn0i 10884 1  |-  3  e.  NN0
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1872   3c3 10667   NN0cn0 10876
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6597  ax-1cn 9604
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-reu 2778  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-iun 4301  df-br 4424  df-opab 4483  df-mpt 4484  df-tr 4519  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-ov 6308  df-om 6707  df-wrecs 7039  df-recs 7101  df-rdg 7139  df-nn 10617  df-2 10675  df-3 10676  df-n0 10877
This theorem is referenced by:  7p4e11  11110  7p7e14  11113  8p4e12  11115  8p6e14  11117  9p4e13  11122  9p5e14  11123  4t4e16  11131  5t4e20  11133  6t4e24  11137  6t6e36  11139  7t4e28  11142  7t6e42  11144  8t4e32  11148  8t5e40  11149  9t4e36  11155  9t5e45  11156  9t7e63  11158  9t8e72  11159  4fvwrd4  11916  expnass  12386  binom3  12399  fac4  12473  4bc2eq6  12520  hash3tr  12651  bpoly3  14110  bpoly4  14111  fsumcube  14112  ef4p  14166  efi4p  14190  resin4p  14191  recos4p  14192  ef01bndlem  14237  sin01bnd  14238  sin01gt0  14243  2exp6  15057  2exp8  15059  2exp16  15060  3exp3  15061  7prm  15081  11prm  15085  13prm  15086  17prm  15087  23prm  15089  prmlem2  15090  37prm  15091  43prm  15092  83prm  15093  139prm  15094  163prm  15095  317prm  15096  631prm  15097  1259lem1  15101  1259lem2  15102  1259lem3  15103  1259lem4  15104  1259lem5  15105  1259prm  15106  2503lem1  15107  2503lem2  15108  2503lem3  15109  2503prm  15110  4001lem1  15111  4001lem2  15112  4001lem3  15113  4001lem4  15114  4001prm  15115  ressunif  21275  tuslem  21280  tangtx  23458  1cubrlem  23765  dcubic1lem  23767  dcubic2  23768  dcubic1  23769  dcubic  23770  mcubic  23771  cubic2  23772  cubic  23773  binom4  23774  dquartlem2  23776  quart1cl  23778  quart1lem  23779  quart1  23780  quartlem1  23781  quartlem2  23782  quart  23785  log2ublem1  23870  log2ublem3  23872  log2ub  23873  log2le1  23874  birthday  23878  ppiublem2  24129  bclbnd  24206  bpos1  24209  bposlem8  24217  pntlemd  24430  pntlema  24432  pntlemb  24433  pntlemf  24441  pntlemo  24443  pntlem3  24445  tgcgr4  24574  iscgra  24849  isinag  24877  isleag  24881  iseqlg  24895  usgraex3elv  25124  constr3lem4  25373  constr3trllem3  25378  constr3pthlem3  25383  4cycl4v4e  25392  4cycl4dv  25393  konigsberg  25713  kur14lem8  29944  jm2.23  35821  jm2.20nn  35822  rmydioph  35839  rmxdioph  35841  expdiophlem2  35847  expdioph  35848  amgm3d  36621  lhe4.4ex1a  36648  tgoldbachlt  38779  tgoldbach  38781  zlmodzxzldeplem1  39914
  Copyright terms: Public domain W3C validator