Theorem nnnn0d 12462

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℕcn 12145  ℕ₀cn0 12401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-ss 3918  df-n0 12402

This theorem is referenced by:  nn0ge2m1nn0  12472  nnzd  12514  eluzge2nn0  12805  expgt1  14023  expaddzlem  14028  expaddz  14029  expmulz  14031  expmulnbnd  14158  exp11nnd  14184  facwordi  14212  faclbnd  14213  facavg  14224  bcm1k  14238  wrdeqs1cat  14643  cshwcsh2id  14751  relexpsucnnr  14948  isercolllem2  15589  bcxmas  15758  climcndslem1  15772  climcndslem2  15773  climcnds  15774  pwdif  15791  geo2sum  15796  mertenslem1  15807  prodmolem3  15856  prodmolem2a  15857  bpolydiflem  15977  eftabs  15998  efcllem  16000  eftlub  16034  eirrlem  16129  rpnnen2lem9  16147  rpnnen2lem11  16149  dvdsfac  16253  pwp1fsum  16318  oddpwp1fsum  16319  bitsfzo  16362  bitsfi  16364  sadcaddlem  16384  smumullem  16419  gcdcl  16433  dvdsgcdidd  16464  mulgcd  16475  rplpwr  16485  rprpwr  16486  rppwr  16487  nn0rppwr  16488  expgcd  16490  lcmcl  16528  lcmgcdnn  16538  lcmfcl  16555  nprmdvds1  16633  rpexp  16649  prmdvdsbc  16653  zsqrtelqelz  16685  phiprmpw  16703  eulerthlem2  16709  eulerth  16710  fermltl  16711  odzcllem  16720  odzdvds  16723  odzphi  16724  prm23lt5  16742  pythagtriplem6  16749  pythagtriplem7  16750  pcprmpw2  16810  dvdsprmpweqle  16814  pcprod  16823  pcfac  16827  pcbc  16828  expnprm  16830  pockthlem  16833  pockthg  16834  prmunb  16842  prmreclem2  16845  prmreclem3  16846  prmreclem4  16847  prmreclem5  16848  prmreclem6  16849  mul4sqlem  16881  4sqlem11  16883  4sqlem17  16889  vdwlem1  16909  vdwlem5  16913  vdwlem6  16914  vdwlem8  16916  vdwlem9  16917  vdwlem11  16919  vdwlem12  16920  vdwnnlem3  16925  ramz2  16952  ramub1lem1  16954  ramub1lem2  16955  ramub1  16956  prmgaplem3  16981  2expltfac  17020  psgnunilem3  19425  odfval  19461  mndodconglem  19470  gexcl3  19516  pgpfi1  19524  sylow1lem1  19527  gexexlem  19781  prmcyg  19823  gsumval3  19836  ablfacrplem  19996  ablfacrp  19997  ablfacrp2  19998  ablfac1eu  20004  prmgrpsimpgd  20045  srgbinomlem3  20163  srgbinomlem4  20164  fermltlchr  21484  freshmansdream  21529  chfacfscmulgsum  22804  chfacfpmmulgsum  22808  cpmadugsumlemF  22820  ovoliunlem1  25459  mbfi1fseqlem1  25672  mbfi1fseqlem3  25674  mbfi1fseqlem5  25676  itg2cnlem2  25719  dvply1  26247  aalioulem2  26297  aalioulem5  26300  aaliou3lem1  26306  aaliou3lem2  26307  aaliou3lem8  26309  aaliou3lem6  26312  taylthlem1  26337  taylthlem2  26338  taylthlem2OLD  26339  pserdvlem2  26394  cxpeq  26723  zrtelqelz  26724  dmgmdivn0  26994  lgamgulmlem5  26999  lgamcvg2  27021  wilthlem1  27034  ftalem1  27039  ftalem2  27040  ftalem4  27042  ftalem5  27043  basellem2  27048  basellem3  27049  basellem4  27050  basellem5  27051  isppw2  27081  mpodvdsmulf1o  27160  dvdsmulf1o  27162  sgmmul  27168  fsumvma2  27181  chpchtsum  27186  logfacubnd  27188  mersenne  27194  perfect1  27195  perfectlem1  27196  perfectlem2  27197  perfect  27198  dchrelbas3  27205  dchrelbasd  27206  dchrzrh1  27211  dchrzrhmul  27213  dchrmulcl  27216  dchrn0  27217  dchrfi  27222  dchrghm  27223  dchrabs  27227  dchrinv  27228  dchrptlem1  27231  dchrptlem2  27232  dchrptlem3  27233  dchrpt  27234  dchrsum2  27235  sum2dchr  27241  pcbcctr  27243  bcmono  27244  bclbnd  27247  bposlem1  27251  bposlem3  27253  bposlem5  27255  bposlem6  27256  lgslem1  27264  lgsval2lem  27274  lgsvalmod  27283  lgsmod  27290  lgsdirprm  27298  lgsne0  27302  lgsqrlem1  27313  lgsqrlem2  27314  lgsqrlem3  27315  lgsqrlem4  27316  gausslemma2dlem0b  27324  gausslemma2dlem0c  27325  gausslemma2dlem1  27333  gausslemma2dlem7  27340  gausslemma2d  27341  lgseisenlem1  27342  lgseisenlem2  27343  lgseisenlem3  27344  lgseisenlem4  27345  lgseisen  27346  lgsquadlem2  27348  lgsquadlem3  27349  m1lgs  27355  2lgslem1a  27358  2sqlem3  27387  2sqblem  27398  chebbnd1lem1  27436  chebbnd1lem3  27438  rplogsumlem2  27452  rpvmasumlem  27454  dchrisumlem1  27456  dchrisumlem2  27457  dchrmusum2  27461  dchrvmasumlem3  27466  dchrisum0ff  27474  dchrisum0flblem1  27475  rpvmasum2  27479  dchrisum0re  27480  dchrisum0lem2a  27484  dirith  27496  mudivsum  27497  pntpbnd1a  27552  pntlemq  27568  pntlemr  27569  pntlemj  27570  ostth2lem1  27585  ostth2lem2  27601  ostth2lem3  27602  ostth2  27604  crctcshwlkn0lem6  29888  hashecclwwlkn1  30152  umgrhashecclwwlk  30153  clwwlknon  30165  eucrctshift  30318  numclwlk1lem2  30445  nrt2irr  30548  dipcl  30787  dipcn  30795  bcm1n  32875  expgt0b  32897  nexple  32925  2exple2exp  32926  oexpled  32928  wrdpmtrlast  33175  psgnfzto1st  33187  isarchi2  33267  submarchi  33268  znfermltl  33447  fldextrspundgdvdslem  33837  fldextrspundgdvds  33838  fldext2rspun  33839  constrext2chnlem  33907  cos9thpiminplylem2  33940  submateqlem1  33964  madjusmdetlem2  33985  madjusmdetlem4  33987  mdetlap  33989  oddpwdc  34511  eulerpartlemsv2  34515  eulerpartlemsf  34516  eulerpartlems  34517  eulerpartlemv  34521  eulerpartlemb  34525  plymulx0  34704  signsvtn0  34727  fsum2dsub  34764  reprinfz1  34779  reprpmtf1o  34783  circlemeth  34797  circlemethnat  34798  hgt750lemb  34813  hgt750lema  34814  hgt750leme  34815  tgoldbachgtde  34817  tgoldbachgtda  34818  lpadleft  34840  subfacp1lem1  35373  subfacp1lem6  35379  subfaclim  35382  erdszelem8  35392  erdszelem10  35394  cvmliftlem10  35488  faclim2  35942  poimirlem7  37828  poimirlem17  37838  poimirlem18  37839  poimirlem20  37841  poimirlem21  37842  poimirlem22  37843  poimirlem25  37846  poimirlem26  37847  poimirlem27  37848  poimirlem28  37849  poimirlem32  37853  nninfnub  37952  bfplem1  38023  zndvdchrrhm  42226  lcmineqlem1  42283  lcmineqlem2  42284  lcmineqlem8  42290  lcmineqlem10  42292  lcmineqlem11  42293  lcmineqlem15  42297  lcmineqlem16  42298  lcmineqlem18  42300  lcmineqlem19  42301  lcmineqlem20  42302  lcmineqlem21  42303  lcmineqlem22  42304  3lexlogpow2ineq2  42313  dvrelogpow2b  42322  aks4d1p1p2  42324  aks4d1p1p4  42325  aks4d1p1  42330  aks4d1p3  42332  aks4d1p7d1  42336  aks4d1p7  42337  aks4d1p8  42341  aks4d1p9  42342  isprimroot2  42348  primrootsunit1  42351  primrootscoprmpow  42353  posbezout  42354  primrootscoprbij  42356  primrootlekpowne0  42359  primrootspoweq0  42360  aks6d1c1p2  42363  aks6d1c1p3  42364  aks6d1c1p4  42365  aks6d1c1p5  42366  aks6d1c1p7  42367  aks6d1c1p6  42368  aks6d1c1p8  42369  aks6d1c2p2  42373  hashscontpowcl  42374  hashscontpow1  42375  hashscontpow  42376  aks6d1c4  42378  aks6d1c2lem3  42380  aks6d1c2lem4  42381  aks6d1c2  42384  sticksstones6  42405  sticksstones7  42406  sticksstones10  42409  sticksstones12a  42411  sticksstones12  42412  sticksstones20  42420  sticksstones22  42422  aks6d1c6lem2  42425  aks6d1c6lem3  42426  aks6d1c6lem4  42427  aks6d1c6isolem1  42428  aks6d1c6isolem2  42429  aks6d1c6lem5  42431  bcled  42432  bcle2d  42433  aks6d1c7lem1  42434  aks6d1c7  42438  aks5lem2  42441  aks5lem3a  42443  aks5lem5a  42445  grpods  42448  unitscyglem2  42450  unitscyglem4  42452  aks5lem7  42454  aks5  42458  sumcubes  42568  oexpreposd  42577  exp11d  42581  dvdsexpb  42590  fiabv  42791  fsuppind  42833  dffltz  42877  fltdvdsabdvdsc  42881  fltne  42887  flt4lem4  42892  flt4lem7  42902  fltltc  42904  fltnltalem  42905  fltnlta  42906  3rexfrabdioph  43039  4rexfrabdioph  43040  6rexfrabdioph  43041  7rexfrabdioph  43042  irrapxlem5  43068  pellexlem2  43072  pellexlem6  43076  pell14qrgt0  43101  pell1qrge1  43112  pellfundgt1  43125  ltrmxnn0  43191  jm2.26lem3  43243  jm2.27a  43247  jm2.27c  43249  rmxdiophlem  43257  jm3.1lem1  43259  jm3.1lem2  43260  jm3.1lem3  43261  jm3.1  43262  dgrsub2  43377  mpaaeu  43392  idomsubgmo  43435  relexpxpmin  43958  nzprmdif  44560  binomcxplemwb  44589  fperiodmul  45552  xralrple4  45617  fsumnncl  45818  dvsinexp  46155  dvxpaek  46184  itgsinexplem1  46198  stoweidlem1  46245  stoweidlem17  46261  stoweidlem25  46269  stoweidlem34  46278  stoweidlem38  46282  stoweidlem40  46284  stoweidlem42  46286  stoweidlem45  46289  stirlinglem4  46321  stirlinglem5  46322  stirlinglem10  46327  stirlinglem13  46330  dirkertrigeq  46345  fourierdlem21  46372  fourierdlem25  46376  fourierdlem48  46398  fourierdlem54  46404  fourierdlem64  46414  fourierdlem65  46415  fourierdlem73  46423  fourierdlem81  46431  fourierdlem83  46433  fourierdlem92  46442  fourierdlem103  46453  fourierdlem104  46454  fourierdlem112  46462  fourierdlem113  46463  etransclem1  46479  etransclem4  46482  etransclem8  46486  etransclem15  46493  etransclem17  46495  etransclem18  46496  etransclem19  46497  etransclem20  46498  etransclem21  46499  etransclem22  46500  etransclem23  46501  etransclem24  46502  etransclem25  46503  etransclem27  46505  etransclem32  46510  etransclem35  46513  etransclem41  46519  etransclem44  46522  etransclem46  46524  modmknepk  47608  iccpartigtl  47669  iccpartgt  47673  iccpartgel  47675  iccelpart  47679  odz2prm2pw  47809  fmtnoprmfac1  47811  fmtnoprmfac2  47813  2pwp1prm  47835  sfprmdvdsmersenne  47849  lighneallem4a  47854  proththdlem  47859  proththd  47860  perfectALTVlem1  47967  perfectALTVlem2  47968  perfectALTV  47969  fpprwpprb  47986  gpgedgvtx1  48308  logbpw2m1  48813  nnpw2blenfzo  48827  nnolog2flm1  48836  dignn0fr  48847  nn0sumshdiglemA  48865  nn0sumshdiglemB  48866