Theorem 3nn0 11348

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

Syntax hints:   ∈ wcel 2030  3c3 11109  ℕ₀cn0 11330

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-1cn 10032

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-om 7108  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331

This theorem is referenced by:  7p4e11  11643  7p4e11OLD  11644  7p7e14  11647  8p4e12  11652  8p6e14  11654  9p4e13  11660  9p5e14  11661  4t4e16  11671  5t4e20  11675  5t4e20OLD  11676  6t4e24  11681  6t6e36  11684  6t6e36OLD  11685  7t4e28  11688  7t6e42  11690  8t4e32  11694  8t5e40  11695  8t5e40OLD  11696  9t4e36  11703  9t5e45  11704  9t7e63  11706  9t8e72  11707  fz0to3un2pr  12480  4fvwrd4  12498  fldiv4p1lem1div2  12676  expnass  13010  binom3  13025  fac4  13108  4bc2eq6  13156  hash3tr  13310  bpoly3  14833  bpoly4  14834  fsumcube  14835  ef4p  14887  efi4p  14911  resin4p  14912  recos4p  14913  ef01bndlem  14958  sin01bnd  14959  sin01gt0  14964  2exp6  15842  2exp8  15843  2exp16  15844  3exp3  15845  7prm  15864  11prm  15869  13prm  15870  17prm  15871  23prm  15873  prmlem2  15874  37prm  15875  43prm  15876  83prm  15877  139prm  15878  163prm  15879  317prm  15880  631prm  15881  1259lem1  15885  1259lem2  15886  1259lem3  15887  1259lem4  15888  1259lem5  15889  1259prm  15890  2503lem1  15891  2503lem2  15892  2503lem3  15893  2503prm  15894  4001lem1  15895  4001lem2  15896  4001lem3  15897  4001lem4  15898  4001prm  15899  cnfldfun  19806  ressunif  22113  tuslem  22118  tangtx  24302  1cubrlem  24613  dcubic1lem  24615  dcubic2  24616  dcubic1  24617  dcubic  24618  mcubic  24619  cubic2  24620  cubic  24621  binom4  24622  dquartlem2  24624  quart1cl  24626  quart1lem  24627  quart1  24628  quartlem1  24629  quartlem2  24630  quart  24633  log2ublem1  24718  log2ublem3  24720  log2ub  24721  log2le1  24722  birthday  24726  ppiublem2  24973  bclbnd  25050  bpos1  25053  bposlem8  25061  gausslemma2dlem4  25139  2lgslem3b  25167  2lgslem3d  25169  pntlemd  25328  pntlema  25330  pntlemb  25331  pntlemf  25339  pntlemo  25341  pntlem3  25343  tgcgr4  25471  iscgra  25746  isinag  25774  isleag  25778  iseqlg  25792  usgrexmplef  26196  upgr3v3e3cycl  27158  upgr4cycl4dv4e  27163  konigsbergiedgw  27226  konigsberglem1  27230  konigsberglem2  27231  konigsberglem3  27232  konigsberglem4  27233  ex-prmo  27446  threehalves  29751  circlemethhgt  30849  hgt750lemd  30854  hgt750lem  30857  hgt750lem2  30858  hgt750lemb  30862  hgt750lema  30863  hgt750leme  30864  tgoldbachgtde  30866  tgoldbachgtda  30867  tgoldbachgt  30869  kur14lem8  31321  jm2.23  37880  jm2.20nn  37881  rmydioph  37898  rmxdioph  37900  expdiophlem2  37906  expdioph  37907  amgm3d  38819  lhe4.4ex1a  38845  fmtno3  41788  fmtno4  41789  fmtno5lem1  41790  fmtno5lem2  41791  fmtno5lem3  41792  fmtno5lem4  41793  fmtno5  41794  257prm  41798  fmtnoprmfac2lem1  41803  fmtno4prmfac  41809  fmtno4prmfac193  41810  fmtno4nprmfac193  41811  fmtno5faclem2  41817  2exp5  41832  139prmALT  41836  31prm  41837  m5prm  41838  127prm  41840  2exp11  41842  m11nprm  41843  mod42tp1mod8  41844  tgoldbachlt  42029  tgoldbach  42030  tgoldbachltOLD  42035  tgoldbachOLD  42037  zlmodzxzldeplem1  42614