Theorem nnnn0d 9455

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 9405	. 2 |- NN C_ NN0
2		nnnn0d.1	. 2 |- ( ph -> A e. NN )
3	1, 2	sselid 3225	1 |- ( ph -> A e. NN0 )

Syntax hints:   -> wi 4   e. wcel 2202   NNcn 9143   NN0cn0 9402

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-n0 9403

This theorem is referenced by:  nn0ge2m1nn0  9463  nnzd  9601  eluzge2nn0  9804  modsumfzodifsn  10658  addmodlteq  10660  expnnval  10804  expgt1  10839  expaddzaplem  10844  expaddzap  10845  expmulzap  10847  expnbnd  10925  facwordi  11002  faclbnd  11003  facavg  11008  bcm1k  11022  bcval5  11025  1elfz0hash  11070  pfxfvlsw  11276  wrdeqs1cat  11301  resqrexlemnm  11579  resqrexlemcvg  11580  summodc  11945  zsumdc  11946  bcxmas  12051  geo2sum  12076  geo2lim  12078  geoisum1  12081  geoisum1c  12082  cvgratnnlembern  12085  cvgratnnlemsumlt  12090  cvgratnnlemfm  12091  mertenslemi1  12097  prodmodclem3  12137  prodmodclem2a  12138  zproddc  12141  fprodseq  12145  eftabs  12218  efcllemp  12220  eftlub  12252  eirraplem  12339  dvdsfac  12422  divalglemnqt  12482  divalglemeunn  12483  bitsfzo  12517  bitsfi  12519  gcdval  12531  gcdcl  12538  dvdsgcdidd  12566  mulgcd  12588  rplpwr  12599  rppwr  12600  lcmcl  12645  lcmgcdnn  12655  nprmdvds1  12713  isprm5lem  12714  rpexp  12726  pw2dvdslemn  12738  sqpweven  12748  2sqpwodd  12749  nn0sqrtelqelz  12779  phiprmpw  12795  crth  12797  eulerthlema  12803  eulerthlemth  12805  eulerth  12806  fermltl  12807  odzcllem  12816  odzdvds  12819  odzphi  12820  modprm0  12828  prm23lt5  12837  pythagtriplem6  12844  pythagtriplem7  12845  pcprmpw2  12907  dvdsprmpweqle  12911  pcprod  12920  pcfac  12924  pcbc  12925  expnprm  12927  pockthlem  12930  pockthg  12931  prmunb  12936  mul4sqlem  12967  4sqlem11  12975  4sqlem13m  12977  4sqlem14  12978  4sqlem17  12981  4sqlem18  12982  2expltfac  13013  znf1o  14667  dvply1  15491  logbgcd1irraplemexp  15694  wilthlem1  15706  mpodvdsmulf1o  15716  mersenne  15723  perfect1  15724  perfectlem1  15725  perfectlem2  15726  perfect  15727  lgslem1  15731  lgsval  15735  lgsfvalg  15736  lgsval2lem  15741  lgsvalmod  15750  lgsmod  15757  lgsdirprm  15765  lgsne0  15769  gausslemma2dlem0b  15781  gausslemma2dlem0c  15782  gausslemma2dlem1  15792  gausslemma2dlem7  15799  gausslemma2d  15800  lgseisenlem1  15801  lgseisenlem2  15802  lgseisenlem3  15803  lgseisenlem4  15804  lgseisen  15805  lgsquadlem2  15809  lgsquadlem3  15810  m1lgs  15816  2lgslem1a  15819  2sqlem3  15848  isclwwlkn  16266  clwwlknccat  16276  clwwlknon  16282  cvgcmp2nlemabs  16639  trilpolemlt1  16648  redcwlpolemeq1  16661  nconstwlpolem0  16670