Theorem nnnn0d 9433

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

Syntax hints:   -> wi 4   e. wcel 2200   NNcn 9121   NN0cn0 9380

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-n0 9381

This theorem is referenced by:  nn0ge2m1nn0  9441  nnzd  9579  eluzge2nn0  9776  modsumfzodifsn  10630  addmodlteq  10632  expnnval  10776  expgt1  10811  expaddzaplem  10816  expaddzap  10817  expmulzap  10819  expnbnd  10897  facwordi  10974  faclbnd  10975  facavg  10980  bcm1k  10994  bcval5  10997  1elfz0hash  11041  pfxfvlsw  11243  wrdeqs1cat  11268  resqrexlemnm  11545  resqrexlemcvg  11546  summodc  11910  zsumdc  11911  bcxmas  12016  geo2sum  12041  geo2lim  12043  geoisum1  12046  geoisum1c  12047  cvgratnnlembern  12050  cvgratnnlemsumlt  12055  cvgratnnlemfm  12056  mertenslemi1  12062  prodmodclem3  12102  prodmodclem2a  12103  zproddc  12106  fprodseq  12110  eftabs  12183  efcllemp  12185  eftlub  12217  eirraplem  12304  dvdsfac  12387  divalglemnqt  12447  divalglemeunn  12448  bitsfzo  12482  bitsfi  12484  gcdval  12496  gcdcl  12503  dvdsgcdidd  12531  mulgcd  12553  rplpwr  12564  rppwr  12565  lcmcl  12610  lcmgcdnn  12620  nprmdvds1  12678  isprm5lem  12679  rpexp  12691  pw2dvdslemn  12703  sqpweven  12713  2sqpwodd  12714  nn0sqrtelqelz  12744  phiprmpw  12760  crth  12762  eulerthlema  12768  eulerthlemth  12770  eulerth  12771  fermltl  12772  odzcllem  12781  odzdvds  12784  odzphi  12785  modprm0  12793  prm23lt5  12802  pythagtriplem6  12809  pythagtriplem7  12810  pcprmpw2  12872  dvdsprmpweqle  12876  pcprod  12885  pcfac  12889  pcbc  12890  expnprm  12892  pockthlem  12895  pockthg  12896  prmunb  12901  mul4sqlem  12932  4sqlem11  12940  4sqlem13m  12942  4sqlem14  12943  4sqlem17  12946  4sqlem18  12947  2expltfac  12978  znf1o  14631  dvply1  15455  logbgcd1irraplemexp  15658  wilthlem1  15670  mpodvdsmulf1o  15680  mersenne  15687  perfect1  15688  perfectlem1  15689  perfectlem2  15690  perfect  15691  lgslem1  15695  lgsval  15699  lgsfvalg  15700  lgsval2lem  15705  lgsvalmod  15714  lgsmod  15721  lgsdirprm  15729  lgsne0  15733  gausslemma2dlem0b  15745  gausslemma2dlem0c  15746  gausslemma2dlem1  15756  gausslemma2dlem7  15763  gausslemma2d  15764  lgseisenlem1  15765  lgseisenlem2  15766  lgseisenlem3  15767  lgseisenlem4  15768  lgseisen  15769  lgsquadlem2  15773  lgsquadlem3  15774  m1lgs  15780  2lgslem1a  15783  2sqlem3  15812  clwwlknccat  16165  cvgcmp2nlemabs  16488  trilpolemlt1  16497  redcwlpolemeq1  16510  nconstwlpolem0  16519