Theorem nnnn0d 9624

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   NNcn 9306   NN0cn0 9567

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-n0 9568

This theorem is used by:  nn0ge2m1nn0  9632  nnzd  9771  eluzge2nn0  9979  modsumfzodifsn  10846  addmodlteq  10848  expnnval  10992  expgt1  11027  expaddzaplem  11032  expaddzap  11033  expmulzap  11035  expnbnd  11114  facwordi  11192  faclbnd  11193  facavg  11198  bcm1k  11212  bcval5  11215  bcm1n  11221  1elfz0hash  11261  pfxfvlsw  11481  wrdeqs1cat  11506  resqrexlemnm  11798  resqrexlemcvg  11799  summodc  12166  zsumdc  12167  bcxmas  12272  geo2sum  12297  geo2lim  12299  geoisum1  12302  geoisum1c  12303  cvgratnnlembern  12306  cvgratnnlemsumlt  12311  cvgratnnlemfm  12312  mertenslemi1  12318  prodmodclem3  12358  prodmodclem2a  12359  zproddc  12362  fprodseq  12366  eftabs  12439  efcllemp  12441  eftlub  12473  eirraplem  12560  dvdsfac  12643  divalglemnqt  12703  divalglemeunn  12704  bitsfzo  12738  bitsfi  12740  gcdval  12752  gcdcl  12759  dvdsgcdidd  12787  mulgcd  12809  rplpwr  12820  rppwr  12821  lcmcl  12866  lcmgcdnn  12876  nprmdvds1  12935  isprm5lem  12936  rpexp  12948  pwbdvdslemn  12960  pwbdvds  12961  nnmaxpw  12969  sqpweven  12971  2sqpwodd  12972  nn0sqrtelqelz  13002  phiprmpw  13020  crth  13022  eulerthlema  13028  eulerthlemth  13030  eulerth  13031  fermltl  13032  odzcllem  13041  odzdvds  13044  odzphi  13045  modprm0  13053  prm23lt5  13062  pythagtriplem6  13069  pythagtriplem7  13070  pcprmpw2  13132  dvdsprmpweqle  13136  pcprod  13145  pcfac  13149  pcbc  13150  expnprm  13152  pockthlem  13155  pockthg  13156  prmunb  13161  mul4sqlem  13192  4sqlem11  13200  4sqlem13m  13202  4sqlem14  13203  4sqlem17  13206  4sqlem18  13207  2expltfac  13239  znf1o  15035  dvply1  15915  logbgcd1irraplemexp  16123  pellexlem2  16149  wilthlem1  16151  mpodvdsmulf1o  16185  mersenne  16195  perfect1  16196  perfectlem1  16197  perfectlem2  16198  perfect  16199  pcbcctr  16201  bcmono  16202  bclbnd  16205  bposlem1  16209  bposlem3  16211  bposlem4  16212  bposlem5  16213  lgslem1  16217  lgsval  16221  lgsfvalg  16222  lgsval2lem  16227  lgsvalmod  16236  lgsmod  16243  lgsdirprm  16251  lgsne0  16255  gausslemma2dlem0b  16267  gausslemma2dlem0c  16268  gausslemma2dlem1  16278  gausslemma2dlem7  16285  gausslemma2d  16286  lgseisenlem1  16287  lgseisenlem2  16288  lgseisenlem3  16289  lgseisenlem4  16290  lgseisen  16291  lgsquadlem2  16295  lgsquadlem3  16296  m1lgs  16302  2lgslem1a  16305  2sqlem3  16334  isclwwlkn  16752  clwwlknccat  16762  clwwlknon  16768  depindlem1  16845  cvgcmp2nlemabs  17179  trilpolemlt1  17188  redcwlpolemeq1  17202  nconstwlpolem0  17211