Theorem nnnn0 12429

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

Syntax hints:   → wi 4   ∈ wcel 2106  ℕcn 12162  ℕ₀cn0 12422

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-un 3918  df-in 3920  df-ss 3930  df-n0 12423

This theorem is referenced by:  nnnn0i  12430  elnnnn0b  12466  elnnnn0c  12467  elz2  12526  nn0ind-raph  12612  zindd  12613  fzo1fzo0n0  13633  ubmelfzo  13647  elfzom1elp1fzo  13649  fzo0sn0fzo1  13671  quoremnn0ALT  13772  modmulnn  13804  modsumfzodifsn  13859  addmodlteq  13861  expneg  13985  expcllem  13988  expcl2lem  13989  expeq0  14008  mulexpz  14018  expmordi  14082  rpexpmord  14083  expnlbnd  14146  expmulnbnd  14148  digit2  14149  digit1  14150  facmapnn  14195  facdiv  14197  faclbnd  14200  faclbnd3  14202  faclbnd4lem3  14205  faclbnd4lem4  14206  faclbnd5  14208  faclbnd6  14209  bcval5  14228  ishashinf  14374  iswrdi  14418  pfxn0  14586  repswfsts  14681  repswlsw  14682  repswcshw  14712  relexpnnrn  14942  relexpaddg  14950  absexpz  15202  isercoll  15564  summolem3  15610  summolem2a  15611  climcndslem2  15746  climcnds  15747  harmonic  15755  arisum  15756  expcnv  15760  geo2sum  15769  geo2lim  15771  geoisum1  15775  geoisum1c  15776  0.999...  15777  mertenslem2  15781  fallfacfwd  15930  0fallfac  15931  0risefac  15932  ef0lem  15972  ege2le3  15983  efaddlem  15986  efexp  15994  rpnnen2lem2  16108  rpnnen2lem4  16110  ruclem12  16134  dvdsmodexp  16155  dvdsexp2im  16220  nn0enne  16270  nnehalf  16272  nno  16275  nn0o  16276  pwp1fsum  16284  divalg2  16298  ndvdssub  16302  gcdmultiplez  16427  gcddiv  16443  rpmulgcd  16448  rplpwr  16449  dvdssqlem  16453  eucalgf  16470  lcmflefac  16535  1nprm  16566  2mulprm  16580  isprm5  16594  isprm6  16601  prmdvdsexp  16602  phicl2  16651  phibndlem  16653  phiprmpw  16659  crth  16661  eulerthlem2  16665  hashgcdlem  16671  phisum  16673  pythagtriplem10  16703  pythagtriplem6  16704  pythagtriplem7  16705  pythagtriplem12  16709  pythagtriplem14  16711  pclem  16721  pcexp  16742  pcid  16756  pcprod  16778  pcbc  16783  prmpwdvds  16787  infpnlem1  16793  infpnlem2  16794  prmunb  16797  prmreclem6  16804  1arith  16810  vdwapf  16855  0hashbc  16890  ram0  16905  prmdvdsprmo  16925  prmdvdsprmop  16926  prmolefac  16929  prmgaplem1  16932  prmgaplem2  16933  prmgapprmolem  16944  prmgapprmo  16945  cshwrepswhash1  16986  smndex1n0mnd  18736  ghmmulg  19034  odmodnn0  19336  dfod2  19360  submod  19365  prmirredlem  20930  prmirred  20932  znf1o  20995  znhash  21002  znfi  21003  znfld  21004  znidomb  21005  znunithash  21008  znrrg  21009  cply1mul  21702  cply1coe0  21707  cply1coe0bi  21708  cpmatmcllem  22104  m2cpm  22127  m2cpminvid2lem  22140  fvmptnn04ifa  22236  chfacfisf  22240  chfacfisfcpmat  22241  chfacffsupp  22242  chfacfscmul0  22244  chfacfscmulfsupp  22245  chfacfscmulgsum  22246  chfacfpmmul0  22248  chfacfpmmulfsupp  22249  chfacfpmmulgsum  22250  chfacfpmmulgsum2  22251  cayhamlem1  22252  cpmadugsumlemF  22262  tgpmulg  23481  cmodscexp  24521  cphipval  24644  ovollb2lem  24889  ovoliunlem1  24903  ovoliunlem3  24905  uniioombllem3  24986  uniioombllem4  24987  opnmbllem  25002  mbfi1fseqlem1  25117  mbfi1fseqlem3  25119  mbfi1fseqlem4  25120  mbfi1fseqlem5  25121  mbfi1fseqlem6  25122  dvexp  25354  dvexp3  25379  plyco  25639  dgrcolem1  25671  plydivex  25694  aaliou3lem2  25740  aaliou3lem3  25741  aaliou3lem5  25744  aaliou3lem6  25745  aaliou3lem7  25746  aaliou3lem9  25747  radcnvlem2  25810  dvradcnv  25817  pserdv2  25826  abelthlem6  25832  abelthlem9  25836  logtayllem  26051  logtayl  26052  logtaylsum  26053  logtayl2  26054  cxproot  26082  root1id  26144  logbgcd1irr  26181  atantayl  26324  atantayl2  26325  leibpilem2  26328  leibpi  26329  birthdaylem2  26339  birthdaylem3  26340  dfef2  26357  basellem2  26468  basellem4  26470  basellem5  26471  basellem6  26472  basellem8  26474  isppw2  26501  vmappw  26502  sqf11  26525  vma1  26552  1sgm2ppw  26585  chtublem  26596  fsumvma2  26599  vmasum  26601  dchrelbas4  26628  dchrzrhcl  26630  dchrfi  26640  dchrhash  26656  pcbcctr  26661  bclbnd  26665  bposlem1  26669  lgsval4a  26704  lgsdchrval  26739  lgsdchr  26740  gausslemma2dlem0c  26743  gausslemma2dlem0d  26744  gausslemma2dlem6  26757  2lgslem1a1  26774  2lgslem1c  26778  2lgslem3a1  26785  2lgslem3b1  26786  2lgslem3c1  26787  2lgslem3d1  26788  2sqreunnlem1  26834  2sqreunnltblem  26836  rplogsumlem2  26870  dchrisumlem2  26875  ostth2lem1  27003  ostth2lem3  27020  ostth3  27023  cusgrsize2inds  28464  pthdivtx  28740  crctcshwlkn0lem4  28821  crctcshwlkn0lem5  28822  crctcshwlkn0lem7  28824  0enwwlksnge1  28872  rusgr0edg  28981  clwlkclwwlkf1lem2  29012  clwlkclwwlkf1lem3  29013  clwwisshclwwslem  29021  clwwlkinwwlk  29047  clwwlkel  29053  clwwlkf  29054  clwwlkf1  29056  clwwlknwwlksnb  29062  wwlksubclwwlk  29065  erclwwlknref  29076  clwwlknonwwlknonb  29113  numclwwlkqhash  29382  numclwwlk2lem1  29383  numclwlk2lem2f  29384  numclwlk2lem2f1o  29386  ipval2  29712  ipasslem3  29838  ipasslem4  29839  nn0min  31786  frobrhm  32138  znfermltl  32227  ply1fermltlchr  32361  ply1fermltl  32362  esumcst  32751  eulerpartlemb  33057  fibp1  33090  ballotlem1  33175  subfacp1lem6  33866  subfaclim  33869  subfacval3  33870  snmlff  34010  bcprod  34397  faclim2  34407  nn0prpwlem  34870  knoppndvlem18  35068  opnmbllem0  36187  nnubfi  36282  nninfnub  36283  geomcau  36291  heiborlem5  36347  heiborlem6  36348  heiborlem7  36349  heiborlem8  36350  bfplem1  36354  lcmineqlem12  40570  aks4d1p1p2  40600  2ap1caineq  40626  nn0expgcd  40879  dvdsexpnn  40884  dvdsexpnn0  40885  zaddcomlem  40978  dffltz  41030  fltnltalem  41058  irrapxlem2  41204  pellexlem1  41210  pellexlem5  41214  pellqrex  41260  monotoddzzfi  41324  jm2.17c  41344  acongeq  41365  jm2.18  41370  jm2.23  41378  jm2.26lem3  41383  jm3.1  41402  expdiophlem1  41403  idomrootle  41580  idomodle  41581  proot1ex  41586  rp-isfinite6  41912  cnvtrclfv  42118  cotrclrcl  42136  inductionexd  42549  binomcxplemnotnn0  42758  nnne1ge2  43646  dvnmptconst  44302  stoweidlem3  44364  stoweidlem7  44368  stoweidlem34  44395  wallispilem4  44429  wallispilem5  44430  wallispi2lem1  44432  wallispi2lem2  44433  stirlinglem2  44436  stirlinglem3  44437  stirlinglem4  44438  stirlinglem5  44439  stirlinglem7  44441  stirlinglem11  44445  stirlinglem14  44448  stirlinglem15  44449  stirlingr  44451  fourierdlem15  44483  fourierdlem21  44489  fourierdlem22  44490  fourierdlem92  44559  fourierdlem112  44579  fouriersw  44592  sge0rpcpnf  44782  sge0ad2en  44792  ovnsubaddlem1  44931  ovnsubaddlem2  44932  ovolval5lem1  45013  ovolval5lem2  45014  iccpartiltu  45734  iccpartigtl  45735  iccpartlt  45736  iccpartleu  45740  iccpartrn  45742  iccelpart  45745  iccpartiun  45746  iccpartdisj  45749  sqrtpwpw2p  45850  fmtnosqrt  45851  odz2prm2pw  45875  fmtnoprmfac1lem  45876  fmtnoprmfac1  45877  2pwp1prm  45901  lighneallem1  45917  lighneallem2  45918  lighneallem3  45919  lighneallem4a  45920  lighneallem4  45922  nnpw2evenALTV  46014  dfwppr  46050  cznabel  46372  cznrng  46373  ztprmneprm  46543  altgsumbc  46548  altgsumbcALT  46549  pw2m1lepw2m1  46721  nneom  46733  logbpw2m1  46773  blennn  46781  blenpw2m1  46785  blengt1fldiv2p1  46799  dignn0ldlem  46808  dignnld  46809  dig2nn1st  46811  dignn0flhalflem1  46821  nn0sumshdiglemA  46825  nn0sumshdiglemB  46826  itcovalt2lem2lem1  46879  eenglngeehlnm  46945