Theorem nnnn0d 9167

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

Syntax hints:   -> wi 4   e. wcel 2136   NNcn 8857   NN0cn0 9114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-v 2728  df-un 3120  df-in 3122  df-ss 3129  df-n0 9115

This theorem is referenced by:  nn0ge2m1nn0  9175  nnzd  9312  eluzge2nn0  9507  modsumfzodifsn  10331  addmodlteq  10333  expnnval  10458  expgt1  10493  expaddzaplem  10498  expaddzap  10499  expmulzap  10501  expnbnd  10578  facwordi  10653  faclbnd  10654  facavg  10659  bcm1k  10673  bcval5  10676  1elfz0hash  10719  resqrexlemnm  10960  resqrexlemcvg  10961  summodc  11324  zsumdc  11325  bcxmas  11430  geo2sum  11455  geo2lim  11457  geoisum1  11460  geoisum1c  11461  cvgratnnlembern  11464  cvgratnnlemsumlt  11469  cvgratnnlemfm  11470  mertenslemi1  11476  prodmodclem3  11516  prodmodclem2a  11517  zproddc  11520  fprodseq  11524  eftabs  11597  efcllemp  11599  eftlub  11631  eirraplem  11717  dvdsfac  11798  divalglemnqt  11857  divalglemeunn  11858  gcdval  11892  gcdcl  11899  dvdsgcdidd  11927  mulgcd  11949  rplpwr  11960  rppwr  11961  lcmcl  12004  lcmgcdnn  12014  nprmdvds1  12072  isprm5lem  12073  rpexp  12085  pw2dvdslemn  12097  sqpweven  12107  2sqpwodd  12108  nn0sqrtelqelz  12138  phiprmpw  12154  crth  12156  eulerthlema  12162  eulerthlemth  12164  eulerth  12165  fermltl  12166  odzcllem  12174  odzdvds  12177  odzphi  12178  modprm0  12186  prm23lt5  12195  pythagtriplem6  12202  pythagtriplem7  12203  pcprmpw2  12264  dvdsprmpweqle  12268  pcprod  12276  pcfac  12280  pcbc  12281  expnprm  12283  pockthlem  12286  pockthg  12287  prmunb  12292  mul4sqlem  12323  logbgcd1irraplemexp  13526  lgslem1  13541  lgsval  13545  lgsfvalg  13546  lgsval2lem  13551  lgsvalmod  13560  lgsmod  13567  lgsdirprm  13575  lgsne0  13579  2sqlem3  13593  cvgcmp2nlemabs  13911  trilpolemlt1  13920  redcwlpolemeq1  13933  nconstwlpolem0  13941