Theorem abscld 14886

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

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6339  ℂcc 10613  ℝcr 10614  abscabs 14683

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7479  ax-cnex 10671  ax-resscn 10672  ax-1cn 10673  ax-icn 10674  ax-addcl 10675  ax-addrcl 10676  ax-mulcl 10677  ax-mulrcl 10678  ax-mulcom 10679  ax-addass 10680  ax-mulass 10681  ax-distr 10682  ax-i2m1 10683  ax-1ne0 10684  ax-1rid 10685  ax-rnegex 10686  ax-rrecex 10687  ax-cnre 10688  ax-pre-lttri 10689  ax-pre-lttrn 10690  ax-pre-ltadd 10691  ax-pre-mulgt0 10692  ax-pre-sup 10693

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-nel 3039  df-ral 3058  df-rex 3059  df-reu 3060  df-rmo 3061  df-rab 3062  df-v 3400  df-sbc 3681  df-csb 3791  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-pss 3862  df-nul 4212  df-if 4415  df-pw 4490  df-sn 4517  df-pr 4519  df-tp 4521  df-op 4523  df-uni 4797  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5429  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5483  df-we 5485  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6129  df-ord 6175  df-on 6176  df-lim 6177  df-suc 6178  df-iota 6297  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-riota 7127  df-ov 7173  df-oprab 7174  df-mpo 7175  df-om 7600  df-2nd 7715  df-wrecs 7976  df-recs 8037  df-rdg 8075  df-er 8320  df-en 8556  df-dom 8557  df-sdom 8558  df-sup 8979  df-pnf 10755  df-mnf 10756  df-xr 10757  df-ltxr 10758  df-le 10759  df-sub 10950  df-neg 10951  df-div 11376  df-nn 11717  df-2 11779  df-3 11780  df-n0 11977  df-z 12063  df-uz 12325  df-rp 12473  df-seq 13461  df-exp 13522  df-cj 14548  df-re 14549  df-im 14550  df-sqrt 14684  df-abs 14685

