Theorem abscld 14788

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

Syntax hints:   → wi 4   ∈ wcel 2111  ‘cfv 6324  ℂcc 10524  ℝcr 10525  abscabs 14585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-om 7561  df-2nd 7672  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-er 8272  df-en 8493  df-dom 8494  df-sdom 8495  df-sup 8890  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11626  df-2 11688  df-3 11689  df-n0 11886  df-z 11970  df-uz 12232  df-rp 12378  df-seq 13365  df-exp 13426  df-cj 14450  df-re 14451  df-im 14452  df-sqrt 14586  df-abs 14587

This theorem is referenced by:  bhmafibid1  14817  lo1bddrp  14874  elo1mpt  14883  elo1mpt2  14884  elo1d  14885  o1bdd2  14890  o1bddrp  14891  rlimuni  14899  climuni  14901  o1eq  14919  rlimcld2  14927  rlimrege0  14928  climabs0  14934  mulcn2  14944  reccn2  14945  cn1lem  14946  cjcn2  14948  o1add  14962  o1mul  14963  o1sub  14964  rlimo1  14965  o1rlimmul  14967  climsqz  14989  climsqz2  14990  rlimsqzlem  14997  o1le  15001  climbdd  15020  caucvgrlem  15021  caucvgrlem2  15023  iseraltlem3  15032  iseralt  15033  fsumabs  15148  o1fsum  15160  iserabs  15162  cvgcmpce  15165  abscvgcvg  15166  divrcnv  15199  explecnv  15212  geomulcvg  15224  cvgrat  15231  mertenslem1  15232  mertenslem2  15233  fprodabs  15320  efcllem  15423  efaddlem  15438  eftlub  15454  ef01bndlem  15529  sin01bnd  15530  cos01bnd  15531  absef  15542  dvdsabseq  15655  alzdvds  15662  sqnprm  16036  pclem  16165  mul4sqlem  16279  xrsdsreclb  20138  gzrngunitlem  20156  gzrngunit  20157  prmirredlem  20186  nm2dif  23231  blcvx  23403  recld2  23419  addcnlem  23469  cnheiborlem  23559  cnheibor  23560  cnllycmp  23561  cphsqrtcl2  23791  ipcau2  23838  tcphcphlem1  23839  ipcnlem2  23848  cncmet  23926  trirn  24004  rrxdstprj1  24013  pjthlem1  24041  volsup2  24209  mbfi1fseqlem6  24324  iblabslem  24431  iblabs  24432  iblabsr  24433  iblmulc2  24434  itgabs  24438  bddmulibl  24442  bddiblnc  24445  itgcn  24448  dveflem  24582  dvlip  24596  dvlipcn  24597  c1liplem1  24599  dveq0  24603  dv11cn  24604  lhop1lem  24616  dvfsumabs  24626  dvfsumrlim  24634  dvfsumrlim2  24635  ftc1a  24640  ftc1lem4  24642  plyeq0lem  24807  aalioulem2  24929  aalioulem3  24930  aalioulem4  24931  aalioulem5  24932  aalioulem6  24933  aaliou  24934  geolim3  24935  aaliou2b  24937  aaliou3lem9  24946  ulmbdd  24993  ulmcn  24994  ulmdvlem1  24995  mtest  24999  mtestbdd  25000  iblulm  25002  itgulm  25003  radcnvlem1  25008  radcnvlem2  25009  radcnvlt1  25013  radcnvle  25015  dvradcnv  25016  pserulm  25017  psercnlem2  25019  psercnlem1  25020  psercn  25021  pserdvlem1  25022  pserdvlem2  25023  pserdv  25024  abelthlem2  25027  abelthlem3  25028  abelthlem5  25030  abelthlem7  25033  abelthlem8  25034  tanregt0  25131  efif1olem3  25136  efif1olem4  25137  eff1olem  25140  cosargd  25199  cosarg0d  25200  argregt0  25201  argrege0  25202  abslogle  25209  logcnlem3  25235  logcnlem4  25236  efopnlem1  25247  logtayl  25251  abscxp2  25284  cxpcn3lem  25336  abscxpbnd  25342  cosangneg2d  25393  lawcoslem1  25401  lawcos  25402  pythag  25403  isosctrlem3  25406  ssscongptld  25408  chordthmlem3  25420  chordthmlem4  25421  chordthmlem5  25422  heron  25424  bndatandm  25515  efrlim  25555  rlimcxp  25559  o1cxp  25560  cxploglim2  25564  divsqrtsumo1  25569  fsumharmonic  25597  lgamgulmlem2  25615  lgamgulmlem3  25616  lgamgulmlem5  25618  lgambdd  25622  lgamucov  25623  lgamcvg2  25640  ftalem1  25658  ftalem2  25659  ftalem3  25660  ftalem4  25661  ftalem5  25662  ftalem7  25664  logfacbnd3  25807  logfacrlim  25808  logexprlim  25809  dchrabs  25844  lgsdirprm  25915  lgsdilem2  25917  lgsne0  25919  lgsabs1  25920  mul2sq  26003  2sqlem3  26004  2sqblem  26015  vmadivsumb  26067  rplogsumlem2  26069  dchrisumlem2  26074  dchrisumlem3  26075  dchrisum  26076  dchrmusum2  26078  dchrvmasumlem2  26082  dchrvmasumlem3  26083  dchrvmasumiflem1  26085  dchrvmasumiflem2  26086  dchrisum0flblem1  26092  dchrisum0fno1  26095  dchrisum0lem1b  26099  dchrisum0lem1  26100  dchrisum0lem2a  26101  dchrisum0lem2  26102  dchrisum0lem3  26103  mudivsum  26114  mulogsumlem  26115  mulog2sumlem1  26118  mulog2sumlem2  26119  2vmadivsumlem  26124  log2sumbnd  26128  selberglem2  26130  selbergb  26133  selberg2b  26136  chpdifbndlem1  26137  selberg3lem1  26141  selberg3lem2  26142  selberg4lem1  26144  pntrsumo1  26149  pntrsumbnd  26150  pntrsumbnd2  26151  pntrlog2bndlem1  26161  pntrlog2bndlem2  26162  pntrlog2bndlem3  26163  pntrlog2bndlem4  26164  pntrlog2bndlem5  26165  pntrlog2bndlem6  26167  pntrlog2bnd  26168  pntpbnd1a  26169  pntpbnd2  26171  pntibndlem2  26175  pntlemn  26184  pntlemj  26187  pntlemf  26189  pntlemo  26191  pntlem3  26193  pntleml  26195  smcnlem  28480  nmoub3i  28556  isblo3i  28584  htthlem  28700  bcs2  28965  pjhthlem1  29174  nmfnsetre  29660  nmfnleub2  29709  nmfnge0  29710  nmbdfnlbi  29832  nmcfnexi  29834  nmcfnlbi  29835  lnfnconi  29838  cnlnadjlem2  29851  cnlnadjlem7  29856  nmopcoadji  29884  leopnmid  29921  sqsscirc2  31262  subfaclim  32548  subfacval3  32549  sinccvglem  33028  dnicld1  33924  dnibndlem2  33931  dnibndlem6  33935  dnibndlem9  33938  dnibndlem12  33941  dnicn  33944  knoppcnlem4  33948  knoppcnlem6  33950  unblimceq0lem  33958  unblimceq0  33959  unbdqndv2lem1  33961  unbdqndv2lem2  33962  knoppndvlem11  33974  knoppndvlem12  33975  knoppndvlem14  33977  knoppndvlem15  33978  knoppndvlem17  33980  knoppndvlem18  33981  knoppndvlem20  33983  knoppndvlem21  33984  poimirlem29  35086  poimir  35090  iblabsnclem  35120  iblabsnc  35121  iblmulc2nc  35122  itgabsnc  35126  ftc1cnnclem  35128  ftc1anclem1  35130  ftc1anclem2  35131  ftc1anclem4  35133  ftc1anclem5  35134  ftc1anclem6  35135  ftc1anclem7  35136  ftc1anclem8  35137  ftc1anc  35138  ftc2nc  35139  dvasin  35141  areacirclem1  35145  areacirclem2  35146  areacirclem4  35148  areacirclem5  35149  areacirc  35150  geomcau  35197  cntotbnd  35234  rrndstprj1  35268  rrndstprj2  35269  ismrer1  35276  dffltz  39615  rencldnfilem  39761  irrapxlem2  39764  irrapxlem4  39766  irrapxlem5  39767  pellexlem2  39771  pellexlem6  39775  pell14qrgt0  39800  congabseq  39915  acongeq  39924  modabsdifz  39927  jm2.26lem3  39942  sqrtcvallem4  40339  extoimad  40868  imo72b2lem0  40869  imo72b2  40878  dvgrat  41016  cvgdvgrat  41017  radcnvrat  41018  dvconstbi  41038  binomcxplemnotnn0  41060  dstregt0  41912  absnpncan2d  41934  absnpncan3d  41939  abslt2sqd  41992  rexabslelem  42055  fprodabs2  42237  mullimc  42258  mullimcf  42265  limcrecl  42271  lptre2pt  42282  limcleqr  42286  addlimc  42290  0ellimcdiv  42291  limclner  42293  climleltrp  42318  climisp  42388  climxrrelem  42391  cnrefiisplem  42471  climxlim2lem  42487  cncficcgt0  42530  dvdivbd  42565  dvbdfbdioolem1  42570  dvbdfbdioolem2  42571  dvbdfbdioo  42572  ioodvbdlimc1lem1  42573  ioodvbdlimc1lem2  42574  ioodvbdlimc2lem  42576  stoweid  42705  fourierdlem30  42779  fourierdlem39  42788  fourierdlem42  42791  fourierdlem47  42795  fourierdlem68  42816  fourierdlem70  42818  fourierdlem71  42819  fourierdlem73  42821  fourierdlem77  42825  fourierdlem80  42828  fourierdlem83  42831  fourierdlem87  42835  fourierdlem103  42851  fourierdlem104  42852  etransclem23  42899  etransclem48  42924  rrndistlt  42932  ioorrnopnlem  42946  sge0isum  43066  hoicvr  43187  smflimlem4  43407  smfmullem1  43423  smfmullem2  43424  smfmullem3  43425  itsclc0yqsol  45178