Theorem abscld 15353

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 15192	. 2 ⊢ (𝐴 ∈ ℂ → (abs‘𝐴) ∈ ℝ)
3	1, 2	syl 17	1 ⊢ (𝜑 → (abs‘𝐴) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2113  ‘cfv 6489  ℂcc 11015  ℝcr 11016  abscabs 15148

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-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7677  ax-cnex 11073  ax-resscn 11074  ax-1cn 11075  ax-icn 11076  ax-addcl 11077  ax-addrcl 11078  ax-mulcl 11079  ax-mulrcl 11080  ax-mulcom 11081  ax-addass 11082  ax-mulass 11083  ax-distr 11084  ax-i2m1 11085  ax-1ne0 11086  ax-1rid 11087  ax-rnegex 11088  ax-rrecex 11089  ax-cnre 11090  ax-pre-lttri 11091  ax-pre-lttrn 11092  ax-pre-ltadd 11093  ax-pre-mulgt0 11094  ax-pre-sup 11095

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-rmo 3347  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-iun 4945  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6256  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-riota 7312  df-ov 7358  df-oprab 7359  df-mpo 7360  df-om 7806  df-2nd 7931  df-frecs 8220  df-wrecs 8251  df-recs 8300  df-rdg 8338  df-er 8631  df-en 8880  df-dom 8881  df-sdom 8882  df-sup 9337  df-pnf 11159  df-mnf 11160  df-xr 11161  df-ltxr 11162  df-le 11163  df-sub 11357  df-neg 11358  df-div 11786  df-nn 12137  df-2 12199  df-3 12200  df-n0 12393  df-z 12480  df-uz 12743  df-rp 12897  df-seq 13916  df-exp 13976  df-cj 15013  df-re 15014  df-im 15015  df-sqrt 15149  df-abs 15150

This theorem is referenced by:  bhmafibid1  15382  lo1bddrp  15439  elo1mpt  15448  elo1mpt2  15449  elo1d  15450  o1bdd2  15455  o1bddrp  15456  rlimuni  15464  climuni  15466  o1eq  15484  rlimcld2  15492  rlimrege0  15493  climabs0  15499  mulcn2  15510  reccn2  15511  cn1lem  15512  cjcn2  15514  o1add  15528  o1mul  15529  o1sub  15530  rlimo1  15531  o1rlimmul  15533  climsqz  15555  climsqz2  15556  rlimsqzlem  15563  o1le  15567  climbdd  15586  caucvgrlem  15587  caucvgrlem2  15589  iseraltlem3  15598  iseralt  15599  fsumabs  15715  o1fsum  15727  iserabs  15729  cvgcmpce  15732  abscvgcvg  15733  divrcnv  15766  explecnv  15779  geomulcvg  15790  cvgrat  15797  mertenslem1  15798  mertenslem2  15799  fprodabs  15888  efcllem  15991  efaddlem  16007  eftlub  16025  ef01bndlem  16100  sin01bnd  16101  cos01bnd  16102  absef  16113  dvdsabseq  16231  alzdvds  16238  sqnprm  16620  pclem  16757  mul4sqlem  16872  xrsdsreclb  21359  gzrngunitlem  21378  gzrngunit  21379  prmirredlem  21418  nm2dif  24560  blcvx  24733  recld2  24750  addcnlem  24800  cnheiborlem  24900  cnheibor  24901  cnllycmp  24902  cphsqrtcl2  25133  ipcau2  25181  tcphcphlem1  25182  ipcnlem2  25191  cncmet  25269  trirn  25347  rrxdstprj1  25356  pjthlem1  25384  volsup2  25553  mbfi1fseqlem6  25668  iblabslem  25776  iblabs  25777  iblabsr  25778  iblmulc2  25779  itgabs  25783  bddmulibl  25787  bddiblnc  25790  itgcn  25793  dveflem  25930  dvlip  25945  dvlipcn  25946  c1liplem1  25948  dveq0  25952  dv11cn  25953  lhop1lem  25965  dvfsumabs  25976  dvfsumrlim  25985  dvfsumrlim2  25986  ftc1a  25991  ftc1lem4  25993  plyeq0lem  26162  aalioulem2  26288  aalioulem3  26289  aalioulem4  26290  aalioulem5  26291  aalioulem6  26292  aaliou  26293  geolim3  26294  aaliou2b  26296  aaliou3lem9  26305  ulmbdd  26354  ulmcn  26355  ulmdvlem1  26356  mtest  26360  mtestbdd  26361  iblulm  26363  itgulm  26364  radcnvlem1  26369  radcnvlem2  26370  radcnvlt1  26374  radcnvle  26376  dvradcnv  26377  pserulm  26378  psercnlem2  26381  psercnlem1  26382  psercn  26383  pserdvlem1  26384  pserdvlem2  26385  pserdv  26386  abelthlem2  26389  abelthlem3  26390  abelthlem5  26392  abelthlem7  26395  abelthlem8  26396  tanregt0  26495  efif1olem3  26500  efif1olem4  26501  eff1olem  26504  cosargd  26564  cosarg0d  26565  argregt0  26566  argrege0  26567  abslogle  26574  logcnlem3  26600  logcnlem4  26601  efopnlem1  26612  logtayl  26616  abscxp2  26649  cxpcn3lem  26704  abscxpbnd  26710  cosangneg2d  26764  lawcoslem1  26772  lawcos  26773  pythag  26774  isosctrlem3  26777  ssscongptld  26779  chordthmlem3  26791  chordthmlem4  26792  chordthmlem5  26793  heron  26795  bndatandm  26886  efrlim  26926  efrlimOLD  26927  rlimcxp  26931  o1cxp  26932  cxploglim2  26936  divsqrtsumo1  26941  fsumharmonic  26969  lgamgulmlem2  26987  lgamgulmlem3  26988  lgamgulmlem5  26990  lgambdd  26994  lgamucov  26995  lgamcvg2  27012  ftalem1  27030  ftalem2  27031  ftalem3  27032  ftalem4  27033  ftalem5  27034  ftalem7  27036  logfacbnd3  27181  logfacrlim  27182  logexprlim  27183  dchrabs  27218  lgsdirprm  27289  lgsdilem2  27291  lgsne0  27293  lgsabs1  27294  mul2sq  27377  2sqlem3  27378  2sqblem  27389  vmadivsumb  27441  rplogsumlem2  27443  dchrisumlem2  27448  dchrisumlem3  27449  dchrisum  27450  dchrmusum2  27452  dchrvmasumlem2  27456  dchrvmasumlem3  27457  dchrvmasumiflem1  27459  dchrvmasumiflem2  27460  dchrisum0flblem1  27466  dchrisum0fno1  27469  dchrisum0lem1b  27473  dchrisum0lem1  27474  dchrisum0lem2a  27475  dchrisum0lem2  27476  dchrisum0lem3  27477  mudivsum  27488  mulogsumlem  27489  mulog2sumlem1  27492  mulog2sumlem2  27493  2vmadivsumlem  27498  log2sumbnd  27502  selberglem2  27504  selbergb  27507  selberg2b  27510  chpdifbndlem1  27511  selberg3lem1  27515  selberg3lem2  27516  selberg4lem1  27518  pntrsumo1  27523  pntrsumbnd  27524  pntrsumbnd2  27525  pntrlog2bndlem1  27535  pntrlog2bndlem2  27536  pntrlog2bndlem3  27537  pntrlog2bndlem4  27538  pntrlog2bndlem5  27539  pntrlog2bndlem6  27541  pntrlog2bnd  27542  pntpbnd1a  27543  pntpbnd2  27545  pntibndlem2  27549  pntlemn  27558  pntlemj  27561  pntlemf  27563  pntlemo  27565  pntlem3  27567  pntleml  27569  smcnlem  30698  nmoub3i  30774  isblo3i  30802  htthlem  30918  bcs2  31183  pjhthlem1  31392  nmfnsetre  31878  nmfnleub2  31927  nmfnge0  31928  nmbdfnlbi  32050  nmcfnexi  32052  nmcfnlbi  32053  lnfnconi  32056  cnlnadjlem2  32069  cnlnadjlem7  32074  nmopcoadji  32102  leopnmid  32139  constrdircl  33850  iconstr  33851  constrremulcl  33852  constrimcl  33855  constrmulcl  33856  constrinvcl  33858  constrabscl  33863  constrsqrtcl  33864  sqsscirc2  33994  subfaclim  35304  subfacval3  35305  sinccvglem  35788  dnicld1  36588  dnibndlem2  36595  dnibndlem6  36599  dnibndlem9  36602  dnibndlem12  36605  dnicn  36608  knoppcnlem4  36612  knoppcnlem6  36614  unblimceq0lem  36622  unblimceq0  36623  unbdqndv2lem1  36625  unbdqndv2lem2  36626  knoppndvlem11  36638  knoppndvlem12  36639  knoppndvlem14  36641  knoppndvlem15  36642  knoppndvlem17  36644  knoppndvlem18  36645  knoppndvlem20  36647  knoppndvlem21  36648  poimirlem29  37762  poimir  37766  iblabsnclem  37796  iblabsnc  37797  iblmulc2nc  37798  itgabsnc  37802  ftc1cnnclem  37804  ftc1anclem1  37806  ftc1anclem2  37807  ftc1anclem4  37809  ftc1anclem5  37810  ftc1anclem6  37811  ftc1anclem7  37812  ftc1anclem8  37813  ftc1anc  37814  ftc2nc  37815  dvasin  37817  areacirclem1  37821  areacirclem2  37822  areacirclem4  37824  areacirclem5  37825  areacirc  37826  geomcau  37872  cntotbnd  37909  rrndstprj1  37943  rrndstprj2  37944  ismrer1  37951  readvrec  42532  readvcot  42534  dffltz  42792  rencldnfilem  42977  irrapxlem2  42980  irrapxlem4  42982  irrapxlem5  42983  pellexlem2  42987  pellexlem6  42991  pell14qrgt0  43016  congabseq  43131  acongeq  43140  modabsdifz  43143  jm2.26lem3  43158  sqrtcvallem4  43796  extoimad  44321  imo72b2lem0  44322  imo72b2  44329  dvgrat  44469  cvgdvgrat  44470  radcnvrat  44471  dvconstbi  44491  binomcxplemnotnn0  44513  dstregt0  45446  absnpncan2d  45466  absnpncan3d  45471  abslt2sqd  45521  rexabslelem  45578  cvgcaule  45651  fprodabs2  45757  mullimc  45778  mullimcf  45785  limcrecl  45791  lptre2pt  45800  limcleqr  45804  addlimc  45808  0ellimcdiv  45809  limclner  45811  climleltrp  45836  climisp  45906  climxrrelem  45909  cnrefiisplem  45989  climxlim2lem  46005  cncficcgt0  46048  dvdivbd  46083  dvbdfbdioolem1  46088  dvbdfbdioolem2  46089  dvbdfbdioo  46090  ioodvbdlimc1lem1  46091  ioodvbdlimc1lem2  46092  ioodvbdlimc2lem  46094  stoweid  46223  fourierdlem30  46297  fourierdlem39  46306  fourierdlem42  46309  fourierdlem47  46313  fourierdlem68  46334  fourierdlem70  46336  fourierdlem71  46337  fourierdlem73  46339  fourierdlem77  46343  fourierdlem80  46346  fourierdlem83  46349  fourierdlem87  46353  fourierdlem103  46369  fourierdlem104  46370  etransclem23  46417  etransclem48  46442  rrndistlt  46450  ioorrnopnlem  46464  sge0isum  46587  hoicvr  46708  smflimlem4  46934  smfmullem1  46951  smfmullem2  46952  smfmullem3  46953  modlt0b  47525  itsclc0yqsol  48926