Theorem abscld 15615

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ‘cfv 6543  ℂcc 11205  ℝcr 11206  abscabs 15410

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5327  ax-pr 5391  ax-un 7755  ax-cnex 11263  ax-resscn 11264  ax-1cn 11265  ax-icn 11266  ax-addcl 11267  ax-addrcl 11268  ax-mulcl 11269  ax-mulrcl 11270  ax-mulcom 11271  ax-addass 11272  ax-mulass 11273  ax-distr 11274  ax-i2m1 11275  ax-1ne0 11276  ax-1rid 11277  ax-rnegex 11278  ax-rrecex 11279  ax-cnre 11280  ax-pre-lttri 11281  ax-pre-lttrn 11282  ax-pre-ltadd 11283  ax-pre-mulgt0 11284  ax-pre-sup 11285

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3848  df-ss 3897  df-pss 4013  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6307  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6497  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7381  df-ov 7427  df-oprab 7428  df-mpo 7429  df-om 7882  df-2nd 8006  df-frecs 8306  df-wrecs 8337  df-recs 8386  df-rdg 8425  df-er 8724  df-en 8981  df-dom 8982  df-sdom 8983  df-sup 9441  df-pnf 11352  df-mnf 11353  df-xr 11354  df-ltxr 11355  df-le 11356  df-sub 11550  df-neg 11551  df-div 11981  df-nn 12343  df-2 12412  df-3 12413  df-n0 12614  df-z 12701  df-uz 12973  df-rp 13128  df-seq 14152  df-exp 14212  df-cj 15275  df-re 15276  df-im 15277  df-sqrt 15411  df-abs 15412

