Theorem abscld 15453

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

Syntax hints:   → wi 4   ∈ wcel 2108  ‘cfv 6530  ℂcc 11125  ℝcr 11126  abscabs 15251

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727  ax-cnex 11183  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203  ax-pre-mulgt0 11204  ax-pre-sup 11205

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3359  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-riota 7360  df-ov 7406  df-oprab 7407  df-mpo 7408  df-om 7860  df-2nd 7987  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-rdg 8422  df-er 8717  df-en 8958  df-dom 8959  df-sdom 8960  df-sup 9452  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-sub 11466  df-neg 11467  df-div 11893  df-nn 12239  df-2 12301  df-3 12302  df-n0 12500  df-z 12587  df-uz 12851  df-rp 13007  df-seq 14018  df-exp 14078  df-cj 15116  df-re 15117  df-im 15118  df-sqrt 15252  df-abs 15253

This theorem is referenced by:  bhmafibid1  15482  lo1bddrp  15539  elo1mpt  15548  elo1mpt2  15549  elo1d  15550  o1bdd2  15555  o1bddrp  15556  rlimuni  15564  climuni  15566  o1eq  15584  rlimcld2  15592  rlimrege0  15593  climabs0  15599  mulcn2  15610  reccn2  15611  cn1lem  15612  cjcn2  15614  o1add  15628  o1mul  15629  o1sub  15630  rlimo1  15631  o1rlimmul  15633  climsqz  15655  climsqz2  15656  rlimsqzlem  15663  o1le  15667  climbdd  15686  caucvgrlem  15687  caucvgrlem2  15689  iseraltlem3  15698  iseralt  15699  fsumabs  15815  o1fsum  15827  iserabs  15829  cvgcmpce  15832  abscvgcvg  15833  divrcnv  15866  explecnv  15879  geomulcvg  15890  cvgrat  15897  mertenslem1  15898  mertenslem2  15899  fprodabs  15988  efcllem  16091  efaddlem  16107  eftlub  16125  ef01bndlem  16200  sin01bnd  16201  cos01bnd  16202  absef  16213  dvdsabseq  16330  alzdvds  16337  sqnprm  16719  pclem  16856  mul4sqlem  16971  xrsdsreclb  21379  gzrngunitlem  21398  gzrngunit  21399  prmirredlem  21431  nm2dif  24562  blcvx  24735  recld2  24752  addcnlem  24802  cnheiborlem  24902  cnheibor  24903  cnllycmp  24904  cphsqrtcl2  25136  ipcau2  25184  tcphcphlem1  25185  ipcnlem2  25194  cncmet  25272  trirn  25350  rrxdstprj1  25359  pjthlem1  25387  volsup2  25556  mbfi1fseqlem6  25671  iblabslem  25779  iblabs  25780  iblabsr  25781  iblmulc2  25782  itgabs  25786  bddmulibl  25790  bddiblnc  25793  itgcn  25796  dveflem  25933  dvlip  25948  dvlipcn  25949  c1liplem1  25951  dveq0  25955  dv11cn  25956  lhop1lem  25968  dvfsumabs  25979  dvfsumrlim  25988  dvfsumrlim2  25989  ftc1a  25994  ftc1lem4  25996  plyeq0lem  26165  aalioulem2  26291  aalioulem3  26292  aalioulem4  26293  aalioulem5  26294  aalioulem6  26295  aaliou  26296  geolim3  26297  aaliou2b  26299  aaliou3lem9  26308  ulmbdd  26357  ulmcn  26358  ulmdvlem1  26359  mtest  26363  mtestbdd  26364  iblulm  26366  itgulm  26367  radcnvlem1  26372  radcnvlem2  26373  radcnvlt1  26377  radcnvle  26379  dvradcnv  26380  pserulm  26381  psercnlem2  26384  psercnlem1  26385  psercn  26386  pserdvlem1  26387  pserdvlem2  26388  pserdv  26389  abelthlem2  26392  abelthlem3  26393  abelthlem5  26395  abelthlem7  26398  abelthlem8  26399  tanregt0  26498  efif1olem3  26503  efif1olem4  26504  eff1olem  26507  cosargd  26567  cosarg0d  26568  argregt0  26569  argrege0  26570  abslogle  26577  logcnlem3  26603  logcnlem4  26604  efopnlem1  26615  logtayl  26619  abscxp2  26652  cxpcn3lem  26707  abscxpbnd  26713  cosangneg2d  26767  lawcoslem1  26775  lawcos  26776  pythag  26777  isosctrlem3  26780  ssscongptld  26782  chordthmlem3  26794  chordthmlem4  26795  chordthmlem5  26796  heron  26798  bndatandm  26889  efrlim  26929  efrlimOLD  26930  rlimcxp  26934  o1cxp  26935  cxploglim2  26939  divsqrtsumo1  26944  fsumharmonic  26972  lgamgulmlem2  26990  lgamgulmlem3  26991  lgamgulmlem5  26993  lgambdd  26997  lgamucov  26998  lgamcvg2  27015  ftalem1  27033  ftalem2  27034  ftalem3  27035  ftalem4  27036  ftalem5  27037  ftalem7  27039  logfacbnd3  27184  logfacrlim  27185  logexprlim  27186  dchrabs  27221  lgsdirprm  27292  lgsdilem2  27294  lgsne0  27296  lgsabs1  27297  mul2sq  27380  2sqlem3  27381  2sqblem  27392  vmadivsumb  27444  rplogsumlem2  27446  dchrisumlem2  27451  dchrisumlem3  27452  dchrisum  27453  dchrmusum2  27455  dchrvmasumlem2  27459  dchrvmasumlem3  27460  dchrvmasumiflem1  27462  dchrvmasumiflem2  27463  dchrisum0flblem1  27469  dchrisum0fno1  27472  dchrisum0lem1b  27476  dchrisum0lem1  27477  dchrisum0lem2a  27478  dchrisum0lem2  27479  dchrisum0lem3  27480  mudivsum  27491  mulogsumlem  27492  mulog2sumlem1  27495  mulog2sumlem2  27496  2vmadivsumlem  27501  log2sumbnd  27505  selberglem2  27507  selbergb  27510  selberg2b  27513  chpdifbndlem1  27514  selberg3lem1  27518  selberg3lem2  27519  selberg4lem1  27521  pntrsumo1  27526  pntrsumbnd  27527  pntrsumbnd2  27528  pntrlog2bndlem1  27538  pntrlog2bndlem2  27539  pntrlog2bndlem3  27540  pntrlog2bndlem4  27541  pntrlog2bndlem5  27542  pntrlog2bndlem6  27544  pntrlog2bnd  27545  pntpbnd1a  27546  pntpbnd2  27548  pntibndlem2  27552  pntlemn  27561  pntlemj  27564  pntlemf  27566  pntlemo  27568  pntlem3  27570  pntleml  27572  smcnlem  30624  nmoub3i  30700  isblo3i  30728  htthlem  30844  bcs2  31109  pjhthlem1  31318  nmfnsetre  31804  nmfnleub2  31853  nmfnge0  31854  nmbdfnlbi  31976  nmcfnexi  31978  nmcfnlbi  31979  lnfnconi  31982  cnlnadjlem2  31995  cnlnadjlem7  32000  nmopcoadji  32028  leopnmid  32065  constrdircl  33745  iconstr  33746  constrremulcl  33747  constrimcl  33750  constrmulcl  33751  constrinvcl  33753  constrabscl  33758  constrsqrtcl  33759  sqsscirc2  33886  subfaclim  35156  subfacval3  35157  sinccvglem  35640  dnicld1  36436  dnibndlem2  36443  dnibndlem6  36447  dnibndlem9  36450  dnibndlem12  36453  dnicn  36456  knoppcnlem4  36460  knoppcnlem6  36462  unblimceq0lem  36470  unblimceq0  36471  unbdqndv2lem1  36473  unbdqndv2lem2  36474  knoppndvlem11  36486  knoppndvlem12  36487  knoppndvlem14  36489  knoppndvlem15  36490  knoppndvlem17  36492  knoppndvlem18  36493  knoppndvlem20  36495  knoppndvlem21  36496  poimirlem29  37619  poimir  37623  iblabsnclem  37653  iblabsnc  37654  iblmulc2nc  37655  itgabsnc  37659  ftc1cnnclem  37661  ftc1anclem1  37663  ftc1anclem2  37664  ftc1anclem4  37666  ftc1anclem5  37667  ftc1anclem6  37668  ftc1anclem7  37669  ftc1anclem8  37670  ftc1anc  37671  ftc2nc  37672  dvasin  37674  areacirclem1  37678  areacirclem2  37679  areacirclem4  37681  areacirclem5  37682  areacirc  37683  geomcau  37729  cntotbnd  37766  rrndstprj1  37800  rrndstprj2  37801  ismrer1  37808  readvrec  42352  readvcot  42354  dffltz  42604  rencldnfilem  42790  irrapxlem2  42793  irrapxlem4  42795  irrapxlem5  42796  pellexlem2  42800  pellexlem6  42804  pell14qrgt0  42829  congabseq  42945  acongeq  42954  modabsdifz  42957  jm2.26lem3  42972  sqrtcvallem4  43610  extoimad  44135  imo72b2lem0  44136  imo72b2  44143  dvgrat  44284  cvgdvgrat  44285  radcnvrat  44286  dvconstbi  44306  binomcxplemnotnn0  44328  dstregt0  45258  absnpncan2d  45279  absnpncan3d  45284  abslt2sqd  45335  rexabslelem  45393  cvgcaule  45466  fprodabs2  45572  mullimc  45593  mullimcf  45600  limcrecl  45606  lptre2pt  45617  limcleqr  45621  addlimc  45625  0ellimcdiv  45626  limclner  45628  climleltrp  45653  climisp  45723  climxrrelem  45726  cnrefiisplem  45806  climxlim2lem  45822  cncficcgt0  45865  dvdivbd  45900  dvbdfbdioolem1  45905  dvbdfbdioolem2  45906  dvbdfbdioo  45907  ioodvbdlimc1lem1  45908  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  stoweid  46040  fourierdlem30  46114  fourierdlem39  46123  fourierdlem42  46126  fourierdlem47  46130  fourierdlem68  46151  fourierdlem70  46153  fourierdlem71  46154  fourierdlem73  46156  fourierdlem77  46160  fourierdlem80  46163  fourierdlem83  46166  fourierdlem87  46170  fourierdlem103  46186  fourierdlem104  46187  etransclem23  46234  etransclem48  46259  rrndistlt  46267  ioorrnopnlem  46281  sge0isum  46404  hoicvr  46525  smflimlem4  46751  smfmullem1  46768  smfmullem2  46769  smfmullem3  46770  itsclc0yqsol  48692