Theorem abscld 15381

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

Syntax hints:   → wi 4   ∈ wcel 2109  ‘cfv 6499  ℂcc 11042  ℝcr 11043  abscabs 15176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-cnex 11100  ax-resscn 11101  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-mulcom 11108  ax-addass 11109  ax-mulass 11110  ax-distr 11111  ax-i2m1 11112  ax-1ne0 11113  ax-1rid 11114  ax-rnegex 11115  ax-rrecex 11116  ax-cnre 11117  ax-pre-lttri 11118  ax-pre-lttrn 11119  ax-pre-ltadd 11120  ax-pre-mulgt0 11121  ax-pre-sup 11122

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3351  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  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 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-riota 7326  df-ov 7372  df-oprab 7373  df-mpo 7374  df-om 7823  df-2nd 7948  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-er 8648  df-en 8896  df-dom 8897  df-sdom 8898  df-sup 9369  df-pnf 11186  df-mnf 11187  df-xr 11188  df-ltxr 11189  df-le 11190  df-sub 11383  df-neg 11384  df-div 11812  df-nn 12163  df-2 12225  df-3 12226  df-n0 12419  df-z 12506  df-uz 12770  df-rp 12928  df-seq 13943  df-exp 14003  df-cj 15041  df-re 15042  df-im 15043  df-sqrt 15177  df-abs 15178

