Theorem 3nn0 12455

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

Syntax hints:   ∈ wcel 2114  3c3 12237  ℕ₀cn0 12437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375  ax-un 7689  ax-1cn 11096

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-ov 7370  df-om 7818  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-nn 12175  df-2 12244  df-3 12245  df-n0 12438

This theorem is referenced by:  7p4e11  12720  7p7e14  12723  8p4e12  12726  8p6e14  12728  9p4e13  12733  9p5e14  12734  4t4e16  12743  5t4e20  12746  6t4e24  12750  6t6e36  12752  7t4e28  12755  7t6e42  12757  8t4e32  12761  8t5e40  12762  9t4e36  12768  9t5e45  12769  9t7e63  12771  9t8e72  12772  fz0to3un2pr  13583  4fvwrd4  13602  fldiv4p1lem1div2  13794  expnass  14170  binom3  14186  fac4  14243  4bc2eq6  14291  hash3tr  14453  tpf1o  14463  bpoly3  16023  bpoly4  16024  fsumcube  16025  ef4p  16080  efi4p  16104  resin4p  16105  recos4p  16106  ef01bndlem  16151  sin01bnd  16152  sin01gt0  16157  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  26469  1cubrlem  26805  dcubic1lem  26807  dcubic2  26808  dcubic1  26809  dcubic  26810  mcubic  26811  cubic2  26812  cubic  26813  binom4  26814  dquartlem2  26816  quart1cl  26818  quart1lem  26819  quart1  26820  quartlem1  26821  quartlem2  26822  quart  26825  log2ublem1  26910  log2ublem3  26912  log2ub  26913  log2le1  26914  birthday  26918  ppiublem2  27166  bclbnd  27243  bpos1  27246  bposlem8  27254  gausslemma2dlem4  27332  2lgslem3b  27360  2lgslem3d  27362  pntlemd  27557  pntlema  27559  pntlemb  27560  pntlemf  27568  pntlemo  27570  pntlem3  27572  tgcgr4  28599  iscgra  28877  isinag  28906  isleag  28915  iseqlg  28935  usgrexmplef  29328  upgr3v3e3cycl  30250  upgr4cycl4dv4e  30255  konigsbergiedgw  30318  konigsberglem1  30322  konigsberglem2  30323  konigsberglem3  30324  konigsberglem4  30325  ex-prmo  30529  threehalves  32974  evl1deg2  33637  evl1deg3  33638  ply1dg3rt0irred  33644  iconstr  33910  2sqr3minply  33924  2sqr3nconstr  33925  cos9thpiminplylem1  33926  cos9thpiminplylem2  33927  cos9thpiminplylem3  33928  cos9thpiminplylem4  33929  cos9thpiminplylem5  33930  cos9thpiminplylem6  33931  cos9thpiminply  33932  cos9thpinconstrlem2  33934  circlemethhgt  34787  hgt750lemd  34792  hgt750lem  34795  hgt750lem2  34796  hgt750lemb  34800  hgt750lema  34801  hgt750leme  34802  tgoldbachgtde  34804  tgoldbachgtda  34805  tgoldbachgt  34807  cusgracyclt3v  35338  kur14lem8  35395  3exp7  42492  3lexlogpow5ineq1  42493  3lexlogpow2ineq1  42497  3lexlogpow5ineq5  42499  aks4d1p1p7  42513  aks4d1p1p5  42514  aks4d1p1  42515  235t711  42737  ex-decpmul  42738  nicomachus  42744  3cubeslem3l  43118  3cubeslem3r  43119  3cubeslem4  43121  3cubes  43122  jm2.23  43424  jm2.20nn  43425  rmydioph  43442  rmxdioph  43444  expdiophlem2  43450  expdioph  43451  resqrtvalex  44072  amgm3d  44626  lhe4.4ex1a  44756  sin3t  47319  cos3t  47320  sin5tlem1  47321  sin5tlem2  47322  sin5tlem3  47323  sin5tlem4  47324  sin5tlem5  47325  goldratmolem2  47334  8mod5e3  47814  modm2nep1  47820  modm1nep2  47822  fmtno3  48014  fmtno4  48015  fmtno5lem1  48016  fmtno5lem2  48017  fmtno5lem3  48018  fmtno5lem4  48019  fmtno5  48020  257prm  48024  fmtnoprmfac2lem1  48029  fmtno4prmfac  48035  fmtno4prmfac193  48036  fmtno4nprmfac193  48037  fmtno5faclem2  48043  139prmALT  48059  31prm  48060  m5prm  48061  127prm  48062  m11nprm  48064  mod42tp1mod8  48065  ppivalnn4  48090  11t31e341  48208  2exp340mod341  48209  341fppr2  48210  8exp8mod9  48212  nfermltl2rev  48219  tgoldbachlt  48292  tgoldbach  48293  grtriprop  48417  grtriclwlk3  48421  cycl3grtri  48423  usgrexmpl1lem  48497  usgrexmpl2lem  48502  usgrexmpl2nb2  48509  gpg5gricstgr3  48566  gpg5grlim  48569  gpg5grlic  48570  gpgprismgr4cycllem7  48577  gpgprismgr4cycllem10  48580  gpg5edgnedg  48606  zlmodzxzldeplem1  48976  itcoval3  49141  ackval3  49159  ackval0012  49165  ackval1012  49166  ackval2012  49167  ackval3012  49168  ackval40  49169  ackval41a  49170  ackval41  49171  ackval42  49172