Theorem abscld 15356

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

Syntax hints:   → wi 4   ∈ wcel 2113  ‘cfv 6489  ℂcc 11014  ℝcr 11015  abscabs 15151

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7677  ax-cnex 11072  ax-resscn 11073  ax-1cn 11074  ax-icn 11075  ax-addcl 11076  ax-addrcl 11077  ax-mulcl 11078  ax-mulrcl 11079  ax-mulcom 11080  ax-addass 11081  ax-mulass 11082  ax-distr 11083  ax-i2m1 11084  ax-1ne0 11085  ax-1rid 11086  ax-rnegex 11087  ax-rrecex 11088  ax-cnre 11089  ax-pre-lttri 11090  ax-pre-lttrn 11091  ax-pre-ltadd 11092  ax-pre-mulgt0 11093  ax-pre-sup 11094

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2883  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3059  df-rmo 3348  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-iun 4945  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6256  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-riota 7312  df-ov 7358  df-oprab 7359  df-mpo 7360  df-om 7806  df-2nd 7931  df-frecs 8220  df-wrecs 8251  df-recs 8300  df-rdg 8338  df-er 8631  df-en 8879  df-dom 8880  df-sdom 8881  df-sup 9336  df-pnf 11158  df-mnf 11159  df-xr 11160  df-ltxr 11161  df-le 11162  df-sub 11356  df-neg 11357  df-div 11785  df-nn 12136  df-2 12198  df-3 12199  df-n0 12392  df-z 12479  df-uz 12743  df-rp 12901  df-seq 13919  df-exp 13979  df-cj 15016  df-re 15017  df-im 15018  df-sqrt 15152  df-abs 15153

