Theorem nnnn0d 9293

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

Syntax hints:   -> wi 4   e. wcel 2164   NNcn 8982   NN0cn0 9240

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 3157  df-in 3159  df-ss 3166  df-n0 9241

This theorem is referenced by:  nn0ge2m1nn0  9301  nnzd  9438  eluzge2nn0  9634  modsumfzodifsn  10467  addmodlteq  10469  expnnval  10613  expgt1  10648  expaddzaplem  10653  expaddzap  10654  expmulzap  10656  expnbnd  10734  facwordi  10811  faclbnd  10812  facavg  10817  bcm1k  10831  bcval5  10834  1elfz0hash  10877  resqrexlemnm  11162  resqrexlemcvg  11163  summodc  11526  zsumdc  11527  bcxmas  11632  geo2sum  11657  geo2lim  11659  geoisum1  11662  geoisum1c  11663  cvgratnnlembern  11666  cvgratnnlemsumlt  11671  cvgratnnlemfm  11672  mertenslemi1  11678  prodmodclem3  11718  prodmodclem2a  11719  zproddc  11722  fprodseq  11726  eftabs  11799  efcllemp  11801  eftlub  11833  eirraplem  11920  dvdsfac  12002  divalglemnqt  12061  divalglemeunn  12062  gcdval  12096  gcdcl  12103  dvdsgcdidd  12131  mulgcd  12153  rplpwr  12164  rppwr  12165  lcmcl  12210  lcmgcdnn  12220  nprmdvds1  12278  isprm5lem  12279  rpexp  12291  pw2dvdslemn  12303  sqpweven  12313  2sqpwodd  12314  nn0sqrtelqelz  12344  phiprmpw  12360  crth  12362  eulerthlema  12368  eulerthlemth  12370  eulerth  12371  fermltl  12372  odzcllem  12380  odzdvds  12383  odzphi  12384  modprm0  12392  prm23lt5  12401  pythagtriplem6  12408  pythagtriplem7  12409  pcprmpw2  12471  dvdsprmpweqle  12475  pcprod  12484  pcfac  12488  pcbc  12489  expnprm  12491  pockthlem  12494  pockthg  12495  prmunb  12500  mul4sqlem  12531  4sqlem11  12539  4sqlem13m  12541  4sqlem14  12542  4sqlem17  12545  4sqlem18  12546  znf1o  14139  logbgcd1irraplemexp  15100  wilthlem1  15112  lgslem1  15116  lgsval  15120  lgsfvalg  15121  lgsval2lem  15126  lgsvalmod  15135  lgsmod  15142  lgsdirprm  15150  lgsne0  15154  gausslemma2dlem0b  15166  gausslemma2dlem0c  15167  gausslemma2dlem1  15177  gausslemma2dlem7  15184  gausslemma2d  15185  lgseisenlem1  15186  lgseisenlem2  15187  lgseisenlem3  15188  lgseisenlem4  15189  lgseisen  15190  m1lgs  15192  2sqlem3  15204  cvgcmp2nlemabs  15522  trilpolemlt1  15531  redcwlpolemeq1  15544  nconstwlpolem0  15553