Theorem nnnn0d 9350

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

Syntax hints:   -> wi 4   e. wcel 2176   NNcn 9038   NN0cn0 9297

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-un 3170  df-in 3172  df-ss 3179  df-n0 9298

This theorem is referenced by:  nn0ge2m1nn0  9358  nnzd  9496  eluzge2nn0  9692  modsumfzodifsn  10543  addmodlteq  10545  expnnval  10689  expgt1  10724  expaddzaplem  10729  expaddzap  10730  expmulzap  10732  expnbnd  10810  facwordi  10887  faclbnd  10888  facavg  10893  bcm1k  10907  bcval5  10910  1elfz0hash  10953  pfxfvlsw  11149  resqrexlemnm  11362  resqrexlemcvg  11363  summodc  11727  zsumdc  11728  bcxmas  11833  geo2sum  11858  geo2lim  11860  geoisum1  11863  geoisum1c  11864  cvgratnnlembern  11867  cvgratnnlemsumlt  11872  cvgratnnlemfm  11873  mertenslemi1  11879  prodmodclem3  11919  prodmodclem2a  11920  zproddc  11923  fprodseq  11927  eftabs  12000  efcllemp  12002  eftlub  12034  eirraplem  12121  dvdsfac  12204  divalglemnqt  12264  divalglemeunn  12265  bitsfzo  12299  bitsfi  12301  gcdval  12313  gcdcl  12320  dvdsgcdidd  12348  mulgcd  12370  rplpwr  12381  rppwr  12382  lcmcl  12427  lcmgcdnn  12437  nprmdvds1  12495  isprm5lem  12496  rpexp  12508  pw2dvdslemn  12520  sqpweven  12530  2sqpwodd  12531  nn0sqrtelqelz  12561  phiprmpw  12577  crth  12579  eulerthlema  12585  eulerthlemth  12587  eulerth  12588  fermltl  12589  odzcllem  12598  odzdvds  12601  odzphi  12602  modprm0  12610  prm23lt5  12619  pythagtriplem6  12626  pythagtriplem7  12627  pcprmpw2  12689  dvdsprmpweqle  12693  pcprod  12702  pcfac  12706  pcbc  12707  expnprm  12709  pockthlem  12712  pockthg  12713  prmunb  12718  mul4sqlem  12749  4sqlem11  12757  4sqlem13m  12759  4sqlem14  12760  4sqlem17  12763  4sqlem18  12764  2expltfac  12795  znf1o  14446  dvply1  15270  logbgcd1irraplemexp  15473  wilthlem1  15485  mpodvdsmulf1o  15495  mersenne  15502  perfect1  15503  perfectlem1  15504  perfectlem2  15505  perfect  15506  lgslem1  15510  lgsval  15514  lgsfvalg  15515  lgsval2lem  15520  lgsvalmod  15529  lgsmod  15536  lgsdirprm  15544  lgsne0  15548  gausslemma2dlem0b  15560  gausslemma2dlem0c  15561  gausslemma2dlem1  15571  gausslemma2dlem7  15578  gausslemma2d  15579  lgseisenlem1  15580  lgseisenlem2  15581  lgseisenlem3  15582  lgseisenlem4  15583  lgseisen  15584  lgsquadlem2  15588  lgsquadlem3  15589  m1lgs  15595  2lgslem1a  15598  2sqlem3  15627  cvgcmp2nlemabs  16008  trilpolemlt1  16017  redcwlpolemeq1  16030  nconstwlpolem0  16039