Theorem 7nn0 12500

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

Assertion

Ref	Expression
7nn0	⊢ 7 ∈ ℕ0

Proof of Theorem 7nn0

Step	Hyp	Ref	Expression
1		7nn 12310	. 2 ⊢ 7 ∈ ℕ
2	1	nnnn0i 12486	1 ⊢ 7 ∈ ℕ0

Syntax hints:   ∈ wcel 2104  7c7 12278  ℕ₀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-n0 12479

This theorem is referenced by:  7p4e11  12759  7p5e12  12760  7p6e13  12761  7p7e14  12762  8p8e16  12769  9p8e17  12776  9p9e18  12777  7t3e21  12793  7t4e28  12794  7t5e35  12795  7t6e42  12796  7t7e49  12797  8t8e64  12804  9t3e27  12806  9t4e36  12807  9t8e72  12811  9t9e81  12812  7prm  17050  17prm  17056  23prm  17058  prmlem2  17059  37prm  17060  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  quartlem1  26596  quartlem2  26597  log2ublem1  26685  log2ublem3  26687  log2ub  26688  bclbnd  27017  bpos1  27020  slotslnbpsd  27958  ex-prmo  29977  hgt750lemd  33956  hgt750lem  33959  hgt750lem2  33960  hgt750leme  33966  tgoldbachgnn  33967  tgoldbachgtde  33968  tgoldbachgt  33971  60lcm7e420  41183  3exp7  41226  3lexlogpow5ineq1  41227  3lexlogpow5ineq2  41228  3lexlogpow2ineq1  41231  3lexlogpow5ineq5  41233  aks4d1p1  41249  235t711  41509  ex-decpmul  41510  3cubeslem3l  41728  3cubeslem3r  41729  expdiophlem2  42065  resqrtvalex  42700  imsqrtvalex  42701  fmtno5lem2  46522  fmtno5lem4  46524  fmtno5  46525  257prm  46529  fmtno4nprmfac193  46542  fmtno5faclem1  46547  fmtno5faclem2  46548  fmtno5fac  46550  fmtno5nprm  46551  139prmALT  46564  127prm  46567  m11nprm  46569  2exp340mod341  46701  tgoldbach  46785  ackval2012  47466