Theorem abscld 15341

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

Syntax hints:   → wi 4   ∈ wcel 2111  ‘cfv 6476  ℂcc 10999  ℝcr 11000  abscabs 15136

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pow 5298  ax-pr 5365  ax-un 7663  ax-cnex 11057  ax-resscn 11058  ax-1cn 11059  ax-icn 11060  ax-addcl 11061  ax-addrcl 11062  ax-mulcl 11063  ax-mulrcl 11064  ax-mulcom 11065  ax-addass 11066  ax-mulass 11067  ax-distr 11068  ax-i2m1 11069  ax-1ne0 11070  ax-1rid 11071  ax-rnegex 11072  ax-rrecex 11073  ax-cnre 11074  ax-pre-lttri 11075  ax-pre-lttrn 11076  ax-pre-ltadd 11077  ax-pre-mulgt0 11078  ax-pre-sup 11079

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 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rmo 3346  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4279  df-if 4471  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-iun 4938  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5506  df-eprel 5511  df-po 5519  df-so 5520  df-fr 5564  df-we 5566  df-xp 5617  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-rn 5622  df-res 5623  df-ima 5624  df-pred 6243  df-ord 6304  df-on 6305  df-lim 6306  df-suc 6307  df-iota 6432  df-fun 6478  df-fn 6479  df-f 6480  df-f1 6481  df-fo 6482  df-f1o 6483  df-fv 6484  df-riota 7298  df-ov 7344  df-oprab 7345  df-mpo 7346  df-om 7792  df-2nd 7917  df-frecs 8206  df-wrecs 8237  df-recs 8286  df-rdg 8324  df-er 8617  df-en 8865  df-dom 8866  df-sdom 8867  df-sup 9321  df-pnf 11143  df-mnf 11144  df-xr 11145  df-ltxr 11146  df-le 11147  df-sub 11341  df-neg 11342  df-div 11770  df-nn 12121  df-2 12183  df-3 12184  df-n0 12377  df-z 12464  df-uz 12728  df-rp 12886  df-seq 13904  df-exp 13964  df-cj 15001  df-re 15002  df-im 15003  df-sqrt 15137  df-abs 15138

