Theorem abscld 15495

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2143  ‘cfv 6536  ℂcc 11102  ℝcr 11103  abscabs 15290

This proof depends on 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 11160  ax-resscn 11161  ax-1cn 11162  ax-icn 11163  ax-addcl 11164  ax-addrcl 11165  ax-mulcl 11166  ax-mulrcl 11167  ax-mulcom 11168  ax-addass 11169  ax-mulass 11170  ax-distr 11171  ax-i2m1 11172  ax-1ne0 11173  ax-1rid 11174  ax-rnegex 11175  ax-rrecex 11176  ax-cnre 11177  ax-pre-lttri 11178  ax-pre-lttrn 11179  ax-pre-ltadd 11180  ax-pre-mulgt0 11181  ax-pre-sup 11182

This proof 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 11249  df-mnf 11250  df-xr 11251  df-ltxr 11252  df-le 11253  df-sub 11447  df-neg 11448  df-div 11876  df-nn 12238  df-2 12307  df-3 12308  df-n0 12509  df-z 12596  df-uz 12867  df-rp 13021  df-seq 14043  df-exp 14103  df-cj 15155  df-re 15156  df-im 15157  df-sqrt 15291  df-abs 15292

This theorem is used by:  bhmafibid1  15524  lo1bddrp  15581  elo1mpt  15590  elo1mpt2  15591  elo1d  15592  o1bdd2  15597  o1bddrp  15598  rlimuni  15606  climuni  15608  o1eq  15626  rlimcld2  15634  rlimrege0  15635  climabs0  15641  mulcn2  15652  reccn2  15653  cn1lem  15654  cjcn2  15656  o1add  15670  o1mul  15671  o1sub  15672  rlimo1  15673  o1rlimmul  15675  climsqz  15697  climsqz2  15698  rlimsqzlem  15705  o1le  15709  climbdd  15728  caucvgrlem  15729  caucvgrlem2  15731  iseraltlem3  15740  iseralt  15741  fsumabs  15858  o1fsum  15870  iserabs  15872  cvgcmpce  15875  abscvgcvg  15876  divrcnv  15911  explecnv  15924  geomulcvg  15935  cvgrat  15942  mertenslem1  15943  mertenslem2  15944  fprodabs  16033  efcllem  16135  efaddlem  16151  eftlub  16169  ef01bndlem  16244  sin01bnd  16245  cos01bnd  16246  absef  16257  dvdsabseq  16375  alzdvds  16382  sqnprm  16765  pclem  16902  mul4sqlem  17017  xrsdsreclb  21573  gzrngunitlem  21591  gzrngunit  21592  prmirredlem  21631  nm2dif  24791  blcvx  24964  recld2  24981  addcnlem  25031  cnheiborlem  25122  cnheibor  25123  cnllycmp  25124  cphsqrtcl2  25354  ipcau2  25402  tcphcphlem1  25403  ipcnlem2  25412  cncmet  25490  trirn  25568  rrxdstprj1  25577  pjthlem1  25605  volsup2  25773  mbfi1fseqlem6  25888  iblabslem  25996  iblabs  25997  iblabsr  25998  iblmulc2  25999  itgabs  26003  bddmulibl  26007  bddiblnc  26010  itgcn  26013  dveflem  26147  dvlip  26161  dvlipcn  26162  c1liplem1  26164  dveq0  26168  dv11cn  26169  lhop1lem  26181  dvfsumabs  26191  dvfsumrlim  26199  dvfsumrlim2  26200  ftc1a  26205  ftc1lem4  26207  plyeq0lem  26376  aalioulem2  26505  aalioulem3  26506  aalioulem4  26507  aalioulem5  26508  aalioulem6  26509  aaliou  26510  geolim3  26511  aaliou2b  26513  aaliou3lem9  26522  ulmbdd  26570  ulmcn  26571  ulmdvlem1  26572  mtest  26576  mtestbdd  26577  iblulm  26579  itgulm  26580  radcnvlem1  26585  radcnvlem2  26586  radcnvlt1  26590  radcnvle  26592  dvradcnv  26593  pserulm  26594  psercnlem2  26596  psercnlem1  26597  psercn  26598  pserdvlem1  26599  pserdvlem2  26600  pserdv  26601  abelthlem2  26604  abelthlem3  26605  abelthlem5  26607  abelthlem7  26610  abelthlem8  26611  tanregt0  26713  efif1olem3  26718  efif1olem4  26719  eff1olem  26722  cosargd  26782  cosarg0d  26783  argregt0  26784  argrege0  26785  abslogle  26792  logcnlem3  26818  logcnlem4  26819  efopnlem1  26830  logtayl  26834  abscxp2  26867  cxpcn3lem  26921  abscxpbnd  26927  cosangneg2d  26981  lawcoslem1  26989  lawcos  26990  pythag  26991  isosctrlem3  26994  ssscongptld  26996  chordthmlem3  27008  chordthmlem4  27009  chordthmlem5  27010  heron  27012  bndatandm  27103  efrlim  27143  rlimcxp  27147  o1cxp  27148  cxploglim2  27152  divsqrtsumo1  27157  fsumharmonic  27185  lgamgulmlem2  27203  lgamgulmlem3  27204  lgamgulmlem5  27206  lgambdd  27210  lgamucov  27211  lgamcvg2  27228  ftalem1  27246  ftalem2  27247  ftalem3  27248  ftalem4  27249  ftalem5  27250  ftalem7  27252  logfacbnd3  27396  logfacrlim  27397  logexprlim  27398  dchrabs  27433  lgsdirprm  27504  lgsdilem2  27506  lgsne0  27508  lgsabs1  27509  mul2sq  27592  2sqlem3  27593  2sqblem  27604  vmadivsumb  27656  rplogsumlem2  27658  dchrisumlem2  27663  dchrisumlem3  27664  dchrisum  27665  dchrmusum2  27667  dchrvmasumlem2  27671  dchrvmasumlem3  27672  dchrvmasumiflem1  27674  dchrvmasumiflem2  27675  dchrisum0flblem1  27681  dchrisum0fno1  27684  dchrisum0lem1b  27688  dchrisum0lem1  27689  dchrisum0lem2a  27690  dchrisum0lem2  27691  dchrisum0lem3  27692  mudivsum  27703  mulogsumlem  27704  mulog2sumlem1  27707  mulog2sumlem2  27708  2vmadivsumlem  27713  log2sumbnd  27717  selberglem2  27719  selbergb  27722  selberg2b  27725  chpdifbndlem1  27726  selberg3lem1  27730  selberg3lem2  27731  selberg4lem1  27733  pntrsumo1  27738  pntrsumbnd  27739  pntrsumbnd2  27740  pntrlog2bndlem1  27750  pntrlog2bndlem2  27751  pntrlog2bndlem3  27752  pntrlog2bndlem4  27753  pntrlog2bndlem5  27754  pntrlog2bndlem6  27756  pntrlog2bnd  27757  pntpbnd1a  27758  pntpbnd2  27760  pntibndlem2  27764  pntlemn  27773  pntlemj  27776  pntlemf  27778  pntlemo  27780  pntlem3  27782  pntleml  27784  smcnlem  31058  nmoub3i  31134  isblo3i  31162  htthlem  31278  bcs2  31543  pjhthlem1  31752  nmfnsetre  32238  nmfnleub2  32287  nmfnge0  32288  nmbdfnlbi  32410  nmcfnexi  32412  nmcfnlbi  32413  lnfnconi  32416  cnlnadjlem2  32429  cnlnadjlem7  32434  nmopcoadji  32462  leopnmid  32499  constrdircl  34164  iconstr  34165  constrremulcl  34166  constrimcl  34169  constrmulcl  34170  constrinvcl  34172  constrabscl  34177  constrsqrtcl  34178  sqsscirc2  34308  subfaclim  35688  subfacval3  35689  sinccvglem  36172  dnicld1  37089  dnibndlem2  37096  dnibndlem6  37100  dnibndlem9  37103  dnibndlem12  37106  dnicn  37109  knoppcnlem4  37113  knoppcnlem6  37115  unblimceq0lem  37123  unblimceq0  37124  unbdqndv2lem1  37126  unbdqndv2lem2  37127  knoppndvlem11  37139  knoppndvlem12  37140  knoppndvlem14  37142  knoppndvlem15  37143  knoppndvlem17  37145  knoppndvlem18  37146  knoppndvlem20  37148  knoppndvlem21  37149  poimirlem29  38328  poimir  38332  iblabsnclem  38362  iblabsnc  38363  iblmulc2nc  38364  itgabsnc  38368  ftc1cnnclem  38370  ftc1anclem1  38372  ftc1anclem2  38373  ftc1anclem4  38375  ftc1anclem5  38376  ftc1anclem6  38377  ftc1anclem7  38378  ftc1anclem8  38379  ftc1anc  38380  ftc2nc  38381  dvasin  38383  areacirclem1  38387  areacirclem2  38388  areacirclem4  38390  areacirclem5  38391  areacirc  38392  geomcau  38438  cntotbnd  38475  rrndstprj1  38509  rrndstprj2  38510  ismrer1  38517  readvrec  43151  readvcot  43153  dffltz  43394  rencldnfilem  43575  irrapxlem2  43578  irrapxlem4  43580  irrapxlem5  43581  pellexlem2  43585  pellexlem6  43589  pell14qrgt0  43614  congabseq  43729  acongeq  43738  modabsdifz  43741  jm2.26lem3  43756  sqrtcvallem4  44393  extoimad  44918  imo72b2lem0  44919  imo72b2  44926  dvgrat  45050  cvgdvgrat  45051  radcnvrat  45052  dvconstbi  45072  binomcxplemnotnn0  45094  dstregt0  46029  absnpncan2d  46049  absnpncan3d  46054  abslt2sqd  46104  rexabslelem  46160  cvgcaule  46233  fprodabs2  46339  mullimc  46360  mullimcf  46367  limcrecl  46373  lptre2pt  46382  limcleqr  46386  addlimc  46390  0ellimcdiv  46391  limclner  46393  climleltrp  46418  climisp  46488  climxrrelem  46491  cnrefiisplem  46571  climxlim2lem  46587  cncficcgt0  46630  dvdivbd  46665  dvbdfbdioolem1  46670  dvbdfbdioolem2  46671  dvbdfbdioo  46672  ioodvbdlimc1lem1  46673  ioodvbdlimc1lem2  46674  ioodvbdlimc2lem  46676  stoweid  46805  fourierdlem30  46879  fourierdlem39  46888  fourierdlem42  46891  fourierdlem47  46895  fourierdlem68  46916  fourierdlem70  46918  fourierdlem71  46919  fourierdlem73  46921  fourierdlem77  46925  fourierdlem80  46928  fourierdlem83  46931  fourierdlem87  46935  fourierdlem103  46951  fourierdlem104  46952  etransclem23  46999  etransclem48  47024  rrndistlt  47032  ioorrnopnlem  47046  sge0isum  47169  hoicvr  47290  smflimlem4  47516  smfmullem1  47533  smfmullem2  47534  smfmullem3  47535  modlt0b  48134  itsclc0yqsol  49572