Theorem nnnn0d 9229

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

Syntax hints:   -> wi 4   e. wcel 2148   NNcn 8919   NN0cn0 9176

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2740  df-un 3134  df-in 3136  df-ss 3143  df-n0 9177

This theorem is referenced by:  nn0ge2m1nn0  9237  nnzd  9374  eluzge2nn0  9569  modsumfzodifsn  10396  addmodlteq  10398  expnnval  10523  expgt1  10558  expaddzaplem  10563  expaddzap  10564  expmulzap  10566  expnbnd  10644  facwordi  10720  faclbnd  10721  facavg  10726  bcm1k  10740  bcval5  10743  1elfz0hash  10786  resqrexlemnm  11027  resqrexlemcvg  11028  summodc  11391  zsumdc  11392  bcxmas  11497  geo2sum  11522  geo2lim  11524  geoisum1  11527  geoisum1c  11528  cvgratnnlembern  11531  cvgratnnlemsumlt  11536  cvgratnnlemfm  11537  mertenslemi1  11543  prodmodclem3  11583  prodmodclem2a  11584  zproddc  11587  fprodseq  11591  eftabs  11664  efcllemp  11666  eftlub  11698  eirraplem  11784  dvdsfac  11866  divalglemnqt  11925  divalglemeunn  11926  gcdval  11960  gcdcl  11967  dvdsgcdidd  11995  mulgcd  12017  rplpwr  12028  rppwr  12029  lcmcl  12072  lcmgcdnn  12082  nprmdvds1  12140  isprm5lem  12141  rpexp  12153  pw2dvdslemn  12165  sqpweven  12175  2sqpwodd  12176  nn0sqrtelqelz  12206  phiprmpw  12222  crth  12224  eulerthlema  12230  eulerthlemth  12232  eulerth  12233  fermltl  12234  odzcllem  12242  odzdvds  12245  odzphi  12246  modprm0  12254  prm23lt5  12263  pythagtriplem6  12270  pythagtriplem7  12271  pcprmpw2  12332  dvdsprmpweqle  12336  pcprod  12344  pcfac  12348  pcbc  12349  expnprm  12351  pockthlem  12354  pockthg  12355  prmunb  12360  mul4sqlem  12391  logbgcd1irraplemexp  14389  lgslem1  14404  lgsval  14408  lgsfvalg  14409  lgsval2lem  14414  lgsvalmod  14423  lgsmod  14430  lgsdirprm  14438  lgsne0  14442  lgseisenlem1  14453  lgseisenlem2  14454  m1lgs  14455  2sqlem3  14467  cvgcmp2nlemabs  14783  trilpolemlt1  14792  redcwlpolemeq1  14805  nconstwlpolem0  14813