Theorem abscld 15471

Description: Real closure of absolute value. (Contributed by Mario Carneiro, 29-May-2016.)

Hypothesis

Ref	Expression
abscld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)

Assertion

Ref	Expression
abscld	⊢ (𝜑 → (abs‘𝐴) ∈ ℝ)

Proof of Theorem abscld

Step	Hyp	Ref	Expression
1		abscld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		abscl 15313	. 2 ⊢ (𝐴 ∈ ℂ → (abs‘𝐴) ∈ ℝ)
3	1, 2	syl 17	1 ⊢ (𝜑 → (abs‘𝐴) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2105  ‘cfv 6562  ℂcc 11150  ℝcr 11151  abscabs 15269

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-pre-sup 11230

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-sup 9479  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918  df-nn 12264  df-2 12326  df-3 12327  df-n0 12524  df-z 12611  df-uz 12876  df-rp 13032  df-seq 14039  df-exp 14099  df-cj 15134  df-re 15135  df-im 15136  df-sqrt 15270  df-abs 15271

This theorem is referenced by:  bhmafibid1  15500  lo1bddrp  15557  elo1mpt  15566  elo1mpt2  15567  elo1d  15568  o1bdd2  15573  o1bddrp  15574  rlimuni  15582  climuni  15584  o1eq  15602  rlimcld2  15610  rlimrege0  15611  climabs0  15617  mulcn2  15628  reccn2  15629  cn1lem  15630  cjcn2  15632  o1add  15646  o1mul  15647  o1sub  15648  rlimo1  15649  o1rlimmul  15651  climsqz  15673  climsqz2  15674  rlimsqzlem  15681  o1le  15685  climbdd  15704  caucvgrlem  15705  caucvgrlem2  15707  iseraltlem3  15716  iseralt  15717  fsumabs  15833  o1fsum  15845  iserabs  15847  cvgcmpce  15850  abscvgcvg  15851  divrcnv  15884  explecnv  15897  geomulcvg  15908  cvgrat  15915  mertenslem1  15916  mertenslem2  15917  fprodabs  16006  efcllem  16109  efaddlem  16125  eftlub  16141  ef01bndlem  16216  sin01bnd  16217  cos01bnd  16218  absef  16229  dvdsabseq  16346  alzdvds  16353  sqnprm  16735  pclem  16871  mul4sqlem  16986  xrsdsreclb  21448  gzrngunitlem  21467  gzrngunit  21468  prmirredlem  21500  nm2dif  24653  blcvx  24833  recld2  24849  addcnlem  24899  cnheiborlem  24999  cnheibor  25000  cnllycmp  25001  cphsqrtcl2  25233  ipcau2  25281  tcphcphlem1  25282  ipcnlem2  25291  cncmet  25369  trirn  25447  rrxdstprj1  25456  pjthlem1  25484  volsup2  25653  mbfi1fseqlem6  25769  iblabslem  25877  iblabs  25878  iblabsr  25879  iblmulc2  25880  itgabs  25884  bddmulibl  25888  bddiblnc  25891  itgcn  25894  dveflem  26031  dvlip  26046  dvlipcn  26047  c1liplem1  26049  dveq0  26053  dv11cn  26054  lhop1lem  26066  dvfsumabs  26077  dvfsumrlim  26086  dvfsumrlim2  26087  ftc1a  26092  ftc1lem4  26094  plyeq0lem  26263  aalioulem2  26389  aalioulem3  26390  aalioulem4  26391  aalioulem5  26392  aalioulem6  26393  aaliou  26394  geolim3  26395  aaliou2b  26397  aaliou3lem9  26406  ulmbdd  26455  ulmcn  26456  ulmdvlem1  26457  mtest  26461  mtestbdd  26462  iblulm  26464  itgulm  26465  radcnvlem1  26470  radcnvlem2  26471  radcnvlt1  26475  radcnvle  26477  dvradcnv  26478  pserulm  26479  psercnlem2  26482  psercnlem1  26483  psercn  26484  pserdvlem1  26485  pserdvlem2  26486  pserdv  26487  abelthlem2  26490  abelthlem3  26491  abelthlem5  26493  abelthlem7  26496  abelthlem8  26497  tanregt0  26595  efif1olem3  26600  efif1olem4  26601  eff1olem  26604  cosargd  26664  cosarg0d  26665  argregt0  26666  argrege0  26667  abslogle  26674  logcnlem3  26700  logcnlem4  26701  efopnlem1  26712  logtayl  26716  abscxp2  26749  cxpcn3lem  26804  abscxpbnd  26810  cosangneg2d  26864  lawcoslem1  26872  lawcos  26873  pythag  26874  isosctrlem3  26877  ssscongptld  26879  chordthmlem3  26891  chordthmlem4  26892  chordthmlem5  26893  heron  26895  bndatandm  26986  efrlim  27026  efrlimOLD  27027  rlimcxp  27031  o1cxp  27032  cxploglim2  27036  divsqrtsumo1  27041  fsumharmonic  27069  lgamgulmlem2  27087  lgamgulmlem3  27088  lgamgulmlem5  27090  lgambdd  27094  lgamucov  27095  lgamcvg2  27112  ftalem1  27130  ftalem2  27131  ftalem3  27132  ftalem4  27133  ftalem5  27134  ftalem7  27136  logfacbnd3  27281  logfacrlim  27282  logexprlim  27283  dchrabs  27318  lgsdirprm  27389  lgsdilem2  27391  lgsne0  27393  lgsabs1  27394  mul2sq  27477  2sqlem3  27478  2sqblem  27489  vmadivsumb  27541  rplogsumlem2  27543  dchrisumlem2  27548  dchrisumlem3  27549  dchrisum  27550  dchrmusum2  27552  dchrvmasumlem2  27556  dchrvmasumlem3  27557  dchrvmasumiflem1  27559  dchrvmasumiflem2  27560  dchrisum0flblem1  27566  dchrisum0fno1  27569  dchrisum0lem1b  27573  dchrisum0lem1  27574  dchrisum0lem2a  27575  dchrisum0lem2  27576  dchrisum0lem3  27577  mudivsum  27588  mulogsumlem  27589  mulog2sumlem1  27592  mulog2sumlem2  27593  2vmadivsumlem  27598  log2sumbnd  27602  selberglem2  27604  selbergb  27607  selberg2b  27610  chpdifbndlem1  27611  selberg3lem1  27615  selberg3lem2  27616  selberg4lem1  27618  pntrsumo1  27623  pntrsumbnd  27624  pntrsumbnd2  27625  pntrlog2bndlem1  27635  pntrlog2bndlem2  27636  pntrlog2bndlem3  27637  pntrlog2bndlem4  27638  pntrlog2bndlem5  27639  pntrlog2bndlem6  27641  pntrlog2bnd  27642  pntpbnd1a  27643  pntpbnd2  27645  pntibndlem2  27649  pntlemn  27658  pntlemj  27661  pntlemf  27663  pntlemo  27665  pntlem3  27667  pntleml  27669  smcnlem  30725  nmoub3i  30801  isblo3i  30829  htthlem  30945  bcs2  31210  pjhthlem1  31419  nmfnsetre  31905  nmfnleub2  31954  nmfnge0  31955  nmbdfnlbi  32077  nmcfnexi  32079  nmcfnlbi  32080  lnfnconi  32083  cnlnadjlem2  32096  cnlnadjlem7  32101  nmopcoadji  32129  leopnmid  32166  sqsscirc2  33869  subfaclim  35172  subfacval3  35173  sinccvglem  35656  dnicld1  36454  dnibndlem2  36461  dnibndlem6  36465  dnibndlem9  36468  dnibndlem12  36471  dnicn  36474  knoppcnlem4  36478  knoppcnlem6  36480  unblimceq0lem  36488  unblimceq0  36489  unbdqndv2lem1  36491  unbdqndv2lem2  36492  knoppndvlem11  36504  knoppndvlem12  36505  knoppndvlem14  36507  knoppndvlem15  36508  knoppndvlem17  36510  knoppndvlem18  36511  knoppndvlem20  36513  knoppndvlem21  36514  poimirlem29  37635  poimir  37639  iblabsnclem  37669  iblabsnc  37670  iblmulc2nc  37671  itgabsnc  37675  ftc1cnnclem  37677  ftc1anclem1  37679  ftc1anclem2  37680  ftc1anclem4  37682  ftc1anclem5  37683  ftc1anclem6  37684  ftc1anclem7  37685  ftc1anclem8  37686  ftc1anc  37687  ftc2nc  37688  dvasin  37690  areacirclem1  37694  areacirclem2  37695  areacirclem4  37697  areacirclem5  37698  areacirc  37699  geomcau  37745  cntotbnd  37782  rrndstprj1  37816  rrndstprj2  37817  ismrer1  37824  readvrec  42370  dffltz  42620  rencldnfilem  42807  irrapxlem2  42810  irrapxlem4  42812  irrapxlem5  42813  pellexlem2  42817  pellexlem6  42821  pell14qrgt0  42846  congabseq  42962  acongeq  42971  modabsdifz  42974  jm2.26lem3  42989  sqrtcvallem4  43628  extoimad  44153  imo72b2lem0  44154  imo72b2  44161  dvgrat  44307  cvgdvgrat  44308  radcnvrat  44309  dvconstbi  44329  binomcxplemnotnn0  44351  dstregt0  45231  absnpncan2d  45252  absnpncan3d  45257  abslt2sqd  45309  rexabslelem  45367  cvgcaule  45441  fprodabs2  45550  mullimc  45571  mullimcf  45578  limcrecl  45584  lptre2pt  45595  limcleqr  45599  addlimc  45603  0ellimcdiv  45604  limclner  45606  climleltrp  45631  climisp  45701  climxrrelem  45704  cnrefiisplem  45784  climxlim2lem  45800  cncficcgt0  45843  dvdivbd  45878  dvbdfbdioolem1  45883  dvbdfbdioolem2  45884  dvbdfbdioo  45885  ioodvbdlimc1lem1  45886  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  stoweid  46018  fourierdlem30  46092  fourierdlem39  46101  fourierdlem42  46104  fourierdlem47  46108  fourierdlem68  46129  fourierdlem70  46131  fourierdlem71  46132  fourierdlem73  46134  fourierdlem77  46138  fourierdlem80  46141  fourierdlem83  46144  fourierdlem87  46148  fourierdlem103  46164  fourierdlem104  46165  etransclem23  46212  etransclem48  46237  rrndistlt  46245  ioorrnopnlem  46259  sge0isum  46382  hoicvr  46503  smflimlem4  46729  smfmullem1  46746  smfmullem2  46747  smfmullem3  46748  itsclc0yqsol  48613