Theorem 3nn0 12544

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

Syntax hints:   ∈ wcel 2108  3c3 12322  ℕ₀cn0 12526

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755  ax-1cn 11213

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-nn 12267  df-2 12329  df-3 12330  df-n0 12527

This theorem is referenced by:  7p4e11  12809  7p7e14  12812  8p4e12  12815  8p6e14  12817  9p4e13  12822  9p5e14  12823  4t4e16  12832  5t4e20  12835  6t4e24  12839  6t6e36  12841  7t4e28  12844  7t6e42  12846  8t4e32  12850  8t5e40  12851  9t4e36  12857  9t5e45  12858  9t7e63  12860  9t8e72  12861  fz0to3un2pr  13669  4fvwrd4  13688  fldiv4p1lem1div2  13875  expnass  14247  binom3  14263  fac4  14320  4bc2eq6  14368  hash3tr  14530  tpf1o  14540  bpoly3  16094  bpoly4  16095  fsumcube  16096  ef4p  16149  efi4p  16173  resin4p  16174  recos4p  16175  ef01bndlem  16220  sin01bnd  16221  sin01gt0  16226  2exp5  17123  2exp6  17124  2exp8  17126  2exp11  17127  2exp16  17128  3exp3  17129  7prm  17148  11prm  17152  13prm  17153  17prm  17154  23prm  17156  prmlem2  17157  37prm  17158  43prm  17159  83prm  17160  139prm  17161  163prm  17162  317prm  17163  631prm  17164  1259lem1  17168  1259lem2  17169  1259lem3  17170  1259lem4  17171  1259lem5  17172  1259prm  17173  2503lem1  17174  2503lem2  17175  2503lem3  17176  2503prm  17177  4001lem1  17178  4001lem2  17179  4001lem3  17180  4001lem4  17181  4001prm  17182  dsndxnmulrndx  17435  basendxltunifndx  17442  unifndxntsetndx  17444  slotsdifunifndx  17445  cnfldfunALTOLDOLD  21393  tuslemOLD  24276  tangtx  26547  1cubrlem  26884  dcubic1lem  26886  dcubic2  26887  dcubic1  26888  dcubic  26889  mcubic  26890  cubic2  26891  cubic  26892  binom4  26893  dquartlem2  26895  quart1cl  26897  quart1lem  26898  quart1  26899  quartlem1  26900  quartlem2  26901  quart  26904  log2ublem1  26989  log2ublem3  26991  log2ub  26992  log2le1  26993  birthday  26997  ppiublem2  27247  bclbnd  27324  bpos1  27327  bposlem8  27335  gausslemma2dlem4  27413  2lgslem3b  27441  2lgslem3d  27443  pntlemd  27638  pntlema  27640  pntlemb  27641  pntlemf  27649  pntlemo  27651  pntlem3  27653  tgcgr4  28539  iscgra  28817  isinag  28846  isleag  28855  iseqlg  28875  usgrexmplef  29276  upgr3v3e3cycl  30199  upgr4cycl4dv4e  30204  konigsbergiedgw  30267  konigsberglem1  30271  konigsberglem2  30272  konigsberglem3  30273  konigsberglem4  30274  ex-prmo  30478  threehalves  32897  evl1deg2  33602  evl1deg3  33603  ply1dg3rt0irred  33607  2sqr3minply  33791  circlemethhgt  34658  hgt750lemd  34663  hgt750lem  34666  hgt750lem2  34667  hgt750lemb  34671  hgt750lema  34672  hgt750leme  34673  tgoldbachgtde  34675  tgoldbachgtda  34676  tgoldbachgt  34678  cusgracyclt3v  35161  kur14lem8  35218  3exp7  42054  3lexlogpow5ineq1  42055  3lexlogpow2ineq1  42059  3lexlogpow5ineq5  42061  aks4d1p1p7  42075  aks4d1p1p5  42076  aks4d1p1  42077  235t711  42339  ex-decpmul  42340  nicomachus  42346  3cubeslem3l  42697  3cubeslem3r  42698  3cubeslem4  42700  3cubes  42701  jm2.23  43008  jm2.20nn  43009  rmydioph  43026  rmxdioph  43028  expdiophlem2  43034  expdioph  43035  resqrtvalex  43658  amgm3d  44212  lhe4.4ex1a  44348  fmtno3  47538  fmtno4  47539  fmtno5lem1  47540  fmtno5lem2  47541  fmtno5lem3  47542  fmtno5lem4  47543  fmtno5  47544  257prm  47548  fmtnoprmfac2lem1  47553  fmtno4prmfac  47559  fmtno4prmfac193  47560  fmtno4nprmfac193  47561  fmtno5faclem2  47567  139prmALT  47583  31prm  47584  m5prm  47585  127prm  47586  m11nprm  47588  mod42tp1mod8  47589  11t31e341  47719  2exp340mod341  47720  341fppr2  47721  8exp8mod9  47723  nfermltl2rev  47730  tgoldbachlt  47803  tgoldbach  47804  grtriprop  47908  grtriclwlk3  47912  cycl3grtri  47914  usgrexmpl1lem  47980  usgrexmpl2lem  47985  usgrexmpl2nb2  47992  gpg5gricstgr3  48046  gpg5grlic  48047  zlmodzxzldeplem1  48417  itcoval3  48586  ackval3  48604  ackval0012  48610  ackval1012  48611  ackval2012  48612  ackval3012  48613  ackval40  48614  ackval41a  48615  ackval41  48616  ackval42  48617