Theorem nnnn0 10823

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 10819	. 2 |- NN C_ NN0
2	1	sseli 3495	1 |- ( A e. NN -> A e. NN0 )

Syntax hints:   -> wi 4   e. wcel 1819   NNcn 10556   NN0cn0 10816

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3476  df-in 3478  df-ss 3485  df-n0 10817

This theorem is referenced by:  nnnn0i  10824  elnnnn0b  10861  elnnnn0c  10862  elz2  10902  nn0ind-raph  10985  zindd  10986  fzo1fzo0n0  11862  ubmelfzo  11883  elfzom1elp1fzo  11885  fzo0sn0fzo1  11904  quoremnn0ALT  11986  modmulnn  12015  expneg  12176  expcllem  12179  expcl2lem  12180  expeq0  12198  mulexpz  12208  expnlbnd  12298  expmulnbnd  12300  digit2  12301  digit1  12302  facdiv  12367  faclbnd  12370  faclbnd3  12372  faclbnd4lem3  12375  faclbnd4lem4  12376  faclbnd5  12378  faclbnd6  12379  bcval5  12398  iswrdi  12556  swrdn0  12665  swrdtrcfv  12676  swrdccatwrd  12704  repswfsts  12764  repswlsw  12765  repswcshw  12791  absexpz  13149  isercoll  13501  summolem3  13547  summolem2a  13548  climcndslem2  13673  climcnds  13674  harmonic  13681  arisum  13682  expcnv  13686  geo2sum  13693  geo2lim  13695  geoisum1  13699  geoisum1c  13700  0.999...  13701  mertenslem2  13705  ef0lem  13825  ege2le3  13836  efaddlem  13839  efexp  13847  xpnnenOLD  13954  rpnnen2lem2  13960  rpnnen2lem4  13962  ruclem12  13985  divalg2  14074  ndvdssub  14076  gcddiv  14198  gcdmultiple  14199  gcdmultiplez  14200  rpmulgcd  14204  rplpwr  14205  dvdssqlem  14208  eucalgf  14223  1nprm  14233  isprm6  14261  isprm5  14264  prmdvdsexp  14266  phicl2  14309  phibndlem  14311  phiprmpw  14317  crt  14319  eulerthlem2  14323  pythagtriplem10  14355  pythagtriplem6  14356  pythagtriplem7  14357  pythagtriplem12  14361  pythagtriplem14  14363  pclem  14373  pcexp  14394  pcid  14407  pcprod  14425  pcbc  14430  prmpwdvds  14433  infpnlem1  14439  infpnlem2  14440  prmunb  14443  prmreclem6  14450  1arith  14456  vdwapf  14501  0hashbc  14536  ram0  14551  cshwrepswhash1  14598  ghmmulg  16405  odmodnn0  16690  dfod2  16712  submod  16715  cply1mul  18461  cply1coe0  18467  cply1coe0bi  18468  prmirredlem  18649  prmirred  18651  prmirredlemOLD  18652  prmirredOLD  18654  znf1o  18716  znhash  18723  znfi  18724  znfld  18725  znidomb  18726  znunithash  18729  znrrg  18730  cpmatmcllem  19345  m2cpm  19368  m2cpminvid2lem  19381  fvmptnn04ifa  19477  chfacfisf  19481  chfacfisfcpmat  19482  chfacffsupp  19483  chfacfscmul0  19485  chfacfscmulfsupp  19486  chfacfscmulgsum  19487  chfacfpmmul0  19489  chfacfpmmulfsupp  19490  chfacfpmmulgsum  19491  chfacfpmmulgsum2  19492  cayhamlem1  19493  cpmadugsumlemF  19503  tgpmulg  20717  ovollb2lem  22024  ovoliunlem1  22038  ovoliunlem3  22040  uniioombllem3  22119  uniioombllem4  22120  opnmbllem  22135  mbfi1fseqlem1  22247  mbfi1fseqlem3  22249  mbfi1fseqlem4  22250  mbfi1fseqlem5  22251  mbfi1fseqlem6  22252  dvexp  22481  dvexp3  22504  plyco  22763  dgrcolem1  22795  plydivex  22818  aaliou3lem2  22864  aaliou3lem3  22865  aaliou3lem5  22868  aaliou3lem6  22869  aaliou3lem7  22870  aaliou3lem9  22871  radcnvlem2  22934  dvradcnv  22941  pserdv2  22950  abelthlem6  22956  abelthlem9  22960  logtayllem  23165  logtayl  23166  logtaylsum  23167  logtayl2  23168  cxproot  23196  root1id  23253  atantayl  23393  atantayl2  23394  leibpilem2  23397  leibpi  23398  birthdaylem2  23407  birthdaylem3  23408  dfef2  23425  basellem2  23480  basellem4  23482  basellem5  23483  basellem6  23484  basellem8  23486  isppw2  23514  vmappw  23515  sqf11  23538  vma1  23565  1sgm2ppw  23600  chtublem  23611  fsumvma2  23614  vmasum  23616  dchrelbas4  23643  dchrzrhcl  23645  dchrfi  23655  dchrhash  23671  pcbcctr  23676  bclbnd  23680  bposlem1  23684  lgsval4a  23718  lgsdchrval  23747  lgsdchr  23748  rplogsumlem2  23795  dchrisumlem2  23800  ostth2lem1  23928  ostth2lem3  23945  ostth3  23948  cusgrasize2inds  24603  cyclnspth  24757  clwwlkel  24919  clwwlkf  24920  clwwlkf1  24922  wwlksubclwwlk  24930  clwwisshclwwlem  24932  clwlkf1clwwlklem  24975  rusgra0edg  25081  clwlknclwlkdifnum  25087  clwwlkextfrlem1  25202  numclwwlkqhash  25226  numclwwlk2lem1  25228  numclwlk2lem2f  25229  numclwlk2lem2f1o  25231  gxcl  25393  ipval2  25743  ipasslem3  25874  ipasslem4  25875  ishashinf  27758  nn0min  27763  esumcst  28226  eulerpartlemb  28482  fibp1  28515  ballotlem1  28600  subfacp1lem6  28804  subfaclim  28807  subfacval3  28808  snmlff  28949  fallfacfwd  29333  0fallfac  29334  0risefac  29335  faclim2  29348  dvdspw  29350  opnmbllem0  30212  nn0prpwlem  30302  nnubfi  30405  nninfnub  30406  geomcau  30414  heiborlem5  30473  heiborlem6  30474  heiborlem7  30475  heiborlem8  30476  bfplem1  30480  irrapxlem2  30921  pellexlem1  30927  pellexlem5  30931  pellqrex  30977  monotoddzzfi  31040  expmordi  31045  rpexpmord  31046  jm2.17c  31062  acongeq  31083  jm2.18  31092  jm2.23  31100  jm2.26lem3  31105  jm3.1  31124  expdiophlem1  31125  idomrootle  31314  idomodle  31315  hashgcdlem  31319  phisum  31321  proot1ex  31323  binomcxplemnotnn0  31423  nnne1ge2  31642  dvnmptconst  31899  stoweidlem3  31946  stoweidlem7  31950  stoweidlem34  31977  wallispilem4  32011  wallispilem5  32012  wallispi2lem1  32014  wallispi2lem2  32015  stirlinglem2  32018  stirlinglem3  32019  stirlinglem4  32020  stirlinglem5  32021  stirlinglem7  32023  stirlinglem11  32027  stirlinglem14  32030  stirlinglem15  32031  stirlingr  32033  fourierdlem15  32065  fourierdlem21  32071  fourierdlem22  32072  fourierdlem92  32142  fourierdlem112  32162  fouriersw  32175  pfxn0  32469  cznabel  32864  cznrng  32865  ztprmneprm  33038  altgsumbc  33043  altgsumbcALT  33044  rp-isfinite6  37845  inductionexd  38068