Theorem nnnn0d 9224

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

Syntax hints:   -> wi 4   e. wcel 2148   NNcn 8914   NN0cn0 9171

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 2739  df-un 3133  df-in 3135  df-ss 3142  df-n0 9172

This theorem is referenced by:  nn0ge2m1nn0  9232  nnzd  9369  eluzge2nn0  9564  modsumfzodifsn  10390  addmodlteq  10392  expnnval  10517  expgt1  10552  expaddzaplem  10557  expaddzap  10558  expmulzap  10560  expnbnd  10637  facwordi  10712  faclbnd  10713  facavg  10718  bcm1k  10732  bcval5  10735  1elfz0hash  10778  resqrexlemnm  11019  resqrexlemcvg  11020  summodc  11383  zsumdc  11384  bcxmas  11489  geo2sum  11514  geo2lim  11516  geoisum1  11519  geoisum1c  11520  cvgratnnlembern  11523  cvgratnnlemsumlt  11528  cvgratnnlemfm  11529  mertenslemi1  11535  prodmodclem3  11575  prodmodclem2a  11576  zproddc  11579  fprodseq  11583  eftabs  11656  efcllemp  11658  eftlub  11690  eirraplem  11776  dvdsfac  11857  divalglemnqt  11916  divalglemeunn  11917  gcdval  11951  gcdcl  11958  dvdsgcdidd  11986  mulgcd  12008  rplpwr  12019  rppwr  12020  lcmcl  12063  lcmgcdnn  12073  nprmdvds1  12131  isprm5lem  12132  rpexp  12144  pw2dvdslemn  12156  sqpweven  12166  2sqpwodd  12167  nn0sqrtelqelz  12197  phiprmpw  12213  crth  12215  eulerthlema  12221  eulerthlemth  12223  eulerth  12224  fermltl  12225  odzcllem  12233  odzdvds  12236  odzphi  12237  modprm0  12245  prm23lt5  12254  pythagtriplem6  12261  pythagtriplem7  12262  pcprmpw2  12323  dvdsprmpweqle  12327  pcprod  12335  pcfac  12339  pcbc  12340  expnprm  12342  pockthlem  12345  pockthg  12346  prmunb  12351  mul4sqlem  12382  logbgcd1irraplemexp  14248  lgslem1  14263  lgsval  14267  lgsfvalg  14268  lgsval2lem  14273  lgsvalmod  14282  lgsmod  14289  lgsdirprm  14297  lgsne0  14301  2sqlem3  14315  cvgcmp2nlemabs  14631  trilpolemlt1  14640  redcwlpolemeq1  14653  nconstwlpolem0  14661