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

Theorem abscld 14794
Description: Real closure of absolute value. (Contributed by Mario Carneiro, 29-May-2016.)
Hypothesis
Ref Expression
abscld.1 (𝜑𝐴 ∈ ℂ)
Assertion
Ref Expression
abscld (𝜑 → (abs‘𝐴) ∈ ℝ)

Proof of Theorem abscld
StepHypRef Expression
1 abscld.1 . 2 (𝜑𝐴 ∈ ℂ)
2 abscl 14636 . 2 (𝐴 ∈ ℂ → (abs‘𝐴) ∈ ℝ)
31, 2syl 17 1 (𝜑 → (abs‘𝐴) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2115  cfv 6344  cc 10529  cr 10530  abscabs 14591
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5190  ax-nul 5197  ax-pow 5254  ax-pr 5318  ax-un 7452  ax-cnex 10587  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608  ax-pre-sup 10609
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4826  df-iun 4908  df-br 5054  df-opab 5116  df-mpt 5134  df-tr 5160  df-id 5448  df-eprel 5453  df-po 5462  df-so 5463  df-fr 5502  df-we 5504  df-xp 5549  df-rel 5550  df-cnv 5551  df-co 5552  df-dm 5553  df-rn 5554  df-res 5555  df-ima 5556  df-pred 6136  df-ord 6182  df-on 6183  df-lim 6184  df-suc 6185  df-iota 6303  df-fun 6346  df-fn 6347  df-f 6348  df-f1 6349  df-fo 6350  df-f1o 6351  df-fv 6352  df-riota 7104  df-ov 7149  df-oprab 7150  df-mpo 7151  df-om 7572  df-2nd 7682  df-wrecs 7939  df-recs 8000  df-rdg 8038  df-er 8281  df-en 8502  df-dom 8503  df-sdom 8504  df-sup 8899  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-div 11292  df-nn 11633  df-2 11695  df-3 11696  df-n0 11893  df-z 11977  df-uz 12239  df-rp 12385  df-seq 13372  df-exp 13433  df-cj 14456  df-re 14457  df-im 14458  df-sqrt 14592  df-abs 14593
This theorem is referenced by:  bhmafibid1  14823  lo1bddrp  14880  elo1mpt  14889  elo1mpt2  14890  elo1d  14891  o1bdd2  14896  o1bddrp  14897  rlimuni  14905  climuni  14907  o1eq  14925  rlimcld2  14933  rlimrege0  14934  climabs0  14940  mulcn2  14950  reccn2  14951  cn1lem  14952  cjcn2  14954  o1add  14968  o1mul  14969  o1sub  14970  rlimo1  14971  o1rlimmul  14973  climsqz  14995  climsqz2  14996  rlimsqzlem  15003  o1le  15007  climbdd  15026  caucvgrlem  15027  caucvgrlem2  15029  iseraltlem3  15038  iseralt  15039  fsumabs  15154  o1fsum  15166  iserabs  15168  cvgcmpce  15171  abscvgcvg  15172  divrcnv  15205  explecnv  15218  geomulcvg  15230  cvgrat  15237  mertenslem1  15238  mertenslem2  15239  fprodabs  15326  efcllem  15429  efaddlem  15444  eftlub  15460  ef01bndlem  15535  sin01bnd  15536  cos01bnd  15537  absef  15548  dvdsabseq  15661  alzdvds  15668  sqnprm  16042  pclem  16171  mul4sqlem  16285  xrsdsreclb  20587  gzrngunitlem  20605  gzrngunit  20606  prmirredlem  20635  nm2dif  23229  blcvx  23401  recld2  23417  addcnlem  23467  cnheiborlem  23557  cnheibor  23558  cnllycmp  23559  cphsqrtcl2  23789  ipcau2  23836  tcphcphlem1  23837  ipcnlem2  23846  cncmet  23924  trirn  24002  rrxdstprj1  24011  pjthlem1  24039  volsup2  24207  mbfi1fseqlem6  24322  iblabslem  24429  iblabs  24430  iblabsr  24431  iblmulc2  24432  itgabs  24436  bddmulibl  24440  bddiblnc  24443  itgcn  24446  dveflem  24580  dvlip  24594  dvlipcn  24595  c1liplem1  24597  dveq0  24601  dv11cn  24602  lhop1lem  24614  dvfsumabs  24624  dvfsumrlim  24632  dvfsumrlim2  24633  ftc1a  24638  ftc1lem4  24640  plyeq0lem  24805  aalioulem2  24927  aalioulem3  24928  aalioulem4  24929  aalioulem5  24930  aalioulem6  24931  aaliou  24932  geolim3  24933  aaliou2b  24935  aaliou3lem9  24944  ulmbdd  24991  ulmcn  24992  ulmdvlem1  24993  mtest  24997  mtestbdd  24998  iblulm  25000  itgulm  25001  radcnvlem1  25006  radcnvlem2  25007  radcnvlt1  25011  radcnvle  25013  dvradcnv  25014  pserulm  25015  psercnlem2  25017  psercnlem1  25018  psercn  25019  pserdvlem1  25020  pserdvlem2  25021  pserdv  25022  abelthlem2  25025  abelthlem3  25026  abelthlem5  25028  abelthlem7  25031  abelthlem8  25032  tanregt0  25129  efif1olem3  25134  efif1olem4  25135  eff1olem  25138  cosargd  25197  cosarg0d  25198  argregt0  25199  argrege0  25200  abslogle  25207  logcnlem3  25233  logcnlem4  25234  efopnlem1  25245  logtayl  25249  abscxp2  25282  cxpcn3lem  25334  abscxpbnd  25340  cosangneg2d  25391  lawcoslem1  25399  lawcos  25400  pythag  25401  isosctrlem3  25404  ssscongptld  25406  chordthmlem3  25418  chordthmlem4  25419  chordthmlem5  25420  heron  25422  bndatandm  25513  efrlim  25553  rlimcxp  25557  o1cxp  25558  cxploglim2  25562  divsqrtsumo1  25567  fsumharmonic  25595  lgamgulmlem2  25613  lgamgulmlem3  25614  lgamgulmlem5  25616  lgambdd  25620  lgamucov  25621  lgamcvg2  25638  ftalem1  25656  ftalem2  25657  ftalem3  25658  ftalem4  25659  ftalem5  25660  ftalem7  25662  logfacbnd3  25805  logfacrlim  25806  logexprlim  25807  dchrabs  25842  lgsdirprm  25913  lgsdilem2  25915  lgsne0  25917  lgsabs1  25918  mul2sq  26001  2sqlem3  26002  2sqblem  26013  vmadivsumb  26065  rplogsumlem2  26067  dchrisumlem2  26072  dchrisumlem3  26073  dchrisum  26074  dchrmusum2  26076  dchrvmasumlem2  26080  dchrvmasumlem3  26081  dchrvmasumiflem1  26083  dchrvmasumiflem2  26084  dchrisum0flblem1  26090  dchrisum0fno1  26093  dchrisum0lem1b  26097  dchrisum0lem1  26098  dchrisum0lem2a  26099  dchrisum0lem2  26100  dchrisum0lem3  26101  mudivsum  26112  mulogsumlem  26113  mulog2sumlem1  26116  mulog2sumlem2  26117  2vmadivsumlem  26122  log2sumbnd  26126  selberglem2  26128  selbergb  26131  selberg2b  26134  chpdifbndlem1  26135  selberg3lem1  26139  selberg3lem2  26140  selberg4lem1  26142  pntrsumo1  26147  pntrsumbnd  26148  pntrsumbnd2  26149  pntrlog2bndlem1  26159  pntrlog2bndlem2  26160  pntrlog2bndlem3  26161  pntrlog2bndlem4  26162  pntrlog2bndlem5  26163  pntrlog2bndlem6  26165  pntrlog2bnd  26166  pntpbnd1a  26167  pntpbnd2  26169  pntibndlem2  26173  pntlemn  26182  pntlemj  26185  pntlemf  26187  pntlemo  26189  pntlem3  26191  pntleml  26193  smcnlem  28478  nmoub3i  28554  isblo3i  28582  htthlem  28698  bcs2  28963  pjhthlem1  29172  nmfnsetre  29658  nmfnleub2  29707  nmfnge0  29708  nmbdfnlbi  29830  nmcfnexi  29832  nmcfnlbi  29833  lnfnconi  29836  cnlnadjlem2  29849  cnlnadjlem7  29854  nmopcoadji  29882  leopnmid  29919  sqsscirc2  31179  subfaclim  32462  subfacval3  32463  sinccvglem  32942  dnicld1  33838  dnibndlem2  33845  dnibndlem6  33849  dnibndlem9  33852  dnibndlem12  33855  dnicn  33858  knoppcnlem4  33862  knoppcnlem6  33864  unblimceq0lem  33872  unblimceq0  33873  unbdqndv2lem1  33875  unbdqndv2lem2  33876  knoppndvlem11  33888  knoppndvlem12  33889  knoppndvlem14  33891  knoppndvlem15  33892  knoppndvlem17  33894  knoppndvlem18  33895  knoppndvlem20  33897  knoppndvlem21  33898  poimirlem29  34998  poimir  35002  iblabsnclem  35032  iblabsnc  35033  iblmulc2nc  35034  itgabsnc  35038  ftc1cnnclem  35040  ftc1anclem1  35042  ftc1anclem2  35043  ftc1anclem4  35045  ftc1anclem5  35046  ftc1anclem6  35047  ftc1anclem7  35048  ftc1anclem8  35049  ftc1anc  35050  ftc2nc  35051  dvasin  35053  areacirclem1  35057  areacirclem2  35058  areacirclem4  35060  areacirclem5  35061  areacirc  35062  geomcau  35109  cntotbnd  35146  rrndstprj1  35180  rrndstprj2  35181  ismrer1  35188  dffltz  39471  rencldnfilem  39617  irrapxlem2  39620  irrapxlem4  39622  irrapxlem5  39623  pellexlem2  39627  pellexlem6  39631  pell14qrgt0  39656  congabseq  39771  acongeq  39780  modabsdifz  39783  jm2.26lem3  39798  sqrtcvallem4  40195  extoimad  40727  imo72b2lem0  40728  imo72b2  40737  dvgrat  40876  cvgdvgrat  40877  radcnvrat  40878  dvconstbi  40898  binomcxplemnotnn0  40920  dstregt0  41778  absnpncan2d  41800  absnpncan3d  41805  abslt2sqd  41858  rexabslelem  41921  fprodabs2  42103  mullimc  42124  mullimcf  42131  limcrecl  42137  lptre2pt  42148  limcleqr  42152  addlimc  42156  0ellimcdiv  42157  limclner  42159  climleltrp  42184  climisp  42254  climxrrelem  42257  cnrefiisplem  42337  climxlim2lem  42353  cncficcgt0  42396  dvdivbd  42431  dvbdfbdioolem1  42436  dvbdfbdioolem2  42437  dvbdfbdioo  42438  ioodvbdlimc1lem1  42439  ioodvbdlimc1lem2  42440  ioodvbdlimc2lem  42442  stoweid  42571  fourierdlem30  42645  fourierdlem39  42654  fourierdlem42  42657  fourierdlem47  42661  fourierdlem68  42682  fourierdlem70  42684  fourierdlem71  42685  fourierdlem73  42687  fourierdlem77  42691  fourierdlem80  42694  fourierdlem83  42697  fourierdlem87  42701  fourierdlem103  42717  fourierdlem104  42718  etransclem23  42765  etransclem48  42790  rrndistlt  42798  ioorrnopnlem  42812  sge0isum  42932  hoicvr  43053  smflimlem4  43273  smfmullem1  43289  smfmullem2  43290  smfmullem3  43291  itsclc0yqsol  45032
  Copyright terms: Public domain W3C validator