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

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

Proof of Theorem 8nn0
StepHypRef Expression
1 8nn 10774 . 2  |-  8  e.  NN
21nnnn0i 10878 1  |-  8  e.  NN0
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1868   8c8 10666   NN0cn0 10870
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 4552  ax-pow 4599  ax-pr 4657  ax-un 6594  ax-1cn 9598
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 4761  df-id 4765  df-po 4771  df-so 4772  df-fr 4809  df-we 4811  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-rn 4861  df-res 4862  df-ima 4863  df-pred 5396  df-ord 5442  df-on 5443  df-lim 5444  df-suc 5445  df-iota 5562  df-fun 5600  df-fn 5601  df-f 5602  df-f1 5603  df-fo 5604  df-f1o 5605  df-fv 5606  df-ov 6305  df-om 6704  df-wrecs 7033  df-recs 7095  df-rdg 7133  df-nn 10611  df-2 10669  df-3 10670  df-4 10671  df-5 10672  df-6 10673  df-7 10674  df-8 10675  df-n0 10871
This theorem is referenced by:  8p3e11  11108  8p4e12  11109  8p5e13  11110  8p6e14  11111  8p7e15  11112  8p8e16  11113  9p9e18  11121  6t4e24  11131  7t5e35  11137  8t3e24  11141  8t4e32  11142  8t5e40  11143  8t6e48  11144  8t7e56  11145  8t8e64  11146  9t3e27  11148  9t9e81  11154  2exp16  15049  19prm  15077  prmlem2  15079  37prm  15080  43prm  15081  83prm  15082  139prm  15083  163prm  15084  317prm  15085  631prm  15086  1259lem1  15090  1259lem2  15091  1259lem3  15092  1259lem4  15093  1259lem5  15094  1259prm  15095  2503lem1  15096  2503lem2  15097  2503lem3  15098  2503prm  15099  4001lem1  15100  4001lem2  15101  4001lem3  15102  4001lem4  15103  4001prm  15104  srads  18397  log2ublem3  23861  log2ub  23862  bpos1  24198  tgblthelfgott  38620  tgoldbachlt  38621
  Copyright terms: Public domain W3C validator