Theorem nnnn0d 12536

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 12478	. 2 ⊢ ℕ ⊆ ℕ0
2		nnnn0d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
3	1, 2	sselid 3932	1 ⊢ (𝜑 → 𝐴 ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2141  ℕcn 12204  ℕ₀cn0 12475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3907  df-ss 3919  df-n0 12476

This theorem is referenced by:  nn0ge2m1nn0  12546  nnzd  12588  eluzge2nn0  12887  expgt1  14107  expaddzlem  14112  expaddz  14113  expmulz  14115  expmulnbnd  14242  exp11nnd  14268  facwordi  14296  faclbnd  14297  facavg  14308  bcm1k  14322  wrdeqs1cat  14727  cshwcsh2id  14835  relexpsucnnr  15032  isercolllem2  15684  bcxmas  15856  climcndslem1  15870  climcndslem2  15871  climcnds  15872  pwdif  15889  geo2sum  15894  mertenslem1  15905  prodmolem3  15954  prodmolem2a  15955  bpolydiflem  16075  eftabs  16096  efcllem  16098  eftlub  16132  eirrlem  16227  rpnnen2lem9  16245  rpnnen2lem11  16247  dvdsfac  16351  pwp1fsum  16416  oddpwp1fsum  16417  bitsfzo  16460  bitsfi  16462  sadcaddlem  16482  smumullem  16517  gcdcl  16531  dvdsgcdidd  16562  mulgcd  16573  rplpwr  16583  rprpwr  16584  rppwr  16585  nn0rppwr  16586  expgcd  16588  lcmcl  16626  lcmgcdnn  16636  lcmfcl  16653  nprmdvds1  16732  rpexp  16748  prmdvdsbc  16752  zsqrtelqelz  16784  phiprmpw  16802  eulerthlem2  16808  eulerth  16809  fermltl  16810  odzcllem  16819  odzdvds  16822  odzphi  16823  prm23lt5  16841  pythagtriplem6  16848  pythagtriplem7  16849  pcprmpw2  16909  dvdsprmpweqle  16913  pcprod  16922  pcfac  16926  pcbc  16927  expnprm  16929  pockthlem  16932  pockthg  16933  prmunb  16941  prmreclem2  16944  prmreclem3  16945  prmreclem4  16946  prmreclem5  16947  prmreclem6  16948  mul4sqlem  16980  4sqlem11  16982  4sqlem17  16988  vdwlem1  17008  vdwlem5  17012  vdwlem6  17013  vdwlem8  17015  vdwlem9  17016  vdwlem11  17018  vdwlem12  17019  vdwnnlem3  17024  ramz2  17051  ramub1lem1  17053  ramub1lem2  17054  ramub1  17055  prmgaplem3  17080  2expltfac  17119  psgnunilem3  19527  odfval  19563  mndodconglem  19572  gexcl3  19618  pgpfi1  19626  sylow1lem1  19629  gexexlem  19883  prmcyg  19925  gsumval3  19938  ablfacrplem  20098  ablfacrp  20099  ablfacrp2  20100  ablfac1eu  20106  prmgrpsimpgd  20147  srgbinomlem3  20265  srgbinomlem4  20266  fermltlchr  21569  freshmansdream  21614  chfacfscmulgsum  22908  chfacfpmmulgsum  22912  cpmadugsumlemF  22924  ovoliunlem1  25552  mbfi1fseqlem1  25765  mbfi1fseqlem3  25767  mbfi1fseqlem5  25769  itg2cnlem2  25812  plyn0mulidp  26333  dvply1  26336  aalioulem2  26385  aalioulem5  26388  aaliou3lem1  26394  aaliou3lem2  26395  aaliou3lem8  26397  aaliou3lem6  26400  taylthlem1  26424  taylthlem2  26425  pserdvlem2  26479  cxpeq  26810  zrtelqelz  26811  dmgmdivn0  27080  lgamgulmlem5  27085  lgamcvg2  27107  wilthlem1  27120  ftalem1  27125  ftalem2  27126  ftalem4  27128  ftalem5  27129  basellem2  27134  basellem3  27135  basellem4  27136  basellem5  27137  isppw2  27167  mpodvdsmulf1o  27246  dvdsmulf1o  27248  sgmmul  27253  fsumvma2  27266  chpchtsum  27271  logfacubnd  27273  mersenne  27279  perfect1  27280  perfectlem1  27281  perfectlem2  27282  perfect  27283  dchrelbas3  27290  dchrelbasd  27291  dchrzrh1  27296  dchrzrhmul  27298  dchrmulcl  27301  dchrn0  27302  dchrfi  27307  dchrghm  27308  dchrabs  27312  dchrinv  27313  dchrptlem1  27316  dchrptlem2  27317  dchrptlem3  27318  dchrpt  27319  dchrsum2  27320  sum2dchr  27326  pcbcctr  27328  bcmono  27329  bclbnd  27332  bposlem1  27336  bposlem3  27338  bposlem5  27340  bposlem6  27341  lgslem1  27349  lgsval2lem  27359  lgsvalmod  27368  lgsmod  27375  lgsdirprm  27383  lgsne0  27387  lgsqrlem1  27398  lgsqrlem2  27399  lgsqrlem3  27400  lgsqrlem4  27401  gausslemma2dlem0b  27409  gausslemma2dlem0c  27410  gausslemma2dlem1  27418  gausslemma2dlem7  27425  gausslemma2d  27426  lgseisenlem1  27427  lgseisenlem2  27428  lgseisenlem3  27429  lgseisenlem4  27430  lgseisen  27431  lgsquadlem2  27433  lgsquadlem3  27434  m1lgs  27440  2lgslem1a  27443  2sqlem3  27472  2sqblem  27483  chebbnd1lem1  27521  chebbnd1lem3  27523  rplogsumlem2  27537  rpvmasumlem  27539  dchrisumlem1  27541  dchrisumlem2  27542  dchrmusum2  27546  dchrvmasumlem3  27551  dchrisum0ff  27559  dchrisum0flblem1  27560  rpvmasum2  27564  dchrisum0re  27565  dchrisum0lem2a  27569  dirith  27581  mudivsum  27582  pntpbnd1a  27637  pntlemq  27653  pntlemr  27654  pntlemj  27655  ostth2lem1  27670  ostth2lem2  27686  ostth2lem3  27687  ostth2  27689  crctcshwlkn0lem6  29972  hashecclwwlkn1  30236  umgrhashecclwwlk  30237  clwwlknon  30249  eucrctshift  30402  numclwlk1lem2  30529  nrt2irr  30632  dipcl  30872  dipcn  30880  bcm1n  32958  expgt0b  32980  nexple  32996  2exple2exp  32997  oexpled  32999  wrdpmtrlast  33234  psgnfzto1st  33246  isarchi2  33326  submarchi  33327  znfermltl  33513  fldextrspundgdvdslem  33938  fldextrspundgdvds  33939  fldext2rspun  33940  constrext2chnlem  34008  cos9thpiminplylem2  34041  submateqlem1  34065  madjusmdetlem2  34086  madjusmdetlem4  34088  mdetlap  34090  oddpwdc  34612  eulerpartlemsv2  34616  eulerpartlemsf  34617  eulerpartlems  34618  eulerpartlemv  34622  eulerpartlemb  34626  signsvtn0  34825  fsum2dsub  34862  reprinfz1  34877  reprpmtf1o  34881  circlemeth  34895  circlemethnat  34896  hgt750lemb  34911  hgt750lema  34912  hgt750leme  34913  tgoldbachgtde  34915  tgoldbachgtda  34916  lpadleft  34941  subfacp1lem1  35490  subfacp1lem6  35496  subfaclim  35499  erdszelem8  35509  erdszelem10  35511  cvmliftlem10  35605  faclim2  36059  poimirlem7  38087  poimirlem17  38097  poimirlem18  38098  poimirlem20  38100  poimirlem21  38101  poimirlem22  38102  poimirlem25  38105  poimirlem26  38106  poimirlem27  38107  poimirlem28  38108  poimirlem32  38112  nninfnub  38211  bfplem1  38282  zndvdchrrhm  42551  lcmineqlem1  42607  lcmineqlem2  42608  lcmineqlem8  42614  lcmineqlem10  42616  lcmineqlem11  42617  lcmineqlem15  42621  lcmineqlem16  42622  lcmineqlem18  42624  lcmineqlem19  42625  lcmineqlem20  42626  lcmineqlem21  42627  lcmineqlem22  42628  3lexlogpow2ineq2  42637  dvrelogpow2b  42646  aks4d1p1p2  42648  aks4d1p1p4  42649  aks4d1p1  42654  aks4d1p3  42656  aks4d1p7d1  42660  aks4d1p7  42661  aks4d1p8  42665  aks4d1p9  42666  isprimroot2  42672  primrootsunit1  42675  primrootscoprmpow  42677  posbezout  42678  primrootscoprbij  42680  primrootlekpowne0  42683  primrootspoweq0  42684  aks6d1c1p2  42687  aks6d1c1p3  42688  aks6d1c1p4  42689  aks6d1c1p5  42690  aks6d1c1p7  42691  aks6d1c1p6  42692  aks6d1c1p8  42693  aks6d1c2p2  42697  hashscontpowcl  42698  hashscontpow1  42699  hashscontpow  42700  aks6d1c4  42702  aks6d1c2lem3  42704  aks6d1c2lem4  42705  aks6d1c2  42708  sticksstones6  42729  sticksstones7  42730  sticksstones10  42733  sticksstones12a  42735  sticksstones12  42736  sticksstones20  42744  sticksstones22  42746  aks6d1c6lem2  42749  aks6d1c6lem3  42750  aks6d1c6lem4  42751  aks6d1c6isolem1  42752  aks6d1c6isolem2  42753  aks6d1c6lem5  42755  bcled  42756  bcle2d  42757  aks6d1c7lem1  42758  aks6d1c7  42762  aks5lem2  42765  aks5lem3a  42767  aks5lem5a  42769  grpods  42772  unitscyglem2  42774  unitscyglem4  42776  aks5lem7  42778  aks5  42782  sumcubes  42883  oexpreposd  42892  exp11d  42896  dvdsexpb  42905  fiabv  43115  fsuppind  43133  dffltz  43177  fltdvdsabdvdsc  43181  fltne  43187  flt4lem4  43192  flt4lem7  43202  fltltc  43204  fltnltalem  43205  fltnlta  43206  3rexfrabdioph  43335  4rexfrabdioph  43336  6rexfrabdioph  43337  7rexfrabdioph  43338  irrapxlem5  43364  pellexlem2  43368  pellexlem6  43372  pell14qrgt0  43397  pell1qrge1  43408  pellfundgt1  43421  ltrmxnn0  43487  jm2.26lem3  43539  jm2.27a  43543  jm2.27c  43545  rmxdiophlem  43553  jm3.1lem1  43555  jm3.1lem2  43556  jm3.1lem3  43557  jm3.1  43558  dgrsub2  43673  mpaaeu  43688  idomsubgmo  43731  relexpxpmin  44254  nzprmdif  44856  binomcxplemwb  44885  fperiodmul  45844  xralrple4  45909  fsumnncl  46109  dvsinexp  46446  dvxpaek  46475  itgsinexplem1  46489  stoweidlem1  46536  stoweidlem17  46552  stoweidlem25  46560  stoweidlem34  46569  stoweidlem38  46573  stoweidlem40  46575  stoweidlem42  46577  stoweidlem45  46580  stirlinglem4  46612  stirlinglem5  46613  stirlinglem10  46618  stirlinglem13  46621  dirkertrigeq  46636  fourierdlem21  46663  fourierdlem25  46667  fourierdlem48  46689  fourierdlem54  46695  fourierdlem64  46705  fourierdlem65  46706  fourierdlem73  46714  fourierdlem81  46722  fourierdlem83  46724  fourierdlem92  46733  fourierdlem103  46744  fourierdlem104  46745  fourierdlem112  46753  fourierdlem113  46754  etransclem1  46770  etransclem4  46773  etransclem8  46777  etransclem15  46784  etransclem17  46786  etransclem18  46787  etransclem19  46788  etransclem20  46789  etransclem21  46790  etransclem22  46791  etransclem23  46792  etransclem24  46793  etransclem25  46794  etransclem27  46796  etransclem32  46801  etransclem35  46804  etransclem41  46810  etransclem44  46813  etransclem46  46815  modmknepk  47923  iccpartigtl  47990  iccpartgt  47994  iccpartgel  47996  iccelpart  48000  odz2prm2pw  48133  fmtnoprmfac1  48135  fmtnoprmfac2  48137  2pwp1prm  48159  sfprmdvdsmersenne  48173  lighneallem4a  48178  proththdlem  48183  proththd  48184  perfectALTVlem1  48304  perfectALTVlem2  48305  perfectALTV  48306  fpprwpprb  48323  gpgedgvtx1  48645  logbpw2m1  49150  nnpw2blenfzo  49164  nnolog2flm1  49173  dignn0fr  49184  nn0sumshdiglemA  49202  nn0sumshdiglemB  49203