This theorem is referenced by:  bhmafibid1  15370  lo1bddrp  15427  elo1mpt  15436  elo1mpt2  15437  elo1d  15438  o1bdd2  15443  o1bddrp  15444  rlimuni  15452  climuni  15454  o1eq  15472  rlimcld2  15480  rlimrege0  15481  climabs0  15487  mulcn2  15498  reccn2  15499  cn1lem  15500  cjcn2  15502  o1add  15516  o1mul  15517  o1sub  15518  rlimo1  15519  o1rlimmul  15521  climsqz  15543  climsqz2  15544  rlimsqzlem  15551  o1le  15555  climbdd  15574  caucvgrlem  15575  caucvgrlem2  15577  iseraltlem3  15586  iseralt  15587  fsumabs  15703  o1fsum  15715  iserabs  15717  cvgcmpce  15720  abscvgcvg  15721  divrcnv  15754  explecnv  15767  geomulcvg  15778  cvgrat  15785  mertenslem1  15786  mertenslem2  15787  fprodabs  15876  efcllem  15979  efaddlem  15995  eftlub  16013  ef01bndlem  16088  sin01bnd  16089  cos01bnd  16090  absef  16101  dvdsabseq  16219  alzdvds  16226  sqnprm  16608  pclem  16745  mul4sqlem  16860  xrsdsreclb  21345  gzrngunitlem  21364  gzrngunit  21365  prmirredlem  21404  nm2dif  24535  blcvx  24708  recld2  24725  addcnlem  24775  cnheiborlem  24875  cnheibor  24876  cnllycmp  24877  cphsqrtcl2  25108  ipcau2  25156  tcphcphlem1  25157  ipcnlem2  25166  cncmet  25244  trirn  25322  rrxdstprj1  25331  pjthlem1  25359  volsup2  25528  mbfi1fseqlem6  25643  iblabslem  25751  iblabs  25752  iblabsr  25753  iblmulc2  25754  itgabs  25758  bddmulibl  25762  bddiblnc  25765  itgcn  25768  dveflem  25905  dvlip  25920  dvlipcn  25921  c1liplem1  25923  dveq0  25927  dv11cn  25928  lhop1lem  25940  dvfsumabs  25951  dvfsumrlim  25960  dvfsumrlim2  25961  ftc1a  25966  ftc1lem4  25968  plyeq0lem  26137  aalioulem2  26263  aalioulem3  26264  aalioulem4  26265  aalioulem5  26266  aalioulem6  26267  aaliou  26268  geolim3  26269  aaliou2b  26271  aaliou3lem9  26280  ulmbdd  26329  ulmcn  26330  ulmdvlem1  26331  mtest  26335  mtestbdd  26336  iblulm  26338  itgulm  26339  radcnvlem1  26344  radcnvlem2  26345  radcnvlt1  26349  radcnvle  26351  dvradcnv  26352  pserulm  26353  psercnlem2  26356  psercnlem1  26357  psercn  26358  pserdvlem1  26359  pserdvlem2  26360  pserdv  26361  abelthlem2  26364  abelthlem3  26365  abelthlem5  26367  abelthlem7  26370  abelthlem8  26371  tanregt0  26470  efif1olem3  26475  efif1olem4  26476  eff1olem  26479  cosargd  26539  cosarg0d  26540  argregt0  26541  argrege0  26542  abslogle  26549  logcnlem3  26575  logcnlem4  26576  efopnlem1  26587  logtayl  26591  abscxp2  26624  cxpcn3lem  26679  abscxpbnd  26685  cosangneg2d  26739  lawcoslem1  26747  lawcos  26748  pythag  26749  isosctrlem3  26752  ssscongptld  26754  chordthmlem3  26766  chordthmlem4  26767  chordthmlem5  26768  heron  26770  bndatandm  26861  efrlim  26901  efrlimOLD  26902  rlimcxp  26906  o1cxp  26907  cxploglim2  26911  divsqrtsumo1  26916  fsumharmonic  26944  lgamgulmlem2  26962  lgamgulmlem3  26963  lgamgulmlem5  26965  lgambdd  26969  lgamucov  26970  lgamcvg2  26987  ftalem1  27005  ftalem2  27006  ftalem3  27007  ftalem4  27008  ftalem5  27009  ftalem7  27011  logfacbnd3  27156  logfacrlim  27157  logexprlim  27158  dchrabs  27193  lgsdirprm  27264  lgsdilem2  27266  lgsne0  27268  lgsabs1  27269  mul2sq  27352  2sqlem3  27353  2sqblem  27364  vmadivsumb  27416  rplogsumlem2  27418  dchrisumlem2  27423  dchrisumlem3  27424  dchrisum  27425  dchrmusum2  27427  dchrvmasumlem2  27431  dchrvmasumlem3  27432  dchrvmasumiflem1  27434  dchrvmasumiflem2  27435  dchrisum0flblem1  27441  dchrisum0fno1  27444  dchrisum0lem1b  27448  dchrisum0lem1  27449  dchrisum0lem2a  27450  dchrisum0lem2  27451  dchrisum0lem3  27452  mudivsum  27463  mulogsumlem  27464  mulog2sumlem1  27467  mulog2sumlem2  27468  2vmadivsumlem  27473  log2sumbnd  27477  selberglem2  27479  selbergb  27482  selberg2b  27485  chpdifbndlem1  27486  selberg3lem1  27490  selberg3lem2  27491  selberg4lem1  27493  pntrsumo1  27498  pntrsumbnd  27499  pntrsumbnd2  27500  pntrlog2bndlem1  27510  pntrlog2bndlem2  27511  pntrlog2bndlem3  27512  pntrlog2bndlem4  27513  pntrlog2bndlem5  27514  pntrlog2bndlem6  27516  pntrlog2bnd  27517  pntpbnd1a  27518  pntpbnd2  27520  pntibndlem2  27524  pntlemn  27533  pntlemj  27536  pntlemf  27538  pntlemo  27540  pntlem3  27542  pntleml  27544  smcnlem  30669  nmoub3i  30745  isblo3i  30773  htthlem  30889  bcs2  31154  pjhthlem1  31363  nmfnsetre  31849  nmfnleub2  31898  nmfnge0  31899  nmbdfnlbi  32021  nmcfnexi  32023  nmcfnlbi  32024  lnfnconi  32027  cnlnadjlem2  32040  cnlnadjlem7  32045  nmopcoadji  32073  leopnmid  32110  constrdircl  33770  iconstr  33771  constrremulcl  33772  constrimcl  33775  constrmulcl  33776  constrinvcl  33778  constrabscl  33783  constrsqrtcl  33784  sqsscirc2  33914  subfaclim  35224  subfacval3  35225  sinccvglem  35708  dnicld1  36506  dnibndlem2  36513  dnibndlem6  36517  dnibndlem9  36520  dnibndlem12  36523  dnicn  36526  knoppcnlem4  36530  knoppcnlem6  36532  unblimceq0lem  36540  unblimceq0  36541  unbdqndv2lem1  36543  unbdqndv2lem2  36544  knoppndvlem11  36556  knoppndvlem12  36557  knoppndvlem14  36559  knoppndvlem15  36560  knoppndvlem17  36562  knoppndvlem18  36563  knoppndvlem20  36565  knoppndvlem21  36566  poimirlem29  37689  poimir  37693  iblabsnclem  37723  iblabsnc  37724  iblmulc2nc  37725  itgabsnc  37729  ftc1cnnclem  37731  ftc1anclem1  37733  ftc1anclem2  37734  ftc1anclem4  37736  ftc1anclem5  37737  ftc1anclem6  37738  ftc1anclem7  37739  ftc1anclem8  37740  ftc1anc  37741  ftc2nc  37742  dvasin  37744  areacirclem1  37748  areacirclem2  37749  areacirclem4  37751  areacirclem5  37752  areacirc  37753  geomcau  37799  cntotbnd  37836  rrndstprj1  37870  rrndstprj2  37871  ismrer1  37878  readvrec  42395  readvcot  42397  dffltz  42667  rencldnfilem  42853  irrapxlem2  42856  irrapxlem4  42858  irrapxlem5  42859  pellexlem2  42863  pellexlem6  42867  pell14qrgt0  42892  congabseq  43007  acongeq  43016  modabsdifz  43019  jm2.26lem3  43034  sqrtcvallem4  43672  extoimad  44197  imo72b2lem0  44198  imo72b2  44205  dvgrat  44345  cvgdvgrat  44346  radcnvrat  44347  dvconstbi  44367  binomcxplemnotnn0  44389  dstregt0  45323  absnpncan2d  45343  absnpncan3d  45348  abslt2sqd  45399  rexabslelem  45456  cvgcaule  45529  fprodabs2  45635  mullimc  45656  mullimcf  45663  limcrecl  45669  lptre2pt  45678  limcleqr  45682  addlimc  45686  0ellimcdiv  45687  limclner  45689  climleltrp  45714  climisp  45784  climxrrelem  45787  cnrefiisplem  45867  climxlim2lem  45883  cncficcgt0  45926  dvdivbd  45961  dvbdfbdioolem1  45966  dvbdfbdioolem2  45967  dvbdfbdioo  45968  ioodvbdlimc1lem1  45969  ioodvbdlimc1lem2  45970  ioodvbdlimc2lem  45972  stoweid  46101  fourierdlem30  46175  fourierdlem39  46184  fourierdlem42  46187  fourierdlem47  46191  fourierdlem68  46212  fourierdlem70  46214  fourierdlem71  46215  fourierdlem73  46217  fourierdlem77  46221  fourierdlem80  46224  fourierdlem83  46227  fourierdlem87  46231  fourierdlem103  46247  fourierdlem104  46248  etransclem23  46295  etransclem48  46320  rrndistlt  46328  ioorrnopnlem  46342  sge0isum  46465  hoicvr  46586  smflimlem4  46812  smfmullem1  46829  smfmullem2  46830  smfmullem3  46831  modlt0b  47394  itsclc0yqsol  48796