Theorem nnnn0d 9175

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

Syntax hints:   -> wi 4   e. wcel 2141   NNcn 8865   NN0cn0 9122

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-un 3125  df-in 3127  df-ss 3134  df-n0 9123

This theorem is referenced by:  nn0ge2m1nn0  9183  nnzd  9320  eluzge2nn0  9515  modsumfzodifsn  10339  addmodlteq  10341  expnnval  10466  expgt1  10501  expaddzaplem  10506  expaddzap  10507  expmulzap  10509  expnbnd  10586  facwordi  10661  faclbnd  10662  facavg  10667  bcm1k  10681  bcval5  10684  1elfz0hash  10728  resqrexlemnm  10969  resqrexlemcvg  10970  summodc  11333  zsumdc  11334  bcxmas  11439  geo2sum  11464  geo2lim  11466  geoisum1  11469  geoisum1c  11470  cvgratnnlembern  11473  cvgratnnlemsumlt  11478  cvgratnnlemfm  11479  mertenslemi1  11485  prodmodclem3  11525  prodmodclem2a  11526  zproddc  11529  fprodseq  11533  eftabs  11606  efcllemp  11608  eftlub  11640  eirraplem  11726  dvdsfac  11807  divalglemnqt  11866  divalglemeunn  11867  gcdval  11901  gcdcl  11908  dvdsgcdidd  11936  mulgcd  11958  rplpwr  11969  rppwr  11970  lcmcl  12013  lcmgcdnn  12023  nprmdvds1  12081  isprm5lem  12082  rpexp  12094  pw2dvdslemn  12106  sqpweven  12116  2sqpwodd  12117  nn0sqrtelqelz  12147  phiprmpw  12163  crth  12165  eulerthlema  12171  eulerthlemth  12173  eulerth  12174  fermltl  12175  odzcllem  12183  odzdvds  12186  odzphi  12187  modprm0  12195  prm23lt5  12204  pythagtriplem6  12211  pythagtriplem7  12212  pcprmpw2  12273  dvdsprmpweqle  12277  pcprod  12285  pcfac  12289  pcbc  12290  expnprm  12292  pockthlem  12295  pockthg  12296  prmunb  12301  mul4sqlem  12332  logbgcd1irraplemexp  13639  lgslem1  13654  lgsval  13658  lgsfvalg  13659  lgsval2lem  13664  lgsvalmod  13673  lgsmod  13680  lgsdirprm  13688  lgsne0  13692  2sqlem3  13706  cvgcmp2nlemabs  14024  trilpolemlt1  14033  redcwlpolemeq1  14046  nconstwlpolem0  14054