Theorem 4nn0 12406

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 12214	. 2 ⊢ 4 ∈ ℕ
2	1	nnnn0i 12395	1 ⊢ 4 ∈ ℕ0

Syntax hints:   ∈ wcel 2111  4c4 12188  ℕ₀cn0 12387

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5236  ax-nul 5246  ax-pr 5372  ax-un 7674  ax-1cn 11070

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 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-iun 4943  df-br 5094  df-opab 5156  df-mpt 5175  df-tr 5201  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6254  df-ord 6315  df-on 6316  df-lim 6317  df-suc 6318  df-iota 6443  df-fun 6489  df-fn 6490  df-f 6491  df-f1 6492  df-fo 6493  df-f1o 6494  df-fv 6495  df-ov 7355  df-om 7803  df-2nd 7928  df-frecs 8217  df-wrecs 8248  df-recs 8297  df-rdg 8335  df-nn 12132  df-2 12194  df-3 12195  df-4 12196  df-n0 12388

This theorem is referenced by:  6p5e11  12667  7p5e12  12671  8p5e13  12677  8p7e15  12679  9p5e14  12684  9p6e15  12685  4t3e12  12692  4t4e16  12693  5t5e25  12697  6t4e24  12700  6t5e30  12701  7t3e21  12704  7t5e35  12706  7t7e49  12708  8t3e24  12710  8t4e32  12711  8t5e40  12712  8t6e48  12713  8t7e56  12714  8t8e64  12715  9t5e45  12719  9t6e54  12720  9t7e63  12721  decbin3  12736  fzo0to42pr  13659  4bc3eq4  14241  bpoly4  15972  fsumcube  15973  resin4p  16053  recos4p  16054  ef01bndlem  16099  sin01bnd  16100  cos01bnd  16101  prm23lt5  16732  2exp7  17005  2exp8  17006  2exp11  17007  2exp16  17008  2expltfac  17010  13prm  17033  19prm  17035  prmlem2  17037  37prm  17038  43prm  17039  83prm  17040  139prm  17041  163prm  17042  317prm  17043  631prm  17044  1259lem1  17048  1259lem2  17049  1259lem3  17050  1259lem4  17051  1259lem5  17052  1259prm  17053  2503lem1  17054  2503lem2  17055  2503lem3  17056  2503prm  17057  4001lem1  17058  4001lem2  17059  4001lem3  17060  4001lem4  17061  4001prm  17062  slotsdifdsndx  17304  slotsdifunifndx  17311  slotsbhcdif  17325  prdsvalstr  17362  catstr  17873  lt6abl  19813  binom4  26793  dquart  26796  quart1cl  26797  quart1lem  26798  quart1  26799  log2ublem3  26891  log2ub  26892  ppiublem2  27147  bclbnd  27224  bpos1  27227  bposlem8  27235  bposlem9  27236  bpos  27237  2lgslem3a  27340  2lgslem3b  27341  2lgslem3c  27342  2lgslem3d  27343  usgrexmplef  29244  upgr4cycl4dv4e  30172  ex-exp  30437  ex-fac  30438  ex-bc  30439  ex-ind-dvds  30448  evl1deg3  33548  hgt750lemd  34668  hgt750lem  34671  hgt750lem2  34672  hgt750leme  34678  tgoldbachgtde  34680  kur14lem9  35265  60gcd7e1  42104  420gcd8e4  42105  60lcm7e420  42109  420lcm8e840  42110  lcmineqlem  42151  3exp7  42152  3lexlogpow5ineq1  42153  3lexlogpow5ineq2  42154  3lexlogpow5ineq5  42159  aks4d1p1p2  42169  aks4d1p1p4  42170  aks4d1p1p6  42172  aks4d1p1p7  42173  aks4d1p1p5  42174  aks4d1p1  42175  5bc2eq10  42241  235t711  42404  ex-decpmul  42405  flt4lem6  42757  flt4lem7  42758  nna4b4nsq  42759  sq45  42770  sum9cubes  42771  3cubeslem3l  42784  3cubeslem3r  42785  rmxdioph  43114  resqrtvalex  43743  imsqrtvalex  43744  inductionexd  44253  amgm4d  44298  wallispi2lem1  46174  wallispi2lem2  46175  wallispi2  46176  stirlinglem3  46179  stirlinglem8  46184  stirlinglem15  46191  smfmullem2  46895  modm1p1ne  47475  fmtno4  47657  fmtno5lem4  47661  fmtno5  47662  257prm  47666  fmtno4prmfac  47677  fmtno4prmfac193  47678  fmtno4nprmfac193  47679  fmtno4prm  47680  fmtnofz04prm  47682  fmtnole4prm  47683  fmtno5faclem1  47684  fmtno5faclem2  47685  fmtno5faclem3  47686  fmtno5fac  47687  fmtno5nprm  47688  139prmALT  47701  127prm  47704  m11nprm  47706  3exp4mod41  47721  41prothprmlem2  47723  2exp340mod341  47838  341fppr2  47839  8exp8mod9  47841  nfermltl2rev  47848  usgrexmpl1lem  48126  usgrexmpl2lem  48131  usgrexmpl2nb0  48136  usgrexmpl2nb1  48137  usgrexmpl2nb2  48138  usgrexmpl2nb3  48139  usgrexmpl2trifr  48142  gpgprismgr4cycllem7  48206  ackval1012  48796  ackval42  48802  ackval50  48804