Theorem 8nn0 12501

Description: 8 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.)

Assertion

Ref	Expression
8nn0	⊢ 8 ∈ ℕ0

Proof of Theorem 8nn0

Step	Hyp	Ref	Expression
1		8nn 12313	. 2 ⊢ 8 ∈ ℕ
2	1	nnnn0i 12486	1 ⊢ 8 ∈ ℕ0

Syntax hints:   ∈ wcel 2104  8c8 12279  ℕ₀cn0 12478

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7729  ax-1cn 11172

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7416  df-om 7860  df-2nd 7980  df-frecs 8270  df-wrecs 8301  df-recs 8375  df-rdg 8414  df-nn 12219  df-2 12281  df-3 12282  df-4 12283  df-5 12284  df-6 12285  df-7 12286  df-8 12287  df-n0 12479

This theorem is referenced by:  8p3e11  12764  8p4e12  12765  8p5e13  12766  8p6e14  12767  8p7e15  12768  8p8e16  12769  9p9e18  12777  6t4e24  12789  7t5e35  12795  8t3e24  12799  8t4e32  12800  8t5e40  12801  8t6e48  12802  8t7e56  12803  8t8e64  12804  9t3e27  12806  9t9e81  12812  2exp11  17029  2exp16  17030  19prm  17057  prmlem2  17059  37prm  17060  43prm  17061  83prm  17062  139prm  17063  163prm  17064  317prm  17065  631prm  17066  1259lem1  17070  1259lem2  17071  1259lem3  17072  1259lem4  17073  1259lem5  17074  1259prm  17075  2503lem1  17076  2503lem2  17077  2503lem3  17078  2503prm  17079  4001lem1  17080  4001lem2  17081  4001lem3  17082  4001lem4  17083  4001prm  17084  slotsdnscsi  17343  sradsOLD  20954  log2ublem3  26687  log2ub  26688  bpos1  27020  2lgslem3a  27133  2lgslem3b  27134  2lgslem3c  27135  2lgslem3d  27136  basendxltedgfndx  28518  baseltedgfOLD  28519  ex-exp  29968  hgt750lem  33959  hgt750lem2  33960  tgoldbachgtde  33968  420gcd8e4  41179  420lcm8e840  41184  lcmineqlem  41225  3exp7  41226  3lexlogpow5ineq1  41227  3lexlogpow5ineq2  41228  3lexlogpow5ineq5  41233  aks4d1p1  41249  235t711  41509  ex-decpmul  41510  sum9cubes  41718  3cubeslem3l  41728  3cubeslem3r  41729  fmtno5lem1  46521  fmtno5lem3  46523  fmtno5lem4  46524  257prm  46529  fmtno4prmfac  46540  fmtno4nprmfac193  46542  fmtno5faclem1  46547  fmtno5faclem3  46549  fmtno5fac  46550  139prmALT  46564  127prm  46567  m7prm  46568  m11nprm  46569  2exp340mod341  46701  8exp8mod9  46704  nfermltl8rev  46710  bgoldbachlt  46781  tgblthelfgott  46783  tgoldbachlt  46784