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

Theorem 6nn0 9981
Description: 6 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.)
Assertion
Ref Expression
6nn0  |-  6  e.  NN0

Proof of Theorem 6nn0
StepHypRef Expression
1 6nn 9876 . 2  |-  6  e.  NN
21nnnn0i 9968 1  |-  6  e.  NN0
Colors of variables: wff set class
Syntax hints:    e. wcel 1685   6c6 9794   NN0cn0 9960
This theorem is referenced by:  6p5e11  10169  6p6e12  10170  7p7e14  10174  8p7e15  10179  9p7e16  10186  9p8e17  10187  6t3e18  10197  6t4e24  10198  6t5e30  10199  6t6e36  10200  7t7e49  10206  8t3e24  10208  8t7e56  10212  8t8e64  10213  9t4e36  10216  9t5e45  10217  9t7e63  10219  9t8e72  10220  2exp6  13095  2exp8  13096  2exp16  13097  2expltfac  13099  19prm  13113  prmlem2  13115  37prm  13116  43prm  13117  139prm  13119  163prm  13120  317prm  13121  631prm  13122  1259lem1  13123  1259lem2  13124  1259lem3  13125  1259lem4  13126  1259lem5  13127  2503lem1  13129  2503lem2  13130  2503lem3  13131  2503prm  13132  4001lem1  13133  4001lem2  13134  4001lem3  13135  4001lem4  13136  4001prm  13137  srads  15932  log2ublem2  20237  log2ublem3  20238  log2ub  20239  birthday  20243  bclbnd  20513  bpos1  20516  bposlem8  20524  bposlem9  20525  bpos  20526  kur14lem8  23148  expdiophlem2  26514  wallispi2lem2  27220
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-13 1687  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265  ax-sep 4142  ax-nul 4150  ax-pr 4213  ax-un 4511  ax-1cn 8790
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 937  df-3an 938  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-eu 2148  df-mo 2149  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-ral 2549  df-rex 2550  df-reu 2551  df-rab 2553  df-v 2791  df-sbc 2993  df-csb 3083  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-pss 3169  df-nul 3457  df-if 3567  df-pw 3628  df-sn 3647  df-pr 3648  df-tp 3649  df-op 3650  df-uni 3829  df-iun 3908  df-br 4025  df-opab 4079  df-mpt 4080  df-tr 4115  df-eprel 4304  df-id 4308  df-po 4313  df-so 4314  df-fr 4351  df-we 4353  df-ord 4394  df-on 4395  df-lim 4396  df-suc 4397  df-om 4656  df-xp 4694  df-rel 4695  df-cnv 4696  df-co 4697  df-dm 4698  df-rn 4699  df-res 4700  df-ima 4701  df-fun 5223  df-fn 5224  df-f 5225  df-f1 5226  df-fo 5227  df-f1o 5228  df-fv 5229  df-ov 5822  df-recs 6383  df-rdg 6418  df-nn 9742  df-2 9799  df-3 9800  df-4 9801  df-5 9802  df-6 9803  df-n0 9961
  Copyright terms: Public domain W3C validator