Theorem nnnn0 12420

Description: A positive integer is a nonnegative integer. (Contributed by NM, 9-May-2004.)

Assertion

Ref	Expression
nnnn0	⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℕ0)

Proof of Theorem nnnn0

Step	Hyp	Ref	Expression
1		nnssnn0 12416	. 2 ⊢ ℕ ⊆ ℕ0
2	1	sseli 3931	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2114  ℕcn 12157  ℕ₀cn0 12413

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-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-ss 3920  df-n0 12414

This theorem is referenced by:  nnnn0i  12421  elnnnn0b  12457  elnnnn0c  12458  elz2  12518  nn0ind-raph  12604  zindd  12605  fzo1fzo0n0  13643  ubmelfzo  13658  elfzom1elp1fzo  13660  fzo0sn0fzo1  13683  quoremnn0ALT  13789  modmulnn  13821  modsumfzodifsn  13879  addmodlteq  13881  expneg  14004  expcllem  14007  expcl2lem  14008  expeq0  14027  mulexpz  14037  expmordi  14102  rpexpmord  14103  expnlbnd  14168  expmulnbnd  14170  digit2  14171  digit1  14172  facmapnn  14220  facdiv  14222  faclbnd  14225  faclbnd3  14227  faclbnd4lem3  14230  faclbnd4lem4  14231  faclbnd5  14233  faclbnd6  14234  bcval5  14253  ishashinf  14398  iswrdi  14452  pfxn0  14622  repswfsts  14716  repswlsw  14717  repswcshw  14747  relexpnnrn  14980  relexpaddg  14988  absexpz  15240  isercoll  15603  summolem3  15649  summolem2a  15650  climcndslem2  15785  climcnds  15786  harmonic  15794  arisum  15795  expcnv  15799  geo2sum  15808  geo2lim  15810  geoisum1  15814  geoisum1c  15815  0.999...  15816  mertenslem2  15820  fallfacfwd  15971  0fallfac  15972  0risefac  15973  ef0lem  16013  ege2le3  16025  efaddlem  16028  efexp  16038  rpnnen2lem2  16152  rpnnen2lem4  16154  ruclem12  16178  dvdsmodexp  16199  dvdsexp2im  16266  nn0enne  16316  nnehalf  16318  nno  16321  nn0o  16322  pwp1fsum  16330  divalg2  16344  ndvdssub  16348  gcdmultiplez  16474  gcddiv  16490  rpmulgcd  16496  rplpwr  16497  nn0expgcd  16503  dvdssqlem  16505  eucalgf  16522  lcmflefac  16587  1nprm  16618  2mulprm  16632  isprm5  16646  isprm6  16653  prmdvdsexp  16654  phicl2  16707  phibndlem  16709  phiprmpw  16715  crth  16717  eulerthlem2  16721  hashgcdlem  16727  phisum  16730  pythagtriplem10  16760  pythagtriplem6  16761  pythagtriplem7  16762  pythagtriplem12  16766  pythagtriplem14  16768  pclem  16778  pcexp  16799  pcid  16813  pcprod  16835  pcbc  16840  prmpwdvds  16844  infpnlem1  16850  infpnlem2  16851  prmunb  16854  prmreclem6  16861  1arith  16867  vdwapf  16912  0hashbc  16947  ram0  16962  prmdvdsprmo  16982  prmdvdsprmop  16983  prmolefac  16986  prmgaplem1  16989  prmgaplem2  16990  prmgapprmolem  17001  prmgapprmo  17002  cshwrepswhash1  17042  smndex1n0mnd  18849  ghmmulg  19169  odmodnn0  19481  dfod2  19505  submod  19510  prmirredlem  21439  prmirred  21441  znf1o  21518  znhash  21525  znfi  21526  znfld  21527  znidomb  21528  znunithash  21531  znrrg  21532  frobrhm  21542  cply1mul  22252  cply1coe0  22257  cply1coe0bi  22258  ply1fermltlchr  22268  cpmatmcllem  22674  m2cpm  22697  m2cpminvid2lem  22710  fvmptnn04ifa  22806  chfacfisf  22810  chfacfisfcpmat  22811  chfacffsupp  22812  chfacfscmul0  22814  chfacfscmulfsupp  22815  chfacfscmulgsum  22816  chfacfpmmul0  22818  chfacfpmmulfsupp  22819  chfacfpmmulgsum  22820  chfacfpmmulgsum2  22821  cayhamlem1  22822  cpmadugsumlemF  22832  tgpmulg  24049  cmodscexp  25089  cphipval  25211  ovollb2lem  25457  ovoliunlem1  25471  ovoliunlem3  25473  uniioombllem3  25554  uniioombllem4  25555  opnmbllem  25570  mbfi1fseqlem1  25684  mbfi1fseqlem3  25686  mbfi1fseqlem4  25687  mbfi1fseqlem5  25688  mbfi1fseqlem6  25689  dvexp  25925  dvexp3  25950  idomrootle  26146  plyco  26214  dgrcolem1  26247  plydivex  26273  aaliou3lem2  26319  aaliou3lem3  26320  aaliou3lem5  26323  aaliou3lem6  26324  aaliou3lem7  26325  aaliou3lem9  26326  radcnvlem2  26391  dvradcnv  26398  pserdv2  26408  abelthlem6  26414  abelthlem9  26418  logtayllem  26636  logtayl  26637  logtaylsum  26638  logtayl2  26639  cxproot  26667  root1id  26732  logbgcd1irr  26772  atantayl  26915  atantayl2  26916  leibpilem2  26919  leibpi  26920  birthdaylem2  26930  birthdaylem3  26931  dfef2  26949  basellem2  27060  basellem4  27062  basellem5  27063  basellem6  27064  basellem8  27066  isppw2  27093  vmappw  27094  sqf11  27117  vma1  27144  1sgm2ppw  27179  chtublem  27190  fsumvma2  27193  vmasum  27195  dchrelbas4  27222  dchrzrhcl  27224  dchrfi  27234  dchrhash  27250  pcbcctr  27255  bclbnd  27259  bposlem1  27263  lgsval4a  27298  lgsdchrval  27333  lgsdchr  27334  gausslemma2dlem0c  27337  gausslemma2dlem0d  27338  gausslemma2dlem6  27351  2lgslem1a1  27368  2lgslem1c  27372  2lgslem3a1  27379  2lgslem3b1  27380  2lgslem3c1  27381  2lgslem3d1  27382  2sqreunnlem1  27428  2sqreunnltblem  27430  rplogsumlem2  27464  dchrisumlem2  27469  ostth2lem1  27597  ostth2lem3  27614  ostth3  27617  cusgrsize2inds  29539  pthdivtx  29812  cyclnumvtx  29885  crctcshwlkn0lem4  29898  crctcshwlkn0lem5  29899  crctcshwlkn0lem7  29901  0enwwlksnge1  29949  rusgr0edg  30061  clwlkclwwlkf1lem2  30092  clwlkclwwlkf1lem3  30093  clwwisshclwwslem  30101  clwwlkinwwlk  30127  clwwlkel  30133  clwwlkf  30134  clwwlkf1  30136  clwwlknwwlksnb  30142  wwlksubclwwlk  30145  erclwwlknref  30156  clwwlknonwwlknonb  30193  numclwwlkqhash  30462  numclwwlk2lem1  30463  numclwlk2lem2f  30464  numclwlk2lem2f1o  30466  ipval2  30794  ipasslem3  30920  ipasslem4  30921  nn0min  32911  znfermltl  33458  ply1fermltl  33678  esumcst  34240  eulerpartlemb  34545  fibp1  34578  ballotlem1  34664  subfacp1lem6  35398  subfaclim  35401  subfacval3  35402  snmlff  35542  bcprod  35951  faclim2  35961  nn0prpwlem  36535  knoppndvlem18  36748  opnmbllem0  37901  nnubfi  37995  nninfnub  37996  geomcau  38004  heiborlem5  38060  heiborlem6  38061  heiborlem7  38062  heiborlem8  38063  bfplem1  38067  lcmineqlem12  42404  aks4d1p1p2  42434  primrootscoprmpow  42463  2ap1caineq  42509  dvdsexpnn  42697  dvdsexpnn0  42698  zaddcomlem  42827  fidomncyc  42899  dffltz  42986  fltnltalem  43014  irrapxlem2  43174  pellexlem1  43180  pellexlem5  43184  pellqrex  43230  monotoddzzfi  43293  jm2.17c  43313  acongeq  43334  jm2.18  43339  jm2.23  43347  jm2.26lem3  43352  jm3.1  43371  expdiophlem1  43372  idomodle  43542  proot1ex  43547  rp-isfinite6  43868  cnvtrclfv  44074  cotrclrcl  44092  inductionexd  44505  binomcxplemnotnn0  44706  nnne1ge2  45647  dvnmptconst  46293  stoweidlem3  46355  stoweidlem7  46359  stoweidlem34  46386  wallispilem4  46420  wallispilem5  46421  wallispi2lem1  46423  wallispi2lem2  46424  stirlinglem2  46427  stirlinglem3  46428  stirlinglem4  46429  stirlinglem5  46430  stirlinglem7  46432  stirlinglem11  46436  stirlinglem14  46439  stirlinglem15  46440  stirlingr  46442  fourierdlem15  46474  fourierdlem21  46480  fourierdlem22  46481  fourierdlem92  46550  fourierdlem112  46570  fouriersw  46583  sge0rpcpnf  46773  sge0ad2en  46783  ovnsubaddlem1  46922  ovnsubaddlem2  46923  ovolval5lem1  47004  ovolval5lem2  47005  nthrucw  47238  ceilhalfelfzo1  47684  modlt0b  47717  iccpartiltu  47776  iccpartigtl  47777  iccpartlt  47778  iccpartleu  47782  iccpartrn  47784  iccelpart  47787  iccpartiun  47788  iccpartdisj  47791  sqrtpwpw2p  47892  fmtnosqrt  47893  odz2prm2pw  47917  fmtnoprmfac1lem  47918  fmtnoprmfac1  47919  2pwp1prm  47943  lighneallem1  47959  lighneallem2  47960  lighneallem3  47961  lighneallem4a  47962  lighneallem4  47964  nnpw2evenALTV  48056  dfwppr  48092  gpgorder  48413  gpgedgvtx0  48415  gpgedgvtx1  48416  cznabel  48614  cznrng  48615  ztprmneprm  48701  altgsumbc  48706  altgsumbcALT  48707  pw2m1lepw2m1  48874  nneom  48881  logbpw2m1  48921  blennn  48929  blenpw2m1  48933  blengt1fldiv2p1  48947  dignn0ldlem  48956  dignnld  48957  dig2nn1st  48959  dignn0flhalflem1  48969  nn0sumshdiglemA  48973  nn0sumshdiglemB  48974  itcovalt2lem2lem1  49027  eenglngeehlnm  49093