Theorem abscld 14796

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

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6355  ℂcc 10535  ℝcr 10536  abscabs 14593

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-cnex 10593  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-mulcom 10601  ax-addass 10602  ax-mulass 10603  ax-distr 10604  ax-i2m1 10605  ax-1ne0 10606  ax-1rid 10607  ax-rnegex 10608  ax-rrecex 10609  ax-cnre 10610  ax-pre-lttri 10611  ax-pre-lttrn 10612  ax-pre-ltadd 10613  ax-pre-mulgt0 10614  ax-pre-sup 10615

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-om 7581  df-2nd 7690  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-er 8289  df-en 8510  df-dom 8511  df-sdom 8512  df-sup 8906  df-pnf 10677  df-mnf 10678  df-xr 10679  df-ltxr 10680  df-le 10681  df-sub 10872  df-neg 10873  df-div 11298  df-nn 11639  df-2 11701  df-3 11702  df-n0 11899  df-z 11983  df-uz 12245  df-rp 12391  df-seq 13371  df-exp 13431  df-cj 14458  df-re 14459  df-im 14460  df-sqrt 14594  df-abs 14595

This theorem is referenced by:  bhmafibid1  14825  lo1bddrp  14882  elo1mpt  14891  elo1mpt2  14892  elo1d  14893  o1bdd2  14898  o1bddrp  14899  rlimuni  14907  climuni  14909  o1eq  14927  rlimcld2  14935  rlimrege0  14936  climabs0  14942  mulcn2  14952  reccn2  14953  cn1lem  14954  cjcn2  14956  o1add  14970  o1mul  14971  o1sub  14972  rlimo1  14973  o1rlimmul  14975  climsqz  14997  climsqz2  14998  rlimsqzlem  15005  o1le  15009  climbdd  15028  caucvgrlem  15029  caucvgrlem2  15031  iseraltlem3  15040  iseralt  15041  fsumabs  15156  o1fsum  15168  iserabs  15170  cvgcmpce  15173  abscvgcvg  15174  divrcnv  15207  explecnv  15220  geomulcvg  15232  cvgrat  15239  mertenslem1  15240  mertenslem2  15241  fprodabs  15328  efcllem  15431  efaddlem  15446  eftlub  15462  ef01bndlem  15537  sin01bnd  15538  cos01bnd  15539  absef  15550  dvdsabseq  15663  alzdvds  15670  sqnprm  16046  pclem  16175  mul4sqlem  16289  xrsdsreclb  20592  gzrngunitlem  20610  gzrngunit  20611  prmirredlem  20640  nm2dif  23234  blcvx  23406  recld2  23422  addcnlem  23472  cnheiborlem  23558  cnheibor  23559  cnllycmp  23560  cphsqrtcl2  23790  ipcau2  23837  tcphcphlem1  23838  ipcnlem2  23847  cncmet  23925  trirn  24003  rrxdstprj1  24012  pjthlem1  24040  volsup2  24206  mbfi1fseqlem6  24321  iblabslem  24428  iblabs  24429  iblabsr  24430  iblmulc2  24431  itgabs  24435  bddmulibl  24439  itgcn  24443  dveflem  24576  dvlip  24590  dvlipcn  24591  c1liplem1  24593  dveq0  24597  dv11cn  24598  lhop1lem  24610  dvfsumabs  24620  dvfsumrlim  24628  dvfsumrlim2  24629  ftc1a  24634  ftc1lem4  24636  plyeq0lem  24800  aalioulem2  24922  aalioulem3  24923  aalioulem4  24924  aalioulem5  24925  aalioulem6  24926  aaliou  24927  geolim3  24928  aaliou2b  24930  aaliou3lem9  24939  ulmbdd  24986  ulmcn  24987  ulmdvlem1  24988  mtest  24992  mtestbdd  24993  iblulm  24995  itgulm  24996  radcnvlem1  25001  radcnvlem2  25002  radcnvlt1  25006  radcnvle  25008  dvradcnv  25009  pserulm  25010  psercnlem2  25012  psercnlem1  25013  psercn  25014  pserdvlem1  25015  pserdvlem2  25016  pserdv  25017  abelthlem2  25020  abelthlem3  25021  abelthlem5  25023  abelthlem7  25026  abelthlem8  25027  tanregt0  25123  efif1olem3  25128  efif1olem4  25129  eff1olem  25132  cosargd  25191  cosarg0d  25192  argregt0  25193  argrege0  25194  abslogle  25201  logcnlem3  25227  logcnlem4  25228  efopnlem1  25239  logtayl  25243  abscxp2  25276  cxpcn3lem  25328  abscxpbnd  25334  cosangneg2d  25385  lawcoslem1  25393  lawcos  25394  pythag  25395  isosctrlem3  25398  ssscongptld  25400  chordthmlem3  25412  chordthmlem4  25413  chordthmlem5  25414  heron  25416  bndatandm  25507  efrlim  25547  rlimcxp  25551  o1cxp  25552  cxploglim2  25556  divsqrtsumo1  25561  fsumharmonic  25589  lgamgulmlem2  25607  lgamgulmlem3  25608  lgamgulmlem5  25610  lgambdd  25614  lgamucov  25615  lgamcvg2  25632  ftalem1  25650  ftalem2  25651  ftalem3  25652  ftalem4  25653  ftalem5  25654  ftalem7  25656  logfacbnd3  25799  logfacrlim  25800  logexprlim  25801  dchrabs  25836  lgsdirprm  25907  lgsdilem2  25909  lgsne0  25911  lgsabs1  25912  mul2sq  25995  2sqlem3  25996  2sqblem  26007  vmadivsumb  26059  rplogsumlem2  26061  dchrisumlem2  26066  dchrisumlem3  26067  dchrisum  26068  dchrmusum2  26070  dchrvmasumlem2  26074  dchrvmasumlem3  26075  dchrvmasumiflem1  26077  dchrvmasumiflem2  26078  dchrisum0flblem1  26084  dchrisum0fno1  26087  dchrisum0lem1b  26091  dchrisum0lem1  26092  dchrisum0lem2a  26093  dchrisum0lem2  26094  dchrisum0lem3  26095  mudivsum  26106  mulogsumlem  26107  mulog2sumlem1  26110  mulog2sumlem2  26111  2vmadivsumlem  26116  log2sumbnd  26120  selberglem2  26122  selbergb  26125  selberg2b  26128  chpdifbndlem1  26129  selberg3lem1  26133  selberg3lem2  26134  selberg4lem1  26136  pntrsumo1  26141  pntrsumbnd  26142  pntrsumbnd2  26143  pntrlog2bndlem1  26153  pntrlog2bndlem2  26154  pntrlog2bndlem3  26155  pntrlog2bndlem4  26156  pntrlog2bndlem5  26157  pntrlog2bndlem6  26159  pntrlog2bnd  26160  pntpbnd1a  26161  pntpbnd2  26163  pntibndlem2  26167  pntlemn  26176  pntlemj  26179  pntlemf  26181  pntlemo  26183  pntlem3  26185  pntleml  26187  smcnlem  28474  nmoub3i  28550  isblo3i  28578  htthlem  28694  bcs2  28959  pjhthlem1  29168  nmfnsetre  29654  nmfnleub2  29703  nmfnge0  29704  nmbdfnlbi  29826  nmcfnexi  29828  nmcfnlbi  29829  lnfnconi  29832  cnlnadjlem2  29845  cnlnadjlem7  29850  nmopcoadji  29878  leopnmid  29915  sqsscirc2  31152  subfaclim  32435  subfacval3  32436  sinccvglem  32915  dnicld1  33811  dnibndlem2  33818  dnibndlem6  33822  dnibndlem9  33825  dnibndlem12  33828  dnicn  33831  knoppcnlem4  33835  knoppcnlem6  33837  unblimceq0lem  33845  unblimceq0  33846  unbdqndv2lem1  33848  unbdqndv2lem2  33849  knoppndvlem11  33861  knoppndvlem12  33862  knoppndvlem14  33864  knoppndvlem15  33865  knoppndvlem17  33867  knoppndvlem18  33868  knoppndvlem20  33870  knoppndvlem21  33871  poimirlem29  34936  poimir  34940  iblabsnclem  34970  iblabsnc  34971  iblmulc2nc  34972  itgabsnc  34976  bddiblnc  34977  ftc1cnnclem  34980  ftc1anclem1  34982  ftc1anclem2  34983  ftc1anclem4  34985  ftc1anclem5  34986  ftc1anclem6  34987  ftc1anclem7  34988  ftc1anclem8  34989  ftc1anc  34990  ftc2nc  34991  dvasin  34993  areacirclem1  34997  areacirclem2  34998  areacirclem4  35000  areacirclem5  35001  areacirc  35002  geomcau  35049  cntotbnd  35089  rrndstprj1  35123  rrndstprj2  35124  ismrer1  35131  dffltz  39291  rencldnfilem  39437  irrapxlem2  39440  irrapxlem4  39442  irrapxlem5  39443  pellexlem2  39447  pellexlem6  39451  pell14qrgt0  39476  congabseq  39591  acongeq  39600  modabsdifz  39603  jm2.26lem3  39618  extoimad  40535  imo72b2lem0  40536  imo72b2  40545  dvgrat  40664  cvgdvgrat  40665  radcnvrat  40666  dvconstbi  40686  binomcxplemnotnn0  40708  dstregt0  41567  absnpncan2d  41589  absnpncan3d  41594  abslt2sqd  41648  rexabslelem  41712  fprodabs2  41896  mullimc  41917  mullimcf  41924  limcrecl  41930  lptre2pt  41941  limcleqr  41945  addlimc  41949  0ellimcdiv  41950  limclner  41952  climleltrp  41977  climisp  42047  climxrrelem  42050  cnrefiisplem  42130  climxlim2lem  42146  cncficcgt0  42191  dvdivbd  42228  dvbdfbdioolem1  42233  dvbdfbdioolem2  42234  dvbdfbdioo  42235  ioodvbdlimc1lem1  42236  ioodvbdlimc1lem2  42237  ioodvbdlimc2lem  42239  stoweid  42368  fourierdlem30  42442  fourierdlem39  42451  fourierdlem42  42454  fourierdlem47  42458  fourierdlem68  42479  fourierdlem70  42481  fourierdlem71  42482  fourierdlem73  42484  fourierdlem77  42488  fourierdlem80  42491  fourierdlem83  42494  fourierdlem87  42498  fourierdlem103  42514  fourierdlem104  42515  etransclem23  42562  etransclem48  42587  rrndistlt  42595  ioorrnopnlem  42609  sge0isum  42729  hoicvr  42850  smflimlem4  43070  smfmullem1  43086  smfmullem2  43087  smfmullem3  43088  itsclc0yqsol  44771