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

Theorem abscld 13241
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 13085 . 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 1802   ` cfv 5574   CCcc 9488   RRcr 9489   abscabs 13041
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554  ax-nul 4562  ax-pow 4611  ax-pr 4672  ax-un 6573  ax-cnex 9546  ax-resscn 9547  ax-1cn 9548  ax-icn 9549  ax-addcl 9550  ax-addrcl 9551  ax-mulcl 9552  ax-mulrcl 9553  ax-mulcom 9554  ax-addass 9555  ax-mulass 9556  ax-distr 9557  ax-i2m1 9558  ax-1ne0 9559  ax-1rid 9560  ax-rnegex 9561  ax-rrecex 9562  ax-cnre 9563  ax-pre-lttri 9564  ax-pre-lttrn 9565  ax-pre-ltadd 9566  ax-pre-mulgt0 9567  ax-pre-sup 9568
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 973  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-nel 2639  df-ral 2796  df-rex 2797  df-reu 2798  df-rmo 2799  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3418  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-pss 3474  df-nul 3768  df-if 3923  df-pw 3995  df-sn 4011  df-pr 4013  df-tp 4015  df-op 4017  df-uni 4231  df-iun 4313  df-br 4434  df-opab 4492  df-mpt 4493  df-tr 4527  df-eprel 4777  df-id 4781  df-po 4786  df-so 4787  df-fr 4824  df-we 4826  df-ord 4867  df-on 4868  df-lim 4869  df-suc 4870  df-xp 4991  df-rel 4992  df-cnv 4993  df-co 4994  df-dm 4995  df-rn 4996  df-res 4997  df-ima 4998  df-iota 5537  df-fun 5576  df-fn 5577  df-f 5578  df-f1 5579  df-fo 5580  df-f1o 5581  df-fv 5582  df-riota 6238  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-om 6682  df-2nd 6782  df-recs 7040  df-rdg 7074  df-er 7309  df-en 7515  df-dom 7516  df-sdom 7517  df-sup 7899  df-pnf 9628  df-mnf 9629  df-xr 9630  df-ltxr 9631  df-le 9632  df-sub 9807  df-neg 9808  df-div 10208  df-nn 10538  df-2 10595  df-3 10596  df-n0 10797  df-z 10866  df-uz 11086  df-rp 11225  df-seq 12082  df-exp 12141  df-cj 12906  df-re 12907  df-im 12908  df-sqrt 13042  df-abs 13043
This theorem is referenced by:  lo1bddrp  13322  elo1mpt  13331  elo1mpt2  13332  elo1d  13333  o1bdd2  13338  o1bddrp  13339  rlimuni  13347  climuni  13349  o1eq  13367  rlimcld2  13375  rlimrege0  13376  climabs0  13382  mulcn2  13392  reccn2  13393  cn1lem  13394  cjcn2  13396  o1add  13410  o1mul  13411  o1sub  13412  rlimo1  13413  o1rlimmul  13415  climsqz  13437  climsqz2  13438  rlimsqzlem  13445  o1le  13449  climbdd  13468  caucvgrlem  13469  caucvgrlem2  13471  iseraltlem3  13480  iseralt  13481  fsumabs  13589  o1fsum  13601  iserabs  13603  cvgcmpce  13606  abscvgcvg  13607  divrcnv  13638  explecnv  13650  geomulcvg  13659  cvgrat  13666  mertenslem1  13667  mertenslem2  13668  efcllem  13686  efaddlem  13701  eftlub  13716  ef01bndlem  13791  sin01bnd  13792  cos01bnd  13793  absef  13804  alzdvds  13908  sqnprm  14111  pclem  14234  mul4sqlem  14343  xrsdsreclb  18333  gzrngunitlem  18350  gzrngunit  18351  prmirredlem  18390  prmirredlemOLD  18393  nm2dif  21010  blcvx  21169  recld2  21185  addcnlem  21234  cnheiborlem  21320  cnheibor  21321  cnllycmp  21322  cphsqrtcl2  21499  ipcau2  21543  tchcphlem1  21544  ipcnlem2  21550  cncmet  21627  trirn  21693  rrxdstprj1  21702  pjthlem1  21718  volsup2  21880  mbfi1fseqlem6  21993  iblabslem  22100  iblabs  22101  iblabsr  22102  iblmulc2  22103  itgabs  22107  bddmulibl  22111  itgcn  22115  dveflem  22246  dvlip  22260  dvlipcn  22261  c1liplem1  22263  dveq0  22267  dv11cn  22268  lhop1lem  22280  dvfsumabs  22290  dvfsumrlim  22298  dvfsumrlim2  22299  ftc1a  22304  ftc1lem4  22306  plyeq0lem  22473  aalioulem2  22594  aalioulem3  22595  aalioulem4  22596  aalioulem5  22597  aalioulem6  22598  aaliou  22599  geolim3  22600  aaliou2b  22602  aaliou3lem9  22611  ulmbdd  22658  ulmcn  22659  ulmdvlem1  22660  mtest  22664  mtestbdd  22665  iblulm  22667  itgulm  22668  radcnvlem1  22673  radcnvlem2  22674  radcnvlt1  22678  radcnvle  22680  dvradcnv  22681  pserulm  22682  psercnlem2  22684  psercnlem1  22685  psercn  22686  pserdvlem1  22687  pserdvlem2  22688  pserdv  22689  abelthlem2  22692  abelthlem3  22693  abelthlem5  22695  abelthlem7  22698  abelthlem8  22699  sineq0  22779  tanregt0  22791  efif1olem3  22796  efif1olem4  22797  eff1olem  22800  cosargd  22858  cosarg0d  22859  argrege0  22861  abslogle  22868  logcnlem3  22890  logcnlem4  22891  efopnlem1  22902  logtayl  22906  abscxp2  22939  cxpcn3lem  22986  abscxpbnd  22992  cosangneg2d  23004  lawcoslem1  23012  lawcos  23013  pythag  23014  isosctrlem3  23019  ssscongptld  23021  chordthmlem3  23030  chordthmlem4  23031  chordthmlem5  23032  heron  23034  bndatandm  23125  efrlim  23164  rlimcxp  23168  o1cxp  23169  cxploglim2  23173  divsqrtsumo1  23178  fsumharmonic  23206  ftalem1  23211  ftalem2  23212  ftalem3  23213  ftalem4  23214  ftalem5  23215  ftalem7  23217  logfacbnd3  23363  logfacrlim  23364  logexprlim  23365  dchrabs  23400  lgsdirprm  23469  lgsdilem2  23471  lgsne0  23473  lgsabs1  23474  mul2sq  23505  2sqlem3  23506  2sqblem  23517  vmadivsumb  23533  rplogsumlem2  23535  dchrisumlem2  23540  dchrisumlem3  23541  dchrisum  23542  dchrmusum2  23544  dchrvmasumlem2  23548  dchrvmasumlem3  23549  dchrvmasumiflem1  23551  dchrvmasumiflem2  23552  dchrisum0flblem1  23558  dchrisum0fno1  23561  dchrisum0lem1b  23565  dchrisum0lem1  23566  dchrisum0lem2a  23567  dchrisum0lem2  23568  dchrisum0lem3  23569  mudivsum  23580  mulogsumlem  23581  mulog2sumlem1  23584  mulog2sumlem2  23585  2vmadivsumlem  23590  log2sumbnd  23594  selberglem2  23596  selbergb  23599  selberg2b  23602  chpdifbndlem1  23603  selberg3lem1  23607  selberg3lem2  23608  selberg4lem1  23610  pntrsumo1  23615  pntrsumbnd  23616  pntrsumbnd2  23617  pntrlog2bndlem1  23627  pntrlog2bndlem2  23628  pntrlog2bndlem3  23629  pntrlog2bndlem4  23630  pntrlog2bndlem5  23631  pntrlog2bndlem6  23633  pntrlog2bnd  23634  pntpbnd1a  23635  pntpbnd2  23637  pntibndlem2  23641  pntlemn  23650  pntlemj  23653  pntlemf  23655  pntlemo  23657  pntlem3  23659  pntleml  23661  smcnlem  25472  nmoub3i  25553  isblo3i  25581  htthlem  25699  bcs2  25964  pjhthlem1  26174  nmfnsetre  26661  nmfnleub2  26710  nmfnge0  26711  nmbdfnlbi  26833  nmcfnexi  26835  nmcfnlbi  26836  lnfnconi  26839  cnlnadjlem2  26852  cnlnadjlem7  26857  nmopcoadji  26885  leopnmid  26922  bhmafibid1  27498  sqsscirc2  27757  lgamgulmlem2  28438  lgamgulmlem3  28439  lgamgulmlem5  28441  lgambdd  28445  lgamucov  28446  lgamcvg2  28463  subfaclim  28498  subfacval3  28499  sinccvglem  28904  fprodabs  29071  iblabsnclem  30046  iblabsnc  30047  iblmulc2nc  30048  itgabsnc  30052  bddiblnc  30053  ftc1cnnclem  30056  ftc1anclem1  30058  ftc1anclem2  30059  ftc1anclem4  30061  ftc1anclem5  30062  ftc1anclem6  30063  ftc1anclem7  30064  ftc1anclem8  30065  ftc1anc  30066  ftc2nc  30067  dvasin  30071  areacirclem1  30075  areacirclem2  30076  areacirclem4  30078  areacirclem5  30079  areacirc  30080  geomcau  30220  cntotbnd  30260  rrndstprj1  30294  rrndstprj2  30295  ismrer1  30302  rencldnfilem  30722  irrapxlem2  30727  irrapxlem4  30729  irrapxlem5  30730  pellexlem2  30734  pellexlem6  30738  pell14qrgt0  30763  congabseq  30880  acongeq  30889  modabsdifz  30895  jm2.26lem3  30911  dvgrat  31162  cvgdvgrat  31163  radcnvrat  31164  dvconstbi  31208  dstregt0  31408  absnpncan2d  31447  absnpncan3d  31452  mullimc  31526  mullimcf  31533  limcrecl  31539  lptre2pt  31550  limcleqr  31554  addlimc  31558  0ellimcdiv  31559  limclner  31561  cncficcgt0  31594  dvdivbd  31620  dvbdfbdioolem1  31625  dvbdfbdioolem2  31626  dvbdfbdioo  31627  ioodvbdlimc1lem1  31628  ioodvbdlimc1lem2  31629  ioodvbdlimc2lem  31631  stoweid  31730  fourierdlem30  31804  fourierdlem39  31813  fourierdlem42  31816  fourierdlem47  31821  fourierdlem68  31842  fourierdlem70  31844  fourierdlem71  31845  fourierdlem73  31847  fourierdlem77  31851  fourierdlem80  31854  fourierdlem83  31857  fourierdlem87  31861  fourierdlem103  31877  fourierdlem104  31878  extoimad  37586  imo72b2lem0  37587  imo72b2  37598
  Copyright terms: Public domain W3C validator