Theorem nnnn0 10904

Description: A positive integer is a nonnegative integer. (Contributed by NM, 9-May-2004.)

Assertion

Ref	Expression
nnnn0	|- ( A e. NN -> A e. NN0 )

Proof of Theorem nnnn0

Step	Hyp	Ref	Expression
1		nnssnn0 10900	. 2 |- NN C_ NN0
2	1	sseli 3439	1 |- ( A e. NN -> A e. NN0 )

Syntax hints:   -> wi 4   e. wcel 1897   NNcn 10636   NN0cn0 10897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-v 3058  df-un 3420  df-in 3422  df-ss 3429  df-n0 10898

This theorem is referenced by:  nnnn0i  10905  elnnnn0b  10942  elnnnn0c  10943  elz2  10982  nn0ind-raph  11063  zindd  11064  fzo1fzo0n0  11987  ubmelfzo  12009  elfzom1elp1fzo  12011  fzo0sn0fzo1  12031  quoremnn0ALT  12115  modmulnn  12145  expneg  12311  expcllem  12314  expcl2lem  12315  expeq0  12333  mulexpz  12343  expnlbnd  12433  expmulnbnd  12435  digit2  12436  digit1  12437  facmapnn  12501  facdiv  12503  faclbnd  12506  faclbnd3  12508  faclbnd4lem3  12511  faclbnd4lem4  12512  faclbnd5  12514  faclbnd6  12515  bcval5  12534  ishashinf  12658  iswrdi  12707  swrdn0  12822  swrdtrcfv  12833  swrdccatwrd  12860  repswfsts  12920  repswlsw  12921  repswcshw  12947  relexpnnrn  13156  relexpaddg  13164  absexpz  13416  isercoll  13779  summolem3  13828  summolem2a  13829  climcndslem2  13956  climcnds  13957  harmonic  13965  arisum  13966  expcnv  13970  geo2sum  13977  geo2lim  13979  geoisum1  13983  geoisum1c  13984  0.999...  13985  mertenslem2  13989  fallfacfwd  14137  0fallfac  14138  0risefac  14139  ef0lem  14181  ege2le3  14192  efaddlem  14195  efexp  14203  rpnnen2lem2  14316  rpnnen2lem4  14318  ruclem12  14341  divalg2  14434  ndvdssub  14436  gcddiv  14565  gcdmultiple  14566  gcdmultiplez  14567  rpmulgcd  14571  rplpwr  14572  dvdssqlem  14575  eucalgf  14590  lcmslefacOLD  14634  lcmflefac  14669  1nprm  14677  isprm5  14699  isprm6  14714  prmdvdsexp  14715  phicl2  14764  phibndlem  14766  phiprmpw  14772  crt  14774  eulerthlem2  14778  pythagtriplem10  14818  pythagtriplem6  14819  pythagtriplem7  14820  pythagtriplem12  14824  pythagtriplem14  14826  pclem  14836  pcexp  14857  pcid  14870  pcprod  14888  pcbc  14893  prmpwdvds  14896  infpnlem1  14902  infpnlem2  14903  prmunb  14906  prmreclem6  14913  1arith  14919  vdwapf  14970  0hashbc  15007  ram0  15028  prmdvdsprmo  15048  prmdvdsprmop  15049  prmolefac  15052  prmgaplem1  15055  prmgaplem2  15056  prmorlefacOLD  15066  prmgapprmolem  15080  prmgapprmo  15081  cshwrepswhash1  15121  ghmmulg  16943  odmodnn0  17237  dfod2  17263  submod  17266  cply1mul  18935  cply1coe0  18941  cply1coe0bi  18942  prmirredlem  19112  prmirred  19114  znf1o  19170  znhash  19177  znfi  19178  znfld  19179  znidomb  19180  znunithash  19183  znrrg  19184  cpmatmcllem  19790  m2cpm  19813  m2cpminvid2lem  19826  fvmptnn04ifa  19922  chfacfisf  19926  chfacfisfcpmat  19927  chfacffsupp  19928  chfacfscmul0  19930  chfacfscmulfsupp  19931  chfacfscmulgsum  19932  chfacfpmmul0  19934  chfacfpmmulfsupp  19935  chfacfpmmulgsum  19936  chfacfpmmulgsum2  19937  cayhamlem1  19938  cpmadugsumlemF  19948  tgpmulg  21156  ovollb2lem  22489  ovoliunlem1  22503  ovoliunlem3  22505  uniioombllem3  22591  uniioombllem4  22592  opnmbllem  22607  mbfi1fseqlem1  22721  mbfi1fseqlem3  22723  mbfi1fseqlem4  22724  mbfi1fseqlem5  22725  mbfi1fseqlem6  22726  dvexp  22955  dvexp3  22978  plyco  23243  dgrcolem1  23275  plydivex  23298  aaliou3lem2  23347  aaliou3lem3  23348  aaliou3lem5  23351  aaliou3lem6  23352  aaliou3lem7  23353  aaliou3lem9  23354  radcnvlem2  23417  dvradcnv  23424  pserdv2  23433  abelthlem6  23439  abelthlem9  23443  logtayllem  23652  logtayl  23653  logtaylsum  23654  logtayl2  23655  cxproot  23683  root1id  23742  atantayl  23911  atantayl2  23912  leibpilem2  23915  leibpi  23916  birthdaylem2  23926  birthdaylem3  23927  dfef2  23944  basellem2  24056  basellem4  24058  basellem5  24059  basellem6  24060  basellem8  24062  isppw2  24090  vmappw  24091  sqf11  24114  vma1  24141  1sgm2ppw  24176  chtublem  24187  fsumvma2  24190  vmasum  24192  dchrelbas4  24219  dchrzrhcl  24221  dchrfi  24231  dchrhash  24247  pcbcctr  24252  bclbnd  24256  bposlem1  24260  lgsval4a  24294  lgsdchrval  24323  lgsdchr  24324  rplogsumlem2  24371  dchrisumlem2  24376  ostth2lem1  24504  ostth2lem3  24521  ostth3  24524  cusgrasize2inds  25253  cyclnspth  25407  clwwlkel  25569  clwwlkf  25570  clwwlkf1  25572  wwlksubclwwlk  25580  clwwisshclwwlem  25582  clwlkf1clwwlklem  25625  rusgra0edg  25731  clwlknclwlkdifnum  25737  clwwlkextfrlem1  25852  numclwwlkqhash  25876  numclwwlk2lem1  25878  numclwlk2lem2f  25879  numclwlk2lem2f1o  25881  gxcl  26041  ipval2  26391  ipasslem3  26522  ipasslem4  26523  nn0min  28432  esumcst  28932  eulerpartlemb  29249  fibp1  29282  ballotlem1  29367  subfacp1lem6  29956  subfaclim  29959  subfacval3  29960  snmlff  30100  bcprod  30422  faclim2  30432  dvdspw  30434  nn0prpwlem  31026  opnmbllem0  32020  nnubfi  32123  nninfnub  32124  geomcau  32132  heiborlem5  32191  heiborlem6  32192  heiborlem7  32193  heiborlem8  32194  bfplem1  32198  irrapxlem2  35711  pellexlem1  35717  pellexlem5  35721  pellqrex  35770  monotoddzzfi  35834  expmordi  35839  rpexpmord  35840  jm2.17c  35856  acongeq  35877  jm2.18  35887  jm2.23  35895  jm2.26lem3  35900  jm3.1  35919  expdiophlem1  35920  idomrootle  36113  idomodle  36114  hashgcdlem  36118  phisum  36120  proot1ex  36122  rp-isfinite6  36207  cnvtrclfv  36360  cotrclrcl  36378  inductionexd  36637  binomcxplemnotnn0  36748  nnne1ge2  37542  dvnmptconst  37853  stoweidlem3  37900  stoweidlem7  37904  stoweidlem34  37932  wallispilem4  37967  wallispilem5  37968  wallispi2lem1  37970  wallispi2lem2  37971  stirlinglem2  37974  stirlinglem3  37975  stirlinglem4  37976  stirlinglem5  37977  stirlinglem7  37979  stirlinglem11  37983  stirlinglem14  37986  stirlinglem15  37987  stirlingr  37989  fourierdlem15  38021  fourierdlem21  38027  fourierdlem22  38028  fourierdlem92  38099  fourierdlem112  38119  fouriersw  38132  sge0rpcpnf  38300  sge0ad2en  38310  ovnsubaddlem1  38429  ovnsubaddlem2  38430  iccpartiltu  38773  iccpartigtl  38774  iccpartlt  38775  iccpartleu  38779  iccpartrn  38781  iccelpart  38784  iccpartiun  38785  iccpartdisj  38788  nnpw2evenALTV  38866  pfxn0  38974  cusgrsize2inds  39563  pthdivtx  39761  cznabel  40228  cznrng  40229  ztprmneprm  40400  altgsumbc  40405  altgsumbcALT  40406  pw2m1lepw2m1  40590  nn0enne  40598  nno  40600  nn0o  40601  nneom  40606  logbpw2m1  40650  blennn  40658  blenpw2m1  40662  blengt1fldiv2p1  40676  dignn0ldlem  40685  dignnld  40686  dig2nn1st  40688  dignn0flhalflem1  40698  nn0sumshdiglemA  40702  nn0sumshdiglemB  40703