Theorem nnnn0d 9599

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

Syntax hints:   -> wi 4   e. wcel 2209   NNcn 9283   NN0cn0 9542

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 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 theorem 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 9543

This theorem is referenced by:  nn0ge2m1nn0  9607  nnzd  9746  eluzge2nn0  9949  modsumfzodifsn  10811  addmodlteq  10813  expnnval  10957  expgt1  10992  expaddzaplem  10997  expaddzap  10998  expmulzap  11000  expnbnd  11079  facwordi  11156  faclbnd  11157  facavg  11162  bcm1k  11176  bcval5  11179  bcm1n  11185  1elfz0hash  11225  pfxfvlsw  11445  wrdeqs1cat  11470  resqrexlemnm  11762  resqrexlemcvg  11763  summodc  12128  zsumdc  12129  bcxmas  12234  geo2sum  12259  geo2lim  12261  geoisum1  12264  geoisum1c  12265  cvgratnnlembern  12268  cvgratnnlemsumlt  12273  cvgratnnlemfm  12274  mertenslemi1  12280  prodmodclem3  12320  prodmodclem2a  12321  zproddc  12324  fprodseq  12328  eftabs  12401  efcllemp  12403  eftlub  12435  eirraplem  12522  dvdsfac  12605  divalglemnqt  12665  divalglemeunn  12666  bitsfzo  12700  bitsfi  12702  gcdval  12714  gcdcl  12721  dvdsgcdidd  12749  mulgcd  12771  rplpwr  12782  rppwr  12783  lcmcl  12828  lcmgcdnn  12838  nprmdvds1  12896  isprm5lem  12897  rpexp  12909  pw2dvdslemn  12921  sqpweven  12931  2sqpwodd  12932  nn0sqrtelqelz  12962  phiprmpw  12978  crth  12980  eulerthlema  12986  eulerthlemth  12988  eulerth  12989  fermltl  12990  odzcllem  12999  odzdvds  13002  odzphi  13003  modprm0  13011  prm23lt5  13020  pythagtriplem6  13027  pythagtriplem7  13028  pcprmpw2  13090  dvdsprmpweqle  13094  pcprod  13103  pcfac  13107  pcbc  13108  expnprm  13110  pockthlem  13113  pockthg  13114  prmunb  13119  mul4sqlem  13150  4sqlem11  13158  4sqlem13m  13160  4sqlem14  13161  4sqlem17  13164  4sqlem18  13165  2expltfac  13196  znf1o  14958  dvply1  15789  logbgcd1irraplemexp  15993  pellexlem2  16006  wilthlem1  16008  mpodvdsmulf1o  16018  mersenne  16025  perfect1  16026  perfectlem1  16027  perfectlem2  16028  perfect  16029  lgslem1  16033  lgsval  16037  lgsfvalg  16038  lgsval2lem  16043  lgsvalmod  16052  lgsmod  16059  lgsdirprm  16067  lgsne0  16071  gausslemma2dlem0b  16083  gausslemma2dlem0c  16084  gausslemma2dlem1  16094  gausslemma2dlem7  16101  gausslemma2d  16102  lgseisenlem1  16103  lgseisenlem2  16104  lgseisenlem3  16105  lgseisenlem4  16106  lgseisen  16107  lgsquadlem2  16111  lgsquadlem3  16112  m1lgs  16118  2lgslem1a  16121  2sqlem3  16150  isclwwlkn  16568  clwwlknccat  16578  clwwlknon  16584  depindlem1  16661  cvgcmp2nlemabs  16986  trilpolemlt1  16995  redcwlpolemeq1  17009  nconstwlpolem0  17018