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

Theorem abscld 13349
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 13193 . 2  |-  ( A  e.  CC  ->  ( abs `  A )  e.  RR )
31, 2syl 16 1  |-  ( ph  ->  ( abs `  A
)  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1823   ` cfv 5570   CCcc 9479   RRcr 9480   abscabs 13149
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565  ax-cnex 9537  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-mulcom 9545  ax-addass 9546  ax-mulass 9547  ax-distr 9548  ax-i2m1 9549  ax-1ne0 9550  ax-1rid 9551  ax-rnegex 9552  ax-rrecex 9553  ax-cnre 9554  ax-pre-lttri 9555  ax-pre-lttrn 9556  ax-pre-ltadd 9557  ax-pre-mulgt0 9558  ax-pre-sup 9559
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-nel 2652  df-ral 2809  df-rex 2810  df-reu 2811  df-rmo 2812  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-tp 4021  df-op 4023  df-uni 4236  df-iun 4317  df-br 4440  df-opab 4498  df-mpt 4499  df-tr 4533  df-eprel 4780  df-id 4784  df-po 4789  df-so 4790  df-fr 4827  df-we 4829  df-ord 4870  df-on 4871  df-lim 4872  df-suc 4873  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-riota 6232  df-ov 6273  df-oprab 6274  df-mpt2 6275  df-om 6674  df-2nd 6774  df-recs 7034  df-rdg 7068  df-er 7303  df-en 7510  df-dom 7511  df-sdom 7512  df-sup 7893  df-pnf 9619  df-mnf 9620  df-xr 9621  df-ltxr 9622  df-le 9623  df-sub 9798  df-neg 9799  df-div 10203  df-nn 10532  df-2 10590  df-3 10591  df-n0 10792  df-z 10861  df-uz 11083  df-rp 11222  df-seq 12090  df-exp 12149  df-cj 13014  df-re 13015  df-im 13016  df-sqrt 13150  df-abs 13151
This theorem is referenced by:  lo1bddrp  13430  elo1mpt  13439  elo1mpt2  13440  elo1d  13441  o1bdd2  13446  o1bddrp  13447  rlimuni  13455  climuni  13457  o1eq  13475  rlimcld2  13483  rlimrege0  13484  climabs0  13490  mulcn2  13500  reccn2  13501  cn1lem  13502  cjcn2  13504  o1add  13518  o1mul  13519  o1sub  13520  rlimo1  13521  o1rlimmul  13523  climsqz  13545  climsqz2  13546  rlimsqzlem  13553  o1le  13557  climbdd  13576  caucvgrlem  13577  caucvgrlem2  13579  iseraltlem3  13588  iseralt  13589  fsumabs  13697  o1fsum  13709  iserabs  13711  cvgcmpce  13714  abscvgcvg  13715  divrcnv  13746  explecnv  13758  geomulcvg  13767  cvgrat  13774  mertenslem1  13775  mertenslem2  13776  fprodabs  13860  efcllem  13895  efaddlem  13910  eftlub  13926  ef01bndlem  14001  sin01bnd  14002  cos01bnd  14003  absef  14014  alzdvds  14120  sqnprm  14323  pclem  14446  mul4sqlem  14555  xrsdsreclb  18660  gzrngunitlem  18677  gzrngunit  18678  prmirredlem  18705  nm2dif  21310  blcvx  21469  recld2  21485  addcnlem  21534  cnheiborlem  21620  cnheibor  21621  cnllycmp  21622  cphsqrtcl2  21799  ipcau2  21843  tchcphlem1  21844  ipcnlem2  21850  cncmet  21927  trirn  21993  rrxdstprj1  22002  pjthlem1  22018  volsup2  22180  mbfi1fseqlem6  22293  iblabslem  22400  iblabs  22401  iblabsr  22402  iblmulc2  22403  itgabs  22407  bddmulibl  22411  itgcn  22415  dveflem  22546  dvlip  22560  dvlipcn  22561  c1liplem1  22563  dveq0  22567  dv11cn  22568  lhop1lem  22580  dvfsumabs  22590  dvfsumrlim  22598  dvfsumrlim2  22599  ftc1a  22604  ftc1lem4  22606  plyeq0lem  22773  aalioulem2  22895  aalioulem3  22896  aalioulem4  22897  aalioulem5  22898  aalioulem6  22899  aaliou  22900  geolim3  22901  aaliou2b  22903  aaliou3lem9  22912  ulmbdd  22959  ulmcn  22960  ulmdvlem1  22961  mtest  22965  mtestbdd  22966  iblulm  22968  itgulm  22969  radcnvlem1  22974  radcnvlem2  22975  radcnvlt1  22979  radcnvle  22981  dvradcnv  22982  pserulm  22983  psercnlem2  22985  psercnlem1  22986  psercn  22987  pserdvlem1  22988  pserdvlem2  22989  pserdv  22990  abelthlem2  22993  abelthlem3  22994  abelthlem5  22996  abelthlem7  22999  abelthlem8  23000  sineq0  23080  tanregt0  23092  efif1olem3  23097  efif1olem4  23098  eff1olem  23101  cosargd  23161  cosarg0d  23162  argrege0  23164  abslogle  23171  logcnlem3  23193  logcnlem4  23194  efopnlem1  23205  logtayl  23209  abscxp2  23242  cxpcn3lem  23289  abscxpbnd  23295  cosangneg2d  23338  lawcoslem1  23346  lawcos  23347  pythag  23348  isosctrlem3  23351  ssscongptld  23353  chordthmlem3  23362  chordthmlem4  23363  chordthmlem5  23364  heron  23366  bndatandm  23457  efrlim  23497  rlimcxp  23501  o1cxp  23502  cxploglim2  23506  divsqrtsumo1  23511  fsumharmonic  23539  ftalem1  23544  ftalem2  23545  ftalem3  23546  ftalem4  23547  ftalem5  23548  ftalem7  23550  logfacbnd3  23696  logfacrlim  23697  logexprlim  23698  dchrabs  23733  lgsdirprm  23802  lgsdilem2  23804  lgsne0  23806  lgsabs1  23807  mul2sq  23838  2sqlem3  23839  2sqblem  23850  vmadivsumb  23866  rplogsumlem2  23868  dchrisumlem2  23873  dchrisumlem3  23874  dchrisum  23875  dchrmusum2  23877  dchrvmasumlem2  23881  dchrvmasumlem3  23882  dchrvmasumiflem1  23884  dchrvmasumiflem2  23885  dchrisum0flblem1  23891  dchrisum0fno1  23894  dchrisum0lem1b  23898  dchrisum0lem1  23899  dchrisum0lem2a  23900  dchrisum0lem2  23901  dchrisum0lem3  23902  mudivsum  23913  mulogsumlem  23914  mulog2sumlem1  23917  mulog2sumlem2  23918  2vmadivsumlem  23923  log2sumbnd  23927  selberglem2  23929  selbergb  23932  selberg2b  23935  chpdifbndlem1  23936  selberg3lem1  23940  selberg3lem2  23941  selberg4lem1  23943  pntrsumo1  23948  pntrsumbnd  23949  pntrsumbnd2  23950  pntrlog2bndlem1  23960  pntrlog2bndlem2  23961  pntrlog2bndlem3  23962  pntrlog2bndlem4  23963  pntrlog2bndlem5  23964  pntrlog2bndlem6  23966  pntrlog2bnd  23967  pntpbnd1a  23968  pntpbnd2  23970  pntibndlem2  23974  pntlemn  23983  pntlemj  23986  pntlemf  23988  pntlemo  23990  pntlem3  23992  pntleml  23994  smcnlem  25805  nmoub3i  25886  isblo3i  25914  htthlem  26032  bcs2  26297  pjhthlem1  26507  nmfnsetre  26994  nmfnleub2  27043  nmfnge0  27044  nmbdfnlbi  27166  nmcfnexi  27168  nmcfnlbi  27169  lnfnconi  27172  cnlnadjlem2  27185  cnlnadjlem7  27190  nmopcoadji  27218  leopnmid  27255  bhmafibid1  27866  sqsscirc2  28126  lgamgulmlem2  28836  lgamgulmlem3  28837  lgamgulmlem5  28839  lgambdd  28843  lgamucov  28844  lgamcvg2  28861  subfaclim  28896  subfacval3  28897  sinccvglem  29302  iblabsnclem  30318  iblabsnc  30319  iblmulc2nc  30320  itgabsnc  30324  bddiblnc  30325  ftc1cnnclem  30328  ftc1anclem1  30330  ftc1anclem2  30331  ftc1anclem4  30333  ftc1anclem5  30334  ftc1anclem6  30335  ftc1anclem7  30336  ftc1anclem8  30337  ftc1anc  30338  ftc2nc  30339  dvasin  30343  areacirclem1  30347  areacirclem2  30348  areacirclem4  30350  areacirclem5  30351  areacirc  30352  geomcau  30492  cntotbnd  30532  rrndstprj1  30566  rrndstprj2  30567  ismrer1  30574  rencldnfilem  30993  irrapxlem2  30998  irrapxlem4  31000  irrapxlem5  31001  pellexlem2  31005  pellexlem6  31009  pell14qrgt0  31034  congabseq  31151  acongeq  31160  modabsdifz  31166  jm2.26lem3  31182  dvgrat  31434  cvgdvgrat  31435  radcnvrat  31436  dvconstbi  31480  binomcxplemnotnn0  31502  dstregt0  31703  absnpncan2d  31741  absnpncan3d  31746  fprodabs2  31841  mullimc  31861  mullimcf  31868  limcrecl  31874  lptre2pt  31885  limcleqr  31889  addlimc  31893  0ellimcdiv  31894  limclner  31896  cncficcgt0  31930  dvdivbd  31959  dvbdfbdioolem1  31964  dvbdfbdioolem2  31965  dvbdfbdioo  31966  ioodvbdlimc1lem1  31967  ioodvbdlimc1lem2  31968  ioodvbdlimc2lem  31970  stoweid  32084  fourierdlem30  32158  fourierdlem39  32167  fourierdlem42  32170  fourierdlem47  32175  fourierdlem68  32196  fourierdlem70  32198  fourierdlem71  32199  fourierdlem73  32201  fourierdlem77  32205  fourierdlem80  32208  fourierdlem83  32211  fourierdlem87  32215  fourierdlem103  32231  fourierdlem104  32232  etransclem23  32279  etransclem48  32304  extoimad  38433  imo72b2lem0  38434  imo72b2  38445
  Copyright terms: Public domain W3C validator