Theorem nnnn0 12249

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 12245	. 2 ⊢ ℕ ⊆ ℕ0
2	1	sseli 3918	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2107  ℕcn 11982  ℕ₀cn0 12242

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-un 3893  df-in 3895  df-ss 3905  df-n0 12243

This theorem is referenced by:  nnnn0i  12250  elnnnn0b  12286  elnnnn0c  12287  elz2  12346  nn0ind-raph  12429  zindd  12430  fzo1fzo0n0  13447  ubmelfzo  13461  elfzom1elp1fzo  13463  fzo0sn0fzo1  13485  quoremnn0ALT  13586  modmulnn  13618  modsumfzodifsn  13673  addmodlteq  13675  expneg  13799  expcllem  13802  expcl2lem  13803  expeq0  13822  mulexpz  13832  expmordi  13894  rpexpmord  13895  expnlbnd  13957  expmulnbnd  13959  digit2  13960  digit1  13961  facmapnn  14008  facdiv  14010  faclbnd  14013  faclbnd3  14015  faclbnd4lem3  14018  faclbnd4lem4  14019  faclbnd5  14021  faclbnd6  14022  bcval5  14041  ishashinf  14186  iswrdi  14230  pfxn0  14408  repswfsts  14503  repswlsw  14504  repswcshw  14534  relexpnnrn  14765  relexpaddg  14773  absexpz  15026  isercoll  15388  summolem3  15435  summolem2a  15436  climcndslem2  15571  climcnds  15572  harmonic  15580  arisum  15581  expcnv  15585  geo2sum  15594  geo2lim  15596  geoisum1  15600  geoisum1c  15601  0.999...  15602  mertenslem2  15606  fallfacfwd  15755  0fallfac  15756  0risefac  15757  ef0lem  15797  ege2le3  15808  efaddlem  15811  efexp  15819  rpnnen2lem2  15933  rpnnen2lem4  15935  ruclem12  15959  dvdsmodexp  15980  dvdsexp2im  16045  nn0enne  16095  nnehalf  16097  nno  16100  nn0o  16101  pwp1fsum  16109  divalg2  16123  ndvdssub  16127  gcdmultiplez  16252  gcddiv  16268  gcdmultipleOLD  16269  gcdmultiplezOLD  16270  rpmulgcd  16275  rplpwr  16276  dvdssqlem  16280  eucalgf  16297  lcmflefac  16362  1nprm  16393  2mulprm  16407  isprm5  16421  isprm6  16428  prmdvdsexp  16429  phicl2  16478  phibndlem  16480  phiprmpw  16486  crth  16488  eulerthlem2  16492  hashgcdlem  16498  phisum  16500  pythagtriplem10  16530  pythagtriplem6  16531  pythagtriplem7  16532  pythagtriplem12  16536  pythagtriplem14  16538  pclem  16548  pcexp  16569  pcid  16583  pcprod  16605  pcbc  16610  prmpwdvds  16614  infpnlem1  16620  infpnlem2  16621  prmunb  16624  prmreclem6  16631  1arith  16637  vdwapf  16682  0hashbc  16717  ram0  16732  prmdvdsprmo  16752  prmdvdsprmop  16753  prmolefac  16756  prmgaplem1  16759  prmgaplem2  16760  prmgapprmolem  16771  prmgapprmo  16772  cshwrepswhash1  16813  smndex1n0mnd  18560  ghmmulg  18855  odmodnn0  19157  dfod2  19180  submod  19183  prmirredlem  20703  prmirred  20705  znf1o  20768  znhash  20775  znfi  20776  znfld  20777  znidomb  20778  znunithash  20781  znrrg  20782  cply1mul  21474  cply1coe0  21479  cply1coe0bi  21480  cpmatmcllem  21876  m2cpm  21899  m2cpminvid2lem  21912  fvmptnn04ifa  22008  chfacfisf  22012  chfacfisfcpmat  22013  chfacffsupp  22014  chfacfscmul0  22016  chfacfscmulfsupp  22017  chfacfscmulgsum  22018  chfacfpmmul0  22020  chfacfpmmulfsupp  22021  chfacfpmmulgsum  22022  chfacfpmmulgsum2  22023  cayhamlem1  22024  cpmadugsumlemF  22034  tgpmulg  23253  cmodscexp  24293  cphipval  24416  ovollb2lem  24661  ovoliunlem1  24675  ovoliunlem3  24677  uniioombllem3  24758  uniioombllem4  24759  opnmbllem  24774  mbfi1fseqlem1  24889  mbfi1fseqlem3  24891  mbfi1fseqlem4  24892  mbfi1fseqlem5  24893  mbfi1fseqlem6  24894  dvexp  25126  dvexp3  25151  plyco  25411  dgrcolem1  25443  plydivex  25466  aaliou3lem2  25512  aaliou3lem3  25513  aaliou3lem5  25516  aaliou3lem6  25517  aaliou3lem7  25518  aaliou3lem9  25519  radcnvlem2  25582  dvradcnv  25589  pserdv2  25598  abelthlem6  25604  abelthlem9  25608  logtayllem  25823  logtayl  25824  logtaylsum  25825  logtayl2  25826  cxproot  25854  root1id  25916  logbgcd1irr  25953  atantayl  26096  atantayl2  26097  leibpilem2  26100  leibpi  26101  birthdaylem2  26111  birthdaylem3  26112  dfef2  26129  basellem2  26240  basellem4  26242  basellem5  26243  basellem6  26244  basellem8  26246  isppw2  26273  vmappw  26274  sqf11  26297  vma1  26324  1sgm2ppw  26357  chtublem  26368  fsumvma2  26371  vmasum  26373  dchrelbas4  26400  dchrzrhcl  26402  dchrfi  26412  dchrhash  26428  pcbcctr  26433  bclbnd  26437  bposlem1  26441  lgsval4a  26476  lgsdchrval  26511  lgsdchr  26512  gausslemma2dlem0c  26515  gausslemma2dlem0d  26516  gausslemma2dlem6  26529  2lgslem1a1  26546  2lgslem1c  26550  2lgslem3a1  26557  2lgslem3b1  26558  2lgslem3c1  26559  2lgslem3d1  26560  2sqreunnlem1  26606  2sqreunnltblem  26608  rplogsumlem2  26642  dchrisumlem2  26647  ostth2lem1  26775  ostth2lem3  26792  ostth3  26795  cusgrsize2inds  27829  pthdivtx  28106  crctcshwlkn0lem4  28187  crctcshwlkn0lem5  28188  crctcshwlkn0lem7  28190  0enwwlksnge1  28238  rusgr0edg  28347  clwlkclwwlkf1lem2  28378  clwlkclwwlkf1lem3  28379  clwwisshclwwslem  28387  clwwlkinwwlk  28413  clwwlkel  28419  clwwlkf  28420  clwwlkf1  28422  clwwlknwwlksnb  28428  wwlksubclwwlk  28431  erclwwlknref  28442  clwwlknonwwlknonb  28479  numclwwlkqhash  28748  numclwwlk2lem1  28749  numclwlk2lem2f  28750  numclwlk2lem2f1o  28752  ipval2  29078  ipasslem3  29204  ipasslem4  29205  nn0min  31143  frobrhm  31494  znfermltl  31571  ply1fermltl  31679  esumcst  32040  eulerpartlemb  32344  fibp1  32377  ballotlem1  32462  subfacp1lem6  33156  subfaclim  33159  subfacval3  33160  snmlff  33300  bcprod  33713  faclim2  33723  nn0prpwlem  34520  knoppndvlem18  34718  opnmbllem0  35822  nnubfi  35917  nninfnub  35918  geomcau  35926  heiborlem5  35982  heiborlem6  35983  heiborlem7  35984  heiborlem8  35985  bfplem1  35989  lcmineqlem12  40055  aks4d1p1p2  40085  2ap1caineq  40108  nn0expgcd  40342  dvdsexpnn  40347  dvdsexpnn0  40348  dffltz  40478  fltnltalem  40506  irrapxlem2  40652  pellexlem1  40658  pellexlem5  40662  pellqrex  40708  monotoddzzfi  40771  jm2.17c  40791  acongeq  40812  jm2.18  40817  jm2.23  40825  jm2.26lem3  40830  jm3.1  40849  expdiophlem1  40850  idomrootle  41027  idomodle  41028  proot1ex  41033  rp-isfinite6  41132  cnvtrclfv  41339  cotrclrcl  41357  inductionexd  41772  binomcxplemnotnn0  41981  nnne1ge2  42837  dvnmptconst  43489  stoweidlem3  43551  stoweidlem7  43555  stoweidlem34  43582  wallispilem4  43616  wallispilem5  43617  wallispi2lem1  43619  wallispi2lem2  43620  stirlinglem2  43623  stirlinglem3  43624  stirlinglem4  43625  stirlinglem5  43626  stirlinglem7  43628  stirlinglem11  43632  stirlinglem14  43635  stirlinglem15  43636  stirlingr  43638  fourierdlem15  43670  fourierdlem21  43676  fourierdlem22  43677  fourierdlem92  43746  fourierdlem112  43766  fouriersw  43779  sge0rpcpnf  43966  sge0ad2en  43976  ovnsubaddlem1  44115  ovnsubaddlem2  44116  ovolval5lem1  44197  ovolval5lem2  44198  iccpartiltu  44885  iccpartigtl  44886  iccpartlt  44887  iccpartleu  44891  iccpartrn  44893  iccelpart  44896  iccpartiun  44897  iccpartdisj  44900  sqrtpwpw2p  45001  fmtnosqrt  45002  odz2prm2pw  45026  fmtnoprmfac1lem  45027  fmtnoprmfac1  45028  2pwp1prm  45052  lighneallem1  45068  lighneallem2  45069  lighneallem3  45070  lighneallem4a  45071  lighneallem4  45073  nnpw2evenALTV  45165  dfwppr  45201  cznabel  45523  cznrng  45524  ztprmneprm  45694  altgsumbc  45699  altgsumbcALT  45700  pw2m1lepw2m1  45872  nneom  45884  logbpw2m1  45924  blennn  45932  blenpw2m1  45936  blengt1fldiv2p1  45950  dignn0ldlem  45959  dignnld  45960  dig2nn1st  45962  dignn0flhalflem1  45972  nn0sumshdiglemA  45976  nn0sumshdiglemB  45977  itcovalt2lem2lem1  46030  eenglngeehlnm  46096