Theorem 8nn0 12533

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

This proof depends on syntax axioms:   ∈ wcel 2142  8c8 12307  ℕ₀cn0 12510

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5256  ax-nul 5268  ax-pr 5403  ax-un 7734  ax-1cn 11164

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1103  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-reu 3369  df-rab 3416  df-v 3456  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-iun 4957  df-br 5109  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5555  df-eprel 5560  df-po 5568  df-so 5569  df-fr 5613  df-we 5615  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7415  df-om 7861  df-2nd 7985  df-frecs 8276  df-wrecs 8307  df-recs 8356  df-rdg 8395  df-nn 12240  df-2 12309  df-3 12310  df-4 12311  df-5 12312  df-6 12313  df-7 12314  df-8 12315  df-n0 12511

This theorem is used by:  8p3e11  12803  8p4e12  12804  8p5e13  12805  8p6e14  12806  8p7e15  12807  8p8e16  12808  9p9e18  12816  6t4e24  12828  7t5e35  12834  8t3e24  12838  8t4e32  12839  8t5e40  12840  8t6e48  12841  8t7e56  12842  8t8e64  12843  9t3e27  12845  9t9e81  12851  8lt10  12855  2exp11  17155  2exp16  17156  19prm  17184  prmlem2  17186  37prm  17187  43prm  17188  83prm  17189  139prm  17190  163prm  17191  317prm  17192  631prm  17193  1259lem1  17197  1259lem2  17198  1259lem3  17199  1259lem4  17200  1259lem5  17201  1259prm  17202  2503lem1  17203  2503lem2  17204  2503lem3  17205  2503prm  17206  4001lem1  17207  4001lem2  17208  4001lem3  17209  4001lem4  17210  4001prm  17211  slotsdnscsi  17451  log2ublem3  27124  log2ub  27125  bpos1  27458  2lgslem3a  27571  2lgslem3b  27572  2lgslem3c  27573  2lgslem3d  27574  basendxltedgfndx  29355  ex-exp  30812  cos9thpiminplylem1  34181  hgt750lem  35047  hgt750lem2  35048  tgoldbachgtde  35056  420gcd8e4  42801  420lcm8e840  42806  lcmineqlem  42847  3exp7  42848  3lexlogpow5ineq1  42849  3lexlogpow5ineq2  42850  3lexlogpow5ineq5  42855  aks4d1p1  42871  235t711  43094  ex-decpmul  43095  sum9cubes  43432  3cubeslem3l  43445  3cubeslem3r  43446  fmtno5lem1  48333  fmtno5lem3  48335  fmtno5lem4  48336  257prm  48341  fmtno4prmfac  48352  fmtno4nprmfac193  48354  fmtno5faclem1  48359  fmtno5faclem3  48361  fmtno5fac  48362  139prmALT  48376  127prm  48379  m7prm  48380  m11nprm  48381  2exp340mod341  48526  8exp8mod9  48529  nfermltl8rev  48535  bgoldbachlt  48606  tgblthelfgott  48608  tgoldbachlt  48609