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

Theorem 6nn0 10890
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 10771 . 2  |-  6  e.  NN
21nnnn0i 10877 1  |-  6  e.  NN0
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1868   6c6 10663   NN0cn0 10869
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593  ax-1cn 9597
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 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-reu 2782  df-rab 2784  df-v 3083  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 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4760  df-id 4764  df-po 4770  df-so 4771  df-fr 4808  df-we 4810  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-pred 5395  df-ord 5441  df-on 5442  df-lim 5443  df-suc 5444  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-ov 6304  df-om 6703  df-wrecs 7032  df-recs 7094  df-rdg 7132  df-nn 10610  df-2 10668  df-3 10669  df-4 10670  df-5 10671  df-6 10672  df-n0 10870
This theorem is referenced by:  6p5e11  11101  6p6e12  11102  7p7e14  11106  8p7e15  11111  9p7e16  11118  9p8e17  11119  6t3e18  11129  6t4e24  11130  6t5e30  11131  6t6e36  11132  7t7e49  11138  8t3e24  11140  8t7e56  11144  8t8e64  11145  9t4e36  11148  9t5e45  11149  9t7e63  11151  9t8e72  11152  6lcm4e12  14568  2exp6OLD  15046  2exp8  15047  2exp16  15048  2expltfac  15050  19prm  15076  prmlem2  15078  37prm  15079  43prm  15080  139prm  15082  163prm  15083  317prm  15084  631prm  15085  1259lem1  15089  1259lem2  15090  1259lem3  15091  1259lem4  15092  1259lem5  15093  2503lem1  15095  2503lem2  15096  2503lem3  15097  2503prm  15098  4001lem1  15099  4001lem2  15100  4001lem3  15101  4001lem4  15102  4001prm  15103  log2ublem2  23859  log2ublem3  23860  log2ub  23861  log2le1  23862  birthday  23866  bclbnd  24194  bpos1  24197  bposlem8  24205  bposlem9  24206  bpos  24207  ttgval  24891  ttglem  24892  ttgbas  24893  ttgplusg  24894  ttgvsca  24896  eengstr  24996  zlmds  28763  kur14lem8  29931  expdiophlem2  35796  wallispi2lem2  37753  baseltedgf  38762  uhgrepe  38961
  Copyright terms: Public domain W3C validator