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

Theorem abscld 12165
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 12010 . 2  |-  ( A  e.  CC  ->  ( abs `  A )  e.  RR )
31, 2syl 16 1  |-  ( ph  ->  ( abs `  A
)  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1717   ` cfv 5394   CCcc 8921   RRcr 8922   abscabs 11966
This theorem is referenced by:  lo1bddrp  12246  elo1mpt  12255  elo1mpt2  12256  elo1d  12257  o1bdd2  12262  o1bddrp  12263  rlimuni  12271  climuni  12273  o1eq  12291  rlimcld2  12299  rlimrege0  12300  climabs0  12306  mulcn2  12316  reccn2  12317  cn1lem  12318  cjcn2  12320  o1add  12334  o1mul  12335  o1sub  12336  rlimo1  12337  o1rlimmul  12339  climsqz  12361  climsqz2  12362  rlimsqzlem  12369  o1le  12373  climbdd  12392  caucvgrlem  12393  caucvgrlem2  12395  iseraltlem3  12404  iseralt  12405  fsumabs  12507  o1fsum  12519  iserabs  12521  cvgcmpce  12524  abscvgcvg  12525  divrcnv  12559  explecnv  12571  geomulcvg  12580  cvgrat  12587  mertenslem1  12588  mertenslem2  12589  efcllem  12607  efaddlem  12622  eftlub  12637  ef01bndlem  12712  sin01bnd  12713  cos01bnd  12714  absef  12725  alzdvds  12826  sqnprm  13025  pclem  13139  mul4sqlem  13248  xrsdsreclb  16668  gzrngunitlem  16686  gzrngunit  16687  prmirredlem  16696  nm2dif  18542  blcvx  18700  recld2  18716  addcnlem  18765  cnheiborlem  18850  cnheibor  18851  cnllycmp  18852  cphsqrcl2  19020  ipcau2  19062  tchcphlem1  19063  ipcnlem2  19069  cncmet  19144  pjthlem1  19205  volsup2  19364  mbfi1fseqlem6  19479  iblabslem  19586  iblabs  19587  iblabsr  19588  iblmulc2  19589  itgabs  19593  bddmulibl  19597  itgcn  19601  dveflem  19730  dvlip  19744  dvlipcn  19745  c1liplem1  19747  dveq0  19751  dv11cn  19752  lhop1lem  19764  dvfsumabs  19774  dvfsumrlim  19782  dvfsumrlim2  19783  ftc1a  19788  ftc1lem4  19790  plyeq0lem  19996  aalioulem2  20117  aalioulem3  20118  aalioulem4  20119  aalioulem5  20120  aalioulem6  20121  aaliou  20122  geolim3  20123  aaliou2b  20125  aaliou3lem9  20134  ulmbdd  20181  ulmcn  20182  ulmdvlem1  20183  mtest  20187  mtestbdd  20188  iblulm  20190  itgulm  20191  radcnvlem1  20196  radcnvlem2  20197  radcnvlt1  20201  radcnvle  20203  dvradcnv  20204  pserulm  20205  psercnlem2  20207  psercnlem1  20208  psercn  20209  pserdvlem1  20210  pserdvlem2  20211  pserdv  20212  abelthlem2  20215  abelthlem3  20216  abelthlem5  20218  abelthlem7  20221  abelthlem8  20222  sineq0  20296  tanregt0  20308  efif1olem3  20313  efif1olem4  20314  eff1olem  20317  cosargd  20370  cosarg0d  20371  argrege0  20373  abslogle  20380  logcnlem3  20402  logcnlem4  20403  efopnlem1  20414  logtayl  20418  abscxp2  20451  cxpcn3lem  20498  abscxpbnd  20504  cosangneg2d  20516  lawcoslem1  20524  lawcos  20525  pythag  20526  isosctrlem3  20531  ssscongptld  20533  chordthmlem3  20542  chordthmlem4  20543  chordthmlem5  20544  bndatandm  20636  efrlim  20675  rlimcxp  20679  o1cxp  20680  cxploglim2  20684  divsqrsumo1  20689  fsumharmonic  20717  ftalem1  20722  ftalem2  20723  ftalem3  20724  ftalem4  20725  ftalem5  20726  ftalem7  20728  logfacbnd3  20874  logfacrlim  20875  logexprlim  20876  dchrabs  20911  lgsdirprm  20980  lgsdilem2  20982  lgsne0  20984  lgsabs1  20985  mul2sq  21016  2sqlem3  21017  2sqblem  21028  vmadivsumb  21044  rplogsumlem2  21046  dchrisumlem2  21051  dchrisumlem3  21052  dchrisum  21053  dchrmusum2  21055  dchrvmasumlem2  21059  dchrvmasumlem3  21060  dchrvmasumiflem1  21062  dchrvmasumiflem2  21063  dchrisum0flblem1  21069  dchrisum0fno1  21072  dchrisum0lem1b  21076  dchrisum0lem1  21077  dchrisum0lem2a  21078  dchrisum0lem2  21079  dchrisum0lem3  21080  mudivsum  21091  mulogsumlem  21092  mulog2sumlem1  21095  mulog2sumlem2  21096  2vmadivsumlem  21101  log2sumbnd  21105  selberglem2  21107  selbergb  21110  selberg2b  21113  chpdifbndlem1  21114  selberg3lem1  21118  selberg3lem2  21119  selberg4lem1  21121  pntrsumo1  21126  pntrsumbnd  21127  pntrsumbnd2  21128  pntrlog2bndlem1  21138  pntrlog2bndlem2  21139  pntrlog2bndlem3  21140  pntrlog2bndlem4  21141  pntrlog2bndlem5  21142  pntrlog2bndlem6  21144  pntrlog2bnd  21145  pntpbnd1a  21146  pntpbnd2  21148  pntibndlem2  21152  pntlemn  21161  pntlemj  21164  pntlemf  21166  pntlemo  21168  pntlem3  21170  pntleml  21172  smcnlem  22041  nmoub3i  22122  isblo3i  22150  htthlem  22268  bcs2  22532  pjhthlem1  22741  nmfnsetre  23228  nmfnleub2  23277  nmfnge0  23278  nmbdfnlbi  23400  nmcfnexi  23402  nmcfnlbi  23403  lnfnconi  23406  cnlnadjlem2  23419  cnlnadjlem7  23424  nmopcoadji  23452  leopnmid  23489  sqsscirc2  24111  lgamgulmlem2  24593  lgamgulmlem3  24594  lgamgulmlem5  24596  lgambdd  24600  lgamucov  24601  lgamcvg2  24618  subfaclim  24653  subfacval3  24654  sinccvglem  24888  fprodabs  25076  iblabsnclem  25968  iblabsnc  25969  iblmulc2nc  25970  itgabsnc  25974  bddiblnc  25975  ftc1cnnclem  25978  dvreasin  25980  dvreacos  25981  areacirclem2  25982  areacirclem3  25983  areacirclem4  25984  areacirclem5  25986  areacirclem6  25987  areacirc  25988  trirn  26148  geomcau  26156  cntotbnd  26196  rrndstprj1  26230  rrndstprj2  26231  ismrer1  26238  rencldnfilem  26572  irrapxlem2  26577  irrapxlem4  26579  irrapxlem5  26580  pellexlem2  26584  pellexlem6  26588  pell14qrgt0  26613  congabseq  26730  acongeq  26739  modabsdifz  26747  jm2.26lem3  26763  dvconstbi  27220  stoweid  27480
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-sep 4271  ax-nul 4279  ax-pow 4318  ax-pr 4344  ax-un 4641  ax-cnex 8979  ax-resscn 8980  ax-1cn 8981  ax-icn 8982  ax-addcl 8983  ax-addrcl 8984  ax-mulcl 8985  ax-mulrcl 8986  ax-mulcom 8987  ax-addass 8988  ax-mulass 8989  ax-distr 8990  ax-i2m1 8991  ax-1ne0 8992  ax-1rid 8993  ax-rnegex 8994  ax-rrecex 8995  ax-cnre 8996  ax-pre-lttri 8997  ax-pre-lttrn 8998  ax-pre-ltadd 8999  ax-pre-mulgt0 9000  ax-pre-sup 9001
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2242  df-mo 2243  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-nel 2553  df-ral 2654  df-rex 2655  df-reu 2656  df-rmo 2657  df-rab 2658  df-v 2901  df-sbc 3105  df-csb 3195  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-pss 3279  df-nul 3572  df-if 3683  df-pw 3744  df-sn 3763  df-pr 3764  df-tp 3765  df-op 3766  df-uni 3958  df-iun 4037  df-br 4154  df-opab 4208  df-mpt 4209  df-tr 4244  df-eprel 4435  df-id 4439  df-po 4444  df-so 4445  df-fr 4482  df-we 4484  df-ord 4525  df-on 4526  df-lim 4527  df-suc 4528  df-om 4786  df-xp 4824  df-rel 4825  df-cnv 4826  df-co 4827  df-dm 4828  df-rn 4829  df-res 4830  df-ima 4831  df-iota 5358  df-fun 5396  df-fn 5397  df-f 5398  df-f1 5399  df-fo 5400  df-f1o 5401  df-fv 5402  df-ov 6023  df-oprab 6024  df-mpt2 6025  df-2nd 6289  df-riota 6485  df-recs 6569  df-rdg 6604  df-er 6841  df-en 7046  df-dom 7047  df-sdom 7048  df-sup 7381  df-pnf 9055  df-mnf 9056  df-xr 9057  df-ltxr 9058  df-le 9059  df-sub 9225  df-neg 9226  df-div 9610  df-nn 9933  df-2 9990  df-3 9991  df-n0 10154  df-z 10215  df-uz 10421  df-rp 10545  df-seq 11251  df-exp 11310  df-cj 11831  df-re 11832  df-im 11833  df-sqr 11967  df-abs 11968
  Copyright terms: Public domain W3C validator