MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  abscld Structured version   Visualization version   GIF version

Theorem abscld 14392
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
StepHypRef Expression
1 abscld.1 . 2 (𝜑𝐴 ∈ ℂ)
2 abscl 14235 . 2 (𝐴 ∈ ℂ → (abs‘𝐴) ∈ ℝ)
31, 2syl 17 1 (𝜑 → (abs‘𝐴) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2155  cfv 6095  cc 10213  cr 10214  abscabs 14191
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-8 2157  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781  ax-sep 4968  ax-nul 4977  ax-pow 5029  ax-pr 5090  ax-un 7173  ax-cnex 10271  ax-resscn 10272  ax-1cn 10273  ax-icn 10274  ax-addcl 10275  ax-addrcl 10276  ax-mulcl 10277  ax-mulrcl 10278  ax-mulcom 10279  ax-addass 10280  ax-mulass 10281  ax-distr 10282  ax-i2m1 10283  ax-1ne0 10284  ax-1rid 10285  ax-rnegex 10286  ax-rrecex 10287  ax-cnre 10288  ax-pre-lttri 10289  ax-pre-lttrn 10290  ax-pre-ltadd 10291  ax-pre-mulgt0 10292  ax-pre-sup 10293
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-eu 2633  df-mo 2634  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-ne 2975  df-nel 3078  df-ral 3097  df-rex 3098  df-reu 3099  df-rmo 3100  df-rab 3101  df-v 3389  df-sbc 3628  df-csb 3723  df-dif 3766  df-un 3768  df-in 3770  df-ss 3777  df-pss 3779  df-nul 4111  df-if 4274  df-pw 4347  df-sn 4365  df-pr 4367  df-tp 4369  df-op 4371  df-uni 4624  df-iun 4707  df-br 4838  df-opab 4900  df-mpt 4917  df-tr 4940  df-id 5213  df-eprel 5218  df-po 5226  df-so 5227  df-fr 5264  df-we 5266  df-xp 5311  df-rel 5312  df-cnv 5313  df-co 5314  df-dm 5315  df-rn 5316  df-res 5317  df-ima 5318  df-pred 5887  df-ord 5933  df-on 5934  df-lim 5935  df-suc 5936  df-iota 6058  df-fun 6097  df-fn 6098  df-f 6099  df-f1 6100  df-fo 6101  df-f1o 6102  df-fv 6103  df-riota 6829  df-ov 6871  df-oprab 6872  df-mpt2 6873  df-om 7290  df-2nd 7393  df-wrecs 7636  df-recs 7698  df-rdg 7736  df-er 7973  df-en 8187  df-dom 8188  df-sdom 8189  df-sup 8581  df-pnf 10355  df-mnf 10356  df-xr 10357  df-ltxr 10358  df-le 10359  df-sub 10547  df-neg 10548  df-div 10964  df-nn 11300  df-2 11358  df-3 11359  df-n0 11554  df-z 11638  df-uz 11899  df-rp 12041  df-seq 13019  df-exp 13078  df-cj 14056  df-re 14057  df-im 14058  df-sqrt 14192  df-abs 14193
This theorem is referenced by:  lo1bddrp  14473  elo1mpt  14482  elo1mpt2  14483  elo1d  14484  o1bdd2  14489  o1bddrp  14490  rlimuni  14498  climuni  14500  o1eq  14518  rlimcld2  14526  rlimrege0  14527  climabs0  14533  mulcn2  14543  reccn2  14544  cn1lem  14545  cjcn2  14547  o1add  14561  o1mul  14562  o1sub  14563  rlimo1  14564  o1rlimmul  14566  climsqz  14588  climsqz2  14589  rlimsqzlem  14596  o1le  14600  climbdd  14619  caucvgrlem  14620  caucvgrlem2  14622  iseraltlem3  14631  iseralt  14632  fsumabs  14749  o1fsum  14761  iserabs  14763  cvgcmpce  14766  abscvgcvg  14767  divrcnv  14800  explecnv  14813  geomulcvg  14823  cvgrat  14830  mertenslem1  14831  mertenslem2  14832  fprodabs  14919  efcllem  15022  efaddlem  15037  eftlub  15053  ef01bndlem  15128  sin01bnd  15129  cos01bnd  15130  absef  15141  dvdsabseq  15252  alzdvds  15259  sqnprm  15625  pclem  15754  mul4sqlem  15868  xrsdsreclb  19995  gzrngunitlem  20013  gzrngunit  20014  prmirredlem  20043  nm2dif  22636  blcvx  22808  recld2  22824  addcnlem  22874  cnheiborlem  22960  cnheibor  22961  cnllycmp  22962  cphsqrtcl2  23192  ipcau2  23239  tchcphlem1  23240  ipcnlem2  23249  cncmet  23325  trirn  23389  rrxdstprj1  23398  pjthlem1  23414  volsup2  23580  mbfi1fseqlem6  23695  iblabslem  23802  iblabs  23803  iblabsr  23804  iblmulc2  23805  itgabs  23809  bddmulibl  23813  itgcn  23817  dveflem  23950  dvlip  23964  dvlipcn  23965  c1liplem1  23967  dveq0  23971  dv11cn  23972  lhop1lem  23984  dvfsumabs  23994  dvfsumrlim  24002  dvfsumrlim2  24003  ftc1a  24008  ftc1lem4  24010  plyeq0lem  24174  aalioulem2  24296  aalioulem3  24297  aalioulem4  24298  aalioulem5  24299  aalioulem6  24300  aaliou  24301  geolim3  24302  aaliou2b  24304  aaliou3lem9  24313  ulmbdd  24360  ulmcn  24361  ulmdvlem1  24362  mtest  24366  mtestbdd  24367  iblulm  24369  itgulm  24370  radcnvlem1  24375  radcnvlem2  24376  radcnvlt1  24380  radcnvle  24382  dvradcnv  24383  pserulm  24384  psercnlem2  24386  psercnlem1  24387  psercn  24388  pserdvlem1  24389  pserdvlem2  24390  pserdv  24391  abelthlem2  24394  abelthlem3  24395  abelthlem5  24397  abelthlem7  24400  abelthlem8  24401  tanregt0  24494  efif1olem3  24499  efif1olem4  24500  eff1olem  24503  cosargd  24562  cosarg0d  24563  argrege0  24565  abslogle  24572  logcnlem3  24598  logcnlem4  24599  efopnlem1  24610  logtayl  24614  abscxp2  24647  cxpcn3lem  24696  abscxpbnd  24702  cosangneg2d  24745  lawcoslem1  24753  lawcos  24754  pythag  24755  isosctrlem3  24758  ssscongptld  24760  chordthmlem3  24769  chordthmlem4  24770  chordthmlem5  24771  heron  24773  bndatandm  24864  efrlim  24904  rlimcxp  24908  o1cxp  24909  cxploglim2  24913  divsqrtsumo1  24918  fsumharmonic  24946  lgamgulmlem2  24964  lgamgulmlem3  24965  lgamgulmlem5  24967  lgambdd  24971  lgamucov  24972  lgamcvg2  24989  ftalem1  25007  ftalem2  25008  ftalem3  25009  ftalem4  25010  ftalem5  25011  ftalem7  25013  logfacbnd3  25156  logfacrlim  25157  logexprlim  25158  dchrabs  25193  lgsdirprm  25264  lgsdilem2  25266  lgsne0  25268  lgsabs1  25269  mul2sq  25352  2sqlem3  25353  2sqblem  25364  vmadivsumb  25380  rplogsumlem2  25382  dchrisumlem2  25387  dchrisumlem3  25388  dchrisum  25389  dchrmusum2  25391  dchrvmasumlem2  25395  dchrvmasumlem3  25396  dchrvmasumiflem1  25398  dchrvmasumiflem2  25399  dchrisum0flblem1  25405  dchrisum0fno1  25408  dchrisum0lem1b  25412  dchrisum0lem1  25413  dchrisum0lem2a  25414  dchrisum0lem2  25415  dchrisum0lem3  25416  mudivsum  25427  mulogsumlem  25428  mulog2sumlem1  25431  mulog2sumlem2  25432  2vmadivsumlem  25437  log2sumbnd  25441  selberglem2  25443  selbergb  25446  selberg2b  25449  chpdifbndlem1  25450  selberg3lem1  25454  selberg3lem2  25455  selberg4lem1  25457  pntrsumo1  25462  pntrsumbnd  25463  pntrsumbnd2  25464  pntrlog2bndlem1  25474  pntrlog2bndlem2  25475  pntrlog2bndlem3  25476  pntrlog2bndlem4  25477  pntrlog2bndlem5  25478  pntrlog2bndlem6  25480  pntrlog2bnd  25481  pntpbnd1a  25482  pntpbnd2  25484  pntibndlem2  25488  pntlemn  25497  pntlemj  25500  pntlemf  25502  pntlemo  25504  pntlem3  25506  pntleml  25508  smcnlem  27874  nmoub3i  27950  isblo3i  27978  htthlem  28096  bcs2  28361  pjhthlem1  28572  nmfnsetre  29058  nmfnleub2  29107  nmfnge0  29108  nmbdfnlbi  29230  nmcfnexi  29232  nmcfnlbi  29233  lnfnconi  29236  cnlnadjlem2  29249  cnlnadjlem7  29254  nmopcoadji  29282  leopnmid  29319  bhmafibid1  29963  sqsscirc2  30274  subfaclim  31487  subfacval3  31488  sinccvglem  31882  dnicld1  32773  dnibndlem2  32780  dnibndlem6  32784  dnibndlem9  32787  dnibndlem12  32790  dnicn  32793  knoppcnlem4  32797  knoppcnlem6  32799  unblimceq0lem  32808  unblimceq0  32809  unbdqndv2lem1  32811  unbdqndv2lem2  32812  knoppndvlem11  32824  knoppndvlem12  32825  knoppndvlem14  32827  knoppndvlem15  32828  knoppndvlem17  32830  knoppndvlem18  32831  knoppndvlem20  32833  knoppndvlem21  32834  poimirlem29  33745  poimir  33749  iblabsnclem  33779  iblabsnc  33780  iblmulc2nc  33781  itgabsnc  33785  bddiblnc  33786  ftc1cnnclem  33789  ftc1anclem1  33791  ftc1anclem2  33792  ftc1anclem4  33794  ftc1anclem5  33795  ftc1anclem6  33796  ftc1anclem7  33797  ftc1anclem8  33798  ftc1anc  33799  ftc2nc  33800  dvasin  33802  areacirclem1  33806  areacirclem2  33807  areacirclem4  33809  areacirclem5  33810  areacirc  33811  geomcau  33860  cntotbnd  33900  rrndstprj1  33934  rrndstprj2  33935  ismrer1  33942  rencldnfilem  37880  irrapxlem2  37883  irrapxlem4  37885  irrapxlem5  37886  pellexlem2  37890  pellexlem6  37894  pell14qrgt0  37919  congabseq  38036  acongeq  38045  modabsdifz  38048  jm2.26lem3  38063  extoimad  38958  imo72b2lem0  38959  imo72b2  38969  dvgrat  39005  cvgdvgrat  39006  radcnvrat  39007  dvconstbi  39027  binomcxplemnotnn0  39049  dstregt0  39969  absnpncan2d  39991  absnpncan3d  39996  abslt2sqd  40050  rexabslelem  40118  fprodabs2  40301  mullimc  40322  mullimcf  40329  limcrecl  40335  lptre2pt  40346  limcleqr  40350  addlimc  40354  0ellimcdiv  40355  limclner  40357  climleltrp  40382  climisp  40452  climxrrelem  40455  cnrefiisplem  40529  climxlim2lem  40545  cncficcgt0  40575  dvdivbd  40612  dvbdfbdioolem1  40617  dvbdfbdioolem2  40618  dvbdfbdioo  40619  ioodvbdlimc1lem1  40620  ioodvbdlimc1lem2  40621  ioodvbdlimc2lem  40623  stoweid  40753  fourierdlem30  40827  fourierdlem39  40836  fourierdlem42  40839  fourierdlem47  40843  fourierdlem68  40864  fourierdlem70  40866  fourierdlem71  40867  fourierdlem73  40869  fourierdlem77  40873  fourierdlem80  40876  fourierdlem83  40879  fourierdlem87  40883  fourierdlem103  40899  fourierdlem104  40900  etransclem23  40947  etransclem48  40972  rrndistlt  40983  ioorrnopnlem  40997  sge0isum  41117  hoicvr  41238  smflimlem4  41458  smfmullem1  41474  smfmullem2  41475  smfmullem3  41476
  Copyright terms: Public domain W3C validator