Theorem 3nn0 12467

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 12272	. 2 ⊢ 3 ∈ ℕ
2	1	nnnn0i 12457	1 ⊢ 3 ∈ ℕ0

Syntax hints:   ∈ wcel 2109  3c3 12249  ℕ₀cn0 12449

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714  ax-1cn 11133

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-ov 7393  df-om 7846  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-nn 12194  df-2 12256  df-3 12257  df-n0 12450

This theorem is referenced by:  7p4e11  12732  7p7e14  12735  8p4e12  12738  8p6e14  12740  9p4e13  12745  9p5e14  12746  4t4e16  12755  5t4e20  12758  6t4e24  12762  6t6e36  12764  7t4e28  12767  7t6e42  12769  8t4e32  12773  8t5e40  12774  9t4e36  12780  9t5e45  12781  9t7e63  12783  9t8e72  12784  fz0to3un2pr  13597  4fvwrd4  13616  fldiv4p1lem1div2  13804  expnass  14180  binom3  14196  fac4  14253  4bc2eq6  14301  hash3tr  14463  tpf1o  14473  bpoly3  16031  bpoly4  16032  fsumcube  16033  ef4p  16088  efi4p  16112  resin4p  16113  recos4p  16114  ef01bndlem  16159  sin01bnd  16160  sin01gt0  16165  2exp5  17063  2exp6  17064  2exp8  17066  2exp11  17067  2exp16  17068  3exp3  17069  7prm  17088  11prm  17092  13prm  17093  17prm  17094  23prm  17096  prmlem2  17097  37prm  17098  43prm  17099  83prm  17100  139prm  17101  163prm  17102  317prm  17103  631prm  17104  1259lem1  17108  1259lem2  17109  1259lem3  17110  1259lem4  17111  1259lem5  17112  1259prm  17113  2503lem1  17114  2503lem2  17115  2503lem3  17116  2503prm  17117  4001lem1  17118  4001lem2  17119  4001lem3  17120  4001lem4  17121  4001prm  17122  dsndxnmulrndx  17361  basendxltunifndx  17368  unifndxntsetndx  17370  slotsdifunifndx  17371  tangtx  26421  1cubrlem  26758  dcubic1lem  26760  dcubic2  26761  dcubic1  26762  dcubic  26763  mcubic  26764  cubic2  26765  cubic  26766  binom4  26767  dquartlem2  26769  quart1cl  26771  quart1lem  26772  quart1  26773  quartlem1  26774  quartlem2  26775  quart  26778  log2ublem1  26863  log2ublem3  26865  log2ub  26866  log2le1  26867  birthday  26871  ppiublem2  27121  bclbnd  27198  bpos1  27201  bposlem8  27209  gausslemma2dlem4  27287  2lgslem3b  27315  2lgslem3d  27317  pntlemd  27512  pntlema  27514  pntlemb  27515  pntlemf  27523  pntlemo  27525  pntlem3  27527  tgcgr4  28465  iscgra  28743  isinag  28772  isleag  28781  iseqlg  28801  usgrexmplef  29193  upgr3v3e3cycl  30116  upgr4cycl4dv4e  30121  konigsbergiedgw  30184  konigsberglem1  30188  konigsberglem2  30189  konigsberglem3  30190  konigsberglem4  30191  ex-prmo  30395  threehalves  32842  evl1deg2  33553  evl1deg3  33554  ply1dg3rt0irred  33558  iconstr  33763  2sqr3minply  33777  2sqr3nconstr  33778  cos9thpiminplylem1  33779  cos9thpiminplylem2  33780  cos9thpiminplylem3  33781  cos9thpiminplylem4  33782  cos9thpiminplylem5  33783  cos9thpiminplylem6  33784  cos9thpiminply  33785  cos9thpinconstrlem2  33787  circlemethhgt  34641  hgt750lemd  34646  hgt750lem  34649  hgt750lem2  34650  hgt750lemb  34654  hgt750lema  34655  hgt750leme  34656  tgoldbachgtde  34658  tgoldbachgtda  34659  tgoldbachgt  34661  cusgracyclt3v  35150  kur14lem8  35207  3exp7  42048  3lexlogpow5ineq1  42049  3lexlogpow2ineq1  42053  3lexlogpow5ineq5  42055  aks4d1p1p7  42069  aks4d1p1p5  42070  aks4d1p1  42071  235t711  42300  ex-decpmul  42301  nicomachus  42307  3cubeslem3l  42681  3cubeslem3r  42682  3cubeslem4  42684  3cubes  42685  jm2.23  42992  jm2.20nn  42993  rmydioph  43010  rmxdioph  43012  expdiophlem2  43018  expdioph  43019  resqrtvalex  43641  amgm3d  44195  lhe4.4ex1a  44325  8mod5e3  47365  modm2nep1  47371  modm1nep2  47373  fmtno3  47556  fmtno4  47557  fmtno5lem1  47558  fmtno5lem2  47559  fmtno5lem3  47560  fmtno5lem4  47561  fmtno5  47562  257prm  47566  fmtnoprmfac2lem1  47571  fmtno4prmfac  47577  fmtno4prmfac193  47578  fmtno4nprmfac193  47579  fmtno5faclem2  47585  139prmALT  47601  31prm  47602  m5prm  47603  127prm  47604  m11nprm  47606  mod42tp1mod8  47607  11t31e341  47737  2exp340mod341  47738  341fppr2  47739  8exp8mod9  47741  nfermltl2rev  47748  tgoldbachlt  47821  tgoldbach  47822  grtriprop  47944  grtriclwlk3  47948  cycl3grtri  47950  usgrexmpl1lem  48016  usgrexmpl2lem  48021  usgrexmpl2nb2  48028  gpg5gricstgr3  48085  gpg5grlic  48088  gpgprismgr4cycllem7  48095  gpgprismgr4cycllem10  48098  zlmodzxzldeplem1  48493  itcoval3  48658  ackval3  48676  ackval0012  48682  ackval1012  48683  ackval2012  48684  ackval3012  48685  ackval40  48686  ackval41a  48687  ackval41  48688  ackval42  48689