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

Theorem abscld 13024
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 12869 . 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 1758   ` cfv 5516   CCcc 9381   RRcr 9382   abscabs 12825
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4511  ax-nul 4519  ax-pow 4568  ax-pr 4629  ax-un 6472  ax-cnex 9439  ax-resscn 9440  ax-1cn 9441  ax-icn 9442  ax-addcl 9443  ax-addrcl 9444  ax-mulcl 9445  ax-mulrcl 9446  ax-mulcom 9447  ax-addass 9448  ax-mulass 9449  ax-distr 9450  ax-i2m1 9451  ax-1ne0 9452  ax-1rid 9453  ax-rnegex 9454  ax-rrecex 9455  ax-cnre 9456  ax-pre-lttri 9457  ax-pre-lttrn 9458  ax-pre-ltadd 9459  ax-pre-mulgt0 9460  ax-pre-sup 9461
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-nel 2647  df-ral 2800  df-rex 2801  df-reu 2802  df-rmo 2803  df-rab 2804  df-v 3070  df-sbc 3285  df-csb 3387  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-pss 3442  df-nul 3736  df-if 3890  df-pw 3960  df-sn 3976  df-pr 3978  df-tp 3980  df-op 3982  df-uni 4190  df-iun 4271  df-br 4391  df-opab 4449  df-mpt 4450  df-tr 4484  df-eprel 4730  df-id 4734  df-po 4739  df-so 4740  df-fr 4777  df-we 4779  df-ord 4820  df-on 4821  df-lim 4822  df-suc 4823  df-xp 4944  df-rel 4945  df-cnv 4946  df-co 4947  df-dm 4948  df-rn 4949  df-res 4950  df-ima 4951  df-iota 5479  df-fun 5518  df-fn 5519  df-f 5520  df-f1 5521  df-fo 5522  df-f1o 5523  df-fv 5524  df-riota 6151  df-ov 6193  df-oprab 6194  df-mpt2 6195  df-om 6577  df-2nd 6678  df-recs 6932  df-rdg 6966  df-er 7201  df-en 7411  df-dom 7412  df-sdom 7413  df-sup 7792  df-pnf 9521  df-mnf 9522  df-xr 9523  df-ltxr 9524  df-le 9525  df-sub 9698  df-neg 9699  df-div 10095  df-nn 10424  df-2 10481  df-3 10482  df-n0 10681  df-z 10748  df-uz 10963  df-rp 11093  df-seq 11908  df-exp 11967  df-cj 12690  df-re 12691  df-im 12692  df-sqr 12826  df-abs 12827
This theorem is referenced by:  lo1bddrp  13105  elo1mpt  13114  elo1mpt2  13115  elo1d  13116  o1bdd2  13121  o1bddrp  13122  rlimuni  13130  climuni  13132  o1eq  13150  rlimcld2  13158  rlimrege0  13159  climabs0  13165  mulcn2  13175  reccn2  13176  cn1lem  13177  cjcn2  13179  o1add  13193  o1mul  13194  o1sub  13195  rlimo1  13196  o1rlimmul  13198  climsqz  13220  climsqz2  13221  rlimsqzlem  13228  o1le  13232  climbdd  13251  caucvgrlem  13252  caucvgrlem2  13254  iseraltlem3  13263  iseralt  13264  fsumabs  13366  o1fsum  13378  iserabs  13380  cvgcmpce  13383  abscvgcvg  13384  divrcnv  13417  explecnv  13429  geomulcvg  13438  cvgrat  13445  mertenslem1  13446  mertenslem2  13447  efcllem  13465  efaddlem  13480  eftlub  13495  ef01bndlem  13570  sin01bnd  13571  cos01bnd  13572  absef  13583  alzdvds  13685  sqnprm  13886  pclem  14007  mul4sqlem  14116  xrsdsreclb  17969  gzrngunitlem  17986  gzrngunit  17987  prmirredlem  18026  prmirredlemOLD  18029  nm2dif  20332  blcvx  20491  recld2  20507  addcnlem  20556  cnheiborlem  20642  cnheibor  20643  cnllycmp  20644  cphsqrcl2  20821  ipcau2  20865  tchcphlem1  20866  ipcnlem2  20872  cncmet  20949  trirn  21015  rrxdstprj1  21024  pjthlem1  21040  volsup2  21201  mbfi1fseqlem6  21314  iblabslem  21421  iblabs  21422  iblabsr  21423  iblmulc2  21424  itgabs  21428  bddmulibl  21432  itgcn  21436  dveflem  21567  dvlip  21581  dvlipcn  21582  c1liplem1  21584  dveq0  21588  dv11cn  21589  lhop1lem  21601  dvfsumabs  21611  dvfsumrlim  21619  dvfsumrlim2  21620  ftc1a  21625  ftc1lem4  21627  plyeq0lem  21794  aalioulem2  21915  aalioulem3  21916  aalioulem4  21917  aalioulem5  21918  aalioulem6  21919  aaliou  21920  geolim3  21921  aaliou2b  21923  aaliou3lem9  21932  ulmbdd  21979  ulmcn  21980  ulmdvlem1  21981  mtest  21985  mtestbdd  21986  iblulm  21988  itgulm  21989  radcnvlem1  21994  radcnvlem2  21995  radcnvlt1  21999  radcnvle  22001  dvradcnv  22002  pserulm  22003  psercnlem2  22005  psercnlem1  22006  psercn  22007  pserdvlem1  22008  pserdvlem2  22009  pserdv  22010  abelthlem2  22013  abelthlem3  22014  abelthlem5  22016  abelthlem7  22019  abelthlem8  22020  sineq0  22099  tanregt0  22111  efif1olem3  22116  efif1olem4  22117  eff1olem  22120  cosargd  22173  cosarg0d  22174  argrege0  22176  abslogle  22183  logcnlem3  22205  logcnlem4  22206  efopnlem1  22217  logtayl  22221  abscxp2  22254  cxpcn3lem  22301  abscxpbnd  22307  cosangneg2d  22319  lawcoslem1  22327  lawcos  22328  pythag  22329  isosctrlem3  22334  ssscongptld  22336  chordthmlem3  22345  chordthmlem4  22346  chordthmlem5  22347  heron  22349  bndatandm  22440  efrlim  22479  rlimcxp  22483  o1cxp  22484  cxploglim2  22488  divsqrsumo1  22493  fsumharmonic  22521  ftalem1  22526  ftalem2  22527  ftalem3  22528  ftalem4  22529  ftalem5  22530  ftalem7  22532  logfacbnd3  22678  logfacrlim  22679  logexprlim  22680  dchrabs  22715  lgsdirprm  22784  lgsdilem2  22786  lgsne0  22788  lgsabs1  22789  mul2sq  22820  2sqlem3  22821  2sqblem  22832  vmadivsumb  22848  rplogsumlem2  22850  dchrisumlem2  22855  dchrisumlem3  22856  dchrisum  22857  dchrmusum2  22859  dchrvmasumlem2  22863  dchrvmasumlem3  22864  dchrvmasumiflem1  22866  dchrvmasumiflem2  22867  dchrisum0flblem1  22873  dchrisum0fno1  22876  dchrisum0lem1b  22880  dchrisum0lem1  22881  dchrisum0lem2a  22882  dchrisum0lem2  22883  dchrisum0lem3  22884  mudivsum  22895  mulogsumlem  22896  mulog2sumlem1  22899  mulog2sumlem2  22900  2vmadivsumlem  22905  log2sumbnd  22909  selberglem2  22911  selbergb  22914  selberg2b  22917  chpdifbndlem1  22918  selberg3lem1  22922  selberg3lem2  22923  selberg4lem1  22925  pntrsumo1  22930  pntrsumbnd  22931  pntrsumbnd2  22932  pntrlog2bndlem1  22942  pntrlog2bndlem2  22943  pntrlog2bndlem3  22944  pntrlog2bndlem4  22945  pntrlog2bndlem5  22946  pntrlog2bndlem6  22948  pntrlog2bnd  22949  pntpbnd1a  22950  pntpbnd2  22952  pntibndlem2  22956  pntlemn  22965  pntlemj  22968  pntlemf  22970  pntlemo  22972  pntlem3  22974  pntleml  22976  smcnlem  24227  nmoub3i  24308  isblo3i  24336  htthlem  24454  bcs2  24719  pjhthlem1  24929  nmfnsetre  25416  nmfnleub2  25465  nmfnge0  25466  nmbdfnlbi  25588  nmcfnexi  25590  nmcfnlbi  25591  lnfnconi  25594  cnlnadjlem2  25607  cnlnadjlem7  25612  nmopcoadji  25640  leopnmid  25677  sqsscirc2  26473  lgamgulmlem2  27150  lgamgulmlem3  27151  lgamgulmlem5  27153  lgambdd  27157  lgamucov  27158  lgamcvg2  27175  subfaclim  27210  subfacval3  27211  sinccvglem  27451  fprodabs  27618  iblabsnclem  28593  iblabsnc  28594  iblmulc2nc  28595  itgabsnc  28599  bddiblnc  28600  ftc1cnnclem  28603  ftc1anclem1  28605  ftc1anclem2  28606  ftc1anclem4  28608  ftc1anclem5  28609  ftc1anclem6  28610  ftc1anclem7  28611  ftc1anclem8  28612  ftc1anc  28613  ftc2nc  28614  dvasin  28618  areacirclem1  28622  areacirclem2  28623  areacirclem4  28625  areacirclem5  28626  areacirc  28627  geomcau  28793  cntotbnd  28833  rrndstprj1  28867  rrndstprj2  28868  ismrer1  28875  rencldnfilem  29297  irrapxlem2  29302  irrapxlem4  29304  irrapxlem5  29305  pellexlem2  29309  pellexlem6  29313  pell14qrgt0  29338  congabseq  29455  acongeq  29464  modabsdifz  29472  jm2.26lem3  29488  dvconstbi  29746  stoweid  29996
  Copyright terms: Public domain W3C validator