Theorem abscld 15486

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

Syntax hints:   → wi 4   ∈ wcel 2143  ‘cfv 6536  ℂcc 11093  ℝcr 11094  abscabs 15281

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-cnex 11151  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-mulcom 11159  ax-addass 11160  ax-mulass 11161  ax-distr 11162  ax-i2m1 11163  ax-1ne0 11164  ax-1rid 11165  ax-rnegex 11166  ax-rrecex 11167  ax-cnre 11168  ax-pre-lttri 11169  ax-pre-lttrn 11170  ax-pre-ltadd 11171  ax-pre-mulgt0 11172  ax-pre-sup 11173

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7859  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-sup 9398  df-pnf 11240  df-mnf 11241  df-xr 11242  df-ltxr 11243  df-le 11244  df-sub 11438  df-neg 11439  df-div 11867  df-nn 12229  df-2 12298  df-3 12299  df-n0 12500  df-z 12587  df-uz 12858  df-rp 13012  df-seq 14034  df-exp 14094  df-cj 15146  df-re 15147  df-im 15148  df-sqrt 15282  df-abs 15283

This theorem is referenced by:  bhmafibid1  15515  lo1bddrp  15572  elo1mpt  15581  elo1mpt2  15582  elo1d  15583  o1bdd2  15588  o1bddrp  15589  rlimuni  15597  climuni  15599  o1eq  15617  rlimcld2  15625  rlimrege0  15626  climabs0  15632  mulcn2  15643  reccn2  15644  cn1lem  15645  cjcn2  15647  o1add  15661  o1mul  15662  o1sub  15663  rlimo1  15664  o1rlimmul  15666  climsqz  15688  climsqz2  15689  rlimsqzlem  15696  o1le  15700  climbdd  15719  caucvgrlem  15720  caucvgrlem2  15722  iseraltlem3  15731  iseralt  15732  fsumabs  15849  o1fsum  15861  iserabs  15863  cvgcmpce  15866  abscvgcvg  15867  divrcnv  15902  explecnv  15915  geomulcvg  15926  cvgrat  15933  mertenslem1  15934  mertenslem2  15935  fprodabs  16024  efcllem  16126  efaddlem  16142  eftlub  16160  ef01bndlem  16235  sin01bnd  16236  cos01bnd  16237  absef  16248  dvdsabseq  16366  alzdvds  16373  sqnprm  16756  pclem  16893  mul4sqlem  17008  xrsdsreclb  21564  gzrngunitlem  21582  gzrngunit  21583  prmirredlem  21622  nm2dif  24782  blcvx  24955  recld2  24972  addcnlem  25022  cnheiborlem  25113  cnheibor  25114  cnllycmp  25115  cphsqrtcl2  25345  ipcau2  25393  tcphcphlem1  25394  ipcnlem2  25403  cncmet  25481  trirn  25559  rrxdstprj1  25568  pjthlem1  25596  volsup2  25764  mbfi1fseqlem6  25879  iblabslem  25987  iblabs  25988  iblabsr  25989  iblmulc2  25990  itgabs  25994  bddmulibl  25998  bddiblnc  26001  itgcn  26004  dveflem  26138  dvlip  26152  dvlipcn  26153  c1liplem1  26155  dveq0  26159  dv11cn  26160  lhop1lem  26172  dvfsumabs  26182  dvfsumrlim  26190  dvfsumrlim2  26191  ftc1a  26196  ftc1lem4  26198  plyeq0lem  26367  aalioulem2  26496  aalioulem3  26497  aalioulem4  26498  aalioulem5  26499  aalioulem6  26500  aaliou  26501  geolim3  26502  aaliou2b  26504  aaliou3lem9  26513  ulmbdd  26561  ulmcn  26562  ulmdvlem1  26563  mtest  26567  mtestbdd  26568  iblulm  26570  itgulm  26571  radcnvlem1  26576  radcnvlem2  26577  radcnvlt1  26581  radcnvle  26583  dvradcnv  26584  pserulm  26585  psercnlem2  26587  psercnlem1  26588  psercn  26589  pserdvlem1  26590  pserdvlem2  26591  pserdv  26592  abelthlem2  26595  abelthlem3  26596  abelthlem5  26598  abelthlem7  26601  abelthlem8  26602  tanregt0  26704  efif1olem3  26709  efif1olem4  26710  eff1olem  26713  cosargd  26773  cosarg0d  26774  argregt0  26775  argrege0  26776  abslogle  26783  logcnlem3  26809  logcnlem4  26810  efopnlem1  26821  logtayl  26825  abscxp2  26858  cxpcn3lem  26912  abscxpbnd  26918  cosangneg2d  26972  lawcoslem1  26980  lawcos  26981  pythag  26982  isosctrlem3  26985  ssscongptld  26987  chordthmlem3  26999  chordthmlem4  27000  chordthmlem5  27001  heron  27003  bndatandm  27094  efrlim  27134  rlimcxp  27138  o1cxp  27139  cxploglim2  27143  divsqrtsumo1  27148  fsumharmonic  27176  lgamgulmlem2  27194  lgamgulmlem3  27195  lgamgulmlem5  27197  lgambdd  27201  lgamucov  27202  lgamcvg2  27219  ftalem1  27237  ftalem2  27238  ftalem3  27239  ftalem4  27240  ftalem5  27241  ftalem7  27243  logfacbnd3  27387  logfacrlim  27388  logexprlim  27389  dchrabs  27424  lgsdirprm  27495  lgsdilem2  27497  lgsne0  27499  lgsabs1  27500  mul2sq  27583  2sqlem3  27584  2sqblem  27595  vmadivsumb  27647  rplogsumlem2  27649  dchrisumlem2  27654  dchrisumlem3  27655  dchrisum  27656  dchrmusum2  27658  dchrvmasumlem2  27662  dchrvmasumlem3  27663  dchrvmasumiflem1  27665  dchrvmasumiflem2  27666  dchrisum0flblem1  27672  dchrisum0fno1  27675  dchrisum0lem1b  27679  dchrisum0lem1  27680  dchrisum0lem2a  27681  dchrisum0lem2  27682  dchrisum0lem3  27683  mudivsum  27694  mulogsumlem  27695  mulog2sumlem1  27698  mulog2sumlem2  27699  2vmadivsumlem  27704  log2sumbnd  27708  selberglem2  27710  selbergb  27713  selberg2b  27716  chpdifbndlem1  27717  selberg3lem1  27721  selberg3lem2  27722  selberg4lem1  27724  pntrsumo1  27729  pntrsumbnd  27730  pntrsumbnd2  27731  pntrlog2bndlem1  27741  pntrlog2bndlem2  27742  pntrlog2bndlem3  27743  pntrlog2bndlem4  27744  pntrlog2bndlem5  27745  pntrlog2bndlem6  27747  pntrlog2bnd  27748  pntpbnd1a  27749  pntpbnd2  27751  pntibndlem2  27755  pntlemn  27764  pntlemj  27767  pntlemf  27769  pntlemo  27771  pntlem3  27773  pntleml  27775  smcnlem  31049  nmoub3i  31125  isblo3i  31153  htthlem  31269  bcs2  31534  pjhthlem1  31743  nmfnsetre  32229  nmfnleub2  32278  nmfnge0  32279  nmbdfnlbi  32401  nmcfnexi  32403  nmcfnlbi  32404  lnfnconi  32407  cnlnadjlem2  32420  cnlnadjlem7  32425  nmopcoadji  32453  leopnmid  32490  constrdircl  34155  iconstr  34156  constrremulcl  34157  constrimcl  34160  constrmulcl  34161  constrinvcl  34163  constrabscl  34168  constrsqrtcl  34169  sqsscirc2  34299  subfaclim  35680  subfacval3  35681  sinccvglem  36164  dnicld1  37061  dnibndlem2  37068  dnibndlem6  37072  dnibndlem9  37075  dnibndlem12  37078  dnicn  37081  knoppcnlem4  37085  knoppcnlem6  37087  unblimceq0lem  37095  unblimceq0  37096  unbdqndv2lem1  37098  unbdqndv2lem2  37099  knoppndvlem11  37111  knoppndvlem12  37112  knoppndvlem14  37114  knoppndvlem15  37115  knoppndvlem17  37117  knoppndvlem18  37118  knoppndvlem20  37120  knoppndvlem21  37121  poimirlem29  38300  poimir  38304  iblabsnclem  38334  iblabsnc  38335  iblmulc2nc  38336  itgabsnc  38340  ftc1cnnclem  38342  ftc1anclem1  38344  ftc1anclem2  38345  ftc1anclem4  38347  ftc1anclem5  38348  ftc1anclem6  38349  ftc1anclem7  38350  ftc1anclem8  38351  ftc1anc  38352  ftc2nc  38353  dvasin  38355  areacirclem1  38359  areacirclem2  38360  areacirclem4  38362  areacirclem5  38363  areacirc  38364  geomcau  38410  cntotbnd  38447  rrndstprj1  38481  rrndstprj2  38482  ismrer1  38489  readvrec  43123  readvcot  43125  dffltz  43366  rencldnfilem  43547  irrapxlem2  43550  irrapxlem4  43552  irrapxlem5  43553  pellexlem2  43557  pellexlem6  43561  pell14qrgt0  43586  congabseq  43701  acongeq  43710  modabsdifz  43713  jm2.26lem3  43728  sqrtcvallem4  44365  extoimad  44890  imo72b2lem0  44891  imo72b2  44898  dvgrat  45022  cvgdvgrat  45023  radcnvrat  45024  dvconstbi  45044  binomcxplemnotnn0  45066  dstregt0  46001  absnpncan2d  46021  absnpncan3d  46026  abslt2sqd  46076  rexabslelem  46132  cvgcaule  46205  fprodabs2  46311  mullimc  46332  mullimcf  46339  limcrecl  46345  lptre2pt  46354  limcleqr  46358  addlimc  46362  0ellimcdiv  46363  limclner  46365  climleltrp  46390  climisp  46460  climxrrelem  46463  cnrefiisplem  46543  climxlim2lem  46559  cncficcgt0  46602  dvdivbd  46637  dvbdfbdioolem1  46642  dvbdfbdioolem2  46643  dvbdfbdioo  46644  ioodvbdlimc1lem1  46645  ioodvbdlimc1lem2  46646  ioodvbdlimc2lem  46648  stoweid  46777  fourierdlem30  46851  fourierdlem39  46860  fourierdlem42  46863  fourierdlem47  46867  fourierdlem68  46888  fourierdlem70  46890  fourierdlem71  46891  fourierdlem73  46893  fourierdlem77  46897  fourierdlem80  46900  fourierdlem83  46903  fourierdlem87  46907  fourierdlem103  46923  fourierdlem104  46924  etransclem23  46971  etransclem48  46996  rrndistlt  47004  ioorrnopnlem  47018  sge0isum  47141  hoicvr  47262  smflimlem4  47488  smfmullem1  47505  smfmullem2  47506  smfmullem3  47507  modlt0b  48106  itsclc0yqsol  49544