Theorem nnnn0d 9516

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

Syntax hints:   -> wi 4   e. wcel 2202   NNcn 9202   NN0cn0 9461

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-un 3205  df-in 3207  df-ss 3214  df-n0 9462

This theorem is referenced by:  nn0ge2m1nn0  9524  nnzd  9662  eluzge2nn0  9865  modsumfzodifsn  10721  addmodlteq  10723  expnnval  10867  expgt1  10902  expaddzaplem  10907  expaddzap  10908  expmulzap  10910  expnbnd  10988  facwordi  11065  faclbnd  11066  facavg  11071  bcm1k  11085  bcval5  11088  1elfz0hash  11133  pfxfvlsw  11342  wrdeqs1cat  11367  resqrexlemnm  11658  resqrexlemcvg  11659  summodc  12024  zsumdc  12025  bcxmas  12130  geo2sum  12155  geo2lim  12157  geoisum1  12160  geoisum1c  12161  cvgratnnlembern  12164  cvgratnnlemsumlt  12169  cvgratnnlemfm  12170  mertenslemi1  12176  prodmodclem3  12216  prodmodclem2a  12217  zproddc  12220  fprodseq  12224  eftabs  12297  efcllemp  12299  eftlub  12331  eirraplem  12418  dvdsfac  12501  divalglemnqt  12561  divalglemeunn  12562  bitsfzo  12596  bitsfi  12598  gcdval  12610  gcdcl  12617  dvdsgcdidd  12645  mulgcd  12667  rplpwr  12678  rppwr  12679  lcmcl  12724  lcmgcdnn  12734  nprmdvds1  12792  isprm5lem  12793  rpexp  12805  pw2dvdslemn  12817  sqpweven  12827  2sqpwodd  12828  nn0sqrtelqelz  12858  phiprmpw  12874  crth  12876  eulerthlema  12882  eulerthlemth  12884  eulerth  12885  fermltl  12886  odzcllem  12895  odzdvds  12898  odzphi  12899  modprm0  12907  prm23lt5  12916  pythagtriplem6  12923  pythagtriplem7  12924  pcprmpw2  12986  dvdsprmpweqle  12990  pcprod  12999  pcfac  13003  pcbc  13004  expnprm  13006  pockthlem  13009  pockthg  13010  prmunb  13015  mul4sqlem  13046  4sqlem11  13054  4sqlem13m  13056  4sqlem14  13057  4sqlem17  13060  4sqlem18  13061  2expltfac  13092  znf1o  14747  dvply1  15576  logbgcd1irraplemexp  15779  pellexlem2  15792  wilthlem1  15794  mpodvdsmulf1o  15804  mersenne  15811  perfect1  15812  perfectlem1  15813  perfectlem2  15814  perfect  15815  lgslem1  15819  lgsval  15823  lgsfvalg  15824  lgsval2lem  15829  lgsvalmod  15838  lgsmod  15845  lgsdirprm  15853  lgsne0  15857  gausslemma2dlem0b  15869  gausslemma2dlem0c  15870  gausslemma2dlem1  15880  gausslemma2dlem7  15887  gausslemma2d  15888  lgseisenlem1  15889  lgseisenlem2  15890  lgseisenlem3  15891  lgseisenlem4  15892  lgseisen  15893  lgsquadlem2  15897  lgsquadlem3  15898  m1lgs  15904  2lgslem1a  15907  2sqlem3  15936  isclwwlkn  16354  clwwlknccat  16364  clwwlknon  16370  depindlem1  16447  cvgcmp2nlemabs  16764  trilpolemlt1  16773  redcwlpolemeq1  16787  nconstwlpolem0  16796