This theorem is referenced by:  bhmafibid1  15385  lo1bddrp  15442  elo1mpt  15451  elo1mpt2  15452  elo1d  15453  o1bdd2  15458  o1bddrp  15459  rlimuni  15467  climuni  15469  o1eq  15487  rlimcld2  15495  rlimrege0  15496  climabs0  15502  mulcn2  15513  reccn2  15514  cn1lem  15515  cjcn2  15517  o1add  15531  o1mul  15532  o1sub  15533  rlimo1  15534  o1rlimmul  15536  climsqz  15558  climsqz2  15559  rlimsqzlem  15566  o1le  15570  climbdd  15589  caucvgrlem  15590  caucvgrlem2  15592  iseraltlem3  15601  iseralt  15602  fsumabs  15718  o1fsum  15730  iserabs  15732  cvgcmpce  15735  abscvgcvg  15736  divrcnv  15769  explecnv  15782  geomulcvg  15793  cvgrat  15800  mertenslem1  15801  mertenslem2  15802  fprodabs  15891  efcllem  15994  efaddlem  16010  eftlub  16028  ef01bndlem  16103  sin01bnd  16104  cos01bnd  16105  absef  16116  dvdsabseq  16234  alzdvds  16241  sqnprm  16623  pclem  16760  mul4sqlem  16875  xrsdsreclb  21360  gzrngunitlem  21379  gzrngunit  21380  prmirredlem  21419  nm2dif  24550  blcvx  24723  recld2  24740  addcnlem  24790  cnheiborlem  24890  cnheibor  24891  cnllycmp  24892  cphsqrtcl2  25123  ipcau2  25171  tcphcphlem1  25172  ipcnlem2  25181  cncmet  25259  trirn  25337  rrxdstprj1  25346  pjthlem1  25374  volsup2  25543  mbfi1fseqlem6  25658  iblabslem  25766  iblabs  25767  iblabsr  25768  iblmulc2  25769  itgabs  25773  bddmulibl  25777  bddiblnc  25780  itgcn  25783  dveflem  25920  dvlip  25935  dvlipcn  25936  c1liplem1  25938  dveq0  25942  dv11cn  25943  lhop1lem  25955  dvfsumabs  25966  dvfsumrlim  25975  dvfsumrlim2  25976  ftc1a  25981  ftc1lem4  25983  plyeq0lem  26152  aalioulem2  26278  aalioulem3  26279  aalioulem4  26280  aalioulem5  26281  aalioulem6  26282  aaliou  26283  geolim3  26284  aaliou2b  26286  aaliou3lem9  26295  ulmbdd  26344  ulmcn  26345  ulmdvlem1  26346  mtest  26350  mtestbdd  26351  iblulm  26353  itgulm  26354  radcnvlem1  26359  radcnvlem2  26360  radcnvlt1  26364  radcnvle  26366  dvradcnv  26367  pserulm  26368  psercnlem2  26371  psercnlem1  26372  psercn  26373  pserdvlem1  26374  pserdvlem2  26375  pserdv  26376  abelthlem2  26379  abelthlem3  26380  abelthlem5  26382  abelthlem7  26385  abelthlem8  26386  tanregt0  26485  efif1olem3  26490  efif1olem4  26491  eff1olem  26494  cosargd  26554  cosarg0d  26555  argregt0  26556  argrege0  26557  abslogle  26564  logcnlem3  26590  logcnlem4  26591  efopnlem1  26602  logtayl  26606  abscxp2  26639  cxpcn3lem  26694  abscxpbnd  26700  cosangneg2d  26754  lawcoslem1  26762  lawcos  26763  pythag  26764  isosctrlem3  26767  ssscongptld  26769  chordthmlem3  26781  chordthmlem4  26782  chordthmlem5  26783  heron  26785  bndatandm  26876  efrlim  26916  efrlimOLD  26917  rlimcxp  26921  o1cxp  26922  cxploglim2  26926  divsqrtsumo1  26931  fsumharmonic  26959  lgamgulmlem2  26977  lgamgulmlem3  26978  lgamgulmlem5  26980  lgambdd  26984  lgamucov  26985  lgamcvg2  27002  ftalem1  27020  ftalem2  27021  ftalem3  27022  ftalem4  27023  ftalem5  27024  ftalem7  27026  logfacbnd3  27171  logfacrlim  27172  logexprlim  27173  dchrabs  27208  lgsdirprm  27279  lgsdilem2  27281  lgsne0  27283  lgsabs1  27284  mul2sq  27367  2sqlem3  27368  2sqblem  27379  vmadivsumb  27431  rplogsumlem2  27433  dchrisumlem2  27438  dchrisumlem3  27439  dchrisum  27440  dchrmusum2  27442  dchrvmasumlem2  27446  dchrvmasumlem3  27447  dchrvmasumiflem1  27449  dchrvmasumiflem2  27450  dchrisum0flblem1  27456  dchrisum0fno1  27459  dchrisum0lem1b  27463  dchrisum0lem1  27464  dchrisum0lem2a  27465  dchrisum0lem2  27466  dchrisum0lem3  27467  mudivsum  27478  mulogsumlem  27479  mulog2sumlem1  27482  mulog2sumlem2  27483  2vmadivsumlem  27488  log2sumbnd  27492  selberglem2  27494  selbergb  27497  selberg2b  27500  chpdifbndlem1  27501  selberg3lem1  27505  selberg3lem2  27506  selberg4lem1  27508  pntrsumo1  27513  pntrsumbnd  27514  pntrsumbnd2  27515  pntrlog2bndlem1  27525  pntrlog2bndlem2  27526  pntrlog2bndlem3  27527  pntrlog2bndlem4  27528  pntrlog2bndlem5  27529  pntrlog2bndlem6  27531  pntrlog2bnd  27532  pntpbnd1a  27533  pntpbnd2  27535  pntibndlem2  27539  pntlemn  27548  pntlemj  27551  pntlemf  27553  pntlemo  27555  pntlem3  27557  pntleml  27559  smcnlem  30688  nmoub3i  30764  isblo3i  30792  htthlem  30908  bcs2  31173  pjhthlem1  31382  nmfnsetre  31868  nmfnleub2  31917  nmfnge0  31918  nmbdfnlbi  32040  nmcfnexi  32042  nmcfnlbi  32043  lnfnconi  32046  cnlnadjlem2  32059  cnlnadjlem7  32064  nmopcoadji  32092  leopnmid  32129  constrdircl  33789  iconstr  33790  constrremulcl  33791  constrimcl  33794  constrmulcl  33795  constrinvcl  33797  constrabscl  33802  constrsqrtcl  33803  sqsscirc2  33933  subfaclim  35243  subfacval3  35244  sinccvglem  35727  dnicld1  36527  dnibndlem2  36534  dnibndlem6  36538  dnibndlem9  36541  dnibndlem12  36544  dnicn  36547  knoppcnlem4  36551  knoppcnlem6  36553  unblimceq0lem  36561  unblimceq0  36562  unbdqndv2lem1  36564  unbdqndv2lem2  36565  knoppndvlem11  36577  knoppndvlem12  36578  knoppndvlem14  36580  knoppndvlem15  36581  knoppndvlem17  36583  knoppndvlem18  36584  knoppndvlem20  36586  knoppndvlem21  36587  poimirlem29  37699  poimir  37703  iblabsnclem  37733  iblabsnc  37734  iblmulc2nc  37735  itgabsnc  37739  ftc1cnnclem  37741  ftc1anclem1  37743  ftc1anclem2  37744  ftc1anclem4  37746  ftc1anclem5  37747  ftc1anclem6  37748  ftc1anclem7  37749  ftc1anclem8  37750  ftc1anc  37751  ftc2nc  37752  dvasin  37754  areacirclem1  37758  areacirclem2  37759  areacirclem4  37761  areacirclem5  37762  areacirc  37763  geomcau  37809  cntotbnd  37846  rrndstprj1  37880  rrndstprj2  37881  ismrer1  37888  readvrec  42470  readvcot  42472  dffltz  42742  rencldnfilem  42927  irrapxlem2  42930  irrapxlem4  42932  irrapxlem5  42933  pellexlem2  42937  pellexlem6  42941  pell14qrgt0  42966  congabseq  43081  acongeq  43090  modabsdifz  43093  jm2.26lem3  43108  sqrtcvallem4  43746  extoimad  44271  imo72b2lem0  44272  imo72b2  44279  dvgrat  44419  cvgdvgrat  44420  radcnvrat  44421  dvconstbi  44441  binomcxplemnotnn0  44463  dstregt0  45397  absnpncan2d  45417  absnpncan3d  45422  abslt2sqd  45473  rexabslelem  45530  cvgcaule  45603  fprodabs2  45709  mullimc  45730  mullimcf  45737  limcrecl  45743  lptre2pt  45752  limcleqr  45756  addlimc  45760  0ellimcdiv  45761  limclner  45763  climleltrp  45788  climisp  45858  climxrrelem  45861  cnrefiisplem  45941  climxlim2lem  45957  cncficcgt0  46000  dvdivbd  46035  dvbdfbdioolem1  46040  dvbdfbdioolem2  46041  dvbdfbdioo  46042  ioodvbdlimc1lem1  46043  ioodvbdlimc1lem2  46044  ioodvbdlimc2lem  46046  stoweid  46175  fourierdlem30  46249  fourierdlem39  46258  fourierdlem42  46261  fourierdlem47  46265  fourierdlem68  46286  fourierdlem70  46288  fourierdlem71  46289  fourierdlem73  46291  fourierdlem77  46295  fourierdlem80  46298  fourierdlem83  46301  fourierdlem87  46305  fourierdlem103  46321  fourierdlem104  46322  etransclem23  46369  etransclem48  46394  rrndistlt  46402  ioorrnopnlem  46416  sge0isum  46539  hoicvr  46660  smflimlem4  46886  smfmullem1  46903  smfmullem2  46904  smfmullem3  46905  modlt0b  47477  itsclc0yqsol  48879