Theorem 3nn0 12460

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

Syntax hints:   ∈ wcel 2109  3c3 12242  ℕ₀cn0 12442

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 5251  ax-nul 5261  ax-pr 5387  ax-un 7711  ax-1cn 11126

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 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-ov 7390  df-om 7843  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-nn 12187  df-2 12249  df-3 12250  df-n0 12443

This theorem is referenced by:  7p4e11  12725  7p7e14  12728  8p4e12  12731  8p6e14  12733  9p4e13  12738  9p5e14  12739  4t4e16  12748  5t4e20  12751  6t4e24  12755  6t6e36  12757  7t4e28  12760  7t6e42  12762  8t4e32  12766  8t5e40  12767  9t4e36  12773  9t5e45  12774  9t7e63  12776  9t8e72  12777  fz0to3un2pr  13590  4fvwrd4  13609  fldiv4p1lem1div2  13797  expnass  14173  binom3  14189  fac4  14246  4bc2eq6  14294  hash3tr  14456  tpf1o  14466  bpoly3  16024  bpoly4  16025  fsumcube  16026  ef4p  16081  efi4p  16105  resin4p  16106  recos4p  16107  ef01bndlem  16152  sin01bnd  16153  sin01gt0  16158  2exp5  17056  2exp6  17057  2exp8  17059  2exp11  17060  2exp16  17061  3exp3  17062  7prm  17081  11prm  17085  13prm  17086  17prm  17087  23prm  17089  prmlem2  17090  37prm  17091  43prm  17092  83prm  17093  139prm  17094  163prm  17095  317prm  17096  631prm  17097  1259lem1  17101  1259lem2  17102  1259lem3  17103  1259lem4  17104  1259lem5  17105  1259prm  17106  2503lem1  17107  2503lem2  17108  2503lem3  17109  2503prm  17110  4001lem1  17111  4001lem2  17112  4001lem3  17113  4001lem4  17114  4001prm  17115  dsndxnmulrndx  17354  basendxltunifndx  17361  unifndxntsetndx  17363  slotsdifunifndx  17364  tangtx  26414  1cubrlem  26751  dcubic1lem  26753  dcubic2  26754  dcubic1  26755  dcubic  26756  mcubic  26757  cubic2  26758  cubic  26759  binom4  26760  dquartlem2  26762  quart1cl  26764  quart1lem  26765  quart1  26766  quartlem1  26767  quartlem2  26768  quart  26771  log2ublem1  26856  log2ublem3  26858  log2ub  26859  log2le1  26860  birthday  26864  ppiublem2  27114  bclbnd  27191  bpos1  27194  bposlem8  27202  gausslemma2dlem4  27280  2lgslem3b  27308  2lgslem3d  27310  pntlemd  27505  pntlema  27507  pntlemb  27508  pntlemf  27516  pntlemo  27518  pntlem3  27520  tgcgr4  28458  iscgra  28736  isinag  28765  isleag  28774  iseqlg  28794  usgrexmplef  29186  upgr3v3e3cycl  30109  upgr4cycl4dv4e  30114  konigsbergiedgw  30177  konigsberglem1  30181  konigsberglem2  30182  konigsberglem3  30183  konigsberglem4  30184  ex-prmo  30388  threehalves  32835  evl1deg2  33546  evl1deg3  33547  ply1dg3rt0irred  33551  iconstr  33756  2sqr3minply  33770  2sqr3nconstr  33771  cos9thpiminplylem1  33772  cos9thpiminplylem2  33773  cos9thpiminplylem3  33774  cos9thpiminplylem4  33775  cos9thpiminplylem5  33776  cos9thpiminplylem6  33777  cos9thpiminply  33778  cos9thpinconstrlem2  33780  circlemethhgt  34634  hgt750lemd  34639  hgt750lem  34642  hgt750lem2  34643  hgt750lemb  34647  hgt750lema  34648  hgt750leme  34649  tgoldbachgtde  34651  tgoldbachgtda  34652  tgoldbachgt  34654  cusgracyclt3v  35143  kur14lem8  35200  3exp7  42041  3lexlogpow5ineq1  42042  3lexlogpow2ineq1  42046  3lexlogpow5ineq5  42048  aks4d1p1p7  42062  aks4d1p1p5  42063  aks4d1p1  42064  235t711  42293  ex-decpmul  42294  nicomachus  42300  3cubeslem3l  42674  3cubeslem3r  42675  3cubeslem4  42677  3cubes  42678  jm2.23  42985  jm2.20nn  42986  rmydioph  43003  rmxdioph  43005  expdiophlem2  43011  expdioph  43012  resqrtvalex  43634  amgm3d  44188  lhe4.4ex1a  44318  8mod5e3  47361  modm2nep1  47367  modm1nep2  47369  fmtno3  47552  fmtno4  47553  fmtno5lem1  47554  fmtno5lem2  47555  fmtno5lem3  47556  fmtno5lem4  47557  fmtno5  47558  257prm  47562  fmtnoprmfac2lem1  47567  fmtno4prmfac  47573  fmtno4prmfac193  47574  fmtno4nprmfac193  47575  fmtno5faclem2  47581  139prmALT  47597  31prm  47598  m5prm  47599  127prm  47600  m11nprm  47602  mod42tp1mod8  47603  11t31e341  47733  2exp340mod341  47734  341fppr2  47735  8exp8mod9  47737  nfermltl2rev  47744  tgoldbachlt  47817  tgoldbach  47818  grtriprop  47940  grtriclwlk3  47944  cycl3grtri  47946  usgrexmpl1lem  48012  usgrexmpl2lem  48017  usgrexmpl2nb2  48024  gpg5gricstgr3  48081  gpg5grlic  48084  gpgprismgr4cycllem7  48091  gpgprismgr4cycllem10  48094  zlmodzxzldeplem1  48489  itcoval3  48654  ackval3  48672  ackval0012  48678  ackval1012  48679  ackval2012  48680  ackval3012  48681  ackval40  48682  ackval41a  48683  ackval41  48684  ackval42  48685