Theorem abscld 14583

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

Syntax hints:   → wi 4   ∈ wcel 2106  ‘cfv 6135  ℂcc 10270  ℝcr 10271  abscabs 14381

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-8 2108  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-cnex 10328  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348  ax-pre-mulgt0 10349  ax-pre-sup 10350

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2550  df-eu 2586  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ne 2969  df-nel 3075  df-ral 3094  df-rex 3095  df-reu 3096  df-rmo 3097  df-rab 3098  df-v 3399  df-sbc 3652  df-csb 3751  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-pss 3807  df-nul 4141  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4672  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-om 7344  df-2nd 7446  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-er 8026  df-en 8242  df-dom 8243  df-sdom 8244  df-sup 8636  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-sub 10608  df-neg 10609  df-div 11033  df-nn 11375  df-2 11438  df-3 11439  df-n0 11643  df-z 11729  df-uz 11993  df-rp 12138  df-seq 13120  df-exp 13179  df-cj 14246  df-re 14247  df-im 14248  df-sqrt 14382  df-abs 14383

This theorem is referenced by:  lo1bddrp  14664  elo1mpt  14673  elo1mpt2  14674  elo1d  14675  o1bdd2  14680  o1bddrp  14681  rlimuni  14689  climuni  14691  o1eq  14709  rlimcld2  14717  rlimrege0  14718  climabs0  14724  mulcn2  14734  reccn2  14735  cn1lem  14736  cjcn2  14738  o1add  14752  o1mul  14753  o1sub  14754  rlimo1  14755  o1rlimmul  14757  climsqz  14779  climsqz2  14780  rlimsqzlem  14787  o1le  14791  climbdd  14810  caucvgrlem  14811  caucvgrlem2  14813  iseraltlem3  14822  iseralt  14823  fsumabs  14937  o1fsum  14949  iserabs  14951  cvgcmpce  14954  abscvgcvg  14955  divrcnv  14988  explecnv  15001  geomulcvg  15011  cvgrat  15018  mertenslem1  15019  mertenslem2  15020  fprodabs  15107  efcllem  15210  efaddlem  15225  eftlub  15241  ef01bndlem  15316  sin01bnd  15317  cos01bnd  15318  absef  15329  dvdsabseq  15442  alzdvds  15449  sqnprm  15818  pclem  15947  mul4sqlem  16061  xrsdsreclb  20189  gzrngunitlem  20207  gzrngunit  20208  prmirredlem  20237  nm2dif  22837  blcvx  23009  recld2  23025  addcnlem  23075  cnheiborlem  23161  cnheibor  23162  cnllycmp  23163  cphsqrtcl2  23393  ipcau2  23440  tcphcphlem1  23441  ipcnlem2  23450  cncmet  23528  trirn  23606  rrxdstprj1  23615  pjthlem1  23643  volsup2  23809  mbfi1fseqlem6  23924  iblabslem  24031  iblabs  24032  iblabsr  24033  iblmulc2  24034  itgabs  24038  bddmulibl  24042  itgcn  24046  dveflem  24179  dvlip  24193  dvlipcn  24194  c1liplem1  24196  dveq0  24200  dv11cn  24201  lhop1lem  24213  dvfsumabs  24223  dvfsumrlim  24231  dvfsumrlim2  24232  ftc1a  24237  ftc1lem4  24239  plyeq0lem  24403  aalioulem2  24525  aalioulem3  24526  aalioulem4  24527  aalioulem5  24528  aalioulem6  24529  aaliou  24530  geolim3  24531  aaliou2b  24533  aaliou3lem9  24542  ulmbdd  24589  ulmcn  24590  ulmdvlem1  24591  mtest  24595  mtestbdd  24596  iblulm  24598  itgulm  24599  radcnvlem1  24604  radcnvlem2  24605  radcnvlt1  24609  radcnvle  24611  dvradcnv  24612  pserulm  24613  psercnlem2  24615  psercnlem1  24616  psercn  24617  pserdvlem1  24618  pserdvlem2  24619  pserdv  24620  abelthlem2  24623  abelthlem3  24624  abelthlem5  24626  abelthlem7  24629  abelthlem8  24630  tanregt0  24723  efif1olem3  24728  efif1olem4  24729  eff1olem  24732  cosargd  24791  cosarg0d  24792  argrege0  24794  abslogle  24801  logcnlem3  24827  logcnlem4  24828  efopnlem1  24839  logtayl  24843  abscxp2  24876  cxpcn3lem  24928  abscxpbnd  24934  cosangneg2d  24985  lawcoslem1  24993  lawcos  24994  pythag  24995  isosctrlem3  24998  ssscongptld  25000  chordthmlem3  25012  chordthmlem4  25013  chordthmlem5  25014  heron  25016  bndatandm  25107  efrlim  25148  rlimcxp  25152  o1cxp  25153  cxploglim2  25157  divsqrtsumo1  25162  fsumharmonic  25190  lgamgulmlem2  25208  lgamgulmlem3  25209  lgamgulmlem5  25211  lgambdd  25215  lgamucov  25216  lgamcvg2  25233  ftalem1  25251  ftalem2  25252  ftalem3  25253  ftalem4  25254  ftalem5  25255  ftalem7  25257  logfacbnd3  25400  logfacrlim  25401  logexprlim  25402  dchrabs  25437  lgsdirprm  25508  lgsdilem2  25510  lgsne0  25512  lgsabs1  25513  mul2sq  25596  2sqlem3  25597  2sqblem  25608  vmadivsumb  25624  rplogsumlem2  25626  dchrisumlem2  25631  dchrisumlem3  25632  dchrisum  25633  dchrmusum2  25635  dchrvmasumlem2  25639  dchrvmasumlem3  25640  dchrvmasumiflem1  25642  dchrvmasumiflem2  25643  dchrisum0flblem1  25649  dchrisum0fno1  25652  dchrisum0lem1b  25656  dchrisum0lem1  25657  dchrisum0lem2a  25658  dchrisum0lem2  25659  dchrisum0lem3  25660  mudivsum  25671  mulogsumlem  25672  mulog2sumlem1  25675  mulog2sumlem2  25676  2vmadivsumlem  25681  log2sumbnd  25685  selberglem2  25687  selbergb  25690  selberg2b  25693  chpdifbndlem1  25694  selberg3lem1  25698  selberg3lem2  25699  selberg4lem1  25701  pntrsumo1  25706  pntrsumbnd  25707  pntrsumbnd2  25708  pntrlog2bndlem1  25718  pntrlog2bndlem2  25719  pntrlog2bndlem3  25720  pntrlog2bndlem4  25721  pntrlog2bndlem5  25722  pntrlog2bndlem6  25724  pntrlog2bnd  25725  pntpbnd1a  25726  pntpbnd2  25728  pntibndlem2  25732  pntlemn  25741  pntlemj  25744  pntlemf  25746  pntlemo  25748  pntlem3  25750  pntleml  25752  smcnlem  28124  nmoub3i  28200  isblo3i  28228  htthlem  28346  bcs2  28611  pjhthlem1  28822  nmfnsetre  29308  nmfnleub2  29357  nmfnge0  29358  nmbdfnlbi  29480  nmcfnexi  29482  nmcfnlbi  29483  lnfnconi  29486  cnlnadjlem2  29499  cnlnadjlem7  29504  nmopcoadji  29532  leopnmid  29569  bhmafibid1  30206  sqsscirc2  30553  subfaclim  31769  subfacval3  31770  sinccvglem  32163  dnicld1  33045  dnibndlem2  33052  dnibndlem6  33056  dnibndlem9  33059  dnibndlem12  33062  dnicn  33065  knoppcnlem4  33069  knoppcnlem6  33071  unblimceq0lem  33079  unblimceq0  33080  unbdqndv2lem1  33082  unbdqndv2lem2  33083  knoppndvlem11  33095  knoppndvlem12  33096  knoppndvlem14  33098  knoppndvlem15  33099  knoppndvlem17  33101  knoppndvlem18  33102  knoppndvlem20  33104  knoppndvlem21  33105  poimirlem29  34048  poimir  34052  iblabsnclem  34082  iblabsnc  34083  iblmulc2nc  34084  itgabsnc  34088  bddiblnc  34089  ftc1cnnclem  34092  ftc1anclem1  34094  ftc1anclem2  34095  ftc1anclem4  34097  ftc1anclem5  34098  ftc1anclem6  34099  ftc1anclem7  34100  ftc1anclem8  34101  ftc1anc  34102  ftc2nc  34103  dvasin  34105  areacirclem1  34109  areacirclem2  34110  areacirclem4  34112  areacirclem5  34113  areacirc  34114  geomcau  34163  cntotbnd  34203  rrndstprj1  34237  rrndstprj2  34238  ismrer1  34245  dffltz  38195  rencldnfilem  38326  irrapxlem2  38329  irrapxlem4  38331  irrapxlem5  38332  pellexlem2  38336  pellexlem6  38340  pell14qrgt0  38365  congabseq  38482  acongeq  38491  modabsdifz  38494  jm2.26lem3  38509  extoimad  39402  imo72b2lem0  39403  imo72b2  39413  dvgrat  39449  cvgdvgrat  39450  radcnvrat  39451  dvconstbi  39471  binomcxplemnotnn0  39493  dstregt0  40385  absnpncan2d  40407  absnpncan3d  40412  abslt2sqd  40466  rexabslelem  40533  fprodabs2  40717  mullimc  40738  mullimcf  40745  limcrecl  40751  lptre2pt  40762  limcleqr  40766  addlimc  40770  0ellimcdiv  40771  limclner  40773  climleltrp  40798  climisp  40868  climxrrelem  40871  cnrefiisplem  40951  climxlim2lem  40967  cncficcgt0  41011  dvdivbd  41048  dvbdfbdioolem1  41053  dvbdfbdioolem2  41054  dvbdfbdioo  41055  ioodvbdlimc1lem1  41056  ioodvbdlimc1lem2  41057  ioodvbdlimc2lem  41059  stoweid  41189  fourierdlem30  41263  fourierdlem39  41272  fourierdlem42  41275  fourierdlem47  41279  fourierdlem68  41300  fourierdlem70  41302  fourierdlem71  41303  fourierdlem73  41305  fourierdlem77  41309  fourierdlem80  41312  fourierdlem83  41315  fourierdlem87  41319  fourierdlem103  41335  fourierdlem104  41336  etransclem23  41383  etransclem48  41408  rrndistlt  41416  ioorrnopnlem  41430  sge0isum  41550  hoicvr  41671  smflimlem4  41891  smfmullem1  41907  smfmullem2  41908  smfmullem3  41909  itsclc0yqsol  43482