Theorem nnnn0d 9348

Description: A positive integer is a nonnegative integer. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
nnnn0d.1	|- ( ph -> A e. NN )

Assertion

Ref	Expression
nnnn0d	|- ( ph -> A e. NN0 )

Proof of Theorem nnnn0d

Step	Hyp	Ref	Expression
1		nnssnn0 9298	. 2 |- NN C_ NN0
2		nnnn0d.1	. 2 |- ( ph -> A e. NN )
3	1, 2	sselid 3191	1 |- ( ph -> A e. NN0 )

Syntax hints:   -> wi 4   e. wcel 2176   NNcn 9036   NN0cn0 9295

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-un 3170  df-in 3172  df-ss 3179  df-n0 9296

This theorem is referenced by:  nn0ge2m1nn0  9356  nnzd  9494  eluzge2nn0  9690  modsumfzodifsn  10541  addmodlteq  10543  expnnval  10687  expgt1  10722  expaddzaplem  10727  expaddzap  10728  expmulzap  10730  expnbnd  10808  facwordi  10885  faclbnd  10886  facavg  10891  bcm1k  10905  bcval5  10908  1elfz0hash  10951  resqrexlemnm  11329  resqrexlemcvg  11330  summodc  11694  zsumdc  11695  bcxmas  11800  geo2sum  11825  geo2lim  11827  geoisum1  11830  geoisum1c  11831  cvgratnnlembern  11834  cvgratnnlemsumlt  11839  cvgratnnlemfm  11840  mertenslemi1  11846  prodmodclem3  11886  prodmodclem2a  11887  zproddc  11890  fprodseq  11894  eftabs  11967  efcllemp  11969  eftlub  12001  eirraplem  12088  dvdsfac  12171  divalglemnqt  12231  divalglemeunn  12232  bitsfzo  12266  bitsfi  12268  gcdval  12280  gcdcl  12287  dvdsgcdidd  12315  mulgcd  12337  rplpwr  12348  rppwr  12349  lcmcl  12394  lcmgcdnn  12404  nprmdvds1  12462  isprm5lem  12463  rpexp  12475  pw2dvdslemn  12487  sqpweven  12497  2sqpwodd  12498  nn0sqrtelqelz  12528  phiprmpw  12544  crth  12546  eulerthlema  12552  eulerthlemth  12554  eulerth  12555  fermltl  12556  odzcllem  12565  odzdvds  12568  odzphi  12569  modprm0  12577  prm23lt5  12586  pythagtriplem6  12593  pythagtriplem7  12594  pcprmpw2  12656  dvdsprmpweqle  12660  pcprod  12669  pcfac  12673  pcbc  12674  expnprm  12676  pockthlem  12679  pockthg  12680  prmunb  12685  mul4sqlem  12716  4sqlem11  12724  4sqlem13m  12726  4sqlem14  12727  4sqlem17  12730  4sqlem18  12731  2expltfac  12762  znf1o  14413  dvply1  15237  logbgcd1irraplemexp  15440  wilthlem1  15452  mpodvdsmulf1o  15462  mersenne  15469  perfect1  15470  perfectlem1  15471  perfectlem2  15472  perfect  15473  lgslem1  15477  lgsval  15481  lgsfvalg  15482  lgsval2lem  15487  lgsvalmod  15496  lgsmod  15503  lgsdirprm  15511  lgsne0  15515  gausslemma2dlem0b  15527  gausslemma2dlem0c  15528  gausslemma2dlem1  15538  gausslemma2dlem7  15545  gausslemma2d  15546  lgseisenlem1  15547  lgseisenlem2  15548  lgseisenlem3  15549  lgseisenlem4  15550  lgseisen  15551  lgsquadlem2  15555  lgsquadlem3  15556  m1lgs  15562  2lgslem1a  15565  2sqlem3  15594  cvgcmp2nlemabs  15971  trilpolemlt1  15980  redcwlpolemeq1  15993  nconstwlpolem0  16002