Theorem abscld 15388

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

Syntax hints:   → wi 4   ∈ wcel 2105  ‘cfv 6543  ℂcc 11112  ℝcr 11113  abscabs 15186

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729  ax-cnex 11170  ax-resscn 11171  ax-1cn 11172  ax-icn 11173  ax-addcl 11174  ax-addrcl 11175  ax-mulcl 11176  ax-mulrcl 11177  ax-mulcom 11178  ax-addass 11179  ax-mulass 11180  ax-distr 11181  ax-i2m1 11182  ax-1ne0 11183  ax-1rid 11184  ax-rnegex 11185  ax-rrecex 11186  ax-cnre 11187  ax-pre-lttri 11188  ax-pre-lttrn 11189  ax-pre-ltadd 11190  ax-pre-mulgt0 11191  ax-pre-sup 11192

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7860  df-2nd 7980  df-frecs 8270  df-wrecs 8301  df-recs 8375  df-rdg 8414  df-er 8707  df-en 8944  df-dom 8945  df-sdom 8946  df-sup 9441  df-pnf 11255  df-mnf 11256  df-xr 11257  df-ltxr 11258  df-le 11259  df-sub 11451  df-neg 11452  df-div 11877  df-nn 12218  df-2 12280  df-3 12281  df-n0 12478  df-z 12564  df-uz 12828  df-rp 12980  df-seq 13972  df-exp 14033  df-cj 15051  df-re 15052  df-im 15053  df-sqrt 15187  df-abs 15188