This theorem is used by:  bhmafibid1  15644  lo1bddrp  15701  elo1mpt  15710  elo1mpt2  15711  elo1d  15712  o1bdd2  15717  o1bddrp  15718  rlimuni  15726  climuni  15728  o1eq  15746  rlimcld2  15754  rlimrege0  15755  climabs0  15761  mulcn2  15772  reccn2  15773  cn1lem  15774  cjcn2  15776  o1add  15790  o1mul  15791  o1sub  15792  rlimo1  15793  o1rlimmul  15795  climsqz  15817  climsqz2  15818  rlimsqzlem  15825  o1le  15829  climbdd  15848  caucvgrlem  15849  caucvgrlem2  15851  iseraltlem3  15860  iseralt  15861  fsumabs  15977  o1fsum  15989  iserabs  15991  cvgcmpce  15994  abscvgcvg  15995  divrcnv  16030  explecnv  16043  geomulcvg  16054  cvgrat  16061  mertenslem1  16062  mertenslem2  16063  fprodabs  16150  efcllem  16252  efaddlem  16268  eftlub  16286  ef01bndlem  16361  sin01bnd  16362  cos01bnd  16363  absef  16374  dvdsabseq  16492  alzdvds  16499  sqnprm  16887  pclem  17025  mul4sqlem  17140  xrsdsreclb  21729  gzrngunitlem  21747  gzrngunit  21748  prmirredlem  21787  nm2dif  24953  blcvx  25126  recld2  25143  addcnlem  25193  cnheiborlem  25284  cnheibor  25285  cnllycmp  25286  cphsqrtcl2  25516  ipcau2  25564  tcphcphlem1  25565  ipcnlem2  25574  cncmet  25652  trirn  25730  rrxdstprj1  25739  pjthlem1  25767  volsup2  25935  mbfi1fseqlem6  26050  iblabslem  26157  iblabs  26158  iblabsr  26159  iblmulc2  26160  itgabs  26164  bddmulibl  26168  bddiblnc  26171  itgcn  26174  dveflem  26308  dvlip  26322  dvlipcn  26323  c1liplem1  26325  dveq0  26329  dv11cn  26330  lhop1lem  26342  dvfsumabs  26352  dvfsumrlim  26360  dvfsumrlim2  26361  ftc1a  26366  ftc1lem4  26368  plyeq0lem  26538  aalioulem2  26669  aalioulem3  26670  aalioulem4  26671  aalioulem5  26672  aalioulem6  26673  aaliou  26674  geolim3  26675  aaliou2b  26677  aaliou3lem9  26686  ulmbdd  26734  ulmcn  26735  ulmdvlem1  26736  mtest  26740  mtestbdd  26741  iblulm  26743  itgulm  26744  radcnvlem1  26749  radcnvlem2  26750  radcnvlt1  26754  radcnvle  26756  dvradcnv  26757  pserulm  26758  psercnlem2  26760  psercnlem1  26761  psercn  26762  pserdvlem1  26763  pserdvlem2  26764  pserdv  26765  abelthlem2  26768  abelthlem3  26769  abelthlem5  26771  abelthlem7  26774  abelthlem8  26775  tanregt0  26876  efif1olem3  26881  efif1olem4  26882  eff1olem  26885  cosargd  26945  cosarg0d  26946  argregt0  26947  argrege0  26948  abslogle  26955  logcnlem3  26981  logcnlem4  26982  efopnlem1  26993  logtayl  26997  abscxp2  27030  cxpcn3lem  27084  abscxpbnd  27090  cosangneg2d  27144  lawcoslem1  27152  lawcos  27153  pythag  27154  isosctrlem3  27157  ssscongptld  27159  chordthmlem3  27171  chordthmlem4  27172  chordthmlem5  27173  heron  27175  bndatandm  27266  efrlim  27306  rlimcxp  27310  o1cxp  27311  cxploglim2  27315  divsqrtsumo1  27320  fsumharmonic  27348  lgamgulmlem2  27366  lgamgulmlem3  27367  lgamgulmlem5  27369  lgambdd  27373  lgamucov  27374  lgamcvg2  27391  ftalem1  27409  ftalem2  27410  ftalem3  27411  ftalem4  27412  ftalem5  27413  ftalem7  27415  logfacbnd3  27559  logfacrlim  27560  logexprlim  27561  dchrabs  27596  lgsdirprm  27667  lgsdilem2  27669  lgsne0  27671  lgsabs1  27672  mul2sq  27755  2sqlem3  27756  2sqblem  27767  vmadivsumb  27819  rplogsumlem2  27821  dchrisumlem2  27826  dchrisumlem3  27827  dchrisum  27828  dchrmusum2  27830  dchrvmasumlem2  27834  dchrvmasumlem3  27835  dchrvmasumiflem1  27837  dchrvmasumiflem2  27838  dchrisum0flblem1  27844  dchrisum0fno1  27847  dchrisum0lem1b  27851  dchrisum0lem1  27852  dchrisum0lem2a  27853  dchrisum0lem2  27854  dchrisum0lem3  27855  mudivsum  27866  mulogsumlem  27867  mulog2sumlem1  27870  mulog2sumlem2  27871  2vmadivsumlem  27876  log2sumbnd  27880  selberglem2  27882  selbergb  27885  selberg2b  27888  chpdifbndlem1  27889  selberg3lem1  27893  selberg3lem2  27894  selberg4lem1  27896  pntrsumo1  27901  pntrsumbnd  27902  pntrsumbnd2  27903  pntrlog2bndlem1  27913  pntrlog2bndlem2  27914  pntrlog2bndlem3  27915  pntrlog2bndlem4  27916  pntrlog2bndlem5  27917  pntrlog2bndlem6  27919  pntrlog2bnd  27920  pntpbnd1a  27921  pntpbnd2  27923  pntibndlem2  27927  pntlemn  27936  pntlemj  27939  pntlemf  27941  pntlemo  27943  pntlem3  27945  pntleml  27947  smcnlem  31308  nmoub3i  31384  isblo3i  31412  htthlem  31528  bcs2  31793  pjhthlem1  32002  nmfnsetre  32488  nmfnleub2  32537  nmfnge0  32538  nmbdfnlbi  32660  nmcfnexi  32662  nmcfnlbi  32663  lnfnconi  32666  cnlnadjlem2  32679  cnlnadjlem7  32684  nmopcoadji  32712  leopnmid  32749  constrdircl  34447  iconstr  34448  constrremulcl  34449  constrimcl  34452  constrmulcl  34453  constrinvcl  34455  constrabscl  34460  constrsqrtcl  34461  sqsscirc2  34591  subfaclim  36043  subfacval3  36044  sinccvglem  36527  dnicld1  37434  dnibndlem2  37441  dnibndlem6  37445  dnibndlem9  37448  dnibndlem12  37451  dnicn  37454  knoppcnlem4  37458  knoppcnlem6  37460  unblimceq0lem  37468  unblimceq0  37469  unbdqndv2lem1  37471  unbdqndv2lem2  37472  knoppndvlem11  37484  knoppndvlem12  37485  knoppndvlem14  37487  knoppndvlem15  37488  knoppndvlem17  37490  knoppndvlem18  37491  knoppndvlem20  37493  knoppndvlem21  37494  poimirlem29  38676  poimir  38680  iblabsnclem  38710  iblabsnc  38711  iblmulc2nc  38712  itgabsnc  38716  ftc1cnnclem  38718  ftc1anclem1  38720  ftc1anclem2  38721  ftc1anclem4  38723  ftc1anclem5  38724  ftc1anclem6  38725  ftc1anclem7  38726  ftc1anclem8  38727  ftc1anc  38728  ftc2nc  38729  dvasin  38731  areacirclem1  38735  areacirclem2  38736  areacirclem4  38738  areacirclem5  38739  areacirc  38740  geomcau  38802  cntotbnd  38839  rrndstprj1  38873  rrndstprj2  38874  ismrer1  38881  readvrec  43522  readvcot  43524  dffltz  43779  rencldnfilem  43936  irrapxlem2  43939  irrapxlem4  43941  irrapxlem5  43942  pellexlem2  43946  pellexlem6  43950  pell14qrgt0  43975  congabseq  44090  acongeq  44099  modabsdifz  44102  jm2.26lem3  44117  sqrtcvallem4  44748  extoimad  45273  imo72b2lem0  45274  imo72b2  45281  dvgrat  45405  cvgdvgrat  45406  radcnvrat  45407  dvconstbi  45427  binomcxplemnotnn0  45449  dstregt0  46406  absnpncan2d  46426  absnpncan3d  46431  abslt2sqd  46480  rexabslelem  46536  cvgcaule  46609  fprodabs2  46715  mullimc  46736  mullimcf  46743  limcrecl  46749  lptre2pt  46758  limcleqr  46762  addlimc  46766  0ellimcdiv  46767  limclner  46769  climleltrp  46794  climisp  46864  climxrrelem  46867  cnrefiisplem  46947  climxlim2lem  46963  cncficcgt0  47006  dvdivbd  47041  dvbdfbdioolem1  47046  dvbdfbdioolem2  47047  dvbdfbdioo  47048  ioodvbdlimc1lem1  47049  ioodvbdlimc1lem2  47050  ioodvbdlimc2lem  47052  stoweid  47181  fourierdlem30  47255  fourierdlem39  47264  fourierdlem42  47267  fourierdlem47  47271  fourierdlem68  47292  fourierdlem70  47294  fourierdlem71  47295  fourierdlem73  47297  fourierdlem77  47301  fourierdlem80  47304  fourierdlem83  47307  fourierdlem87  47311  fourierdlem103  47327  fourierdlem104  47328  etransclem23  47375  etransclem48  47400  rrndistlt  47408  ioorrnopnlem  47422  sge0isum  47545  hoicvr  47666  smflimlem4  47892  smfmullem1  47909  smfmullem2  47910  smfmullem3  47911  modlt0b  48547  itsclc0yqsol  49984