Theorem 8nn0 12422

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 12238	. 2 ⊢ 8 ∈ ℕ
2	1	nnnn0i 12407	1 ⊢ 8 ∈ ℕ0

Syntax hints:   ∈ wcel 2113  8c8 12204  ℕ₀cn0 12399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375  ax-un 7678  ax-1cn 11082

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-iun 4946  df-br 5097  df-opab 5159  df-mpt 5178  df-tr 5204  df-id 5517  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-pred 6257  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-ov 7359  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-nn 12144  df-2 12206  df-3 12207  df-4 12208  df-5 12209  df-6 12210  df-7 12211  df-8 12212  df-n0 12400

This theorem is referenced by:  8p3e11  12686  8p4e12  12687  8p5e13  12688  8p6e14  12689  8p7e15  12690  8p8e16  12691  9p9e18  12699  6t4e24  12711  7t5e35  12717  8t3e24  12721  8t4e32  12722  8t5e40  12723  8t6e48  12724  8t7e56  12725  8t8e64  12726  9t3e27  12728  9t9e81  12734  2exp11  17015  2exp16  17016  19prm  17043  prmlem2  17045  37prm  17046  43prm  17047  83prm  17048  139prm  17049  163prm  17050  317prm  17051  631prm  17052  1259lem1  17056  1259lem2  17057  1259lem3  17058  1259lem4  17059  1259lem5  17060  1259prm  17061  2503lem1  17062  2503lem2  17063  2503lem3  17064  2503prm  17065  4001lem1  17066  4001lem2  17067  4001lem3  17068  4001lem4  17069  4001prm  17070  slotsdnscsi  17310  log2ublem3  26912  log2ub  26913  bpos1  27248  2lgslem3a  27361  2lgslem3b  27362  2lgslem3c  27363  2lgslem3d  27364  basendxltedgfndx  29016  ex-exp  30474  cos9thpiminplylem1  33888  hgt750lem  34757  hgt750lem2  34758  tgoldbachgtde  34766  420gcd8e4  42199  420lcm8e840  42204  lcmineqlem  42245  3exp7  42246  3lexlogpow5ineq1  42247  3lexlogpow5ineq2  42248  3lexlogpow5ineq5  42253  aks4d1p1  42269  235t711  42502  ex-decpmul  42503  sum9cubes  42857  3cubeslem3l  42870  3cubeslem3r  42871  fmtno5lem1  47741  fmtno5lem3  47743  fmtno5lem4  47744  257prm  47749  fmtno4prmfac  47760  fmtno4nprmfac193  47762  fmtno5faclem1  47767  fmtno5faclem3  47769  fmtno5fac  47770  139prmALT  47784  127prm  47787  m7prm  47788  m11nprm  47789  2exp340mod341  47921  8exp8mod9  47924  nfermltl8rev  47930  bgoldbachlt  48001  tgblthelfgott  48003  tgoldbachlt  48004