Theorem nnnn0 12539

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℕcn 12261  ℕ₀cn0 12532

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-un 3907  df-ss 3919  df-n0 12533

This theorem is used by:  nnnn0i  12540  elnnnn0b  12576  elnnnn0c  12577  elz2  12637  nn0ind-raph  12725  zindd  12726  fzo1fzo0n0  13775  ubmelfzo  13790  elfzom1elp1fzo  13792  fzo0sn0fzo1  13815  quoremnn0ALT  13922  modmulnn  13954  modsumfzodifsn  14012  addmodlteq  14014  expneg  14137  expcllem  14140  expcl2lem  14141  expeq0  14160  mulexpz  14170  expmordi  14235  rpexpmord  14236  expnlbnd  14301  expmulnbnd  14303  digit2  14304  digit1  14305  facmapnn  14353  facdiv  14355  faclbnd  14358  faclbnd3  14360  faclbnd4lem3  14363  faclbnd4lem4  14364  faclbnd5  14366  faclbnd6  14367  bcval5  14386  ishashinf  14532  iswrdi  14586  pfxn0  14760  repswfsts  14856  repswlsw  14857  repswcshw  14887  relexpnnrn  15122  relexpaddg  15130  absexpz  15396  isercoll  15759  summolem3  15804  summolem2a  15805  climcndslem2  15943  climcnds  15944  harmonic  15952  arisum  15953  expcnv  15957  geo2sum  15966  geo2lim  15968  geoisum1  15972  geoisum1c  15973  0.999...  15974  mertenslem2  15978  fallfacfwd  16128  0fallfac  16129  0risefac  16130  ef0lem  16170  ege2le3  16182  efaddlem  16185  efexp  16195  rpnnen2lem2  16309  rpnnen2lem4  16311  ruclem12  16335  dvdsmodexp  16356  dvdsexp2im  16423  nn0enne  16473  nnehalf  16475  nno  16478  nn0o  16479  pwp1fsum  16487  divalg2  16501  ndvdssub  16505  gcdmultiplez  16631  gcddiv  16647  rpmulgcd  16653  rplpwr  16654  nn0expgcd  16660  dvdssqlem  16662  eucalgf  16679  lcmflefac  16744  1nprm  16775  2mulprm  16789  isprm5  16804  isprm6  16811  prmdvdsexp  16812  phicl2  16865  phibndlem  16867  phiprmpw  16873  crth  16875  eulerthlem2  16879  hashgcdlem  16885  phisum  16888  pythagtriplem10  16918  pythagtriplem6  16919  pythagtriplem7  16920  pythagtriplem12  16924  pythagtriplem14  16926  pclem  16936  pcexp  16957  pcid  16971  pcprod  16993  pcbc  16998  prmpwdvds  17002  infpnlem1  17008  infpnlem2  17009  prmunb  17012  prmreclem6  17019  1arith  17025  vdwapf  17070  0hashbc  17105  ram0  17120  prmdvdsprmo  17140  prmdvdsprmop  17141  prmolefac  17144  prmgaplem1  17147  prmgaplem2  17148  prmgapprmolem  17159  prmgapprmo  17160  cshwrepswhash1  17200  smndex1n0mnd  19030  ghmmulg  19361  odmodnn0  19673  dfod2  19697  submod  19702  prmirredlem  21691  prmirred  21693  znf1o  21770  znhash  21777  znfi  21778  znfld  21779  znidomb  21780  znunithash  21783  znrrg  21784  frobrhm  21794  cply1mul  22527  cply1coe0  22532  cply1coe0bi  22533  ply1fermltlchr  22543  cpmatmcllem  22949  m2cpm  22972  m2cpminvid2lem  22985  fvmptnn04ifa  23081  chfacfisf  23085  chfacfisfcpmat  23086  chfacffsupp  23087  chfacfscmul0  23089  chfacfscmulfsupp  23090  chfacfscmulgsum  23091  chfacfpmmul0  23093  chfacfpmmulfsupp  23094  chfacfpmmulgsum  23095  chfacfpmmulgsum2  23096  cayhamlem1  23097  cpmadugsumlemF  23107  tgpmulg  24325  cmodscexp  25355  cphipval  25477  ovollb2lem  25722  ovoliunlem1  25736  ovoliunlem3  25738  uniioombllem3  25819  uniioombllem4  25820  opnmbllem  25835  mbfi1fseqlem1  25949  mbfi1fseqlem3  25951  mbfi1fseqlem4  25952  mbfi1fseqlem5  25953  mbfi1fseqlem6  25954  dvexp  26187  dvexp3  26212  idomrootle  26405  plyco  26474  dgrcolem1  26506  plydivex  26534  aaliou3lem2  26586  aaliou3lem3  26587  aaliou3lem5  26590  aaliou3lem6  26591  aaliou3lem7  26592  aaliou3lem9  26593  radcnvlem2  26657  dvradcnv  26664  pserdv2  26673  abelthlem6  26679  abelthlem9  26683  logtayllem  26904  logtayl  26905  logtaylsum  26906  logtayl2  26907  cxproot  26935  root1id  26999  logbgcd1irr  27039  atantayl  27182  atantayl2  27183  leibpilem2  27186  leibpi  27187  birthdaylem2  27197  birthdaylem3  27198  dfef2  27215  basellem2  27326  basellem4  27328  basellem5  27329  basellem6  27330  basellem8  27332  isppw2  27359  vmappw  27360  sqf11  27383  vma1  27410  1sgm2ppw  27444  chtublem  27455  fsumvma2  27458  vmasum  27460  dchrelbas4  27487  dchrzrhcl  27489  dchrfi  27499  dchrhash  27515  pcbcctr  27520  bclbnd  27524  bposlem1  27528  lgsval4a  27563  lgsdchrval  27598  lgsdchr  27599  gausslemma2dlem0c  27602  gausslemma2dlem0d  27603  gausslemma2dlem6  27616  2lgslem1a1  27633  2lgslem1c  27637  2lgslem3a1  27644  2lgslem3b1  27645  2lgslem3c1  27646  2lgslem3d1  27647  2sqreunnlem1  27693  2sqreunnltblem  27695  rplogsumlem2  27729  dchrisumlem2  27734  ostth2lem1  27862  ostth2lem3  27879  ostth3  27882  cusgrsize2inds  29921  pthdivtx  30199  cyclnumvtx  30275  crctcshwlkn0lem4  30289  crctcshwlkn0lem5  30290  crctcshwlkn0lem7  30292  0enwwlksnge1  30340  rusgr0edg  30452  clwlkclwwlkf1lem2  30483  clwlkclwwlkf1lem3  30484  clwwisshclwwslem  30492  clwwlkinwwlk  30518  clwwlkel  30524  clwwlkf  30525  clwwlkf1  30527  clwwlknwwlksnb  30533  wwlksubclwwlk  30536  erclwwlknref  30547  clwwlknonwwlknonb  30584  numclwwlkqhash  30863  numclwwlk2lem1  30864  numclwlk2lem2f  30865  numclwlk2lem2f1o  30867  ipval2  31196  ipasslem3  31322  ipasslem4  31323  nn0min  33299  znfermltl  33809  ply1fermltl  34004  esumcst  34581  eulerpartlemb  34887  fibp1  34920  ballotlem1  35006  subfacp1lem6  35772  subfaclim  35775  subfacval3  35776  snmlff  35916  bcprod  36325  faclim2  36335  nn0prpwlem  36949  knoppndvlem18  37234  opnmbllem0  38413  nnubfi  38508  nninfnub  38509  geomcau  38517  heiborlem5  38573  heiborlem6  38574  heiborlem7  38575  heiborlem8  38576  bfplem1  38580  lcmineqlem12  42914  aks4d1p1p2  42944  primrootscoprmpow  42973  2ap1caineq  43019  dvdsexpnn  43216  dvdsexpnn0  43217  zaddcomlem  43359  fidomncyc  43425  dffltz  43488  fltnltalem  43516  irrapxlem2  43672  pellexlem1  43678  pellexlem5  43682  pellqrex  43728  monotoddzzfi  43791  jm2.17c  43811  acongeq  43832  jm2.18  43837  jm2.23  43845  jm2.26lem3  43850  jm3.1  43869  expdiophlem1  43870  idomodle  44040  proot1ex  44045  rp-isfinite6  44366  cnvtrclfv  44572  cotrclrcl  44590  inductionexd  45003  binomcxplemnotnn0  45188  nnne1ge2  46132  dvnmptconst  46777  stoweidlem3  46839  stoweidlem7  46843  stoweidlem34  46870  wallispilem4  46904  wallispilem5  46905  wallispi2lem1  46907  wallispi2lem2  46908  stirlinglem2  46911  stirlinglem3  46912  stirlinglem4  46913  stirlinglem5  46914  stirlinglem7  46916  stirlinglem11  46920  stirlinglem14  46923  stirlinglem15  46924  stirlingr  46926  fourierdlem15  46958  fourierdlem21  46964  fourierdlem22  46965  fourierdlem92  47034  fourierdlem112  47054  fouriersw  47067  sge0rpcpnf  47257  sge0ad2en  47267  ovnsubaddlem1  47406  ovnsubaddlem2  47407  ovolval5lem1  47488  ovolval5lem2  47489  ceilhalfelfzo1  48230  modlt0b  48265  muldvdsfacm1  48283  iccpartiltu  48330  iccpartigtl  48331  iccpartlt  48332  iccpartleu  48336  iccpartrn  48338  iccelpart  48341  iccpartiun  48342  iccpartdisj  48345  sqrtpwpw2p  48449  fmtnosqrt  48450  odz2prm2pw  48474  fmtnoprmfac1lem  48475  fmtnoprmfac1  48476  2pwp1prm  48500  lighneallem1  48516  lighneallem2  48517  lighneallem3  48518  lighneallem4a  48519  lighneallem4  48521  nnpw2evenALTV  48626  dfwppr  48662  gpgorder  48983  gpgedgvtx0  48985  gpgedgvtx1  48986  cznabel  49183  cznrng  49184  ztprmneprm  49285  altgsumbc  49290  altgsumbcALT  49291  pw2m1lepw2m1  49458  nneom  49465  logbpw2m1  49505  blennn  49513  blenpw2m1  49517  blengt1fldiv2p1  49531  dignn0ldlem  49540  dignnld  49541  dig2nn1st  49543  dignn0flhalflem1  49553  nn0sumshdiglemA  49557  nn0sumshdiglemB  49558  itcovalt2lem2lem1  49611  eenglngeehlnm  49677