This theorem is referenced by:  bhmafibid1  15410  lo1bddrp  15467  elo1mpt  15476  elo1mpt2  15477  elo1d  15478  o1bdd2  15483  o1bddrp  15484  rlimuni  15492  climuni  15494  o1eq  15512  rlimcld2  15520  rlimrege0  15521  climabs0  15527  mulcn2  15538  reccn2  15539  cn1lem  15540  cjcn2  15542  o1add  15556  o1mul  15557  o1sub  15558  rlimo1  15559  o1rlimmul  15561  climsqz  15583  climsqz2  15584  rlimsqzlem  15591  o1le  15595  climbdd  15614  caucvgrlem  15615  caucvgrlem2  15617  iseraltlem3  15626  iseralt  15627  fsumabs  15743  o1fsum  15755  iserabs  15757  cvgcmpce  15760  abscvgcvg  15761  divrcnv  15794  explecnv  15807  geomulcvg  15818  cvgrat  15825  mertenslem1  15826  mertenslem2  15827  fprodabs  15916  efcllem  16019  efaddlem  16035  eftlub  16053  ef01bndlem  16128  sin01bnd  16129  cos01bnd  16130  absef  16141  dvdsabseq  16259  alzdvds  16266  sqnprm  16648  pclem  16785  mul4sqlem  16900  xrsdsreclb  21306  gzrngunitlem  21325  gzrngunit  21326  prmirredlem  21358  nm2dif  24489  blcvx  24662  recld2  24679  addcnlem  24729  cnheiborlem  24829  cnheibor  24830  cnllycmp  24831  cphsqrtcl2  25062  ipcau2  25110  tcphcphlem1  25111  ipcnlem2  25120  cncmet  25198  trirn  25276  rrxdstprj1  25285  pjthlem1  25313  volsup2  25482  mbfi1fseqlem6  25597  iblabslem  25705  iblabs  25706  iblabsr  25707  iblmulc2  25708  itgabs  25712  bddmulibl  25716  bddiblnc  25719  itgcn  25722  dveflem  25859  dvlip  25874  dvlipcn  25875  c1liplem1  25877  dveq0  25881  dv11cn  25882  lhop1lem  25894  dvfsumabs  25905  dvfsumrlim  25914  dvfsumrlim2  25915  ftc1a  25920  ftc1lem4  25922  plyeq0lem  26091  aalioulem2  26217  aalioulem3  26218  aalioulem4  26219  aalioulem5  26220  aalioulem6  26221  aaliou  26222  geolim3  26223  aaliou2b  26225  aaliou3lem9  26234  ulmbdd  26283  ulmcn  26284  ulmdvlem1  26285  mtest  26289  mtestbdd  26290  iblulm  26292  itgulm  26293  radcnvlem1  26298  radcnvlem2  26299  radcnvlt1  26303  radcnvle  26305  dvradcnv  26306  pserulm  26307  psercnlem2  26310  psercnlem1  26311  psercn  26312  pserdvlem1  26313  pserdvlem2  26314  pserdv  26315  abelthlem2  26318  abelthlem3  26319  abelthlem5  26321  abelthlem7  26324  abelthlem8  26325  tanregt0  26424  efif1olem3  26429  efif1olem4  26430  eff1olem  26433  cosargd  26493  cosarg0d  26494  argregt0  26495  argrege0  26496  abslogle  26503  logcnlem3  26529  logcnlem4  26530  efopnlem1  26541  logtayl  26545  abscxp2  26578  cxpcn3lem  26633  abscxpbnd  26639  cosangneg2d  26693  lawcoslem1  26701  lawcos  26702  pythag  26703  isosctrlem3  26706  ssscongptld  26708  chordthmlem3  26720  chordthmlem4  26721  chordthmlem5  26722  heron  26724  bndatandm  26815  efrlim  26855  efrlimOLD  26856  rlimcxp  26860  o1cxp  26861  cxploglim2  26865  divsqrtsumo1  26870  fsumharmonic  26898  lgamgulmlem2  26916  lgamgulmlem3  26917  lgamgulmlem5  26919  lgambdd  26923  lgamucov  26924  lgamcvg2  26941  ftalem1  26959  ftalem2  26960  ftalem3  26961  ftalem4  26962  ftalem5  26963  ftalem7  26965  logfacbnd3  27110  logfacrlim  27111  logexprlim  27112  dchrabs  27147  lgsdirprm  27218  lgsdilem2  27220  lgsne0  27222  lgsabs1  27223  mul2sq  27306  2sqlem3  27307  2sqblem  27318  vmadivsumb  27370  rplogsumlem2  27372  dchrisumlem2  27377  dchrisumlem3  27378  dchrisum  27379  dchrmusum2  27381  dchrvmasumlem2  27385  dchrvmasumlem3  27386  dchrvmasumiflem1  27388  dchrvmasumiflem2  27389  dchrisum0flblem1  27395  dchrisum0fno1  27398  dchrisum0lem1b  27402  dchrisum0lem1  27403  dchrisum0lem2a  27404  dchrisum0lem2  27405  dchrisum0lem3  27406  mudivsum  27417  mulogsumlem  27418  mulog2sumlem1  27421  mulog2sumlem2  27422  2vmadivsumlem  27427  log2sumbnd  27431  selberglem2  27433  selbergb  27436  selberg2b  27439  chpdifbndlem1  27440  selberg3lem1  27444  selberg3lem2  27445  selberg4lem1  27447  pntrsumo1  27452  pntrsumbnd  27453  pntrsumbnd2  27454  pntrlog2bndlem1  27464  pntrlog2bndlem2  27465  pntrlog2bndlem3  27466  pntrlog2bndlem4  27467  pntrlog2bndlem5  27468  pntrlog2bndlem6  27470  pntrlog2bnd  27471  pntpbnd1a  27472  pntpbnd2  27474  pntibndlem2  27478  pntlemn  27487  pntlemj  27490  pntlemf  27492  pntlemo  27494  pntlem3  27496  pntleml  27498  smcnlem  30599  nmoub3i  30675  isblo3i  30703  htthlem  30819  bcs2  31084  pjhthlem1  31293  nmfnsetre  31779  nmfnleub2  31828  nmfnge0  31829  nmbdfnlbi  31951  nmcfnexi  31953  nmcfnlbi  31954  lnfnconi  31957  cnlnadjlem2  31970  cnlnadjlem7  31975  nmopcoadji  32003  leopnmid  32040  constrdircl  33728  iconstr  33729  constrremulcl  33730  constrimcl  33733  constrmulcl  33734  constrinvcl  33736  constrabscl  33741  constrsqrtcl  33742  sqsscirc2  33872  subfaclim  35148  subfacval3  35149  sinccvglem  35632  dnicld1  36433  dnibndlem2  36440  dnibndlem6  36444  dnibndlem9  36447  dnibndlem12  36450  dnicn  36453  knoppcnlem4  36457  knoppcnlem6  36459  unblimceq0lem  36467  unblimceq0  36468  unbdqndv2lem1  36470  unbdqndv2lem2  36471  knoppndvlem11  36483  knoppndvlem12  36484  knoppndvlem14  36486  knoppndvlem15  36487  knoppndvlem17  36489  knoppndvlem18  36490  knoppndvlem20  36492  knoppndvlem21  36493  poimirlem29  37616  poimir  37620  iblabsnclem  37650  iblabsnc  37651  iblmulc2nc  37652  itgabsnc  37656  ftc1cnnclem  37658  ftc1anclem1  37660  ftc1anclem2  37661  ftc1anclem4  37663  ftc1anclem5  37664  ftc1anclem6  37665  ftc1anclem7  37666  ftc1anclem8  37667  ftc1anc  37668  ftc2nc  37669  dvasin  37671  areacirclem1  37675  areacirclem2  37676  areacirclem4  37678  areacirclem5  37679  areacirc  37680  geomcau  37726  cntotbnd  37763  rrndstprj1  37797  rrndstprj2  37798  ismrer1  37805  readvrec  42323  readvcot  42325  dffltz  42595  rencldnfilem  42781  irrapxlem2  42784  irrapxlem4  42786  irrapxlem5  42787  pellexlem2  42791  pellexlem6  42795  pell14qrgt0  42820  congabseq  42936  acongeq  42945  modabsdifz  42948  jm2.26lem3  42963  sqrtcvallem4  43601  extoimad  44126  imo72b2lem0  44127  imo72b2  44134  dvgrat  44274  cvgdvgrat  44275  radcnvrat  44276  dvconstbi  44296  binomcxplemnotnn0  44318  dstregt0  45253  absnpncan2d  45273  absnpncan3d  45278  abslt2sqd  45329  rexabslelem  45387  cvgcaule  45460  fprodabs2  45566  mullimc  45587  mullimcf  45594  limcrecl  45600  lptre2pt  45611  limcleqr  45615  addlimc  45619  0ellimcdiv  45620  limclner  45622  climleltrp  45647  climisp  45717  climxrrelem  45720  cnrefiisplem  45800  climxlim2lem  45816  cncficcgt0  45859  dvdivbd  45894  dvbdfbdioolem1  45899  dvbdfbdioolem2  45900  dvbdfbdioo  45901  ioodvbdlimc1lem1  45902  ioodvbdlimc1lem2  45903  ioodvbdlimc2lem  45905  stoweid  46034  fourierdlem30  46108  fourierdlem39  46117  fourierdlem42  46120  fourierdlem47  46124  fourierdlem68  46145  fourierdlem70  46147  fourierdlem71  46148  fourierdlem73  46150  fourierdlem77  46154  fourierdlem80  46157  fourierdlem83  46160  fourierdlem87  46164  fourierdlem103  46180  fourierdlem104  46181  etransclem23  46228  etransclem48  46253  rrndistlt  46261  ioorrnopnlem  46275  sge0isum  46398  hoicvr  46519  smflimlem4  46745  smfmullem1  46762  smfmullem2  46763  smfmullem3  46764  modlt0b  47337  itsclc0yqsol  48726