Theorem 7nn0 12532

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

This proof depends on syntax axioms:   ∈ wcel 2142  7c7 12306  ℕ₀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-n0 12511

This theorem is used by:  7p4e11  12798  7p5e12  12799  7p6e13  12800  7p7e14  12801  8p8e16  12808  9p8e17  12815  9p9e18  12816  7t3e21  12832  7t4e28  12833  7t5e35  12834  7t6e42  12835  7t7e49  12836  8t8e64  12843  9t3e27  12845  9t4e36  12846  9t8e72  12850  9t9e81  12851  7lt10  12856  s7f1o  15010  7prm  17176  17prm  17183  23prm  17185  prmlem2  17186  37prm  17187  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  quartlem1  27033  quartlem2  27034  log2ublem1  27122  log2ublem3  27124  log2ub  27125  bclbnd  27455  bpos1  27458  slotslnbpsd  28722  ex-prmo  30821  hgt750lemd  35044  hgt750lem  35047  hgt750lem2  35048  hgt750leme  35054  tgoldbachgnn  35055  tgoldbachgtde  35056  tgoldbachgt  35059  60lcm7e420  42805  3exp7  42848  3lexlogpow5ineq1  42849  3lexlogpow5ineq2  42850  3lexlogpow2ineq1  42853  3lexlogpow5ineq5  42855  aks4d1p1  42871  235t711  43094  ex-decpmul  43095  3cubeslem3l  43445  3cubeslem3r  43446  expdiophlem2  43777  resqrtvalex  44399  imsqrtvalex  44400  fmtno5lem2  48334  fmtno5lem4  48336  fmtno5  48337  257prm  48341  fmtno4nprmfac193  48354  fmtno5faclem1  48359  fmtno5faclem2  48360  fmtno5fac  48362  fmtno5nprm  48363  139prmALT  48376  127prm  48379  m11nprm  48381  2exp340mod341  48526  tgoldbach  48610  ackval2012  49499