Theorem nnnn0d 9242

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

Syntax hints:   -> wi 4   e. wcel 2158   NNcn 8932   NN0cn0 9189

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 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-v 2751  df-un 3145  df-in 3147  df-ss 3154  df-n0 9190

This theorem is referenced by:  nn0ge2m1nn0  9250  nnzd  9387  eluzge2nn0  9582  modsumfzodifsn  10409  addmodlteq  10411  expnnval  10536  expgt1  10571  expaddzaplem  10576  expaddzap  10577  expmulzap  10579  expnbnd  10657  facwordi  10733  faclbnd  10734  facavg  10739  bcm1k  10753  bcval5  10756  1elfz0hash  10799  resqrexlemnm  11040  resqrexlemcvg  11041  summodc  11404  zsumdc  11405  bcxmas  11510  geo2sum  11535  geo2lim  11537  geoisum1  11540  geoisum1c  11541  cvgratnnlembern  11544  cvgratnnlemsumlt  11549  cvgratnnlemfm  11550  mertenslemi1  11556  prodmodclem3  11596  prodmodclem2a  11597  zproddc  11600  fprodseq  11604  eftabs  11677  efcllemp  11679  eftlub  11711  eirraplem  11797  dvdsfac  11879  divalglemnqt  11938  divalglemeunn  11939  gcdval  11973  gcdcl  11980  dvdsgcdidd  12008  mulgcd  12030  rplpwr  12041  rppwr  12042  lcmcl  12085  lcmgcdnn  12095  nprmdvds1  12153  isprm5lem  12154  rpexp  12166  pw2dvdslemn  12178  sqpweven  12188  2sqpwodd  12189  nn0sqrtelqelz  12219  phiprmpw  12235  crth  12237  eulerthlema  12243  eulerthlemth  12245  eulerth  12246  fermltl  12247  odzcllem  12255  odzdvds  12258  odzphi  12259  modprm0  12267  prm23lt5  12276  pythagtriplem6  12283  pythagtriplem7  12284  pcprmpw2  12345  dvdsprmpweqle  12349  pcprod  12357  pcfac  12361  pcbc  12362  expnprm  12364  pockthlem  12367  pockthg  12368  prmunb  12373  mul4sqlem  12404  logbgcd1irraplemexp  14657  lgslem1  14672  lgsval  14676  lgsfvalg  14677  lgsval2lem  14682  lgsvalmod  14691  lgsmod  14698  lgsdirprm  14706  lgsne0  14710  lgseisenlem1  14721  lgseisenlem2  14722  m1lgs  14723  2sqlem3  14735  cvgcmp2nlemabs  15052  trilpolemlt1  15061  redcwlpolemeq1  15074  nconstwlpolem0  15083