Theorem abscld 15380

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

Syntax hints:   → wi 4   ∈ wcel 2107  ‘cfv 6541  ℂcc 11105  ℝcr 11106  abscabs 15178

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 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184  ax-pre-sup 11185

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 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-om 7853  df-2nd 7973  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-sup 9434  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-3 12273  df-n0 12470  df-z 12556  df-uz 12820  df-rp 12972  df-seq 13964  df-exp 14025  df-cj 15043  df-re 15044  df-im 15045  df-sqrt 15179  df-abs 15180

This theorem is referenced by:  bhmafibid1  15409  lo1bddrp  15466  elo1mpt  15475  elo1mpt2  15476  elo1d  15477  o1bdd2  15482  o1bddrp  15483  rlimuni  15491  climuni  15493  o1eq  15511  rlimcld2  15519  rlimrege0  15520  climabs0  15526  mulcn2  15537  reccn2  15538  cn1lem  15539  cjcn2  15541  o1add  15555  o1mul  15556  o1sub  15557  rlimo1  15558  o1rlimmul  15560  climsqz  15582  climsqz2  15583  rlimsqzlem  15592  o1le  15596  climbdd  15615  caucvgrlem  15616  caucvgrlem2  15618  iseraltlem3  15627  iseralt  15628  fsumabs  15744  o1fsum  15756  iserabs  15758  cvgcmpce  15761  abscvgcvg  15762  divrcnv  15795  explecnv  15808  geomulcvg  15819  cvgrat  15826  mertenslem1  15827  mertenslem2  15828  fprodabs  15915  efcllem  16018  efaddlem  16033  eftlub  16049  ef01bndlem  16124  sin01bnd  16125  cos01bnd  16126  absef  16137  dvdsabseq  16253  alzdvds  16260  sqnprm  16636  pclem  16768  mul4sqlem  16883  xrsdsreclb  20985  gzrngunitlem  21003  gzrngunit  21004  prmirredlem  21034  nm2dif  24126  blcvx  24306  recld2  24322  addcnlem  24372  cnheiborlem  24462  cnheibor  24463  cnllycmp  24464  cphsqrtcl2  24695  ipcau2  24743  tcphcphlem1  24744  ipcnlem2  24753  cncmet  24831  trirn  24909  rrxdstprj1  24918  pjthlem1  24946  volsup2  25114  mbfi1fseqlem6  25230  iblabslem  25337  iblabs  25338  iblabsr  25339  iblmulc2  25340  itgabs  25344  bddmulibl  25348  bddiblnc  25351  itgcn  25354  dveflem  25488  dvlip  25502  dvlipcn  25503  c1liplem1  25505  dveq0  25509  dv11cn  25510  lhop1lem  25522  dvfsumabs  25532  dvfsumrlim  25540  dvfsumrlim2  25541  ftc1a  25546  ftc1lem4  25548  plyeq0lem  25716  aalioulem2  25838  aalioulem3  25839  aalioulem4  25840  aalioulem5  25841  aalioulem6  25842  aaliou  25843  geolim3  25844  aaliou2b  25846  aaliou3lem9  25855  ulmbdd  25902  ulmcn  25903  ulmdvlem1  25904  mtest  25908  mtestbdd  25909  iblulm  25911  itgulm  25912  radcnvlem1  25917  radcnvlem2  25918  radcnvlt1  25922  radcnvle  25924  dvradcnv  25925  pserulm  25926  psercnlem2  25928  psercnlem1  25929  psercn  25930  pserdvlem1  25931  pserdvlem2  25932  pserdv  25933  abelthlem2  25936  abelthlem3  25937  abelthlem5  25939  abelthlem7  25942  abelthlem8  25943  tanregt0  26040  efif1olem3  26045  efif1olem4  26046  eff1olem  26049  cosargd  26108  cosarg0d  26109  argregt0  26110  argrege0  26111  abslogle  26118  logcnlem3  26144  logcnlem4  26145  efopnlem1  26156  logtayl  26160  abscxp2  26193  cxpcn3lem  26245  abscxpbnd  26251  cosangneg2d  26302  lawcoslem1  26310  lawcos  26311  pythag  26312  isosctrlem3  26315  ssscongptld  26317  chordthmlem3  26329  chordthmlem4  26330  chordthmlem5  26331  heron  26333  bndatandm  26424  efrlim  26464  rlimcxp  26468  o1cxp  26469  cxploglim2  26473  divsqrtsumo1  26478  fsumharmonic  26506  lgamgulmlem2  26524  lgamgulmlem3  26525  lgamgulmlem5  26527  lgambdd  26531  lgamucov  26532  lgamcvg2  26549  ftalem1  26567  ftalem2  26568  ftalem3  26569  ftalem4  26570  ftalem5  26571  ftalem7  26573  logfacbnd3  26716  logfacrlim  26717  logexprlim  26718  dchrabs  26753  lgsdirprm  26824  lgsdilem2  26826  lgsne0  26828  lgsabs1  26829  mul2sq  26912  2sqlem3  26913  2sqblem  26924  vmadivsumb  26976  rplogsumlem2  26978  dchrisumlem2  26983  dchrisumlem3  26984  dchrisum  26985  dchrmusum2  26987  dchrvmasumlem2  26991  dchrvmasumlem3  26992  dchrvmasumiflem1  26994  dchrvmasumiflem2  26995  dchrisum0flblem1  27001  dchrisum0fno1  27004  dchrisum0lem1b  27008  dchrisum0lem1  27009  dchrisum0lem2a  27010  dchrisum0lem2  27011  dchrisum0lem3  27012  mudivsum  27023  mulogsumlem  27024  mulog2sumlem1  27027  mulog2sumlem2  27028  2vmadivsumlem  27033  log2sumbnd  27037  selberglem2  27039  selbergb  27042  selberg2b  27045  chpdifbndlem1  27046  selberg3lem1  27050  selberg3lem2  27051  selberg4lem1  27053  pntrsumo1  27058  pntrsumbnd  27059  pntrsumbnd2  27060  pntrlog2bndlem1  27070  pntrlog2bndlem2  27071  pntrlog2bndlem3  27072  pntrlog2bndlem4  27073  pntrlog2bndlem5  27074  pntrlog2bndlem6  27076  pntrlog2bnd  27077  pntpbnd1a  27078  pntpbnd2  27080  pntibndlem2  27084  pntlemn  27093  pntlemj  27096  pntlemf  27098  pntlemo  27100  pntlem3  27102  pntleml  27104  smcnlem  29938  nmoub3i  30014  isblo3i  30042  htthlem  30158  bcs2  30423  pjhthlem1  30632  nmfnsetre  31118  nmfnleub2  31167  nmfnge0  31168  nmbdfnlbi  31290  nmcfnexi  31292  nmcfnlbi  31293  lnfnconi  31296  cnlnadjlem2  31309  cnlnadjlem7  31314  nmopcoadji  31342  leopnmid  31379  sqsscirc2  32878  subfaclim  34168  subfacval3  34169  sinccvglem  34646  dnicld1  35337  dnibndlem2  35344  dnibndlem6  35348  dnibndlem9  35351  dnibndlem12  35354  dnicn  35357  knoppcnlem4  35361  knoppcnlem6  35363  unblimceq0lem  35371  unblimceq0  35372  unbdqndv2lem1  35374  unbdqndv2lem2  35375  knoppndvlem11  35387  knoppndvlem12  35388  knoppndvlem14  35390  knoppndvlem15  35391  knoppndvlem17  35393  knoppndvlem18  35394  knoppndvlem20  35396  knoppndvlem21  35397  poimirlem29  36506  poimir  36510  iblabsnclem  36540  iblabsnc  36541  iblmulc2nc  36542  itgabsnc  36546  ftc1cnnclem  36548  ftc1anclem1  36550  ftc1anclem2  36551  ftc1anclem4  36553  ftc1anclem5  36554  ftc1anclem6  36555  ftc1anclem7  36556  ftc1anclem8  36557  ftc1anc  36558  ftc2nc  36559  dvasin  36561  areacirclem1  36565  areacirclem2  36566  areacirclem4  36568  areacirclem5  36569  areacirc  36570  geomcau  36616  cntotbnd  36653  rrndstprj1  36687  rrndstprj2  36688  ismrer1  36695  dffltz  41373  rencldnfilem  41544  irrapxlem2  41547  irrapxlem4  41549  irrapxlem5  41550  pellexlem2  41554  pellexlem6  41558  pell14qrgt0  41583  congabseq  41699  acongeq  41708  modabsdifz  41711  jm2.26lem3  41726  sqrtcvallem4  42376  extoimad  42902  imo72b2lem0  42903  imo72b2  42910  dvgrat  43057  cvgdvgrat  43058  radcnvrat  43059  dvconstbi  43079  binomcxplemnotnn0  43101  dstregt0  43978  absnpncan2d  43999  absnpncan3d  44004  abslt2sqd  44057  rexabslelem  44115  cvgcaule  44189  fprodabs2  44298  mullimc  44319  mullimcf  44326  limcrecl  44332  lptre2pt  44343  limcleqr  44347  addlimc  44351  0ellimcdiv  44352  limclner  44354  climleltrp  44379  climisp  44449  climxrrelem  44452  cnrefiisplem  44532  climxlim2lem  44548  cncficcgt0  44591  dvdivbd  44626  dvbdfbdioolem1  44631  dvbdfbdioolem2  44632  dvbdfbdioo  44633  ioodvbdlimc1lem1  44634  ioodvbdlimc1lem2  44635  ioodvbdlimc2lem  44637  stoweid  44766  fourierdlem30  44840  fourierdlem39  44849  fourierdlem42  44852  fourierdlem47  44856  fourierdlem68  44877  fourierdlem70  44879  fourierdlem71  44880  fourierdlem73  44882  fourierdlem77  44886  fourierdlem80  44889  fourierdlem83  44892  fourierdlem87  44896  fourierdlem103  44912  fourierdlem104  44913  etransclem23  44960  etransclem48  44985  rrndistlt  44993  ioorrnopnlem  45007  sge0isum  45130  hoicvr  45251  smflimlem4  45477  smfmullem1  45494  smfmullem2  45495  smfmullem3  45496  itsclc0yqsol  47404