Theorem 3nn0 12450

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

Syntax hints:   ∈ wcel 2121  3c3 12232  ℕ₀cn0 12432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5221  ax-nul 5231  ax-pr 5365  ax-un 7682  ax-1cn 11091

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3or 1094  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-ral 3056  df-rex 3066  df-reu 3347  df-rab 3394  df-v 3435  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-pss 3905  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-iun 4926  df-br 5076  df-opab 5138  df-mpt 5157  df-tr 5183  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6256  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-ov 7363  df-om 7811  df-2nd 7936  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-nn 12170  df-2 12239  df-3 12240  df-n0 12433

This theorem is referenced by:  7p4e11  12715  7p7e14  12718  8p4e12  12721  8p6e14  12723  9p4e13  12728  9p5e14  12729  4t4e16  12738  5t4e20  12741  6t4e24  12745  6t6e36  12747  7t4e28  12750  7t6e42  12752  8t4e32  12756  8t5e40  12757  9t4e36  12763  9t5e45  12764  9t7e63  12766  9t8e72  12767  fz0to3un2pr  13578  4fvwrd4  13597  fldiv4p1lem1div2  13789  expnass  14165  binom3  14181  fac4  14238  4bc2eq6  14286  hash3tr  14448  tpf1o  14458  bpoly3  16018  bpoly4  16019  fsumcube  16020  ef4p  16075  efi4p  16099  resin4p  16100  recos4p  16101  ef01bndlem  16146  sin01bnd  16147  sin01gt0  16152  2exp5  17051  2exp6  17052  2exp8  17054  2exp11  17055  2exp16  17056  3exp3  17057  7prm  17076  11prm  17080  13prm  17081  17prm  17082  23prm  17084  prmlem2  17085  37prm  17086  43prm  17087  83prm  17088  139prm  17089  163prm  17090  317prm  17091  631prm  17092  1259lem1  17096  1259lem2  17097  1259lem3  17098  1259lem4  17099  1259lem5  17100  1259prm  17101  2503lem1  17102  2503lem2  17103  2503lem3  17104  2503prm  17105  4001lem1  17106  4001lem2  17107  4001lem3  17108  4001lem4  17109  4001prm  17110  dsndxnmulrndx  17349  basendxltunifndx  17356  unifndxntsetndx  17358  slotsdifunifndx  17359  tangtx  26491  1cubrlem  26827  dcubic1lem  26829  dcubic2  26830  dcubic1  26831  dcubic  26832  mcubic  26833  cubic2  26834  cubic  26835  binom4  26836  dquartlem2  26838  quart1cl  26840  quart1lem  26841  quart1  26842  quartlem1  26843  quartlem2  26844  quart  26847  log2ublem1  26932  log2ublem3  26934  log2ub  26935  log2le1  26936  birthday  26940  ppiublem2  27188  bclbnd  27265  bpos1  27268  bposlem8  27276  gausslemma2dlem4  27354  2lgslem3b  27382  2lgslem3d  27384  pntlemd  27579  pntlema  27581  pntlemb  27582  pntlemf  27590  pntlemo  27592  pntlem3  27594  tgcgr4  28621  iscgra  28899  isinag  28928  isleag  28937  iseqlg  28957  usgrexmplef  29350  upgr3v3e3cycl  30272  upgr4cycl4dv4e  30277  konigsbergiedgw  30340  konigsberglem1  30344  konigsberglem2  30345  konigsberglem3  30346  konigsberglem4  30347  ex-prmo  30551  threehalves  32997  evl1deg2  33672  evl1deg3  33673  ply1dg3rt0irred  33679  iconstr  33962  2sqr3minply  33976  2sqr3nconstr  33977  cos9thpiminplylem1  33978  cos9thpiminplylem2  33979  cos9thpiminplylem3  33980  cos9thpiminplylem4  33981  cos9thpiminplylem5  33982  cos9thpiminplylem6  33983  cos9thpiminply  33984  cos9thpinconstrlem2  33986  circlemethhgt  34839  hgt750lemd  34844  hgt750lem  34847  hgt750lem2  34848  hgt750lemb  34852  hgt750lema  34853  hgt750leme  34854  tgoldbachgtde  34856  tgoldbachgtda  34857  tgoldbachgt  34859  cusgracyclt3v  35399  kur14lem8  35456  3exp7  42553  3lexlogpow5ineq1  42554  3lexlogpow2ineq1  42558  3lexlogpow5ineq5  42560  aks4d1p1p7  42574  aks4d1p1p5  42575  aks4d1p1  42576  235t711  42797  ex-decpmul  42798  nicomachus  42804  3cubeslem3l  43150  3cubeslem3r  43151  3cubeslem4  43153  3cubes  43154  jm2.23  43456  jm2.20nn  43457  rmydioph  43474  rmxdioph  43476  expdiophlem2  43482  expdioph  43483  resqrtvalex  44104  amgm3d  44658  lhe4.4ex1a  44788  sin3t  47348  cos3t  47349  sin5tlem1  47350  sin5tlem2  47351  sin5tlem3  47352  sin5tlem4  47353  sin5tlem5  47354  goldratmolem2  47363  8mod5e3  47843  modm2nep1  47849  modm1nep2  47851  fmtno3  48043  fmtno4  48044  fmtno5lem1  48045  fmtno5lem2  48046  fmtno5lem3  48047  fmtno5lem4  48048  fmtno5  48049  257prm  48053  fmtnoprmfac2lem1  48058  fmtno4prmfac  48064  fmtno4prmfac193  48065  fmtno4nprmfac193  48066  fmtno5faclem2  48072  139prmALT  48088  31prm  48089  m5prm  48090  127prm  48091  m11nprm  48093  mod42tp1mod8  48094  ppivalnn4  48119  11t31e341  48237  2exp340mod341  48238  341fppr2  48239  8exp8mod9  48241  nfermltl2rev  48248  tgoldbachlt  48321  tgoldbach  48322  grtriprop  48446  grtriclwlk3  48450  cycl3grtri  48452  usgrexmpl1lem  48526  usgrexmpl2lem  48531  usgrexmpl2nb2  48538  gpg5gricstgr3  48595  gpg5grlim  48598  gpg5grlic  48599  gpgprismgr4cycllem7  48606  gpgprismgr4cycllem10  48609  gpg5edgnedg  48635  zlmodzxzldeplem1  49005  itcoval3  49170  ackval3  49188  ackval0012  49194  ackval1012  49195  ackval2012  49196  ackval3012  49197  ackval40  49198  ackval41a  49199  ackval41  49200  ackval42  49201