Theorem 4nn0 12157

Description: 4 is a nonnegative integer. (Contributed by Mario Carneiro, 18-Feb-2014.)

Assertion

Ref	Expression
4nn0	⊢ 4 ∈ ℕ0

Proof of Theorem 4nn0

Step	Hyp	Ref	Expression
1		4nn 11961	. 2 ⊢ 4 ∈ ℕ
2	1	nnnn0i 12146	1 ⊢ 4 ∈ ℕ0

Syntax hints:   ∈ wcel 2112  4c4 11935  ℕ₀cn0 12138

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-sep 5216  ax-nul 5223  ax-pr 5346  ax-un 7563  ax-1cn 10835

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3071  df-rab 3073  df-v 3425  df-sbc 3713  df-csb 3830  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4255  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5153  df-tr 5186  df-id 5479  df-eprel 5485  df-po 5493  df-so 5494  df-fr 5534  df-we 5536  df-xp 5585  df-rel 5586  df-cnv 5587  df-co 5588  df-dm 5589  df-rn 5590  df-res 5591  df-ima 5592  df-pred 6189  df-ord 6251  df-on 6252  df-lim 6253  df-suc 6254  df-iota 6373  df-fun 6417  df-fn 6418  df-f 6419  df-f1 6420  df-fo 6421  df-f1o 6422  df-fv 6423  df-ov 7255  df-om 7685  df-wrecs 8089  df-recs 8150  df-rdg 8188  df-nn 11879  df-2 11941  df-3 11942  df-4 11943  df-n0 12139

This theorem is referenced by:  6p5e11  12414  7p5e12  12418  8p5e13  12424  8p7e15  12426  9p5e14  12431  9p6e15  12432  4t3e12  12439  4t4e16  12440  5t5e25  12444  6t4e24  12447  6t5e30  12448  7t3e21  12451  7t5e35  12453  7t7e49  12455  8t3e24  12457  8t4e32  12458  8t5e40  12459  8t6e48  12460  8t7e56  12461  8t8e64  12462  9t5e45  12466  9t6e54  12467  9t7e63  12468  decbin3  12483  fzo0to42pr  13377  4bc3eq4  13945  bpoly4  15672  fsumcube  15673  resin4p  15750  recos4p  15751  ef01bndlem  15796  sin01bnd  15797  cos01bnd  15798  prm23lt5  16418  decexp2  16679  2exp7  16692  2exp8  16693  2exp11  16694  2exp16  16695  2expltfac  16697  13prm  16720  19prm  16722  prmlem2  16724  37prm  16725  43prm  16726  83prm  16727  139prm  16728  163prm  16729  317prm  16730  631prm  16731  1259lem1  16735  1259lem2  16736  1259lem3  16737  1259lem4  16738  1259lem5  16739  1259prm  16740  2503lem1  16741  2503lem2  16742  2503lem3  16743  2503prm  16744  4001lem1  16745  4001lem2  16746  4001lem3  16747  4001lem4  16748  4001prm  16749  slotsbhcdif  17019  slotsbhcdifOLD  17020  prdsvalstr  17055  oppchomfvalOLD  17316  oppcbasOLD  17321  rescbasOLD  17434  resccoOLD  17438  rescabs  17439  catstr  17565  lt6abl  19386  cnfldfun  20497  binom4  25880  dquart  25883  quart1cl  25884  quart1lem  25885  quart1  25886  log2ublem3  25978  log2ub  25979  ppiublem2  26231  bclbnd  26308  bpos1  26311  bposlem8  26319  bposlem9  26320  bpos  26321  2lgslem3a  26424  2lgslem3b  26425  2lgslem3c  26426  2lgslem3d  26427  usgrexmplef  27504  upgr4cycl4dv4e  28425  ex-exp  28690  ex-fac  28691  ex-bc  28692  ex-ind-dvds  28701  hgt750lemd  32503  hgt750lem  32506  hgt750lem2  32507  hgt750leme  32513  tgoldbachgtde  32515  kur14lem9  33051  60gcd7e1  39920  420gcd8e4  39921  60lcm7e420  39925  420lcm8e840  39926  lcmineqlem  39967  3exp7  39968  3lexlogpow5ineq1  39969  3lexlogpow5ineq2  39970  3lexlogpow5ineq5  39975  aks4d1p1p2  39984  aks4d1p1p4  39985  aks4d1p1p6  39987  aks4d1p1p7  39988  aks4d1p1p5  39989  aks4d1p1  39990  5bc2eq10  39998  235t711  40212  ex-decpmul  40213  flt4lem6  40383  flt4lem7  40384  nna4b4nsq  40385  3cubeslem3l  40396  3cubeslem3r  40397  rmxdioph  40726  resqrtvalex  41114  imsqrtvalex  41115  inductionexd  41627  amgm4d  41673  wallispi2lem1  43475  wallispi2lem2  43476  wallispi2  43477  stirlinglem3  43480  stirlinglem8  43485  stirlinglem15  43492  smfmullem2  44186  fmtno4  44865  fmtno5lem4  44869  fmtno5  44870  257prm  44874  fmtno4prmfac  44885  fmtno4prmfac193  44886  fmtno4nprmfac193  44887  fmtno4prm  44888  fmtnofz04prm  44890  fmtnole4prm  44891  fmtno5faclem1  44892  fmtno5faclem2  44893  fmtno5faclem3  44894  fmtno5fac  44895  fmtno5nprm  44896  139prmALT  44909  127prm  44912  m11nprm  44914  3exp4mod41  44929  41prothprmlem2  44931  2exp340mod341  45046  341fppr2  45047  8exp8mod9  45049  nfermltl2rev  45056  ackval1012  45897  ackval42  45903  ackval50  45905