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

Theorem 8nn0 11906
Description: 8 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.)
Assertion
Ref Expression
8nn0 8 ∈ ℕ0

Proof of Theorem 8nn0
StepHypRef Expression
1 8nn 11718 . 2 8 ∈ ℕ
21nnnn0i 11891 1 8 ∈ ℕ0
Colors of variables: wff setvar class
Syntax hints:  wcel 2115  8c8 11684  0cn0 11883
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5184  ax-nul 5191  ax-pow 5247  ax-pr 5311  ax-un 7444  ax-1cn 10580
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3014  df-ral 3137  df-rex 3138  df-reu 3139  df-rab 3141  df-v 3481  df-sbc 3758  df-csb 3866  df-dif 3921  df-un 3923  df-in 3925  df-ss 3935  df-pss 3937  df-nul 4275  df-if 4449  df-pw 4522  df-sn 4549  df-pr 4551  df-tp 4553  df-op 4555  df-uni 4820  df-iun 4902  df-br 5048  df-opab 5110  df-mpt 5128  df-tr 5154  df-id 5441  df-eprel 5446  df-po 5455  df-so 5456  df-fr 5495  df-we 5497  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-pred 6129  df-ord 6175  df-on 6176  df-lim 6177  df-suc 6178  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-ov 7141  df-om 7564  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-nn 11624  df-2 11686  df-3 11687  df-4 11688  df-5 11689  df-6 11690  df-7 11691  df-8 11692  df-n0 11884
This theorem is referenced by:  8p3e11  12165  8p4e12  12166  8p5e13  12167  8p6e14  12168  8p7e15  12169  8p8e16  12170  9p9e18  12178  6t4e24  12190  7t5e35  12196  8t3e24  12200  8t4e32  12201  8t5e40  12202  8t6e48  12203  8t7e56  12204  8t8e64  12205  9t3e27  12207  9t9e81  12213  2exp16  16413  19prm  16440  prmlem2  16442  37prm  16443  43prm  16444  83prm  16445  139prm  16446  163prm  16447  317prm  16448  631prm  16449  1259lem1  16453  1259lem2  16454  1259lem3  16455  1259lem4  16456  1259lem5  16457  1259prm  16458  2503lem1  16459  2503lem2  16460  2503lem3  16461  2503prm  16462  4001lem1  16463  4001lem2  16464  4001lem3  16465  4001lem4  16466  4001prm  16467  srads  19944  log2ublem3  25523  log2ub  25524  bpos1  25856  2lgslem3a  25969  2lgslem3b  25970  2lgslem3c  25971  2lgslem3d  25972  baseltedgf  26776  ex-exp  28224  hgt750lem  31940  hgt750lem2  31941  tgoldbachgtde  31949  420gcd8e4  39190  420lcm8e840  39195  lcmineqlem  39236  3lexlogpow5ineq1  39237  235t711  39336  ex-decpmul  39337  3cubeslem3l  39459  3cubeslem3r  39460  fmtno5lem1  43912  fmtno5lem3  43914  fmtno5lem4  43915  257prm  43920  fmtno4prmfac  43931  fmtno4nprmfac193  43933  fmtno5faclem1  43938  fmtno5faclem3  43940  fmtno5fac  43941  139prmALT  43955  127prm  43958  m7prm  43959  2exp11  43960  m11nprm  43961  2exp340mod341  44093  8exp8mod9  44096  nfermltl8rev  44102  bgoldbachlt  44173  tgblthelfgott  44175  tgoldbachlt  44176
  Copyright terms: Public domain W3C validator