Theorem abscld 15157

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

Syntax hints:   → wi 4   ∈ wcel 2107  ‘cfv 6437  ℂcc 10878  ℝcr 10879  abscabs 14954

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-cnex 10936  ax-resscn 10937  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-addrcl 10941  ax-mulcl 10942  ax-mulrcl 10943  ax-mulcom 10944  ax-addass 10945  ax-mulass 10946  ax-distr 10947  ax-i2m1 10948  ax-1ne0 10949  ax-1rid 10950  ax-rnegex 10951  ax-rrecex 10952  ax-cnre 10953  ax-pre-lttri 10954  ax-pre-lttrn 10955  ax-pre-ltadd 10956  ax-pre-mulgt0 10957  ax-pre-sup 10958

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-rmo 3072  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6206  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-riota 7241  df-ov 7287  df-oprab 7288  df-mpo 7289  df-om 7722  df-2nd 7841  df-frecs 8106  df-wrecs 8137  df-recs 8211  df-rdg 8250  df-er 8507  df-en 8743  df-dom 8744  df-sdom 8745  df-sup 9210  df-pnf 11020  df-mnf 11021  df-xr 11022  df-ltxr 11023  df-le 11024  df-sub 11216  df-neg 11217  df-div 11642  df-nn 11983  df-2 12045  df-3 12046  df-n0 12243  df-z 12329  df-uz 12592  df-rp 12740  df-seq 13731  df-exp 13792  df-cj 14819  df-re 14820  df-im 14821  df-sqrt 14955  df-abs 14956

