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

Theorem abscld 13483
Description: Real closure of absolute value. (Contributed by Mario Carneiro, 29-May-2016.)
Hypothesis
Ref Expression
abscld.1  |-  ( ph  ->  A  e.  CC )
Assertion
Ref Expression
abscld  |-  ( ph  ->  ( abs `  A
)  e.  RR )

Proof of Theorem abscld
StepHypRef Expression
1 abscld.1 . 2  |-  ( ph  ->  A  e.  CC )
2 abscl 13327 . 2  |-  ( A  e.  CC  ->  ( abs `  A )  e.  RR )
31, 2syl 17 1  |-  ( ph  ->  ( abs `  A
)  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1868   ` cfv 5597   CCcc 9537   RRcr 9538   abscabs 13283
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593  ax-cnex 9595  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-mulcom 9603  ax-addass 9604  ax-mulass 9605  ax-distr 9606  ax-i2m1 9607  ax-1ne0 9608  ax-1rid 9609  ax-rnegex 9610  ax-rrecex 9611  ax-cnre 9612  ax-pre-lttri 9613  ax-pre-lttrn 9614  ax-pre-ltadd 9615  ax-pre-mulgt0 9616  ax-pre-sup 9617
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-nel 2621  df-ral 2780  df-rex 2781  df-reu 2782  df-rmo 2783  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4760  df-id 4764  df-po 4770  df-so 4771  df-fr 4808  df-we 4810  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-pred 5395  df-ord 5441  df-on 5442  df-lim 5443  df-suc 5444  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-riota 6263  df-ov 6304  df-oprab 6305  df-mpt2 6306  df-om 6703  df-2nd 6804  df-wrecs 7032  df-recs 7094  df-rdg 7132  df-er 7367  df-en 7574  df-dom 7575  df-sdom 7576  df-sup 7958  df-pnf 9677  df-mnf 9678  df-xr 9679  df-ltxr 9680  df-le 9681  df-sub 9862  df-neg 9863  df-div 10270  df-nn 10610  df-2 10668  df-3 10669  df-n0 10870  df-z 10938  df-uz 11160  df-rp 11303  df-seq 12213  df-exp 12272  df-cj 13148  df-re 13149  df-im 13150  df-sqrt 13284  df-abs 13285
This theorem is referenced by:  lo1bddrp  13574  elo1mpt  13583  elo1mpt2  13584  elo1d  13585  o1bdd2  13590  o1bddrp  13591  rlimuni  13599  climuni  13601  o1eq  13619  rlimcld2  13627  rlimrege0  13628  climabs0  13634  mulcn2  13644  reccn2  13645  cn1lem  13646  cjcn2  13648  o1add  13662  o1mul  13663  o1sub  13664  rlimo1  13665  o1rlimmul  13667  climsqz  13689  climsqz2  13690  rlimsqzlem  13697  o1le  13701  climbdd  13720  caucvgrlem  13721  caucvgrlemOLD  13722  caucvgrlem2  13725  iseraltlem3  13735  iseralt  13736  fsumabs  13846  o1fsum  13858  iserabs  13860  cvgcmpce  13863  abscvgcvg  13864  divrcnv  13895  explecnv  13908  geomulcvg  13917  cvgrat  13924  mertenslem1  13925  mertenslem2  13926  fprodabs  14013  efcllem  14117  efaddlem  14132  eftlub  14148  ef01bndlem  14223  sin01bnd  14224  cos01bnd  14225  absef  14236  alzdvds  14340  sqnprm  14631  pclem  14773  mul4sqlem  14882  xrsdsreclb  19000  gzrngunitlem  19017  gzrngunit  19018  prmirredlem  19048  nm2dif  21622  blcvx  21800  recld2  21816  addcnlem  21880  cnheiborlem  21966  cnheibor  21967  cnllycmp  21968  cphsqrtcl2  22148  ipcau2  22192  tchcphlem1  22193  ipcnlem2  22199  cncmet  22274  trirn  22338  rrxdstprj1  22347  pjthlem1  22375  volsup2  22547  mbfi1fseqlem6  22662  iblabslem  22769  iblabs  22770  iblabsr  22771  iblmulc2  22772  itgabs  22776  bddmulibl  22780  itgcn  22784  dveflem  22915  dvlip  22929  dvlipcn  22930  c1liplem1  22932  dveq0  22936  dv11cn  22937  lhop1lem  22949  dvfsumabs  22959  dvfsumrlim  22967  dvfsumrlim2  22968  ftc1a  22973  ftc1lem4  22975  plyeq0lem  23148  aalioulem2  23273  aalioulem3  23274  aalioulem4  23275  aalioulem5  23276  aalioulem6  23277  aaliou  23278  geolim3  23279  aaliou2b  23281  aaliou3lem9  23290  ulmbdd  23337  ulmcn  23338  ulmdvlem1  23339  mtest  23343  mtestbdd  23344  iblulm  23346  itgulm  23347  radcnvlem1  23352  radcnvlem2  23353  radcnvlt1  23357  radcnvle  23359  dvradcnv  23360  pserulm  23361  psercnlem2  23363  psercnlem1  23364  psercn  23365  pserdvlem1  23366  pserdvlem2  23367  pserdv  23368  abelthlem2  23371  abelthlem3  23372  abelthlem5  23374  abelthlem7  23377  abelthlem8  23378  sineq0  23460  tanregt0  23472  efif1olem3  23477  efif1olem4  23478  eff1olem  23481  cosargd  23541  cosarg0d  23542  argrege0  23544  abslogle  23551  logcnlem3  23573  logcnlem4  23574  efopnlem1  23585  logtayl  23589  abscxp2  23622  cxpcn3lem  23671  abscxpbnd  23677  cosangneg2d  23720  lawcoslem1  23728  lawcos  23729  pythag  23730  isosctrlem3  23733  ssscongptld  23735  chordthmlem3  23744  chordthmlem4  23745  chordthmlem5  23746  heron  23748  bndatandm  23839  efrlim  23879  rlimcxp  23883  o1cxp  23884  cxploglim2  23888  divsqrtsumo1  23893  fsumharmonic  23921  lgamgulmlem2  23939  lgamgulmlem3  23940  lgamgulmlem5  23942  lgambdd  23946  lgamucov  23947  lgamcvg2  23964  ftalem1  23981  ftalem2  23982  ftalem3  23983  ftalem4  23984  ftalem5  23985  ftalem4OLD  23986  ftalem5OLD  23987  ftalem7  23989  logfacbnd3  24135  logfacrlim  24136  logexprlim  24137  dchrabs  24172  lgsdirprm  24241  lgsdilem2  24243  lgsne0  24245  lgsabs1  24246  mul2sq  24277  2sqlem3  24278  2sqblem  24289  vmadivsumb  24305  rplogsumlem2  24307  dchrisumlem2  24312  dchrisumlem3  24313  dchrisum  24314  dchrmusum2  24316  dchrvmasumlem2  24320  dchrvmasumlem3  24321  dchrvmasumiflem1  24323  dchrvmasumiflem2  24324  dchrisum0flblem1  24330  dchrisum0fno1  24333  dchrisum0lem1b  24337  dchrisum0lem1  24338  dchrisum0lem2a  24339  dchrisum0lem2  24340  dchrisum0lem3  24341  mudivsum  24352  mulogsumlem  24353  mulog2sumlem1  24356  mulog2sumlem2  24357  2vmadivsumlem  24362  log2sumbnd  24366  selberglem2  24368  selbergb  24371  selberg2b  24374  chpdifbndlem1  24375  selberg3lem1  24379  selberg3lem2  24380  selberg4lem1  24382  pntrsumo1  24387  pntrsumbnd  24388  pntrsumbnd2  24389  pntrlog2bndlem1  24399  pntrlog2bndlem2  24400  pntrlog2bndlem3  24401  pntrlog2bndlem4  24402  pntrlog2bndlem5  24403  pntrlog2bndlem6  24405  pntrlog2bnd  24406  pntpbnd1a  24407  pntpbnd2  24409  pntibndlem2  24413  pntlemn  24422  pntlemj  24425  pntlemf  24427  pntlemo  24429  pntlem3  24431  pntleml  24433  smcnlem  26316  nmoub3i  26397  isblo3i  26425  htthlem  26553  bcs2  26818  pjhthlem1  27027  nmfnsetre  27513  nmfnleub2  27562  nmfnge0  27563  nmbdfnlbi  27685  nmcfnexi  27687  nmcfnlbi  27688  lnfnconi  27691  cnlnadjlem2  27704  cnlnadjlem7  27709  nmopcoadji  27737  leopnmid  27774  bhmafibid1  28397  sqsscirc2  28708  subfaclim  29904  subfacval3  29905  sinccvglem  30309  poimirlem29  31880  poimir  31884  iblabsnclem  31916  iblabsnc  31917  iblmulc2nc  31918  itgabsnc  31922  bddiblnc  31923  ftc1cnnclem  31926  ftc1anclem1  31928  ftc1anclem2  31929  ftc1anclem4  31931  ftc1anclem5  31932  ftc1anclem6  31933  ftc1anclem7  31934  ftc1anclem8  31935  ftc1anc  31936  ftc2nc  31937  dvasin  31939  areacirclem1  31943  areacirclem2  31944  areacirclem4  31946  areacirclem5  31947  areacirc  31948  geomcau  31999  cntotbnd  32039  rrndstprj1  32073  rrndstprj2  32074  ismrer1  32081  rencldnfilem  35579  irrapxlem2  35584  irrapxlem4  35586  irrapxlem5  35587  pellexlem2  35591  pellexlem6  35595  pell14qrgt0  35622  congabseq  35741  acongeq  35750  modabsdifz  35756  jm2.26lem3  35773  extoimad  36462  imo72b2lem0  36463  imo72b2  36474  dvgrat  36516  cvgdvgrat  36517  radcnvrat  36518  dvconstbi  36538  binomcxplemnotnn0  36560  dstregt0  37330  absnpncan2d  37359  absnpncan3d  37364  fprodabs2  37492  mullimc  37513  mullimcf  37520  limcrecl  37526  lptre2pt  37537  limcleqr  37542  addlimc  37546  0ellimcdiv  37547  limclner  37549  cncficcgt0  37583  dvdivbd  37612  dvbdfbdioolem1  37617  dvbdfbdioolem2  37618  dvbdfbdioo  37619  ioodvbdlimc1lem1  37620  ioodvbdlimc1lem2  37621  ioodvbdlimc1lem1OLD  37622  ioodvbdlimc1lem2OLD  37623  ioodvbdlimc2lem  37625  ioodvbdlimc2lemOLD  37626  stoweid  37742  fourierdlem30  37816  fourierdlem39  37826  fourierdlem42  37829  fourierdlem42OLD  37830  fourierdlem47  37834  fourierdlem68  37855  fourierdlem70  37857  fourierdlem71  37858  fourierdlem73  37860  fourierdlem77  37864  fourierdlem80  37867  fourierdlem83  37870  fourierdlem87  37874  fourierdlem103  37890  fourierdlem104  37891  etransclem23  37939  etransclem48OLD  37964  etransclem48  37965  sge0isum  38054  hoicvr  38142
  Copyright terms: Public domain W3C validator