Theorem nnnn0d 9319

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

Syntax hints:   -> wi 4   e. wcel 2167   NNcn 9007   NN0cn0 9266

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-in 3163  df-ss 3170  df-n0 9267

This theorem is referenced by:  nn0ge2m1nn0  9327  nnzd  9464  eluzge2nn0  9660  modsumfzodifsn  10505  addmodlteq  10507  expnnval  10651  expgt1  10686  expaddzaplem  10691  expaddzap  10692  expmulzap  10694  expnbnd  10772  facwordi  10849  faclbnd  10850  facavg  10855  bcm1k  10869  bcval5  10872  1elfz0hash  10915  resqrexlemnm  11200  resqrexlemcvg  11201  summodc  11565  zsumdc  11566  bcxmas  11671  geo2sum  11696  geo2lim  11698  geoisum1  11701  geoisum1c  11702  cvgratnnlembern  11705  cvgratnnlemsumlt  11710  cvgratnnlemfm  11711  mertenslemi1  11717  prodmodclem3  11757  prodmodclem2a  11758  zproddc  11761  fprodseq  11765  eftabs  11838  efcllemp  11840  eftlub  11872  eirraplem  11959  dvdsfac  12042  divalglemnqt  12102  divalglemeunn  12103  bitsfzo  12137  bitsfi  12139  gcdval  12151  gcdcl  12158  dvdsgcdidd  12186  mulgcd  12208  rplpwr  12219  rppwr  12220  lcmcl  12265  lcmgcdnn  12275  nprmdvds1  12333  isprm5lem  12334  rpexp  12346  pw2dvdslemn  12358  sqpweven  12368  2sqpwodd  12369  nn0sqrtelqelz  12399  phiprmpw  12415  crth  12417  eulerthlema  12423  eulerthlemth  12425  eulerth  12426  fermltl  12427  odzcllem  12436  odzdvds  12439  odzphi  12440  modprm0  12448  prm23lt5  12457  pythagtriplem6  12464  pythagtriplem7  12465  pcprmpw2  12527  dvdsprmpweqle  12531  pcprod  12540  pcfac  12544  pcbc  12545  expnprm  12547  pockthlem  12550  pockthg  12551  prmunb  12556  mul4sqlem  12587  4sqlem11  12595  4sqlem13m  12597  4sqlem14  12598  4sqlem17  12601  4sqlem18  12602  2expltfac  12633  znf1o  14283  dvply1  15085  logbgcd1irraplemexp  15288  wilthlem1  15300  mpodvdsmulf1o  15310  mersenne  15317  perfect1  15318  perfectlem1  15319  perfectlem2  15320  perfect  15321  lgslem1  15325  lgsval  15329  lgsfvalg  15330  lgsval2lem  15335  lgsvalmod  15344  lgsmod  15351  lgsdirprm  15359  lgsne0  15363  gausslemma2dlem0b  15375  gausslemma2dlem0c  15376  gausslemma2dlem1  15386  gausslemma2dlem7  15393  gausslemma2d  15394  lgseisenlem1  15395  lgseisenlem2  15396  lgseisenlem3  15397  lgseisenlem4  15398  lgseisen  15399  lgsquadlem2  15403  lgsquadlem3  15404  m1lgs  15410  2lgslem1a  15413  2sqlem3  15442  cvgcmp2nlemabs  15763  trilpolemlt1  15772  redcwlpolemeq1  15785  nconstwlpolem0  15794