Theorem 3nn0 12517

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

Syntax hints:   ∈ wcel 2143  3c3 12291  ℕ₀cn0 12499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404  ax-un 7732  ax-1cn 11153

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  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 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7413  df-om 7859  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-nn 12229  df-2 12298  df-3 12299  df-n0 12500

This theorem is referenced by:  7p4e11  12787  7p7e14  12790  8p4e12  12793  8p6e14  12795  9p4e13  12800  9p5e14  12801  4t4e16  12810  5t4e20  12813  6t4e24  12817  6t6e36  12819  7t4e28  12822  7t6e42  12824  8t4e32  12828  8t5e40  12829  9t4e36  12835  9t5e45  12836  9t7e63  12838  9t8e72  12839  3lt10  12849  fz0to3un2pr  13653  4fvwrd4  13672  fldiv4p1lem1div2  13864  expnass  14240  binom3  14256  fac4  14313  4bc2eq6  14361  hash3tr  14524  tpf1o  14534  bpoly3  16107  bpoly4  16108  fsumcube  16109  ef4p  16164  efi4p  16188  resin4p  16189  recos4p  16190  ef01bndlem  16235  sin01bnd  16236  sin01gt0  16241  2exp5  17140  2exp6  17141  2exp8  17143  2exp11  17144  2exp16  17145  3exp3  17146  7prm  17165  11prm  17170  13prm  17171  17prm  17172  23prm  17174  prmlem2  17175  37prm  17176  43prm  17177  83prm  17178  139prm  17179  163prm  17180  317prm  17181  631prm  17182  1259lem1  17186  1259lem2  17187  1259lem3  17188  1259lem4  17189  1259lem5  17190  1259prm  17191  2503lem1  17192  2503lem2  17193  2503lem3  17194  2503prm  17195  4001lem1  17196  4001lem2  17197  4001lem3  17198  4001lem4  17199  4001prm  17200  dsndxnmulrndx  17439  basendxltunifndx  17446  unifndxntsetndx  17448  slotsdifunifndx  17449  tangtx  26670  1cubrlem  27006  dcubic1lem  27008  dcubic2  27009  dcubic1  27010  dcubic  27011  mcubic  27012  cubic2  27013  cubic  27014  binom4  27015  dquartlem2  27017  quart1cl  27019  quart1lem  27020  quart1  27021  quartlem1  27022  quartlem2  27023  quart  27026  log2ublem1  27111  log2ublem3  27113  log2ub  27114  log2le1  27115  birthday  27119  ppiublem2  27367  bclbnd  27444  bpos1  27447  bposlem8  27455  gausslemma2dlem4  27533  2lgslem3b  27561  2lgslem3d  27563  pntlemd  27758  pntlema  27760  pntlemb  27761  pntlemf  27769  pntlemo  27771  pntlem3  27773  tgcgr4  28800  iscgra  29120  isinag  29155  isleag  29164  iseqlg  29184  usgrexmplef  29609  upgr3v3e3cycl  30531  upgr4cycl4dv4e  30536  konigsbergiedgw  30599  konigsberglem1  30603  konigsberglem2  30604  konigsberglem3  30605  konigsberglem4  30606  ex-prmo  30810  threehalves  33234  evl1deg2  33867  evl1deg3  33868  ply1dg3rt0irred  33874  iconstr  34156  2sqr3minply  34170  2sqr3nconstr  34171  cos9thpiminplylem1  34172  cos9thpiminplylem2  34173  cos9thpiminplylem3  34174  cos9thpiminplylem4  34175  cos9thpiminplylem5  34176  cos9thpiminplylem6  34177  cos9thpiminply  34178  cos9thpinconstrlem2  34180  circlemethhgt  35030  hgt750lemd  35035  hgt750lem  35038  hgt750lem2  35039  hgt750lemb  35043  hgt750lema  35044  hgt750leme  35045  tgoldbachgtde  35047  tgoldbachgtda  35048  tgoldbachgt  35050  cusgracyclt3v  35648  kur14lem8  35705  3exp7  42820  3lexlogpow5ineq1  42821  3lexlogpow2ineq1  42825  3lexlogpow5ineq5  42827  aks4d1p1p7  42841  aks4d1p1p5  42842  aks4d1p1  42843  25or6to4  42973  235t711  43066  ex-decpmul  43067  nicomachus  43073  3cubeslem3l  43417  3cubeslem3r  43418  3cubeslem4  43420  3cubes  43421  jm2.23  43723  jm2.20nn  43724  rmydioph  43741  rmxdioph  43743  expdiophlem2  43749  expdioph  43750  resqrtvalex  44371  amgm3d  44925  lhe4.4ex1a  45039  sin3t  47608  cos3t  47609  sin5tlem1  47610  sin5tlem2  47611  sin5tlem3  47612  sin5tlem4  47613  sin5tlem5  47614  goldratmolem2  47623  8mod5e3  48103  modm2nep1  48109  modm1nep2  48111  fmtno3  48303  fmtno4  48304  fmtno5lem1  48305  fmtno5lem2  48306  fmtno5lem3  48307  fmtno5lem4  48308  fmtno5  48309  257prm  48313  fmtnoprmfac2lem1  48318  fmtno4prmfac  48324  fmtno4prmfac193  48325  fmtno4nprmfac193  48326  fmtno5faclem2  48332  139prmALT  48348  31prm  48349  m5prm  48350  127prm  48351  m11nprm  48353  mod42tp1mod8  48354  ppivalnn4  48379  11t31e341  48497  2exp340mod341  48498  341fppr2  48499  8exp8mod9  48501  nfermltl2rev  48508  tgoldbachlt  48581  tgoldbach  48582  grtriprop  48706  grtriclwlk3  48710  cycl3grtri  48712  usgrexmpl1lem  48786  usgrexmpl2lem  48791  usgrexmpl2nb2  48798  gpg5gricstgr3  48855  gpg5grlim  48858  gpg5grlic  48859  gpgprismgr4cycllem7  48866  gpgprismgr4cycllem10  48869  gpg5edgnedg  48895  zlmodzxzldeplem1  49280  itcoval3  49445  ackval3  49463  ackval0012  49469  ackval1012  49470  ackval2012  49471  ackval3012  49472  ackval40  49473  ackval41a  49474  ackval41  49475  ackval42  49476