This theorem is referenced by:  bhmafibid1  15186  lo1bddrp  15243  elo1mpt  15252  elo1mpt2  15253  elo1d  15254  o1bdd2  15259  o1bddrp  15260  rlimuni  15268  climuni  15270  o1eq  15288  rlimcld2  15296  rlimrege0  15297  climabs0  15303  mulcn2  15314  reccn2  15315  cn1lem  15316  cjcn2  15318  o1add  15332  o1mul  15333  o1sub  15334  rlimo1  15335  o1rlimmul  15337  climsqz  15359  climsqz2  15360  rlimsqzlem  15369  o1le  15373  climbdd  15392  caucvgrlem  15393  caucvgrlem2  15395  iseraltlem3  15404  iseralt  15405  fsumabs  15522  o1fsum  15534  iserabs  15536  cvgcmpce  15539  abscvgcvg  15540  divrcnv  15573  explecnv  15586  geomulcvg  15597  cvgrat  15604  mertenslem1  15605  mertenslem2  15606  fprodabs  15693  efcllem  15796  efaddlem  15811  eftlub  15827  ef01bndlem  15902  sin01bnd  15903  cos01bnd  15904  absef  15915  dvdsabseq  16031  alzdvds  16038  sqnprm  16416  pclem  16548  mul4sqlem  16663  xrsdsreclb  20654  gzrngunitlem  20672  gzrngunit  20673  prmirredlem  20703  nm2dif  23790  blcvx  23970  recld2  23986  addcnlem  24036  cnheiborlem  24126  cnheibor  24127  cnllycmp  24128  cphsqrtcl2  24359  ipcau2  24407  tcphcphlem1  24408  ipcnlem2  24417  cncmet  24495  trirn  24573  rrxdstprj1  24582  pjthlem1  24610  volsup2  24778  mbfi1fseqlem6  24894  iblabslem  25001  iblabs  25002  iblabsr  25003  iblmulc2  25004  itgabs  25008  bddmulibl  25012  bddiblnc  25015  itgcn  25018  dveflem  25152  dvlip  25166  dvlipcn  25167  c1liplem1  25169  dveq0  25173  dv11cn  25174  lhop1lem  25186  dvfsumabs  25196  dvfsumrlim  25204  dvfsumrlim2  25205  ftc1a  25210  ftc1lem4  25212  plyeq0lem  25380  aalioulem2  25502  aalioulem3  25503  aalioulem4  25504  aalioulem5  25505  aalioulem6  25506  aaliou  25507  geolim3  25508  aaliou2b  25510  aaliou3lem9  25519  ulmbdd  25566  ulmcn  25567  ulmdvlem1  25568  mtest  25572  mtestbdd  25573  iblulm  25575  itgulm  25576  radcnvlem1  25581  radcnvlem2  25582  radcnvlt1  25586  radcnvle  25588  dvradcnv  25589  pserulm  25590  psercnlem2  25592  psercnlem1  25593  psercn  25594  pserdvlem1  25595  pserdvlem2  25596  pserdv  25597  abelthlem2  25600  abelthlem3  25601  abelthlem5  25603  abelthlem7  25606  abelthlem8  25607  tanregt0  25704  efif1olem3  25709  efif1olem4  25710  eff1olem  25713  cosargd  25772  cosarg0d  25773  argregt0  25774  argrege0  25775  abslogle  25782  logcnlem3  25808  logcnlem4  25809  efopnlem1  25820  logtayl  25824  abscxp2  25857  cxpcn3lem  25909  abscxpbnd  25915  cosangneg2d  25966  lawcoslem1  25974  lawcos  25975  pythag  25976  isosctrlem3  25979  ssscongptld  25981  chordthmlem3  25993  chordthmlem4  25994  chordthmlem5  25995  heron  25997  bndatandm  26088  efrlim  26128  rlimcxp  26132  o1cxp  26133  cxploglim2  26137  divsqrtsumo1  26142  fsumharmonic  26170  lgamgulmlem2  26188  lgamgulmlem3  26189  lgamgulmlem5  26191  lgambdd  26195  lgamucov  26196  lgamcvg2  26213  ftalem1  26231  ftalem2  26232  ftalem3  26233  ftalem4  26234  ftalem5  26235  ftalem7  26237  logfacbnd3  26380  logfacrlim  26381  logexprlim  26382  dchrabs  26417  lgsdirprm  26488  lgsdilem2  26490  lgsne0  26492  lgsabs1  26493  mul2sq  26576  2sqlem3  26577  2sqblem  26588  vmadivsumb  26640  rplogsumlem2  26642  dchrisumlem2  26647  dchrisumlem3  26648  dchrisum  26649  dchrmusum2  26651  dchrvmasumlem2  26655  dchrvmasumlem3  26656  dchrvmasumiflem1  26658  dchrvmasumiflem2  26659  dchrisum0flblem1  26665  dchrisum0fno1  26668  dchrisum0lem1b  26672  dchrisum0lem1  26673  dchrisum0lem2a  26674  dchrisum0lem2  26675  dchrisum0lem3  26676  mudivsum  26687  mulogsumlem  26688  mulog2sumlem1  26691  mulog2sumlem2  26692  2vmadivsumlem  26697  log2sumbnd  26701  selberglem2  26703  selbergb  26706  selberg2b  26709  chpdifbndlem1  26710  selberg3lem1  26714  selberg3lem2  26715  selberg4lem1  26717  pntrsumo1  26722  pntrsumbnd  26723  pntrsumbnd2  26724  pntrlog2bndlem1  26734  pntrlog2bndlem2  26735  pntrlog2bndlem3  26736  pntrlog2bndlem4  26737  pntrlog2bndlem5  26738  pntrlog2bndlem6  26740  pntrlog2bnd  26741  pntpbnd1a  26742  pntpbnd2  26744  pntibndlem2  26748  pntlemn  26757  pntlemj  26760  pntlemf  26762  pntlemo  26764  pntlem3  26766  pntleml  26768  smcnlem  29068  nmoub3i  29144  isblo3i  29172  htthlem  29288  bcs2  29553  pjhthlem1  29762  nmfnsetre  30248  nmfnleub2  30297  nmfnge0  30298  nmbdfnlbi  30420  nmcfnexi  30422  nmcfnlbi  30423  lnfnconi  30426  cnlnadjlem2  30439  cnlnadjlem7  30444  nmopcoadji  30472  leopnmid  30509  sqsscirc2  31868  subfaclim  33159  subfacval3  33160  sinccvglem  33639  dnicld1  34661  dnibndlem2  34668  dnibndlem6  34672  dnibndlem9  34675  dnibndlem12  34678  dnicn  34681  knoppcnlem4  34685  knoppcnlem6  34687  unblimceq0lem  34695  unblimceq0  34696  unbdqndv2lem1  34698  unbdqndv2lem2  34699  knoppndvlem11  34711  knoppndvlem12  34712  knoppndvlem14  34714  knoppndvlem15  34715  knoppndvlem17  34717  knoppndvlem18  34718  knoppndvlem20  34720  knoppndvlem21  34721  poimirlem29  35815  poimir  35819  iblabsnclem  35849  iblabsnc  35850  iblmulc2nc  35851  itgabsnc  35855  ftc1cnnclem  35857  ftc1anclem1  35859  ftc1anclem2  35860  ftc1anclem4  35862  ftc1anclem5  35863  ftc1anclem6  35864  ftc1anclem7  35865  ftc1anclem8  35866  ftc1anc  35867  ftc2nc  35868  dvasin  35870  areacirclem1  35874  areacirclem2  35875  areacirclem4  35877  areacirclem5  35878  areacirc  35879  geomcau  35926  cntotbnd  35963  rrndstprj1  35997  rrndstprj2  35998  ismrer1  36005  dffltz  40478  rencldnfilem  40649  irrapxlem2  40652  irrapxlem4  40654  irrapxlem5  40655  pellexlem2  40659  pellexlem6  40663  pell14qrgt0  40688  congabseq  40803  acongeq  40812  modabsdifz  40815  jm2.26lem3  40830  sqrtcvallem4  41254  extoimad  41782  imo72b2lem0  41783  imo72b2  41790  dvgrat  41937  cvgdvgrat  41938  radcnvrat  41939  dvconstbi  41959  binomcxplemnotnn0  41981  dstregt0  42827  absnpncan2d  42848  absnpncan3d  42853  abslt2sqd  42906  rexabslelem  42965  fprodabs2  43143  mullimc  43164  mullimcf  43171  limcrecl  43177  lptre2pt  43188  limcleqr  43192  addlimc  43196  0ellimcdiv  43197  limclner  43199  climleltrp  43224  climisp  43294  climxrrelem  43297  cnrefiisplem  43377  climxlim2lem  43393  cncficcgt0  43436  dvdivbd  43471  dvbdfbdioolem1  43476  dvbdfbdioolem2  43477  dvbdfbdioo  43478  ioodvbdlimc1lem1  43479  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  stoweid  43611  fourierdlem30  43685  fourierdlem39  43694  fourierdlem42  43697  fourierdlem47  43701  fourierdlem68  43722  fourierdlem70  43724  fourierdlem71  43725  fourierdlem73  43727  fourierdlem77  43731  fourierdlem80  43734  fourierdlem83  43737  fourierdlem87  43741  fourierdlem103  43757  fourierdlem104  43758  etransclem23  43805  etransclem48  43830  rrndistlt  43838  ioorrnopnlem  43852  sge0isum  43972  hoicvr  44093  smflimlem4  44319  smfmullem1  44336  smfmullem2  44337  smfmullem3  44338  itsclc0yqsol  46121