Theorem nnnn0 12170

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℕcn 11903  ℕ₀cn0 12163

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-in 3890  df-ss 3900  df-n0 12164

This theorem is referenced by:  nnnn0i  12171  elnnnn0b  12207  elnnnn0c  12208  elz2  12267  nn0ind-raph  12350  zindd  12351  fzo1fzo0n0  13366  ubmelfzo  13380  elfzom1elp1fzo  13382  fzo0sn0fzo1  13404  quoremnn0ALT  13505  modmulnn  13537  modsumfzodifsn  13592  addmodlteq  13594  expneg  13718  expcllem  13721  expcl2lem  13722  expeq0  13741  mulexpz  13751  expmordi  13813  rpexpmord  13814  expnlbnd  13876  expmulnbnd  13878  digit2  13879  digit1  13880  facmapnn  13927  facdiv  13929  faclbnd  13932  faclbnd3  13934  faclbnd4lem3  13937  faclbnd4lem4  13938  faclbnd5  13940  faclbnd6  13941  bcval5  13960  ishashinf  14105  iswrdi  14149  pfxn0  14327  repswfsts  14422  repswlsw  14423  repswcshw  14453  relexpnnrn  14684  relexpaddg  14692  absexpz  14945  isercoll  15307  summolem3  15354  summolem2a  15355  climcndslem2  15490  climcnds  15491  harmonic  15499  arisum  15500  expcnv  15504  geo2sum  15513  geo2lim  15515  geoisum1  15519  geoisum1c  15520  0.999...  15521  mertenslem2  15525  fallfacfwd  15674  0fallfac  15675  0risefac  15676  ef0lem  15716  ege2le3  15727  efaddlem  15730  efexp  15738  rpnnen2lem2  15852  rpnnen2lem4  15854  ruclem12  15878  dvdsmodexp  15899  dvdsexp2im  15964  nn0enne  16014  nnehalf  16016  nno  16019  nn0o  16020  pwp1fsum  16028  divalg2  16042  ndvdssub  16046  gcdmultiplez  16171  gcddiv  16187  gcdmultipleOLD  16188  gcdmultiplezOLD  16189  rpmulgcd  16194  rplpwr  16195  dvdssqlem  16199  eucalgf  16216  lcmflefac  16281  1nprm  16312  2mulprm  16326  isprm5  16340  isprm6  16347  prmdvdsexp  16348  phicl2  16397  phibndlem  16399  phiprmpw  16405  crth  16407  eulerthlem2  16411  hashgcdlem  16417  phisum  16419  pythagtriplem10  16449  pythagtriplem6  16450  pythagtriplem7  16451  pythagtriplem12  16455  pythagtriplem14  16457  pclem  16467  pcexp  16488  pcid  16502  pcprod  16524  pcbc  16529  prmpwdvds  16533  infpnlem1  16539  infpnlem2  16540  prmunb  16543  prmreclem6  16550  1arith  16556  vdwapf  16601  0hashbc  16636  ram0  16651  prmdvdsprmo  16671  prmdvdsprmop  16672  prmolefac  16675  prmgaplem1  16678  prmgaplem2  16679  prmgapprmolem  16690  prmgapprmo  16691  cshwrepswhash1  16732  smndex1n0mnd  18466  ghmmulg  18761  odmodnn0  19063  dfod2  19086  submod  19089  prmirredlem  20606  prmirred  20608  znf1o  20671  znhash  20678  znfi  20679  znfld  20680  znidomb  20681  znunithash  20684  znrrg  20685  cply1mul  21375  cply1coe0  21380  cply1coe0bi  21381  cpmatmcllem  21775  m2cpm  21798  m2cpminvid2lem  21811  fvmptnn04ifa  21907  chfacfisf  21911  chfacfisfcpmat  21912  chfacffsupp  21913  chfacfscmul0  21915  chfacfscmulfsupp  21916  chfacfscmulgsum  21917  chfacfpmmul0  21919  chfacfpmmulfsupp  21920  chfacfpmmulgsum  21921  chfacfpmmulgsum2  21922  cayhamlem1  21923  cpmadugsumlemF  21933  tgpmulg  23152  cmodscexp  24190  cphipval  24312  ovollb2lem  24557  ovoliunlem1  24571  ovoliunlem3  24573  uniioombllem3  24654  uniioombllem4  24655  opnmbllem  24670  mbfi1fseqlem1  24785  mbfi1fseqlem3  24787  mbfi1fseqlem4  24788  mbfi1fseqlem5  24789  mbfi1fseqlem6  24790  dvexp  25022  dvexp3  25047  plyco  25307  dgrcolem1  25339  plydivex  25362  aaliou3lem2  25408  aaliou3lem3  25409  aaliou3lem5  25412  aaliou3lem6  25413  aaliou3lem7  25414  aaliou3lem9  25415  radcnvlem2  25478  dvradcnv  25485  pserdv2  25494  abelthlem6  25500  abelthlem9  25504  logtayllem  25719  logtayl  25720  logtaylsum  25721  logtayl2  25722  cxproot  25750  root1id  25812  logbgcd1irr  25849  atantayl  25992  atantayl2  25993  leibpilem2  25996  leibpi  25997  birthdaylem2  26007  birthdaylem3  26008  dfef2  26025  basellem2  26136  basellem4  26138  basellem5  26139  basellem6  26140  basellem8  26142  isppw2  26169  vmappw  26170  sqf11  26193  vma1  26220  1sgm2ppw  26253  chtublem  26264  fsumvma2  26267  vmasum  26269  dchrelbas4  26296  dchrzrhcl  26298  dchrfi  26308  dchrhash  26324  pcbcctr  26329  bclbnd  26333  bposlem1  26337  lgsval4a  26372  lgsdchrval  26407  lgsdchr  26408  gausslemma2dlem0c  26411  gausslemma2dlem0d  26412  gausslemma2dlem6  26425  2lgslem1a1  26442  2lgslem1c  26446  2lgslem3a1  26453  2lgslem3b1  26454  2lgslem3c1  26455  2lgslem3d1  26456  2sqreunnlem1  26502  2sqreunnltblem  26504  rplogsumlem2  26538  dchrisumlem2  26543  ostth2lem1  26671  ostth2lem3  26688  ostth3  26691  cusgrsize2inds  27723  pthdivtx  27998  crctcshwlkn0lem4  28079  crctcshwlkn0lem5  28080  crctcshwlkn0lem7  28082  0enwwlksnge1  28130  rusgr0edg  28239  clwlkclwwlkf1lem2  28270  clwlkclwwlkf1lem3  28271  clwwisshclwwslem  28279  clwwlkinwwlk  28305  clwwlkel  28311  clwwlkf  28312  clwwlkf1  28314  clwwlknwwlksnb  28320  wwlksubclwwlk  28323  erclwwlknref  28334  clwwlknonwwlknonb  28371  numclwwlkqhash  28640  numclwwlk2lem1  28641  numclwlk2lem2f  28642  numclwlk2lem2f1o  28644  ipval2  28970  ipasslem3  29096  ipasslem4  29097  nn0min  31036  frobrhm  31387  znfermltl  31464  ply1fermltl  31572  esumcst  31931  eulerpartlemb  32235  fibp1  32268  ballotlem1  32353  subfacp1lem6  33047  subfaclim  33050  subfacval3  33051  snmlff  33191  bcprod  33610  faclim2  33620  nn0prpwlem  34438  knoppndvlem18  34636  opnmbllem0  35740  nnubfi  35835  nninfnub  35836  geomcau  35844  heiborlem5  35900  heiborlem6  35901  heiborlem7  35902  heiborlem8  35903  bfplem1  35907  lcmineqlem12  39976  aks4d1p1p2  40006  2ap1caineq  40029  nn0expgcd  40256  dvdsexpnn  40261  dvdsexpnn0  40262  dffltz  40387  fltnltalem  40415  irrapxlem2  40561  pellexlem1  40567  pellexlem5  40571  pellqrex  40617  monotoddzzfi  40680  jm2.17c  40700  acongeq  40721  jm2.18  40726  jm2.23  40734  jm2.26lem3  40739  jm3.1  40758  expdiophlem1  40759  idomrootle  40936  idomodle  40937  proot1ex  40942  rp-isfinite6  41023  cnvtrclfv  41221  cotrclrcl  41239  inductionexd  41654  binomcxplemnotnn0  41863  nnne1ge2  42720  dvnmptconst  43372  stoweidlem3  43434  stoweidlem7  43438  stoweidlem34  43465  wallispilem4  43499  wallispilem5  43500  wallispi2lem1  43502  wallispi2lem2  43503  stirlinglem2  43506  stirlinglem3  43507  stirlinglem4  43508  stirlinglem5  43509  stirlinglem7  43511  stirlinglem11  43515  stirlinglem14  43518  stirlinglem15  43519  stirlingr  43521  fourierdlem15  43553  fourierdlem21  43559  fourierdlem22  43560  fourierdlem92  43629  fourierdlem112  43649  fouriersw  43662  sge0rpcpnf  43849  sge0ad2en  43859  ovnsubaddlem1  43998  ovnsubaddlem2  43999  ovolval5lem1  44080  ovolval5lem2  44081  iccpartiltu  44762  iccpartigtl  44763  iccpartlt  44764  iccpartleu  44768  iccpartrn  44770  iccelpart  44773  iccpartiun  44774  iccpartdisj  44777  sqrtpwpw2p  44878  fmtnosqrt  44879  odz2prm2pw  44903  fmtnoprmfac1lem  44904  fmtnoprmfac1  44905  2pwp1prm  44929  lighneallem1  44945  lighneallem2  44946  lighneallem3  44947  lighneallem4a  44948  lighneallem4  44950  nnpw2evenALTV  45042  dfwppr  45078  cznabel  45400  cznrng  45401  ztprmneprm  45571  altgsumbc  45576  altgsumbcALT  45577  pw2m1lepw2m1  45749  nneom  45761  logbpw2m1  45801  blennn  45809  blenpw2m1  45813  blengt1fldiv2p1  45827  dignn0ldlem  45836  dignnld  45837  dig2nn1st  45839  dignn0flhalflem1  45849  nn0sumshdiglemA  45853  nn0sumshdiglemB  45854  itcovalt2lem2lem1  45907  eenglngeehlnm  45973