This theorem is referenced by:  bhmafibid1  14915  lo1bddrp  14972  elo1mpt  14981  elo1mpt2  14982  elo1d  14983  o1bdd2  14988  o1bddrp  14989  rlimuni  14997  climuni  14999  o1eq  15017  rlimcld2  15025  rlimrege0  15026  climabs0  15032  mulcn2  15043  reccn2  15044  cn1lem  15045  cjcn2  15047  o1add  15061  o1mul  15062  o1sub  15063  rlimo1  15064  o1rlimmul  15066  climsqz  15088  climsqz2  15089  rlimsqzlem  15098  o1le  15102  climbdd  15121  caucvgrlem  15122  caucvgrlem2  15124  iseraltlem3  15133  iseralt  15134  fsumabs  15249  o1fsum  15261  iserabs  15263  cvgcmpce  15266  abscvgcvg  15267  divrcnv  15300  explecnv  15313  geomulcvg  15324  cvgrat  15331  mertenslem1  15332  mertenslem2  15333  fprodabs  15420  efcllem  15523  efaddlem  15538  eftlub  15554  ef01bndlem  15629  sin01bnd  15630  cos01bnd  15631  absef  15642  dvdsabseq  15758  alzdvds  15765  sqnprm  16143  pclem  16275  mul4sqlem  16389  xrsdsreclb  20264  gzrngunitlem  20282  gzrngunit  20283  prmirredlem  20313  nm2dif  23378  blcvx  23550  recld2  23566  addcnlem  23616  cnheiborlem  23706  cnheibor  23707  cnllycmp  23708  cphsqrtcl2  23938  ipcau2  23986  tcphcphlem1  23987  ipcnlem2  23996  cncmet  24074  trirn  24152  rrxdstprj1  24161  pjthlem1  24189  volsup2  24357  mbfi1fseqlem6  24473  iblabslem  24580  iblabs  24581  iblabsr  24582  iblmulc2  24583  itgabs  24587  bddmulibl  24591  bddiblnc  24594  itgcn  24597  dveflem  24731  dvlip  24745  dvlipcn  24746  c1liplem1  24748  dveq0  24752  dv11cn  24753  lhop1lem  24765  dvfsumabs  24775  dvfsumrlim  24783  dvfsumrlim2  24784  ftc1a  24789  ftc1lem4  24791  plyeq0lem  24959  aalioulem2  25081  aalioulem3  25082  aalioulem4  25083  aalioulem5  25084  aalioulem6  25085  aaliou  25086  geolim3  25087  aaliou2b  25089  aaliou3lem9  25098  ulmbdd  25145  ulmcn  25146  ulmdvlem1  25147  mtest  25151  mtestbdd  25152  iblulm  25154  itgulm  25155  radcnvlem1  25160  radcnvlem2  25161  radcnvlt1  25165  radcnvle  25167  dvradcnv  25168  pserulm  25169  psercnlem2  25171  psercnlem1  25172  psercn  25173  pserdvlem1  25174  pserdvlem2  25175  pserdv  25176  abelthlem2  25179  abelthlem3  25180  abelthlem5  25182  abelthlem7  25185  abelthlem8  25186  tanregt0  25283  efif1olem3  25288  efif1olem4  25289  eff1olem  25292  cosargd  25351  cosarg0d  25352  argregt0  25353  argrege0  25354  abslogle  25361  logcnlem3  25387  logcnlem4  25388  efopnlem1  25399  logtayl  25403  abscxp2  25436  cxpcn3lem  25488  abscxpbnd  25494  cosangneg2d  25545  lawcoslem1  25553  lawcos  25554  pythag  25555  isosctrlem3  25558  ssscongptld  25560  chordthmlem3  25572  chordthmlem4  25573  chordthmlem5  25574  heron  25576  bndatandm  25667  efrlim  25707  rlimcxp  25711  o1cxp  25712  cxploglim2  25716  divsqrtsumo1  25721  fsumharmonic  25749  lgamgulmlem2  25767  lgamgulmlem3  25768  lgamgulmlem5  25770  lgambdd  25774  lgamucov  25775  lgamcvg2  25792  ftalem1  25810  ftalem2  25811  ftalem3  25812  ftalem4  25813  ftalem5  25814  ftalem7  25816  logfacbnd3  25959  logfacrlim  25960  logexprlim  25961  dchrabs  25996  lgsdirprm  26067  lgsdilem2  26069  lgsne0  26071  lgsabs1  26072  mul2sq  26155  2sqlem3  26156  2sqblem  26167  vmadivsumb  26219  rplogsumlem2  26221  dchrisumlem2  26226  dchrisumlem3  26227  dchrisum  26228  dchrmusum2  26230  dchrvmasumlem2  26234  dchrvmasumlem3  26235  dchrvmasumiflem1  26237  dchrvmasumiflem2  26238  dchrisum0flblem1  26244  dchrisum0fno1  26247  dchrisum0lem1b  26251  dchrisum0lem1  26252  dchrisum0lem2a  26253  dchrisum0lem2  26254  dchrisum0lem3  26255  mudivsum  26266  mulogsumlem  26267  mulog2sumlem1  26270  mulog2sumlem2  26271  2vmadivsumlem  26276  log2sumbnd  26280  selberglem2  26282  selbergb  26285  selberg2b  26288  chpdifbndlem1  26289  selberg3lem1  26293  selberg3lem2  26294  selberg4lem1  26296  pntrsumo1  26301  pntrsumbnd  26302  pntrsumbnd2  26303  pntrlog2bndlem1  26313  pntrlog2bndlem2  26314  pntrlog2bndlem3  26315  pntrlog2bndlem4  26316  pntrlog2bndlem5  26317  pntrlog2bndlem6  26319  pntrlog2bnd  26320  pntpbnd1a  26321  pntpbnd2  26323  pntibndlem2  26327  pntlemn  26336  pntlemj  26339  pntlemf  26341  pntlemo  26343  pntlem3  26345  pntleml  26347  smcnlem  28632  nmoub3i  28708  isblo3i  28736  htthlem  28852  bcs2  29117  pjhthlem1  29326  nmfnsetre  29812  nmfnleub2  29861  nmfnge0  29862  nmbdfnlbi  29984  nmcfnexi  29986  nmcfnlbi  29987  lnfnconi  29990  cnlnadjlem2  30003  cnlnadjlem7  30008  nmopcoadji  30036  leopnmid  30073  sqsscirc2  31431  subfaclim  32721  subfacval3  32722  sinccvglem  33201  dnicld1  34295  dnibndlem2  34302  dnibndlem6  34306  dnibndlem9  34309  dnibndlem12  34312  dnicn  34315  knoppcnlem4  34319  knoppcnlem6  34321  unblimceq0lem  34329  unblimceq0  34330  unbdqndv2lem1  34332  unbdqndv2lem2  34333  knoppndvlem11  34345  knoppndvlem12  34346  knoppndvlem14  34348  knoppndvlem15  34349  knoppndvlem17  34351  knoppndvlem18  34352  knoppndvlem20  34354  knoppndvlem21  34355  poimirlem29  35449  poimir  35453  iblabsnclem  35483  iblabsnc  35484  iblmulc2nc  35485  itgabsnc  35489  ftc1cnnclem  35491  ftc1anclem1  35493  ftc1anclem2  35494  ftc1anclem4  35496  ftc1anclem5  35497  ftc1anclem6  35498  ftc1anclem7  35499  ftc1anclem8  35500  ftc1anc  35501  ftc2nc  35502  dvasin  35504  areacirclem1  35508  areacirclem2  35509  areacirclem4  35511  areacirclem5  35512  areacirc  35513  geomcau  35560  cntotbnd  35597  rrndstprj1  35631  rrndstprj2  35632  ismrer1  35639  dffltz  40063  rencldnfilem  40234  irrapxlem2  40237  irrapxlem4  40239  irrapxlem5  40240  pellexlem2  40244  pellexlem6  40248  pell14qrgt0  40273  congabseq  40388  acongeq  40397  modabsdifz  40400  jm2.26lem3  40415  sqrtcvallem4  40812  extoimad  41341  imo72b2lem0  41342  imo72b2  41350  dvgrat  41488  cvgdvgrat  41489  radcnvrat  41490  dvconstbi  41510  binomcxplemnotnn0  41532  dstregt0  42377  absnpncan2d  42399  absnpncan3d  42404  abslt2sqd  42457  rexabslelem  42516  fprodabs2  42698  mullimc  42719  mullimcf  42726  limcrecl  42732  lptre2pt  42743  limcleqr  42747  addlimc  42751  0ellimcdiv  42752  limclner  42754  climleltrp  42779  climisp  42849  climxrrelem  42852  cnrefiisplem  42932  climxlim2lem  42948  cncficcgt0  42991  dvdivbd  43026  dvbdfbdioolem1  43031  dvbdfbdioolem2  43032  dvbdfbdioo  43033  ioodvbdlimc1lem1  43034  ioodvbdlimc1lem2  43035  ioodvbdlimc2lem  43037  stoweid  43166  fourierdlem30  43240  fourierdlem39  43249  fourierdlem42  43252  fourierdlem47  43256  fourierdlem68  43277  fourierdlem70  43279  fourierdlem71  43280  fourierdlem73  43282  fourierdlem77  43286  fourierdlem80  43289  fourierdlem83  43292  fourierdlem87  43296  fourierdlem103  43312  fourierdlem104  43313  etransclem23  43360  etransclem48  43385  rrndistlt  43393  ioorrnopnlem  43407  sge0isum  43527  hoicvr  43648  smflimlem4  43868  smfmullem1  43884  smfmullem2  43885  smfmullem3  43886  itsclc0yqsol  45664