Theorem abscld 15383

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

Syntax hints:   → wi 4   ∈ wcel 2107  ‘cfv 6544  ℂcc 11108  ℝcr 11109  abscabs 15181

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 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187  ax-pre-sup 11188

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-er 8703  df-en 8940  df-dom 8941  df-sdom 8942  df-sup 9437  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-div 11872  df-nn 12213  df-2 12275  df-3 12276  df-n0 12473  df-z 12559  df-uz 12823  df-rp 12975  df-seq 13967  df-exp 14028  df-cj 15046  df-re 15047  df-im 15048  df-sqrt 15182  df-abs 15183

This theorem is referenced by:  bhmafibid1  15412  lo1bddrp  15469  elo1mpt  15478  elo1mpt2  15479  elo1d  15480  o1bdd2  15485  o1bddrp  15486  rlimuni  15494  climuni  15496  o1eq  15514  rlimcld2  15522  rlimrege0  15523  climabs0  15529  mulcn2  15540  reccn2  15541  cn1lem  15542  cjcn2  15544  o1add  15558  o1mul  15559  o1sub  15560  rlimo1  15561  o1rlimmul  15563  climsqz  15585  climsqz2  15586  rlimsqzlem  15595  o1le  15599  climbdd  15618  caucvgrlem  15619  caucvgrlem2  15621  iseraltlem3  15630  iseralt  15631  fsumabs  15747  o1fsum  15759  iserabs  15761  cvgcmpce  15764  abscvgcvg  15765  divrcnv  15798  explecnv  15811  geomulcvg  15822  cvgrat  15829  mertenslem1  15830  mertenslem2  15831  fprodabs  15918  efcllem  16021  efaddlem  16036  eftlub  16052  ef01bndlem  16127  sin01bnd  16128  cos01bnd  16129  absef  16140  dvdsabseq  16256  alzdvds  16263  sqnprm  16639  pclem  16771  mul4sqlem  16886  xrsdsreclb  20992  gzrngunitlem  21010  gzrngunit  21011  prmirredlem  21042  nm2dif  24134  blcvx  24314  recld2  24330  addcnlem  24380  cnheiborlem  24470  cnheibor  24471  cnllycmp  24472  cphsqrtcl2  24703  ipcau2  24751  tcphcphlem1  24752  ipcnlem2  24761  cncmet  24839  trirn  24917  rrxdstprj1  24926  pjthlem1  24954  volsup2  25122  mbfi1fseqlem6  25238  iblabslem  25345  iblabs  25346  iblabsr  25347  iblmulc2  25348  itgabs  25352  bddmulibl  25356  bddiblnc  25359  itgcn  25362  dveflem  25496  dvlip  25510  dvlipcn  25511  c1liplem1  25513  dveq0  25517  dv11cn  25518  lhop1lem  25530  dvfsumabs  25540  dvfsumrlim  25548  dvfsumrlim2  25549  ftc1a  25554  ftc1lem4  25556  plyeq0lem  25724  aalioulem2  25846  aalioulem3  25847  aalioulem4  25848  aalioulem5  25849  aalioulem6  25850  aaliou  25851  geolim3  25852  aaliou2b  25854  aaliou3lem9  25863  ulmbdd  25910  ulmcn  25911  ulmdvlem1  25912  mtest  25916  mtestbdd  25917  iblulm  25919  itgulm  25920  radcnvlem1  25925  radcnvlem2  25926  radcnvlt1  25930  radcnvle  25932  dvradcnv  25933  pserulm  25934  psercnlem2  25936  psercnlem1  25937  psercn  25938  pserdvlem1  25939  pserdvlem2  25940  pserdv  25941  abelthlem2  25944  abelthlem3  25945  abelthlem5  25947  abelthlem7  25950  abelthlem8  25951  tanregt0  26048  efif1olem3  26053  efif1olem4  26054  eff1olem  26057  cosargd  26116  cosarg0d  26117  argregt0  26118  argrege0  26119  abslogle  26126  logcnlem3  26152  logcnlem4  26153  efopnlem1  26164  logtayl  26168  abscxp2  26201  cxpcn3lem  26255  abscxpbnd  26261  cosangneg2d  26312  lawcoslem1  26320  lawcos  26321  pythag  26322  isosctrlem3  26325  ssscongptld  26327  chordthmlem3  26339  chordthmlem4  26340  chordthmlem5  26341  heron  26343  bndatandm  26434  efrlim  26474  rlimcxp  26478  o1cxp  26479  cxploglim2  26483  divsqrtsumo1  26488  fsumharmonic  26516  lgamgulmlem2  26534  lgamgulmlem3  26535  lgamgulmlem5  26537  lgambdd  26541  lgamucov  26542  lgamcvg2  26559  ftalem1  26577  ftalem2  26578  ftalem3  26579  ftalem4  26580  ftalem5  26581  ftalem7  26583  logfacbnd3  26726  logfacrlim  26727  logexprlim  26728  dchrabs  26763  lgsdirprm  26834  lgsdilem2  26836  lgsne0  26838  lgsabs1  26839  mul2sq  26922  2sqlem3  26923  2sqblem  26934  vmadivsumb  26986  rplogsumlem2  26988  dchrisumlem2  26993  dchrisumlem3  26994  dchrisum  26995  dchrmusum2  26997  dchrvmasumlem2  27001  dchrvmasumlem3  27002  dchrvmasumiflem1  27004  dchrvmasumiflem2  27005  dchrisum0flblem1  27011  dchrisum0fno1  27014  dchrisum0lem1b  27018  dchrisum0lem1  27019  dchrisum0lem2a  27020  dchrisum0lem2  27021  dchrisum0lem3  27022  mudivsum  27033  mulogsumlem  27034  mulog2sumlem1  27037  mulog2sumlem2  27038  2vmadivsumlem  27043  log2sumbnd  27047  selberglem2  27049  selbergb  27052  selberg2b  27055  chpdifbndlem1  27056  selberg3lem1  27060  selberg3lem2  27061  selberg4lem1  27063  pntrsumo1  27068  pntrsumbnd  27069  pntrsumbnd2  27070  pntrlog2bndlem1  27080  pntrlog2bndlem2  27081  pntrlog2bndlem3  27082  pntrlog2bndlem4  27083  pntrlog2bndlem5  27084  pntrlog2bndlem6  27086  pntrlog2bnd  27087  pntpbnd1a  27088  pntpbnd2  27090  pntibndlem2  27094  pntlemn  27103  pntlemj  27106  pntlemf  27108  pntlemo  27110  pntlem3  27112  pntleml  27114  smcnlem  29950  nmoub3i  30026  isblo3i  30054  htthlem  30170  bcs2  30435  pjhthlem1  30644  nmfnsetre  31130  nmfnleub2  31179  nmfnge0  31180  nmbdfnlbi  31302  nmcfnexi  31304  nmcfnlbi  31305  lnfnconi  31308  cnlnadjlem2  31321  cnlnadjlem7  31326  nmopcoadji  31354  leopnmid  31391  sqsscirc2  32889  subfaclim  34179  subfacval3  34180  sinccvglem  34657  dnicld1  35348  dnibndlem2  35355  dnibndlem6  35359  dnibndlem9  35362  dnibndlem12  35365  dnicn  35368  knoppcnlem4  35372  knoppcnlem6  35374  unblimceq0lem  35382  unblimceq0  35383  unbdqndv2lem1  35385  unbdqndv2lem2  35386  knoppndvlem11  35398  knoppndvlem12  35399  knoppndvlem14  35401  knoppndvlem15  35402  knoppndvlem17  35404  knoppndvlem18  35405  knoppndvlem20  35407  knoppndvlem21  35408  poimirlem29  36517  poimir  36521  iblabsnclem  36551  iblabsnc  36552  iblmulc2nc  36553  itgabsnc  36557  ftc1cnnclem  36559  ftc1anclem1  36561  ftc1anclem2  36562  ftc1anclem4  36564  ftc1anclem5  36565  ftc1anclem6  36566  ftc1anclem7  36567  ftc1anclem8  36568  ftc1anc  36569  ftc2nc  36570  dvasin  36572  areacirclem1  36576  areacirclem2  36577  areacirclem4  36579  areacirclem5  36580  areacirc  36581  geomcau  36627  cntotbnd  36664  rrndstprj1  36698  rrndstprj2  36699  ismrer1  36706  dffltz  41376  rencldnfilem  41558  irrapxlem2  41561  irrapxlem4  41563  irrapxlem5  41564  pellexlem2  41568  pellexlem6  41572  pell14qrgt0  41597  congabseq  41713  acongeq  41722  modabsdifz  41725  jm2.26lem3  41740  sqrtcvallem4  42390  extoimad  42916  imo72b2lem0  42917  imo72b2  42924  dvgrat  43071  cvgdvgrat  43072  radcnvrat  43073  dvconstbi  43093  binomcxplemnotnn0  43115  dstregt0  43991  absnpncan2d  44012  absnpncan3d  44017  abslt2sqd  44070  rexabslelem  44128  cvgcaule  44202  fprodabs2  44311  mullimc  44332  mullimcf  44339  limcrecl  44345  lptre2pt  44356  limcleqr  44360  addlimc  44364  0ellimcdiv  44365  limclner  44367  climleltrp  44392  climisp  44462  climxrrelem  44465  cnrefiisplem  44545  climxlim2lem  44561  cncficcgt0  44604  dvdivbd  44639  dvbdfbdioolem1  44644  dvbdfbdioolem2  44645  dvbdfbdioo  44646  ioodvbdlimc1lem1  44647  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  stoweid  44779  fourierdlem30  44853  fourierdlem39  44862  fourierdlem42  44865  fourierdlem47  44869  fourierdlem68  44890  fourierdlem70  44892  fourierdlem71  44893  fourierdlem73  44895  fourierdlem77  44899  fourierdlem80  44902  fourierdlem83  44905  fourierdlem87  44909  fourierdlem103  44925  fourierdlem104  44926  etransclem23  44973  etransclem48  44998  rrndistlt  45006  ioorrnopnlem  45020  sge0isum  45143  hoicvr  45264  smflimlem4  45490  smfmullem1  45507  smfmullem2  45508  smfmullem3  45509  itsclc0yqsol  47450