Theorem nnnn0 12435

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℕcn 12165  ℕ₀cn0 12428

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 3432  df-un 3895  df-ss 3907  df-n0 12429

This theorem is referenced by:  nnnn0i  12436  elnnnn0b  12472  elnnnn0c  12473  elz2  12533  nn0ind-raph  12620  zindd  12621  fzo1fzo0n0  13661  ubmelfzo  13676  elfzom1elp1fzo  13678  fzo0sn0fzo1  13701  quoremnn0ALT  13807  modmulnn  13839  modsumfzodifsn  13897  addmodlteq  13899  expneg  14022  expcllem  14025  expcl2lem  14026  expeq0  14045  mulexpz  14055  expmordi  14120  rpexpmord  14121  expnlbnd  14186  expmulnbnd  14188  digit2  14189  digit1  14190  facmapnn  14238  facdiv  14240  faclbnd  14243  faclbnd3  14245  faclbnd4lem3  14248  faclbnd4lem4  14249  faclbnd5  14251  faclbnd6  14252  bcval5  14271  ishashinf  14416  iswrdi  14470  pfxn0  14640  repswfsts  14734  repswlsw  14735  repswcshw  14765  relexpnnrn  14998  relexpaddg  15006  absexpz  15258  isercoll  15621  summolem3  15667  summolem2a  15668  climcndslem2  15806  climcnds  15807  harmonic  15815  arisum  15816  expcnv  15820  geo2sum  15829  geo2lim  15831  geoisum1  15835  geoisum1c  15836  0.999...  15837  mertenslem2  15841  fallfacfwd  15992  0fallfac  15993  0risefac  15994  ef0lem  16034  ege2le3  16046  efaddlem  16049  efexp  16059  rpnnen2lem2  16173  rpnnen2lem4  16175  ruclem12  16199  dvdsmodexp  16220  dvdsexp2im  16287  nn0enne  16337  nnehalf  16339  nno  16342  nn0o  16343  pwp1fsum  16351  divalg2  16365  ndvdssub  16369  gcdmultiplez  16495  gcddiv  16511  rpmulgcd  16517  rplpwr  16518  nn0expgcd  16524  dvdssqlem  16526  eucalgf  16543  lcmflefac  16608  1nprm  16639  2mulprm  16653  isprm5  16668  isprm6  16675  prmdvdsexp  16676  phicl2  16729  phibndlem  16731  phiprmpw  16737  crth  16739  eulerthlem2  16743  hashgcdlem  16749  phisum  16752  pythagtriplem10  16782  pythagtriplem6  16783  pythagtriplem7  16784  pythagtriplem12  16788  pythagtriplem14  16790  pclem  16800  pcexp  16821  pcid  16835  pcprod  16857  pcbc  16862  prmpwdvds  16866  infpnlem1  16872  infpnlem2  16873  prmunb  16876  prmreclem6  16883  1arith  16889  vdwapf  16934  0hashbc  16969  ram0  16984  prmdvdsprmo  17004  prmdvdsprmop  17005  prmolefac  17008  prmgaplem1  17011  prmgaplem2  17012  prmgapprmolem  17023  prmgapprmo  17024  cshwrepswhash1  17064  smndex1n0mnd  18874  ghmmulg  19194  odmodnn0  19506  dfod2  19530  submod  19535  prmirredlem  21462  prmirred  21464  znf1o  21541  znhash  21548  znfi  21549  znfld  21550  znidomb  21551  znunithash  21554  znrrg  21555  frobrhm  21565  cply1mul  22271  cply1coe0  22276  cply1coe0bi  22277  ply1fermltlchr  22287  cpmatmcllem  22693  m2cpm  22716  m2cpminvid2lem  22729  fvmptnn04ifa  22825  chfacfisf  22829  chfacfisfcpmat  22830  chfacffsupp  22831  chfacfscmul0  22833  chfacfscmulfsupp  22834  chfacfscmulgsum  22835  chfacfpmmul0  22837  chfacfpmmulfsupp  22838  chfacfpmmulgsum  22839  chfacfpmmulgsum2  22840  cayhamlem1  22841  cpmadugsumlemF  22851  tgpmulg  24068  cmodscexp  25098  cphipval  25220  ovollb2lem  25465  ovoliunlem1  25479  ovoliunlem3  25481  uniioombllem3  25562  uniioombllem4  25563  opnmbllem  25578  mbfi1fseqlem1  25692  mbfi1fseqlem3  25694  mbfi1fseqlem4  25695  mbfi1fseqlem5  25696  mbfi1fseqlem6  25697  dvexp  25930  dvexp3  25955  idomrootle  26148  plyco  26216  dgrcolem1  26248  plydivex  26274  aaliou3lem2  26320  aaliou3lem3  26321  aaliou3lem5  26324  aaliou3lem6  26325  aaliou3lem7  26326  aaliou3lem9  26327  radcnvlem2  26392  dvradcnv  26399  pserdv2  26408  abelthlem6  26414  abelthlem9  26418  logtayllem  26636  logtayl  26637  logtaylsum  26638  logtayl2  26639  cxproot  26667  root1id  26731  logbgcd1irr  26771  atantayl  26914  atantayl2  26915  leibpilem2  26918  leibpi  26919  birthdaylem2  26929  birthdaylem3  26930  dfef2  26948  basellem2  27059  basellem4  27061  basellem5  27062  basellem6  27063  basellem8  27065  isppw2  27092  vmappw  27093  sqf11  27116  vma1  27143  1sgm2ppw  27177  chtublem  27188  fsumvma2  27191  vmasum  27193  dchrelbas4  27220  dchrzrhcl  27222  dchrfi  27232  dchrhash  27248  pcbcctr  27253  bclbnd  27257  bposlem1  27261  lgsval4a  27296  lgsdchrval  27331  lgsdchr  27332  gausslemma2dlem0c  27335  gausslemma2dlem0d  27336  gausslemma2dlem6  27349  2lgslem1a1  27366  2lgslem1c  27370  2lgslem3a1  27377  2lgslem3b1  27378  2lgslem3c1  27379  2lgslem3d1  27380  2sqreunnlem1  27426  2sqreunnltblem  27428  rplogsumlem2  27462  dchrisumlem2  27467  ostth2lem1  27595  ostth2lem3  27612  ostth3  27615  cusgrsize2inds  29537  pthdivtx  29810  cyclnumvtx  29883  crctcshwlkn0lem4  29896  crctcshwlkn0lem5  29897  crctcshwlkn0lem7  29899  0enwwlksnge1  29947  rusgr0edg  30059  clwlkclwwlkf1lem2  30090  clwlkclwwlkf1lem3  30091  clwwisshclwwslem  30099  clwwlkinwwlk  30125  clwwlkel  30131  clwwlkf  30132  clwwlkf1  30134  clwwlknwwlksnb  30140  wwlksubclwwlk  30143  erclwwlknref  30154  clwwlknonwwlknonb  30191  numclwwlkqhash  30460  numclwwlk2lem1  30461  numclwlk2lem2f  30462  numclwlk2lem2f1o  30464  ipval2  30793  ipasslem3  30919  ipasslem4  30920  nn0min  32909  znfermltl  33441  ply1fermltl  33661  esumcst  34223  eulerpartlemb  34528  fibp1  34561  ballotlem1  34647  subfacp1lem6  35383  subfaclim  35386  subfacval3  35387  snmlff  35527  bcprod  35936  faclim2  35946  nn0prpwlem  36520  knoppndvlem18  36805  opnmbllem0  37991  nnubfi  38085  nninfnub  38086  geomcau  38094  heiborlem5  38150  heiborlem6  38151  heiborlem7  38152  heiborlem8  38153  bfplem1  38157  lcmineqlem12  42493  aks4d1p1p2  42523  primrootscoprmpow  42552  2ap1caineq  42598  dvdsexpnn  42779  dvdsexpnn0  42780  zaddcomlem  42922  fidomncyc  42994  dffltz  43081  fltnltalem  43109  irrapxlem2  43269  pellexlem1  43275  pellexlem5  43279  pellqrex  43325  monotoddzzfi  43388  jm2.17c  43408  acongeq  43429  jm2.18  43434  jm2.23  43442  jm2.26lem3  43447  jm3.1  43466  expdiophlem1  43467  idomodle  43637  proot1ex  43642  rp-isfinite6  43963  cnvtrclfv  44169  cotrclrcl  44187  inductionexd  44600  binomcxplemnotnn0  44801  nnne1ge2  45742  dvnmptconst  46387  stoweidlem3  46449  stoweidlem7  46453  stoweidlem34  46480  wallispilem4  46514  wallispilem5  46515  wallispi2lem1  46517  wallispi2lem2  46518  stirlinglem2  46521  stirlinglem3  46522  stirlinglem4  46523  stirlinglem5  46524  stirlinglem7  46526  stirlinglem11  46530  stirlinglem14  46533  stirlinglem15  46534  stirlingr  46536  fourierdlem15  46568  fourierdlem21  46574  fourierdlem22  46575  fourierdlem92  46644  fourierdlem112  46664  fouriersw  46677  sge0rpcpnf  46867  sge0ad2en  46877  ovnsubaddlem1  47016  ovnsubaddlem2  47017  ovolval5lem1  47098  ovolval5lem2  47099  nthrucw  47332  ceilhalfelfzo1  47794  modlt0b  47829  muldvdsfacm1  47847  iccpartiltu  47894  iccpartigtl  47895  iccpartlt  47896  iccpartleu  47900  iccpartrn  47902  iccelpart  47905  iccpartiun  47906  iccpartdisj  47909  sqrtpwpw2p  48013  fmtnosqrt  48014  odz2prm2pw  48038  fmtnoprmfac1lem  48039  fmtnoprmfac1  48040  2pwp1prm  48064  lighneallem1  48080  lighneallem2  48081  lighneallem3  48082  lighneallem4a  48083  lighneallem4  48085  nnpw2evenALTV  48190  dfwppr  48226  gpgorder  48547  gpgedgvtx0  48549  gpgedgvtx1  48550  cznabel  48748  cznrng  48749  ztprmneprm  48835  altgsumbc  48840  altgsumbcALT  48841  pw2m1lepw2m1  49008  nneom  49015  logbpw2m1  49055  blennn  49063  blenpw2m1  49067  blengt1fldiv2p1  49081  dignn0ldlem  49090  dignnld  49091  dig2nn1st  49093  dignn0flhalflem1  49103  nn0sumshdiglemA  49107  nn0sumshdiglemB  49108  itcovalt2lem2lem1  49161  eenglngeehlnm  49227