Theorem nnnn0d 11949

Description: A positive integer is a nonnegative integer. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
nnnn0d.1	⊢ (𝜑 → 𝐴 ∈ ℕ)

Assertion

Ref	Expression
nnnn0d	⊢ (𝜑 → 𝐴 ∈ ℕ0)

Proof of Theorem nnnn0d

Step	Hyp	Ref	Expression
1		nnssnn0 11894	. 2 ⊢ ℕ ⊆ ℕ0
2		nnnn0d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
3	1, 2	sseldi 3965	1 ⊢ (𝜑 → 𝐴 ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2110  ℕcn 11632  ℕ₀cn0 11891

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3497  df-un 3941  df-in 3943  df-ss 3952  df-n0 11892

This theorem is referenced by:  nn0ge2m1nn0  11959  nnzd  12080  eluzge2nn0  12281  expgt1  13461  expaddzlem  13466  expaddz  13467  expmulz  13469  expmulnbnd  13590  facwordi  13643  faclbnd  13644  facavg  13655  bcm1k  13669  wrdeqs1cat  14076  cshwcsh2id  14184  relexpsucnnr  14378  isercolllem2  15016  bcxmas  15184  climcndslem1  15198  climcndslem2  15199  climcnds  15200  pwdif  15217  geo2sum  15223  mertenslem1  15234  prodmolem3  15281  prodmolem2a  15282  bpolydiflem  15402  eftabs  15423  efcllem  15425  eftlub  15456  eirrlem  15551  rpnnen2lem9  15569  rpnnen2lem11  15571  dvdsfac  15670  pwp1fsum  15736  oddpwp1fsum  15737  bitsfzo  15778  bitsfi  15780  sadcaddlem  15800  smumullem  15835  gcdcl  15849  dvdsgcdidd  15879  mulgcd  15890  rplpwr  15901  rppwr  15902  lcmcl  15939  lcmgcdnn  15949  lcmfcl  15966  nprmdvds1  16044  rpexp  16058  zsqrtelqelz  16092  phiprmpw  16107  eulerthlem2  16113  eulerth  16114  fermltl  16115  odzcllem  16123  odzdvds  16126  odzphi  16127  prm23lt5  16145  pythagtriplem6  16152  pythagtriplem7  16153  pcprmpw2  16212  dvdsprmpweqle  16216  pcprod  16225  pcfac  16229  pcbc  16230  expnprm  16232  pockthlem  16235  pockthg  16236  prmunb  16244  prmreclem2  16247  prmreclem3  16248  prmreclem4  16249  prmreclem5  16250  prmreclem6  16251  mul4sqlem  16283  4sqlem11  16285  4sqlem17  16291  vdwlem1  16311  vdwlem5  16315  vdwlem6  16316  vdwlem8  16318  vdwlem9  16319  vdwlem11  16321  vdwlem12  16322  vdwnnlem3  16327  ramz2  16354  ramub1lem1  16356  ramub1lem2  16357  ramub1  16358  prmgaplem3  16383  2expltfac  16420  psgnunilem3  18618  odfval  18654  mndodconglem  18663  gexcl3  18706  pgpfi1  18714  sylow1lem1  18717  gexexlem  18966  prmcyg  19008  gsumval3  19021  ablfacrplem  19181  ablfacrp  19182  ablfacrp2  19183  ablfac1eu  19189  prmgrpsimpgd  19230  srgbinomlem3  19286  srgbinomlem4  19287  chfacfscmulgsum  21462  chfacfpmmulgsum  21466  cpmadugsumlemF  21478  ovoliunlem1  24097  mbfi1fseqlem1  24310  mbfi1fseqlem3  24312  mbfi1fseqlem5  24314  itg2cnlem2  24357  dvply1  24867  aalioulem2  24916  aalioulem5  24919  aaliou3lem1  24925  aaliou3lem2  24926  aaliou3lem8  24928  aaliou3lem6  24931  taylthlem1  24955  taylthlem2  24956  pserdvlem2  25010  cxpeq  25332  dmgmdivn0  25599  lgamgulmlem5  25604  lgamcvg2  25626  wilthlem1  25639  ftalem1  25644  ftalem2  25645  ftalem4  25647  ftalem5  25648  basellem2  25653  basellem3  25654  basellem4  25655  basellem5  25656  isppw2  25686  dvdsmulf1o  25765  sgmmul  25771  fsumvma2  25784  chpchtsum  25789  logfacubnd  25791  mersenne  25797  perfect1  25798  perfectlem1  25799  perfectlem2  25800  perfect  25801  dchrelbas3  25808  dchrelbasd  25809  dchrzrh1  25814  dchrzrhmul  25816  dchrmulcl  25819  dchrn0  25820  dchrfi  25825  dchrghm  25826  dchrabs  25830  dchrinv  25831  dchrptlem1  25834  dchrptlem2  25835  dchrptlem3  25836  dchrpt  25837  dchrsum2  25838  sum2dchr  25844  pcbcctr  25846  bcmono  25847  bclbnd  25850  bposlem1  25854  bposlem3  25856  bposlem5  25858  bposlem6  25859  lgslem1  25867  lgsval2lem  25877  lgsvalmod  25886  lgsmod  25893  lgsdirprm  25901  lgsne0  25905  lgsqrlem1  25916  lgsqrlem2  25917  lgsqrlem3  25918  lgsqrlem4  25919  gausslemma2dlem0b  25927  gausslemma2dlem0c  25928  gausslemma2dlem1  25936  gausslemma2dlem7  25943  gausslemma2d  25944  lgseisenlem1  25945  lgseisenlem2  25946  lgseisenlem3  25947  lgseisenlem4  25948  lgseisen  25949  lgsquadlem2  25951  lgsquadlem3  25952  m1lgs  25958  2lgslem1a  25961  2sqlem3  25990  2sqblem  26001  chebbnd1lem1  26039  chebbnd1lem3  26041  rplogsumlem2  26055  rpvmasumlem  26057  dchrisumlem1  26059  dchrisumlem2  26060  dchrmusum2  26064  dchrvmasumlem3  26069  dchrisum0ff  26077  dchrisum0flblem1  26078  rpvmasum2  26082  dchrisum0re  26083  dchrisum0lem2a  26087  dirith  26099  mudivsum  26100  pntpbnd1a  26155  pntlemq  26171  pntlemr  26172  pntlemj  26173  ostth2lem1  26188  ostth2lem2  26204  ostth2lem3  26205  ostth2  26207  crctcshwlkn0lem6  27587  hashecclwwlkn1  27850  umgrhashecclwwlk  27851  clwwlknon  27863  eucrctshift  28016  numclwlk1lem2  28143  dipcl  28483  dipcn  28491  bcm1n  30512  prmdvdsbc  30526  psgnfzto1st  30742  isarchi2  30809  submarchi  30810  freshmansdream  30854  submateqlem1  31067  madjusmdetlem2  31088  madjusmdetlem4  31090  mdetlap  31092  nexple  31263  oddpwdc  31607  eulerpartlemsv2  31611  eulerpartlemsf  31612  eulerpartlems  31613  eulerpartlemv  31617  eulerpartlemb  31621  plymulx0  31812  signsvtn0  31835  fsum2dsub  31873  reprinfz1  31888  reprpmtf1o  31892  circlemeth  31906  circlemethnat  31907  hgt750lemb  31922  hgt750lema  31923  hgt750leme  31924  tgoldbachgtde  31926  tgoldbachgtda  31927  lpadleft  31949  subfacp1lem1  32421  subfacp1lem6  32427  subfaclim  32430  erdszelem8  32440  erdszelem10  32442  cvmliftlem10  32536  faclim2  32975  poimirlem7  34893  poimirlem17  34903  poimirlem18  34904  poimirlem20  34906  poimirlem21  34907  poimirlem22  34908  poimirlem25  34911  poimirlem26  34912  poimirlem27  34913  poimirlem28  34914  poimirlem32  34918  nninfnub  35020  bfplem1  35094  oexpreposd  39172  nn0rppwr  39175  expgcd  39176  zrtelqelz  39185  dffltz  39264  fltne  39265  fltltc  39266  fltnltalem  39267  fltnlta  39268  3rexfrabdioph  39387  4rexfrabdioph  39388  6rexfrabdioph  39389  7rexfrabdioph  39390  irrapxlem5  39416  pellexlem2  39420  pellexlem6  39424  pell14qrgt0  39449  pell1qrge1  39460  pellfundgt1  39473  ltrmxnn0  39539  jm2.26lem3  39591  jm2.27a  39595  jm2.27c  39597  rmxdiophlem  39605  jm3.1lem1  39607  jm3.1lem2  39608  jm3.1lem3  39609  jm3.1  39610  dgrsub2  39728  mpaaeu  39743  idomsubgmo  39791  relexpxpmin  40055  nzprmdif  40644  binomcxplemwb  40673  fperiodmul  41563  xralrple4  41633  fsumnncl  41844  dvsinexp  42187  dvxpaek  42217  itgsinexplem1  42231  stoweidlem1  42279  stoweidlem17  42295  stoweidlem25  42303  stoweidlem34  42312  stoweidlem38  42316  stoweidlem40  42318  stoweidlem42  42320  stoweidlem45  42323  stirlinglem4  42355  stirlinglem5  42356  stirlinglem10  42361  stirlinglem13  42364  dirkertrigeq  42379  fourierdlem21  42406  fourierdlem25  42410  fourierdlem48  42432  fourierdlem54  42438  fourierdlem64  42448  fourierdlem65  42449  fourierdlem73  42457  fourierdlem81  42465  fourierdlem83  42467  fourierdlem92  42476  fourierdlem103  42487  fourierdlem104  42488  fourierdlem112  42496  fourierdlem113  42497  etransclem1  42513  etransclem4  42516  etransclem8  42520  etransclem15  42527  etransclem17  42529  etransclem18  42530  etransclem19  42531  etransclem20  42532  etransclem21  42533  etransclem22  42534  etransclem23  42535  etransclem24  42536  etransclem25  42537  etransclem27  42539  etransclem32  42544  etransclem35  42547  etransclem41  42553  etransclem44  42556  etransclem46  42558  iccpartigtl  43576  iccpartgt  43580  iccpartgel  43582  iccelpart  43586  odz2prm2pw  43718  fmtnoprmfac1  43720  fmtnoprmfac2  43722  2pwp1prm  43744  sfprmdvdsmersenne  43761  lighneallem4a  43766  proththdlem  43771  proththd  43772  perfectALTVlem1  43879  perfectALTVlem2  43880  perfectALTV  43881  fpprwpprb  43898  logbpw2m1  44620  nnpw2blenfzo  44634  nnolog2flm1  44643  dignn0fr  44654  nn0sumshdiglemA  44672  nn0sumshdiglemB  44673