Theorem nnnn0d 9296

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

Syntax hints:   -> wi 4   e. wcel 2164   NNcn 8984   NN0cn0 9243

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3158  df-in 3160  df-ss 3167  df-n0 9244

This theorem is referenced by:  nn0ge2m1nn0  9304  nnzd  9441  eluzge2nn0  9637  modsumfzodifsn  10470  addmodlteq  10472  expnnval  10616  expgt1  10651  expaddzaplem  10656  expaddzap  10657  expmulzap  10659  expnbnd  10737  facwordi  10814  faclbnd  10815  facavg  10820  bcm1k  10834  bcval5  10837  1elfz0hash  10880  resqrexlemnm  11165  resqrexlemcvg  11166  summodc  11529  zsumdc  11530  bcxmas  11635  geo2sum  11660  geo2lim  11662  geoisum1  11665  geoisum1c  11666  cvgratnnlembern  11669  cvgratnnlemsumlt  11674  cvgratnnlemfm  11675  mertenslemi1  11681  prodmodclem3  11721  prodmodclem2a  11722  zproddc  11725  fprodseq  11729  eftabs  11802  efcllemp  11804  eftlub  11836  eirraplem  11923  dvdsfac  12005  divalglemnqt  12064  divalglemeunn  12065  gcdval  12099  gcdcl  12106  dvdsgcdidd  12134  mulgcd  12156  rplpwr  12167  rppwr  12168  lcmcl  12213  lcmgcdnn  12223  nprmdvds1  12281  isprm5lem  12282  rpexp  12294  pw2dvdslemn  12306  sqpweven  12316  2sqpwodd  12317  nn0sqrtelqelz  12347  phiprmpw  12363  crth  12365  eulerthlema  12371  eulerthlemth  12373  eulerth  12374  fermltl  12375  odzcllem  12383  odzdvds  12386  odzphi  12387  modprm0  12395  prm23lt5  12404  pythagtriplem6  12411  pythagtriplem7  12412  pcprmpw2  12474  dvdsprmpweqle  12478  pcprod  12487  pcfac  12491  pcbc  12492  expnprm  12494  pockthlem  12497  pockthg  12498  prmunb  12503  mul4sqlem  12534  4sqlem11  12542  4sqlem13m  12544  4sqlem14  12545  4sqlem17  12548  4sqlem18  12549  znf1o  14150  dvply1  14943  logbgcd1irraplemexp  15141  wilthlem1  15153  lgslem1  15157  lgsval  15161  lgsfvalg  15162  lgsval2lem  15167  lgsvalmod  15176  lgsmod  15183  lgsdirprm  15191  lgsne0  15195  gausslemma2dlem0b  15207  gausslemma2dlem0c  15208  gausslemma2dlem1  15218  gausslemma2dlem7  15225  gausslemma2d  15226  lgseisenlem1  15227  lgseisenlem2  15228  lgseisenlem3  15229  lgseisenlem4  15230  lgseisen  15231  lgsquadlem2  15235  lgsquadlem3  15236  m1lgs  15242  2lgslem1a  15245  2sqlem3  15274  cvgcmp2nlemabs  15592  trilpolemlt1  15601  redcwlpolemeq1  15614  nconstwlpolem0  15623