This theorem is referenced by:  bhmafibid1  15417  lo1bddrp  15474  elo1mpt  15483  elo1mpt2  15484  elo1d  15485  o1bdd2  15490  o1bddrp  15491  rlimuni  15499  climuni  15501  o1eq  15519  rlimcld2  15527  rlimrege0  15528  climabs0  15534  mulcn2  15545  reccn2  15546  cn1lem  15547  cjcn2  15549  o1add  15563  o1mul  15564  o1sub  15565  rlimo1  15566  o1rlimmul  15568  climsqz  15590  climsqz2  15591  rlimsqzlem  15600  o1le  15604  climbdd  15623  caucvgrlem  15624  caucvgrlem2  15626  iseraltlem3  15635  iseralt  15636  fsumabs  15752  o1fsum  15764  iserabs  15766  cvgcmpce  15769  abscvgcvg  15770  divrcnv  15803  explecnv  15816  geomulcvg  15827  cvgrat  15834  mertenslem1  15835  mertenslem2  15836  fprodabs  15923  efcllem  16026  efaddlem  16041  eftlub  16057  ef01bndlem  16132  sin01bnd  16133  cos01bnd  16134  absef  16145  dvdsabseq  16261  alzdvds  16268  sqnprm  16644  pclem  16776  mul4sqlem  16891  xrsdsreclb  21193  gzrngunitlem  21211  gzrngunit  21212  prmirredlem  21244  nm2dif  24355  blcvx  24535  recld2  24551  addcnlem  24601  cnheiborlem  24701  cnheibor  24702  cnllycmp  24703  cphsqrtcl2  24935  ipcau2  24983  tcphcphlem1  24984  ipcnlem2  24993  cncmet  25071  trirn  25149  rrxdstprj1  25158  pjthlem1  25186  volsup2  25355  mbfi1fseqlem6  25471  iblabslem  25578  iblabs  25579  iblabsr  25580  iblmulc2  25581  itgabs  25585  bddmulibl  25589  bddiblnc  25592  itgcn  25595  dveflem  25732  dvlip  25746  dvlipcn  25747  c1liplem1  25749  dveq0  25753  dv11cn  25754  lhop1lem  25766  dvfsumabs  25776  dvfsumrlim  25784  dvfsumrlim2  25785  ftc1a  25790  ftc1lem4  25792  plyeq0lem  25960  aalioulem2  26083  aalioulem3  26084  aalioulem4  26085  aalioulem5  26086  aalioulem6  26087  aaliou  26088  geolim3  26089  aaliou2b  26091  aaliou3lem9  26100  ulmbdd  26147  ulmcn  26148  ulmdvlem1  26149  mtest  26153  mtestbdd  26154  iblulm  26156  itgulm  26157  radcnvlem1  26162  radcnvlem2  26163  radcnvlt1  26167  radcnvle  26169  dvradcnv  26170  pserulm  26171  psercnlem2  26173  psercnlem1  26174  psercn  26175  pserdvlem1  26176  pserdvlem2  26177  pserdv  26178  abelthlem2  26181  abelthlem3  26182  abelthlem5  26184  abelthlem7  26187  abelthlem8  26188  tanregt0  26285  efif1olem3  26290  efif1olem4  26291  eff1olem  26294  cosargd  26353  cosarg0d  26354  argregt0  26355  argrege0  26356  abslogle  26363  logcnlem3  26389  logcnlem4  26390  efopnlem1  26401  logtayl  26405  abscxp2  26438  cxpcn3lem  26492  abscxpbnd  26498  cosangneg2d  26549  lawcoslem1  26557  lawcos  26558  pythag  26559  isosctrlem3  26562  ssscongptld  26564  chordthmlem3  26576  chordthmlem4  26577  chordthmlem5  26578  heron  26580  bndatandm  26671  efrlim  26711  rlimcxp  26715  o1cxp  26716  cxploglim2  26720  divsqrtsumo1  26725  fsumharmonic  26753  lgamgulmlem2  26771  lgamgulmlem3  26772  lgamgulmlem5  26774  lgambdd  26778  lgamucov  26779  lgamcvg2  26796  ftalem1  26814  ftalem2  26815  ftalem3  26816  ftalem4  26817  ftalem5  26818  ftalem7  26820  logfacbnd3  26963  logfacrlim  26964  logexprlim  26965  dchrabs  27000  lgsdirprm  27071  lgsdilem2  27073  lgsne0  27075  lgsabs1  27076  mul2sq  27159  2sqlem3  27160  2sqblem  27171  vmadivsumb  27223  rplogsumlem2  27225  dchrisumlem2  27230  dchrisumlem3  27231  dchrisum  27232  dchrmusum2  27234  dchrvmasumlem2  27238  dchrvmasumlem3  27239  dchrvmasumiflem1  27241  dchrvmasumiflem2  27242  dchrisum0flblem1  27248  dchrisum0fno1  27251  dchrisum0lem1b  27255  dchrisum0lem1  27256  dchrisum0lem2a  27257  dchrisum0lem2  27258  dchrisum0lem3  27259  mudivsum  27270  mulogsumlem  27271  mulog2sumlem1  27274  mulog2sumlem2  27275  2vmadivsumlem  27280  log2sumbnd  27284  selberglem2  27286  selbergb  27289  selberg2b  27292  chpdifbndlem1  27293  selberg3lem1  27297  selberg3lem2  27298  selberg4lem1  27300  pntrsumo1  27305  pntrsumbnd  27306  pntrsumbnd2  27307  pntrlog2bndlem1  27317  pntrlog2bndlem2  27318  pntrlog2bndlem3  27319  pntrlog2bndlem4  27320  pntrlog2bndlem5  27321  pntrlog2bndlem6  27323  pntrlog2bnd  27324  pntpbnd1a  27325  pntpbnd2  27327  pntibndlem2  27331  pntlemn  27340  pntlemj  27343  pntlemf  27345  pntlemo  27347  pntlem3  27349  pntleml  27351  smcnlem  30218  nmoub3i  30294  isblo3i  30322  htthlem  30438  bcs2  30703  pjhthlem1  30912  nmfnsetre  31398  nmfnleub2  31447  nmfnge0  31448  nmbdfnlbi  31570  nmcfnexi  31572  nmcfnlbi  31573  lnfnconi  31576  cnlnadjlem2  31589  cnlnadjlem7  31594  nmopcoadji  31622  leopnmid  31659  sqsscirc2  33188  subfaclim  34478  subfacval3  34479  sinccvglem  34956  dnicld1  35652  dnibndlem2  35659  dnibndlem6  35663  dnibndlem9  35666  dnibndlem12  35669  dnicn  35672  knoppcnlem4  35676  knoppcnlem6  35678  unblimceq0lem  35686  unblimceq0  35687  unbdqndv2lem1  35689  unbdqndv2lem2  35690  knoppndvlem11  35702  knoppndvlem12  35703  knoppndvlem14  35705  knoppndvlem15  35706  knoppndvlem17  35708  knoppndvlem18  35709  knoppndvlem20  35711  knoppndvlem21  35712  poimirlem29  36821  poimir  36825  iblabsnclem  36855  iblabsnc  36856  iblmulc2nc  36857  itgabsnc  36861  ftc1cnnclem  36863  ftc1anclem1  36865  ftc1anclem2  36866  ftc1anclem4  36868  ftc1anclem5  36869  ftc1anclem6  36870  ftc1anclem7  36871  ftc1anclem8  36872  ftc1anc  36873  ftc2nc  36874  dvasin  36876  areacirclem1  36880  areacirclem2  36881  areacirclem4  36883  areacirclem5  36884  areacirc  36885  geomcau  36931  cntotbnd  36968  rrndstprj1  37002  rrndstprj2  37003  ismrer1  37010  dffltz  41679  rencldnfilem  41861  irrapxlem2  41864  irrapxlem4  41866  irrapxlem5  41867  pellexlem2  41871  pellexlem6  41875  pell14qrgt0  41900  congabseq  42016  acongeq  42025  modabsdifz  42028  jm2.26lem3  42043  sqrtcvallem4  42693  extoimad  43219  imo72b2lem0  43220  imo72b2  43227  dvgrat  43374  cvgdvgrat  43375  radcnvrat  43376  dvconstbi  43396  binomcxplemnotnn0  43418  dstregt0  44290  absnpncan2d  44311  absnpncan3d  44316  abslt2sqd  44369  rexabslelem  44427  cvgcaule  44501  fprodabs2  44610  mullimc  44631  mullimcf  44638  limcrecl  44644  lptre2pt  44655  limcleqr  44659  addlimc  44663  0ellimcdiv  44664  limclner  44666  climleltrp  44691  climisp  44761  climxrrelem  44764  cnrefiisplem  44844  climxlim2lem  44860  cncficcgt0  44903  dvdivbd  44938  dvbdfbdioolem1  44943  dvbdfbdioolem2  44944  dvbdfbdioo  44945  ioodvbdlimc1lem1  44946  ioodvbdlimc1lem2  44947  ioodvbdlimc2lem  44949  stoweid  45078  fourierdlem30  45152  fourierdlem39  45161  fourierdlem42  45164  fourierdlem47  45168  fourierdlem68  45189  fourierdlem70  45191  fourierdlem71  45192  fourierdlem73  45194  fourierdlem77  45198  fourierdlem80  45201  fourierdlem83  45204  fourierdlem87  45208  fourierdlem103  45224  fourierdlem104  45225  etransclem23  45272  etransclem48  45297  rrndistlt  45305  ioorrnopnlem  45319  sge0isum  45442  hoicvr  45563  smflimlem4  45789  smfmullem1  45806  smfmullem2  45807  smfmullem3  45808  itsclc0yqsol  47538