Theorem nnnn0d 9629

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 9577	. 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 9313   NN0cn0 9574

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 9575

This theorem is used by:  nn0ge2m1nn0  9637  nnzd  9777  eluzge2nn0  9985  modsumfzodifsn  10853  addmodlteq  10855  expnnval  10999  expgt1  11034  expaddzaplem  11039  expaddzap  11040  expmulzap  11042  expnbnd  11121  facwordi  11199  faclbnd  11200  facavg  11205  bcm1k  11219  bcval5  11222  bcm1n  11228  1elfz0hash  11268  pfxfvlsw  11488  wrdeqs1cat  11513  resqrexlemnm  11805  resqrexlemcvg  11806  summodc  12174  zsumdc  12175  bcxmas  12280  geo2sum  12305  geo2lim  12307  geoisum1  12310  geoisum1c  12311  cvgratnnlembern  12314  cvgratnnlemsumlt  12319  cvgratnnlemfm  12320  mertenslemi1  12326  prodmodclem3  12366  prodmodclem2a  12367  zproddc  12370  fprodseq  12374  eftabs  12447  efcllemp  12449  eftlub  12481  eirraplem  12568  dvdsfac  12651  divalglemnqt  12711  divalglemeunn  12712  bitsfzo  12746  bitsfi  12748  gcdval  12760  gcdcl  12767  dvdsgcdidd  12795  mulgcd  12817  rplpwr  12828  rppwr  12829  lcmcl  12874  lcmgcdnn  12884  nprmdvds1  12943  isprm5lem  12944  rpexp  12956  pwbdvdslemn  12968  pwbdvds  12969  nnmaxpw  12977  sqpweven  12979  2sqpwodd  12980  nn0sqrtelqelz  13010  phiprmpw  13028  crth  13030  eulerthlema  13036  eulerthlemth  13038  eulerth  13039  fermltl  13040  odzcllem  13049  odzdvds  13052  odzphi  13053  modprm0  13061  prm23lt5  13070  pythagtriplem6  13077  pythagtriplem7  13078  pcprmpw2  13140  dvdsprmpweqle  13144  pcprod  13153  pcfac  13157  pcbc  13158  expnprm  13160  pockthlem  13163  pockthg  13164  prmunb  13169  mul4sqlem  13200  4sqlem11  13208  4sqlem13m  13210  4sqlem14  13211  4sqlem17  13214  4sqlem18  13215  2expltfac  13247  znf1o  15094  dvply1  16008  efnthr  16193  logbgcd1irraplemexp  16221  pellexlem2  16247  wilthlem1  16249  mpodvdsmulf1o  16301  mersenne  16314  perfect1  16315  perfectlem1  16316  perfectlem2  16317  perfect  16318  pcbcctr  16320  bcmono  16321  bclbnd  16324  bposlem1  16328  bposlem3  16330  bposlem4  16331  bposlem5  16332  bposlem6  16333  lgslem1  16341  lgsval  16345  lgsfvalg  16346  lgsval2lem  16351  lgsvalmod  16360  lgsmod  16367  lgsdirprm  16375  lgsne0  16379  gausslemma2dlem0b  16391  gausslemma2dlem0c  16392  gausslemma2dlem1  16402  gausslemma2dlem7  16409  gausslemma2d  16410  lgseisenlem1  16411  lgseisenlem2  16412  lgseisenlem3  16413  lgseisenlem4  16414  lgseisen  16415  lgsquadlem2  16419  lgsquadlem3  16420  m1lgs  16426  2lgslem1a  16429  2sqlem3  16458  isclwwlkn  16876  clwwlknccat  16886  clwwlknon  16892  depindlem1  16969  cvgcmp2nlemabs  17304  trilpolemlt1  17314  redcwlpolemeq1  17328  nconstwlpolem0  17337