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

Theorem 3nn0 10730
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 10611 . 2  |-  3  e.  NN
21nnnn0i 10720 1  |-  3  e.  NN0
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1826   3c3 10503   NN0cn0 10712
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601  ax-un 6491  ax-1cn 9461
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-reu 2739  df-rab 2741  df-v 3036  df-sbc 3253  df-csb 3349  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-pss 3405  df-nul 3712  df-if 3858  df-pw 3929  df-sn 3945  df-pr 3947  df-tp 3949  df-op 3951  df-uni 4164  df-iun 4245  df-br 4368  df-opab 4426  df-mpt 4427  df-tr 4461  df-eprel 4705  df-id 4709  df-po 4714  df-so 4715  df-fr 4752  df-we 4754  df-ord 4795  df-on 4796  df-lim 4797  df-suc 4798  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5460  df-fun 5498  df-fn 5499  df-f 5500  df-f1 5501  df-fo 5502  df-f1o 5503  df-fv 5504  df-ov 6199  df-om 6600  df-recs 6960  df-rdg 6994  df-nn 10453  df-2 10511  df-3 10512  df-n0 10713
This theorem is referenced by:  7p4e11  10947  7p7e14  10950  8p4e12  10952  8p6e14  10954  9p4e13  10959  9p5e14  10960  4t4e16  10968  5t4e20  10970  6t4e24  10974  6t6e36  10976  7t4e28  10979  7t6e42  10981  8t4e32  10985  8t5e40  10986  9t4e36  10992  9t5e45  10993  9t7e63  10995  9t8e72  10996  4fvwrd4  11715  expnass  12176  binom3  12189  fac4  12263  hash3tr  12433  ef4p  13850  efi4p  13874  resin4p  13875  recos4p  13876  ef01bndlem  13921  sin01bnd  13922  sin01gt0  13927  2exp6  14574  2exp8  14576  2exp16  14577  3exp3  14578  7prm  14598  11prm  14602  13prm  14603  17prm  14604  23prm  14606  prmlem2  14607  37prm  14608  43prm  14609  83prm  14610  139prm  14611  163prm  14612  317prm  14613  631prm  14614  1259lem1  14615  1259lem2  14616  1259lem3  14617  1259lem4  14618  1259lem5  14619  1259prm  14620  2503lem1  14621  2503lem2  14622  2503lem3  14623  2503prm  14624  4001lem1  14625  4001lem2  14626  4001lem3  14627  4001lem4  14628  4001prm  14629  ressunif  20850  tuslem  20855  tangtx  22983  1cubrlem  23288  dcubic1lem  23290  dcubic2  23291  dcubic1  23292  dcubic  23293  mcubic  23294  cubic2  23295  cubic  23296  binom4  23297  dquartlem2  23299  quart1cl  23301  quart1lem  23302  quart1  23303  quartlem1  23304  quartlem2  23305  quart  23308  log2ublem1  23393  log2ublem3  23395  log2ub  23396  log2le1  23397  birthday  23401  ppiublem2  23595  bclbnd  23672  bpos1  23675  bposlem8  23683  pntlemd  23896  pntlema  23898  pntlemb  23899  pntlemf  23907  pntlemo  23909  pntlem3  23911  iscgra  24289  usgraex3elv  24520  constr3lem4  24768  constr3trllem3  24773  constr3pthlem3  24778  4cycl4v4e  24787  4cycl4dv  24788  konigsberg  25108  kur14lem8  28846  4bc2eq6  29278  bpoly3  29973  bpoly4  29974  fsumcube  29975  jm2.23  31104  jm2.20nn  31105  rmydioph  31122  rmxdioph  31124  expdiophlem2  31130  expdioph  31131  lhe4.4ex1a  31402  zlmodzxzldeplem1  33301
  Copyright terms: Public domain W3C validator