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

Theorem 3nn0 10593
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 10476 . 2  |-  3  e.  NN
21nnnn0i 10583 1  |-  3  e.  NN0
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1761   3c3 10368   NN0cn0 10575
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371  ax-1cn 9336
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2261  df-mo 2262  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-reu 2720  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-pss 3341  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-tp 3879  df-op 3881  df-uni 4089  df-iun 4170  df-br 4290  df-opab 4348  df-mpt 4349  df-tr 4383  df-eprel 4628  df-id 4632  df-po 4637  df-so 4638  df-fr 4675  df-we 4677  df-ord 4718  df-on 4719  df-lim 4720  df-suc 4721  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423  df-ov 6093  df-om 6476  df-recs 6828  df-rdg 6862  df-nn 10319  df-2 10376  df-3 10377  df-n0 10576
This theorem is referenced by:  7p4e11  10803  7p7e14  10806  8p4e12  10808  8p6e14  10810  9p4e13  10815  9p5e14  10816  4t4e16  10824  5t4e20  10826  6t4e24  10830  6t6e36  10832  7t4e28  10835  7t6e42  10837  8t4e32  10841  8t5e40  10842  9t4e36  10848  9t5e45  10849  9t7e63  10851  9t8e72  10852  4fvwrd4  11529  expnass  11967  binom3  11981  fac4  12055  ef4p  13393  efi4p  13417  resin4p  13418  recos4p  13419  ef01bndlem  13464  sin01bnd  13465  sin01gt0  13470  2exp8  14112  2exp16  14113  3exp3  14114  7prm  14134  11prm  14138  13prm  14139  17prm  14140  23prm  14142  prmlem2  14143  37prm  14144  43prm  14145  83prm  14146  139prm  14147  163prm  14148  317prm  14149  631prm  14150  1259lem1  14151  1259lem2  14152  1259lem3  14153  1259lem4  14154  1259lem5  14155  1259prm  14156  2503lem1  14157  2503lem2  14158  2503lem3  14159  2503prm  14160  4001lem1  14161  4001lem2  14162  4001lem3  14163  4001lem4  14164  4001prm  14165  ressunif  19796  tuslem  19801  tangtx  21926  1cubrlem  22195  dcubic1lem  22197  dcubic2  22198  dcubic1  22199  dcubic  22200  mcubic  22201  cubic2  22202  cubic  22203  binom4  22204  dquartlem2  22206  quart1cl  22208  quart1lem  22209  quart1  22210  quartlem1  22211  quartlem2  22212  quart  22215  log2ublem1  22300  log2ublem3  22302  log2ub  22303  birthday  22307  ppiublem2  22501  bclbnd  22578  bpos1  22581  bposlem8  22589  pntlemd  22802  pntlema  22804  pntlemb  22805  pntlemf  22813  pntlemo  22815  pntlem3  22817  usgraex3elv  23252  constr3lem4  23468  constr3trllem3  23473  constr3pthlem3  23478  4cycl4v4e  23487  4cycl4dv  23488  konigsberg  23543  log2le1  26402  kur14lem8  27031  4bc2eq6  27320  bpoly3  28130  bpoly4  28131  fsumcube  28132  jm2.23  29270  jm2.20nn  29271  rmydioph  29288  rmxdioph  29290  expdiophlem2  29296  expdioph  29297  lhe4.4ex1a  29528  hash3tr  30159  zlmodzxzldeplem1  30883
  Copyright terms: Public domain W3C validator