Theorem nnnn0d 9570

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

Syntax hints:   -> wi 4   e. wcel 2205   NNcn 9254   NN0cn0 9513

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 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3218  df-in 3220  df-ss 3227  df-n0 9514

This theorem is referenced by:  nn0ge2m1nn0  9578  nnzd  9717  eluzge2nn0  9920  modsumfzodifsn  10782  addmodlteq  10784  expnnval  10928  expgt1  10963  expaddzaplem  10968  expaddzap  10969  expmulzap  10971  expnbnd  11050  facwordi  11127  faclbnd  11128  facavg  11133  bcm1k  11147  bcval5  11150  bcm1n  11156  1elfz0hash  11196  pfxfvlsw  11412  wrdeqs1cat  11437  resqrexlemnm  11728  resqrexlemcvg  11729  summodc  12094  zsumdc  12095  bcxmas  12200  geo2sum  12225  geo2lim  12227  geoisum1  12230  geoisum1c  12231  cvgratnnlembern  12234  cvgratnnlemsumlt  12239  cvgratnnlemfm  12240  mertenslemi1  12246  prodmodclem3  12286  prodmodclem2a  12287  zproddc  12290  fprodseq  12294  eftabs  12367  efcllemp  12369  eftlub  12401  eirraplem  12488  dvdsfac  12571  divalglemnqt  12631  divalglemeunn  12632  bitsfzo  12666  bitsfi  12668  gcdval  12680  gcdcl  12687  dvdsgcdidd  12715  mulgcd  12737  rplpwr  12748  rppwr  12749  lcmcl  12794  lcmgcdnn  12804  nprmdvds1  12862  isprm5lem  12863  rpexp  12875  pw2dvdslemn  12887  sqpweven  12897  2sqpwodd  12898  nn0sqrtelqelz  12928  phiprmpw  12944  crth  12946  eulerthlema  12952  eulerthlemth  12954  eulerth  12955  fermltl  12956  odzcllem  12965  odzdvds  12968  odzphi  12969  modprm0  12977  prm23lt5  12986  pythagtriplem6  12993  pythagtriplem7  12994  pcprmpw2  13056  dvdsprmpweqle  13060  pcprod  13069  pcfac  13073  pcbc  13074  expnprm  13076  pockthlem  13079  pockthg  13080  prmunb  13085  mul4sqlem  13116  4sqlem11  13124  4sqlem13m  13126  4sqlem14  13127  4sqlem17  13130  4sqlem18  13131  2expltfac  13162  znf1o  14925  dvply1  15756  logbgcd1irraplemexp  15959  pellexlem2  15972  wilthlem1  15974  mpodvdsmulf1o  15984  mersenne  15991  perfect1  15992  perfectlem1  15993  perfectlem2  15994  perfect  15995  lgslem1  15999  lgsval  16003  lgsfvalg  16004  lgsval2lem  16009  lgsvalmod  16018  lgsmod  16025  lgsdirprm  16033  lgsne0  16037  gausslemma2dlem0b  16049  gausslemma2dlem0c  16050  gausslemma2dlem1  16060  gausslemma2dlem7  16067  gausslemma2d  16068  lgseisenlem1  16069  lgseisenlem2  16070  lgseisenlem3  16071  lgseisenlem4  16072  lgseisen  16073  lgsquadlem2  16077  lgsquadlem3  16078  m1lgs  16084  2lgslem1a  16087  2sqlem3  16116  isclwwlkn  16534  clwwlknccat  16544  clwwlknon  16550  depindlem1  16627  cvgcmp2nlemabs  16942  trilpolemlt1  16951  redcwlpolemeq1  16965  nconstwlpolem0  16975