Theorem nnnn0 11299

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

Syntax hints:   -> wi 4   e. wcel 1990   NNcn 11020   NN0cn0 11292

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579  df-in 3581  df-ss 3588  df-n0 11293

This theorem is referenced by:  nnnn0i  11300  elnnnn0b  11337  elnnnn0c  11338  elz2  11394  nn0ind-raph  11477  zindd  11478  fzo1fzo0n0  12518  ubmelfzo  12532  elfzom1elp1fzo  12534  fzo0sn0fzo1  12557  quoremnn0ALT  12656  modmulnn  12688  modsumfzodifsn  12743  addmodlteq  12745  expneg  12868  expcllem  12871  expcl2lem  12872  expeq0  12890  mulexpz  12900  expnlbnd  12994  expmulnbnd  12996  digit2  12997  digit1  12998  facmapnn  13072  facdiv  13074  faclbnd  13077  faclbnd3  13079  faclbnd4lem3  13082  faclbnd4lem4  13083  faclbnd5  13085  faclbnd6  13086  bcval5  13105  ishashinf  13247  iswrdi  13309  swrdn0  13430  swrdtrcfv  13441  swrdccatwrd  13468  repswfsts  13528  repswlsw  13529  repswcshw  13558  relexpnnrn  13785  relexpaddg  13793  absexpz  14045  isercoll  14398  summolem3  14445  summolem2a  14446  climcndslem2  14582  climcnds  14583  harmonic  14591  arisum  14592  expcnv  14596  geo2sum  14604  geo2lim  14606  geoisum1  14610  geoisum1c  14611  0.999...  14612  0.999...OLD  14613  mertenslem2  14617  fallfacfwd  14767  0fallfac  14768  0risefac  14769  ef0lem  14809  ege2le3  14820  efaddlem  14823  efexp  14831  rpnnen2lem2  14944  rpnnen2lem4  14946  ruclem12  14970  nn0enne  15094  nnehalf  15096  nno  15098  nn0o  15099  pwp1fsum  15114  divalg2  15128  ndvdssub  15133  gcddiv  15268  gcdmultiple  15269  gcdmultiplez  15270  rpmulgcd  15275  rplpwr  15276  dvdssqlem  15279  eucalgf  15296  lcmflefac  15361  1nprm  15392  isprm5  15419  isprm6  15426  prmdvdsexp  15427  phicl2  15473  phibndlem  15475  phiprmpw  15481  crth  15483  eulerthlem2  15487  hashgcdlem  15493  phisum  15495  pythagtriplem10  15525  pythagtriplem6  15526  pythagtriplem7  15527  pythagtriplem12  15531  pythagtriplem14  15533  pclem  15543  pcexp  15564  pcid  15577  pcprod  15599  pcbc  15604  prmpwdvds  15608  infpnlem1  15614  infpnlem2  15615  prmunb  15618  prmreclem6  15625  1arith  15631  vdwapf  15676  0hashbc  15711  ram0  15726  prmdvdsprmo  15746  prmdvdsprmop  15747  prmolefac  15750  prmgaplem1  15753  prmgaplem2  15754  prmgapprmolem  15765  prmgapprmo  15766  cshwrepswhash1  15809  ghmmulg  17672  odmodnn0  17959  dfod2  17981  submod  17984  cply1mul  19664  cply1coe0  19669  cply1coe0bi  19670  prmirredlem  19841  prmirred  19843  znf1o  19900  znhash  19907  znfi  19908  znfld  19909  znidomb  19910  znunithash  19913  znrrg  19914  cpmatmcllem  20523  m2cpm  20546  m2cpminvid2lem  20559  fvmptnn04ifa  20655  chfacfisf  20659  chfacfisfcpmat  20660  chfacffsupp  20661  chfacfscmul0  20663  chfacfscmulfsupp  20664  chfacfscmulgsum  20665  chfacfpmmul0  20667  chfacfpmmulfsupp  20668  chfacfpmmulgsum  20669  chfacfpmmulgsum2  20670  cayhamlem1  20671  cpmadugsumlemF  20681  tgpmulg  21897  cmodscexp  22921  cphipval  23042  ovollb2lem  23256  ovoliunlem1  23270  ovoliunlem3  23272  uniioombllem3  23353  uniioombllem4  23354  opnmbllem  23369  mbfi1fseqlem1  23482  mbfi1fseqlem3  23484  mbfi1fseqlem4  23485  mbfi1fseqlem5  23486  mbfi1fseqlem6  23487  dvexp  23716  dvexp3  23741  plyco  23997  dgrcolem1  24029  plydivex  24052  aaliou3lem2  24098  aaliou3lem3  24099  aaliou3lem5  24102  aaliou3lem6  24103  aaliou3lem7  24104  aaliou3lem9  24105  radcnvlem2  24168  dvradcnv  24175  pserdv2  24184  abelthlem6  24190  abelthlem9  24194  logtayllem  24405  logtayl  24406  logtaylsum  24407  logtayl2  24408  cxproot  24436  root1id  24495  atantayl  24664  atantayl2  24665  leibpilem2  24668  leibpi  24669  birthdaylem2  24679  birthdaylem3  24680  dfef2  24697  basellem2  24808  basellem4  24810  basellem5  24811  basellem6  24812  basellem8  24814  isppw2  24841  vmappw  24842  sqf11  24865  vma1  24892  1sgm2ppw  24925  chtublem  24936  fsumvma2  24939  vmasum  24941  dchrelbas4  24968  dchrzrhcl  24970  dchrfi  24980  dchrhash  24996  pcbcctr  25001  bclbnd  25005  bposlem1  25009  lgsval4a  25044  lgsdchrval  25079  lgsdchr  25080  gausslemma2dlem0c  25083  gausslemma2dlem0d  25084  gausslemma2dlem6  25097  2lgslem1a1  25114  2lgslem1c  25118  2lgslem3a1  25125  2lgslem3b1  25126  2lgslem3c1  25127  2lgslem3d1  25128  rplogsumlem2  25174  dchrisumlem2  25179  ostth2lem1  25307  ostth2lem3  25324  ostth3  25327  cusgrsize2inds  26349  pthdivtx  26625  crctcshwlkn0lem4  26705  crctcshwlkn0lem5  26706  crctcshwlkn0lem7  26708  0enwwlksnge1  26749  wspniunwspnon  26819  rusgr0edg  26868  clwwlknclwwlkdifnum  26874  clwwlkinwwlk  26905  clwwlksnfi  26913  clwwlksel  26914  clwwlksf  26915  clwwlksf1  26917  wwlksubclwwlks  26925  clwwisshclwwslem  26927  erclwwlksnref  26946  clwlksf1clwwlklem  26968  numclwwlk2lem1  27235  numclwlk2lem2f  27236  numclwwlk4  27244  ipval2  27562  ipasslem3  27688  ipasslem4  27689  nn0min  29567  esumcst  30125  eulerpartlemb  30430  fibp1  30463  ballotlem1  30548  subfacp1lem6  31167  subfaclim  31170  subfacval3  31171  snmlff  31311  bcprod  31624  faclim2  31634  dvdspw  31636  nn0prpwlem  32317  knoppndvlem18  32520  opnmbllem0  33445  nnubfi  33546  nninfnub  33547  geomcau  33555  heiborlem5  33614  heiborlem6  33615  heiborlem7  33616  heiborlem8  33617  bfplem1  33621  irrapxlem2  37387  pellexlem1  37393  pellexlem5  37397  pellqrex  37443  monotoddzzfi  37507  expmordi  37512  rpexpmord  37513  jm2.17c  37529  acongeq  37550  jm2.18  37555  jm2.23  37563  jm2.26lem3  37568  jm3.1  37587  expdiophlem1  37588  idomrootle  37773  idomodle  37774  proot1ex  37779  rp-isfinite6  37864  cnvtrclfv  38016  cotrclrcl  38034  inductionexd  38453  binomcxplemnotnn0  38555  nnne1ge2  39504  dvnmptconst  40156  stoweidlem3  40220  stoweidlem7  40224  stoweidlem34  40251  wallispilem4  40285  wallispilem5  40286  wallispi2lem1  40288  wallispi2lem2  40289  stirlinglem2  40292  stirlinglem3  40293  stirlinglem4  40294  stirlinglem5  40295  stirlinglem7  40297  stirlinglem11  40301  stirlinglem14  40304  stirlinglem15  40305  stirlingr  40307  fourierdlem15  40339  fourierdlem21  40345  fourierdlem22  40346  fourierdlem92  40415  fourierdlem112  40435  fouriersw  40448  sge0rpcpnf  40638  sge0ad2en  40648  ovnsubaddlem1  40784  ovnsubaddlem2  40785  ovolval5lem1  40866  ovolval5lem2  40867  iccpartiltu  41358  iccpartigtl  41359  iccpartlt  41360  iccpartleu  41364  iccpartrn  41366  iccelpart  41369  iccpartiun  41370  iccpartdisj  41373  pfxn0  41394  sqrtpwpw2p  41450  fmtnosqrt  41451  odz2prm2pw  41475  fmtnoprmfac1lem  41476  fmtnoprmfac1  41477  2pwp1prm  41503  lighneallem1  41522  lighneallem2  41523  lighneallem3  41524  lighneallem4a  41525  lighneallem4  41527  nnpw2evenALTV  41611  cznabel  41954  cznrng  41955  ztprmneprm  42125  altgsumbc  42130  altgsumbcALT  42131  pw2m1lepw2m1  42310  nneom  42321  logbpw2m1  42361  blennn  42369  blenpw2m1  42373  blengt1fldiv2p1  42387  dignn0ldlem  42396  dignnld  42397  dig2nn1st  42399  dignn0flhalflem1  42409  nn0sumshdiglemA  42413  nn0sumshdiglemB  42414