Theorem 3nn0 12421

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

Assertion

Ref	Expression
3nn0	⊢ 3 ∈ ℕ0

Proof of Theorem 3nn0

Step	Hyp	Ref	Expression
1		3nn 12226	. 2 ⊢ 3 ∈ ℕ
2	1	nnnn0i 12411	1 ⊢ 3 ∈ ℕ0

Syntax hints:   ∈ wcel 2109  3c3 12203  ℕ₀cn0 12403

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7675  ax-1cn 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-iun 4946  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5518  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-we 5578  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-ov 7356  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-nn 12148  df-2 12210  df-3 12211  df-n0 12404

This theorem is referenced by:  7p4e11  12686  7p7e14  12689  8p4e12  12692  8p6e14  12694  9p4e13  12699  9p5e14  12700  4t4e16  12709  5t4e20  12712  6t4e24  12716  6t6e36  12718  7t4e28  12721  7t6e42  12723  8t4e32  12727  8t5e40  12728  9t4e36  12734  9t5e45  12735  9t7e63  12737  9t8e72  12738  fz0to3un2pr  13551  4fvwrd4  13570  fldiv4p1lem1div2  13758  expnass  14134  binom3  14150  fac4  14207  4bc2eq6  14255  hash3tr  14417  tpf1o  14427  bpoly3  15984  bpoly4  15985  fsumcube  15986  ef4p  16041  efi4p  16065  resin4p  16066  recos4p  16067  ef01bndlem  16112  sin01bnd  16113  sin01gt0  16118  2exp5  17016  2exp6  17017  2exp8  17019  2exp11  17020  2exp16  17021  3exp3  17022  7prm  17041  11prm  17045  13prm  17046  17prm  17047  23prm  17049  prmlem2  17050  37prm  17051  43prm  17052  83prm  17053  139prm  17054  163prm  17055  317prm  17056  631prm  17057  1259lem1  17061  1259lem2  17062  1259lem3  17063  1259lem4  17064  1259lem5  17065  1259prm  17066  2503lem1  17067  2503lem2  17068  2503lem3  17069  2503prm  17070  4001lem1  17071  4001lem2  17072  4001lem3  17073  4001lem4  17074  4001prm  17075  dsndxnmulrndx  17314  basendxltunifndx  17321  unifndxntsetndx  17323  slotsdifunifndx  17324  tangtx  26431  1cubrlem  26768  dcubic1lem  26770  dcubic2  26771  dcubic1  26772  dcubic  26773  mcubic  26774  cubic2  26775  cubic  26776  binom4  26777  dquartlem2  26779  quart1cl  26781  quart1lem  26782  quart1  26783  quartlem1  26784  quartlem2  26785  quart  26788  log2ublem1  26873  log2ublem3  26875  log2ub  26876  log2le1  26877  birthday  26881  ppiublem2  27131  bclbnd  27208  bpos1  27211  bposlem8  27219  gausslemma2dlem4  27297  2lgslem3b  27325  2lgslem3d  27327  pntlemd  27522  pntlema  27524  pntlemb  27525  pntlemf  27533  pntlemo  27535  pntlem3  27537  tgcgr4  28495  iscgra  28773  isinag  28802  isleag  28811  iseqlg  28831  usgrexmplef  29223  upgr3v3e3cycl  30143  upgr4cycl4dv4e  30148  konigsbergiedgw  30211  konigsberglem1  30215  konigsberglem2  30216  konigsberglem3  30217  konigsberglem4  30218  ex-prmo  30422  threehalves  32874  evl1deg2  33531  evl1deg3  33532  ply1dg3rt0irred  33537  iconstr  33752  2sqr3minply  33766  2sqr3nconstr  33767  cos9thpiminplylem1  33768  cos9thpiminplylem2  33769  cos9thpiminplylem3  33770  cos9thpiminplylem4  33771  cos9thpiminplylem5  33772  cos9thpiminplylem6  33773  cos9thpiminply  33774  cos9thpinconstrlem2  33776  circlemethhgt  34630  hgt750lemd  34635  hgt750lem  34638  hgt750lem2  34639  hgt750lemb  34643  hgt750lema  34644  hgt750leme  34645  tgoldbachgtde  34647  tgoldbachgtda  34648  tgoldbachgt  34650  cusgracyclt3v  35148  kur14lem8  35205  3exp7  42046  3lexlogpow5ineq1  42047  3lexlogpow2ineq1  42051  3lexlogpow5ineq5  42053  aks4d1p1p7  42067  aks4d1p1p5  42068  aks4d1p1  42069  235t711  42298  ex-decpmul  42299  nicomachus  42305  3cubeslem3l  42679  3cubeslem3r  42680  3cubeslem4  42682  3cubes  42683  jm2.23  42989  jm2.20nn  42990  rmydioph  43007  rmxdioph  43009  expdiophlem2  43015  expdioph  43016  resqrtvalex  43638  amgm3d  44192  lhe4.4ex1a  44322  8mod5e3  47364  modm2nep1  47370  modm1nep2  47372  fmtno3  47555  fmtno4  47556  fmtno5lem1  47557  fmtno5lem2  47558  fmtno5lem3  47559  fmtno5lem4  47560  fmtno5  47561  257prm  47565  fmtnoprmfac2lem1  47570  fmtno4prmfac  47576  fmtno4prmfac193  47577  fmtno4nprmfac193  47578  fmtno5faclem2  47584  139prmALT  47600  31prm  47601  m5prm  47602  127prm  47603  m11nprm  47605  mod42tp1mod8  47606  11t31e341  47736  2exp340mod341  47737  341fppr2  47738  8exp8mod9  47740  nfermltl2rev  47747  tgoldbachlt  47820  tgoldbach  47821  grtriprop  47945  grtriclwlk3  47949  cycl3grtri  47951  usgrexmpl1lem  48025  usgrexmpl2lem  48030  usgrexmpl2nb2  48037  gpg5gricstgr3  48094  gpg5grlim  48097  gpg5grlic  48098  gpgprismgr4cycllem7  48105  gpgprismgr4cycllem10  48108  gpg5edgnedg  48134  zlmodzxzldeplem1  48505  itcoval3  48670  ackval3  48688  ackval0012  48694  ackval1012  48695  ackval2012  48696  ackval3012  48697  ackval40  48698  ackval41a  48699  ackval41  48700  ackval42  48701