Theorem 3nn0 12279

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

Syntax hints:   ∈ wcel 2101  3c3 12057  ℕ₀cn0 12261

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2103  ax-9 2111  ax-10 2132  ax-11 2149  ax-12 2166  ax-ext 2704  ax-sep 5226  ax-nul 5233  ax-pr 5355  ax-un 7608  ax-1cn 10957

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2063  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2884  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3223  df-rab 3224  df-v 3436  df-sbc 3719  df-csb 3835  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3908  df-nul 4260  df-if 4463  df-pw 4538  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4842  df-iun 4929  df-br 5078  df-opab 5140  df-mpt 5161  df-tr 5195  df-id 5491  df-eprel 5497  df-po 5505  df-so 5506  df-fr 5546  df-we 5548  df-xp 5597  df-rel 5598  df-cnv 5599  df-co 5600  df-dm 5601  df-rn 5602  df-res 5603  df-ima 5604  df-pred 6206  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6399  df-fun 6449  df-fn 6450  df-f 6451  df-f1 6452  df-fo 6453  df-f1o 6454  df-fv 6455  df-ov 7298  df-om 7733  df-2nd 7852  df-frecs 8117  df-wrecs 8148  df-recs 8222  df-rdg 8261  df-nn 12002  df-2 12064  df-3 12065  df-n0 12262

This theorem is referenced by:  7p4e11  12541  7p7e14  12544  8p4e12  12547  8p6e14  12549  9p4e13  12554  9p5e14  12555  4t4e16  12564  5t4e20  12567  6t4e24  12571  6t6e36  12573  7t4e28  12576  7t6e42  12578  8t4e32  12582  8t5e40  12583  9t4e36  12589  9t5e45  12590  9t7e63  12592  9t8e72  12593  fz0to3un2pr  13386  4fvwrd4  13404  fldiv4p1lem1div2  13583  expnass  13952  binom3  13967  fac4  14023  4bc2eq6  14071  hash3tr  14232  bpoly3  15796  bpoly4  15797  fsumcube  15798  ef4p  15850  efi4p  15874  resin4p  15875  recos4p  15876  ef01bndlem  15921  sin01bnd  15922  sin01gt0  15927  2exp5  16815  2exp6  16816  2exp8  16818  2exp11  16819  2exp16  16820  3exp3  16821  7prm  16840  11prm  16844  13prm  16845  17prm  16846  23prm  16848  prmlem2  16849  37prm  16850  43prm  16851  83prm  16852  139prm  16853  163prm  16854  317prm  16855  631prm  16856  1259lem1  16860  1259lem2  16861  1259lem3  16862  1259lem4  16863  1259lem5  16864  1259prm  16865  2503lem1  16866  2503lem2  16867  2503lem3  16868  2503prm  16869  4001lem1  16870  4001lem2  16871  4001lem3  16872  4001lem4  16873  4001prm  16874  dsndxnmulrndx  17129  basendxltunifndx  17136  unifndxntsetndx  17138  slotsdifunifndx  17139  cnfldfunALTOLD  20639  tuslemOLD  23447  tangtx  25690  1cubrlem  26019  dcubic1lem  26021  dcubic2  26022  dcubic1  26023  dcubic  26024  mcubic  26025  cubic2  26026  cubic  26027  binom4  26028  dquartlem2  26030  quart1cl  26032  quart1lem  26033  quart1  26034  quartlem1  26035  quartlem2  26036  quart  26039  log2ublem1  26124  log2ublem3  26126  log2ub  26127  log2le1  26128  birthday  26132  ppiublem2  26379  bclbnd  26456  bpos1  26459  bposlem8  26467  gausslemma2dlem4  26545  2lgslem3b  26573  2lgslem3d  26575  pntlemd  26770  pntlema  26772  pntlemb  26773  pntlemf  26781  pntlemo  26783  pntlem3  26785  tgcgr4  26920  iscgra  27198  isinag  27227  isleag  27236  iseqlg  27256  usgrexmplef  27654  upgr3v3e3cycl  28572  upgr4cycl4dv4e  28577  konigsbergiedgw  28640  konigsberglem1  28644  konigsberglem2  28645  konigsberglem3  28646  konigsberglem4  28647  ex-prmo  28851  threehalves  31217  circlemethhgt  32651  hgt750lemd  32656  hgt750lem  32659  hgt750lem2  32660  hgt750lemb  32664  hgt750lema  32665  hgt750leme  32666  tgoldbachgtde  32668  tgoldbachgtda  32669  tgoldbachgt  32671  cusgracyclt3v  33146  kur14lem8  33203  3exp7  40087  3lexlogpow5ineq1  40088  3lexlogpow2ineq1  40092  3lexlogpow5ineq5  40094  aks4d1p1p7  40108  aks4d1p1p5  40109  aks4d1p1  40110  235t711  40342  ex-decpmul  40343  3cubeslem3l  40531  3cubeslem3r  40532  3cubeslem4  40534  3cubes  40535  jm2.23  40842  jm2.20nn  40843  rmydioph  40860  rmxdioph  40862  expdiophlem2  40868  expdioph  40869  resqrtvalex  41277  amgm3d  41834  lhe4.4ex1a  41971  fmtno3  45043  fmtno4  45044  fmtno5lem1  45045  fmtno5lem2  45046  fmtno5lem3  45047  fmtno5lem4  45048  fmtno5  45049  257prm  45053  fmtnoprmfac2lem1  45058  fmtno4prmfac  45064  fmtno4prmfac193  45065  fmtno4nprmfac193  45066  fmtno5faclem2  45072  139prmALT  45088  31prm  45089  m5prm  45090  127prm  45091  m11nprm  45093  mod42tp1mod8  45094  11t31e341  45224  2exp340mod341  45225  341fppr2  45226  8exp8mod9  45228  nfermltl2rev  45235  tgoldbachlt  45308  tgoldbach  45309  zlmodzxzldeplem1  45881  itcoval3  46051  ackval3  46069  ackval0012  46075  ackval1012  46076  ackval2012  46077  ackval3012  46078  ackval40  46079  ackval41a  46080  ackval41  46081  ackval42  46082