Theorem abscld 15401

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

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6498  ℂcc 11036  ℝcr 11037  abscabs 15196

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115  ax-pre-sup 11116

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-rmo 3342  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-om 7818  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-er 8643  df-en 8894  df-dom 8895  df-sdom 8896  df-sup 9355  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185  df-sub 11379  df-neg 11380  df-div 11808  df-nn 12175  df-2 12244  df-3 12245  df-n0 12438  df-z 12525  df-uz 12789  df-rp 12943  df-seq 13964  df-exp 14024  df-cj 15061  df-re 15062  df-im 15063  df-sqrt 15197  df-abs 15198

This theorem is referenced by:  bhmafibid1  15430  lo1bddrp  15487  elo1mpt  15496  elo1mpt2  15497  elo1d  15498  o1bdd2  15503  o1bddrp  15504  rlimuni  15512  climuni  15514  o1eq  15532  rlimcld2  15540  rlimrege0  15541  climabs0  15547  mulcn2  15558  reccn2  15559  cn1lem  15560  cjcn2  15562  o1add  15576  o1mul  15577  o1sub  15578  rlimo1  15579  o1rlimmul  15581  climsqz  15603  climsqz2  15604  rlimsqzlem  15611  o1le  15615  climbdd  15634  caucvgrlem  15635  caucvgrlem2  15637  iseraltlem3  15646  iseralt  15647  fsumabs  15764  o1fsum  15776  iserabs  15778  cvgcmpce  15781  abscvgcvg  15782  divrcnv  15817  explecnv  15830  geomulcvg  15841  cvgrat  15848  mertenslem1  15849  mertenslem2  15850  fprodabs  15939  efcllem  16042  efaddlem  16058  eftlub  16076  ef01bndlem  16151  sin01bnd  16152  cos01bnd  16153  absef  16164  dvdsabseq  16282  alzdvds  16289  sqnprm  16672  pclem  16809  mul4sqlem  16924  xrsdsreclb  21394  gzrngunitlem  21412  gzrngunit  21413  prmirredlem  21452  nm2dif  24590  blcvx  24763  recld2  24780  addcnlem  24830  cnheiborlem  24921  cnheibor  24922  cnllycmp  24923  cphsqrtcl2  25153  ipcau2  25201  tcphcphlem1  25202  ipcnlem2  25211  cncmet  25289  trirn  25367  rrxdstprj1  25376  pjthlem1  25404  volsup2  25572  mbfi1fseqlem6  25687  iblabslem  25795  iblabs  25796  iblabsr  25797  iblmulc2  25798  itgabs  25802  bddmulibl  25806  bddiblnc  25809  itgcn  25812  dveflem  25946  dvlip  25960  dvlipcn  25961  c1liplem1  25963  dveq0  25967  dv11cn  25968  lhop1lem  25980  dvfsumabs  25990  dvfsumrlim  25998  dvfsumrlim2  25999  ftc1a  26004  ftc1lem4  26006  plyeq0lem  26175  aalioulem2  26299  aalioulem3  26300  aalioulem4  26301  aalioulem5  26302  aalioulem6  26303  aaliou  26304  geolim3  26305  aaliou2b  26307  aaliou3lem9  26316  ulmbdd  26363  ulmcn  26364  ulmdvlem1  26365  mtest  26369  mtestbdd  26370  iblulm  26372  itgulm  26373  radcnvlem1  26378  radcnvlem2  26379  radcnvlt1  26383  radcnvle  26385  dvradcnv  26386  pserulm  26387  psercnlem2  26389  psercnlem1  26390  psercn  26391  pserdvlem1  26392  pserdvlem2  26393  pserdv  26394  abelthlem2  26397  abelthlem3  26398  abelthlem5  26400  abelthlem7  26403  abelthlem8  26404  tanregt0  26503  efif1olem3  26508  efif1olem4  26509  eff1olem  26512  cosargd  26572  cosarg0d  26573  argregt0  26574  argrege0  26575  abslogle  26582  logcnlem3  26608  logcnlem4  26609  efopnlem1  26620  logtayl  26624  abscxp2  26657  cxpcn3lem  26711  abscxpbnd  26717  cosangneg2d  26771  lawcoslem1  26779  lawcos  26780  pythag  26781  isosctrlem3  26784  ssscongptld  26786  chordthmlem3  26798  chordthmlem4  26799  chordthmlem5  26800  heron  26802  bndatandm  26893  efrlim  26933  rlimcxp  26937  o1cxp  26938  cxploglim2  26942  divsqrtsumo1  26947  fsumharmonic  26975  lgamgulmlem2  26993  lgamgulmlem3  26994  lgamgulmlem5  26996  lgambdd  27000  lgamucov  27001  lgamcvg2  27018  ftalem1  27036  ftalem2  27037  ftalem3  27038  ftalem4  27039  ftalem5  27040  ftalem7  27042  logfacbnd3  27186  logfacrlim  27187  logexprlim  27188  dchrabs  27223  lgsdirprm  27294  lgsdilem2  27296  lgsne0  27298  lgsabs1  27299  mul2sq  27382  2sqlem3  27383  2sqblem  27394  vmadivsumb  27446  rplogsumlem2  27448  dchrisumlem2  27453  dchrisumlem3  27454  dchrisum  27455  dchrmusum2  27457  dchrvmasumlem2  27461  dchrvmasumlem3  27462  dchrvmasumiflem1  27464  dchrvmasumiflem2  27465  dchrisum0flblem1  27471  dchrisum0fno1  27474  dchrisum0lem1b  27478  dchrisum0lem1  27479  dchrisum0lem2a  27480  dchrisum0lem2  27481  dchrisum0lem3  27482  mudivsum  27493  mulogsumlem  27494  mulog2sumlem1  27497  mulog2sumlem2  27498  2vmadivsumlem  27503  log2sumbnd  27507  selberglem2  27509  selbergb  27512  selberg2b  27515  chpdifbndlem1  27516  selberg3lem1  27520  selberg3lem2  27521  selberg4lem1  27523  pntrsumo1  27528  pntrsumbnd  27529  pntrsumbnd2  27530  pntrlog2bndlem1  27540  pntrlog2bndlem2  27541  pntrlog2bndlem3  27542  pntrlog2bndlem4  27543  pntrlog2bndlem5  27544  pntrlog2bndlem6  27546  pntrlog2bnd  27547  pntpbnd1a  27548  pntpbnd2  27550  pntibndlem2  27554  pntlemn  27563  pntlemj  27566  pntlemf  27568  pntlemo  27570  pntlem3  27572  pntleml  27574  smcnlem  30768  nmoub3i  30844  isblo3i  30872  htthlem  30988  bcs2  31253  pjhthlem1  31462  nmfnsetre  31948  nmfnleub2  31997  nmfnge0  31998  nmbdfnlbi  32120  nmcfnexi  32122  nmcfnlbi  32123  lnfnconi  32126  cnlnadjlem2  32139  cnlnadjlem7  32144  nmopcoadji  32172  leopnmid  32209  constrdircl  33909  iconstr  33910  constrremulcl  33911  constrimcl  33914  constrmulcl  33915  constrinvcl  33917  constrabscl  33922  constrsqrtcl  33923  sqsscirc2  34053  subfaclim  35370  subfacval3  35371  sinccvglem  35854  dnicld1  36732  dnibndlem2  36739  dnibndlem6  36743  dnibndlem9  36746  dnibndlem12  36749  dnicn  36752  knoppcnlem4  36756  knoppcnlem6  36758  unblimceq0lem  36766  unblimceq0  36767  unbdqndv2lem1  36769  unbdqndv2lem2  36770  knoppndvlem11  36782  knoppndvlem12  36783  knoppndvlem14  36785  knoppndvlem15  36786  knoppndvlem17  36788  knoppndvlem18  36789  knoppndvlem20  36791  knoppndvlem21  36792  poimirlem29  37970  poimir  37974  iblabsnclem  38004  iblabsnc  38005  iblmulc2nc  38006  itgabsnc  38010  ftc1cnnclem  38012  ftc1anclem1  38014  ftc1anclem2  38015  ftc1anclem4  38017  ftc1anclem5  38018  ftc1anclem6  38019  ftc1anclem7  38020  ftc1anclem8  38021  ftc1anc  38022  ftc2nc  38023  dvasin  38025  areacirclem1  38029  areacirclem2  38030  areacirclem4  38032  areacirclem5  38033  areacirc  38034  geomcau  38080  cntotbnd  38117  rrndstprj1  38151  rrndstprj2  38152  ismrer1  38159  readvrec  42794  readvcot  42796  dffltz  43067  rencldnfilem  43248  irrapxlem2  43251  irrapxlem4  43253  irrapxlem5  43254  pellexlem2  43258  pellexlem6  43262  pell14qrgt0  43287  congabseq  43402  acongeq  43411  modabsdifz  43414  jm2.26lem3  43429  sqrtcvallem4  44066  extoimad  44591  imo72b2lem0  44592  imo72b2  44599  dvgrat  44739  cvgdvgrat  44740  radcnvrat  44741  dvconstbi  44761  binomcxplemnotnn0  44783  dstregt0  45715  absnpncan2d  45735  absnpncan3d  45740  abslt2sqd  45790  rexabslelem  45846  cvgcaule  45919  fprodabs2  46025  mullimc  46046  mullimcf  46053  limcrecl  46059  lptre2pt  46068  limcleqr  46072  addlimc  46076  0ellimcdiv  46077  limclner  46079  climleltrp  46104  climisp  46174  climxrrelem  46177  cnrefiisplem  46257  climxlim2lem  46273  cncficcgt0  46316  dvdivbd  46351  dvbdfbdioolem1  46356  dvbdfbdioolem2  46357  dvbdfbdioo  46358  ioodvbdlimc1lem1  46359  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  stoweid  46491  fourierdlem30  46565  fourierdlem39  46574  fourierdlem42  46577  fourierdlem47  46581  fourierdlem68  46602  fourierdlem70  46604  fourierdlem71  46605  fourierdlem73  46607  fourierdlem77  46611  fourierdlem80  46614  fourierdlem83  46617  fourierdlem87  46621  fourierdlem103  46637  fourierdlem104  46638  etransclem23  46685  etransclem48  46710  rrndistlt  46718  ioorrnopnlem  46732  sge0isum  46855  hoicvr  46976  smflimlem4  47202  smfmullem1  47219  smfmullem2  47220  smfmullem3  47221  modlt0b  47817  itsclc0yqsol  49240