Theorem abscld 15514

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

Step	Hyp	Ref	Expression
1		abscld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		abscl 15353	. 2 ⊢ (𝐴 ∈ ℂ → (abs‘𝐴) ∈ ℝ)
3	1, 2	syl 18	1 ⊢ (𝜑 → (abs‘𝐴) ∈ ℝ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ‘cfv 6540  ℂcc 11113  ℝcr 11114  abscabs 15309

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-cnex 11171  ax-resscn 11172  ax-1cn 11173  ax-icn 11174  ax-addcl 11175  ax-addrcl 11176  ax-mulcl 11177  ax-mulrcl 11178  ax-mulcom 11179  ax-addass 11180  ax-mulass 11181  ax-distr 11182  ax-i2m1 11183  ax-1ne0 11184  ax-1rid 11185  ax-rnegex 11186  ax-rrecex 11187  ax-cnre 11188  ax-pre-lttri 11189  ax-pre-lttrn 11190  ax-pre-ltadd 11191  ax-pre-mulgt0 11192  ax-pre-sup 11193

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-rmo 3371  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7376  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7869  df-2nd 7993  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-er 8700  df-en 8950  df-dom 8951  df-sdom 8952  df-sup 9409  df-pnf 11260  df-mnf 11261  df-xr 11262  df-ltxr 11263  df-le 11264  df-sub 11458  df-neg 11459  df-div 11887  df-nn 12249  df-2 12318  df-3 12319  df-n0 12520  df-z 12607  df-uz 12879  df-rp 13033  df-seq 14056  df-exp 14116  df-cj 15174  df-re 15175  df-im 15176  df-sqrt 15310  df-abs 15311

This theorem is used by:  bhmafibid1  15543  lo1bddrp  15600  elo1mpt  15609  elo1mpt2  15610  elo1d  15611  o1bdd2  15616  o1bddrp  15617  rlimuni  15625  climuni  15627  o1eq  15645  rlimcld2  15653  rlimrege0  15654  climabs0  15660  mulcn2  15671  reccn2  15672  cn1lem  15673  cjcn2  15675  o1add  15689  o1mul  15690  o1sub  15691  rlimo1  15692  o1rlimmul  15694  climsqz  15716  climsqz2  15717  rlimsqzlem  15724  o1le  15728  climbdd  15747  caucvgrlem  15748  caucvgrlem2  15750  iseraltlem3  15759  iseralt  15760  fsumabs  15876  o1fsum  15888  iserabs  15890  cvgcmpce  15893  abscvgcvg  15894  divrcnv  15929  explecnv  15942  geomulcvg  15953  cvgrat  15960  mertenslem1  15961  mertenslem2  15962  fprodabs  16051  efcllem  16153  efaddlem  16169  eftlub  16187  ef01bndlem  16262  sin01bnd  16263  cos01bnd  16264  absef  16275  dvdsabseq  16393  alzdvds  16400  sqnprm  16783  pclem  16920  mul4sqlem  17035  xrsdsreclb  21614  gzrngunitlem  21632  gzrngunit  21633  prmirredlem  21672  nm2dif  24833  blcvx  25006  recld2  25023  addcnlem  25073  cnheiborlem  25164  cnheibor  25165  cnllycmp  25166  cphsqrtcl2  25396  ipcau2  25444  tcphcphlem1  25445  ipcnlem2  25454  cncmet  25532  trirn  25610  rrxdstprj1  25619  pjthlem1  25647  volsup2  25815  mbfi1fseqlem6  25930  iblabslem  26038  iblabs  26039  iblabsr  26040  iblmulc2  26041  itgabs  26045  bddmulibl  26049  bddiblnc  26052  itgcn  26055  dveflem  26189  dvlip  26203  dvlipcn  26204  c1liplem1  26206  dveq0  26210  dv11cn  26211  lhop1lem  26223  dvfsumabs  26233  dvfsumrlim  26241  dvfsumrlim2  26242  ftc1a  26247  ftc1lem4  26249  plyeq0lem  26418  aalioulem2  26547  aalioulem3  26548  aalioulem4  26549  aalioulem5  26550  aalioulem6  26551  aaliou  26552  geolim3  26553  aaliou2b  26555  aaliou3lem9  26564  ulmbdd  26612  ulmcn  26613  ulmdvlem1  26614  mtest  26618  mtestbdd  26619  iblulm  26621  itgulm  26622  radcnvlem1  26627  radcnvlem2  26628  radcnvlt1  26632  radcnvle  26634  dvradcnv  26635  pserulm  26636  psercnlem2  26638  psercnlem1  26639  psercn  26640  pserdvlem1  26641  pserdvlem2  26642  pserdv  26643  abelthlem2  26646  abelthlem3  26647  abelthlem5  26649  abelthlem7  26652  abelthlem8  26653  tanregt0  26755  efif1olem3  26760  efif1olem4  26761  eff1olem  26764  cosargd  26824  cosarg0d  26825  argregt0  26826  argrege0  26827  abslogle  26834  logcnlem3  26860  logcnlem4  26861  efopnlem1  26872  logtayl  26876  abscxp2  26909  cxpcn3lem  26963  abscxpbnd  26969  cosangneg2d  27023  lawcoslem1  27031  lawcos  27032  pythag  27033  isosctrlem3  27036  ssscongptld  27038  chordthmlem3  27050  chordthmlem4  27051  chordthmlem5  27052  heron  27054  bndatandm  27145  efrlim  27185  rlimcxp  27189  o1cxp  27190  cxploglim2  27194  divsqrtsumo1  27199  fsumharmonic  27227  lgamgulmlem2  27245  lgamgulmlem3  27246  lgamgulmlem5  27248  lgambdd  27252  lgamucov  27253  lgamcvg2  27270  ftalem1  27288  ftalem2  27289  ftalem3  27290  ftalem4  27291  ftalem5  27292  ftalem7  27294  logfacbnd3  27438  logfacrlim  27439  logexprlim  27440  dchrabs  27475  lgsdirprm  27546  lgsdilem2  27548  lgsne0  27550  lgsabs1  27551  mul2sq  27634  2sqlem3  27635  2sqblem  27646  vmadivsumb  27698  rplogsumlem2  27700  dchrisumlem2  27705  dchrisumlem3  27706  dchrisum  27707  dchrmusum2  27709  dchrvmasumlem2  27713  dchrvmasumlem3  27714  dchrvmasumiflem1  27716  dchrvmasumiflem2  27717  dchrisum0flblem1  27723  dchrisum0fno1  27726  dchrisum0lem1b  27730  dchrisum0lem1  27731  dchrisum0lem2a  27732  dchrisum0lem2  27733  dchrisum0lem3  27734  mudivsum  27745  mulogsumlem  27746  mulog2sumlem1  27749  mulog2sumlem2  27750  2vmadivsumlem  27755  log2sumbnd  27759  selberglem2  27761  selbergb  27764  selberg2b  27767  chpdifbndlem1  27768  selberg3lem1  27772  selberg3lem2  27773  selberg4lem1  27775  pntrsumo1  27780  pntrsumbnd  27781  pntrsumbnd2  27782  pntrlog2bndlem1  27792  pntrlog2bndlem2  27793  pntrlog2bndlem3  27794  pntrlog2bndlem4  27795  pntrlog2bndlem5  27796  pntrlog2bndlem6  27798  pntrlog2bnd  27799  pntpbnd1a  27800  pntpbnd2  27802  pntibndlem2  27806  pntlemn  27815  pntlemj  27818  pntlemf  27820  pntlemo  27822  pntlem3  27824  pntleml  27826  smcnlem  31120  nmoub3i  31196  isblo3i  31224  htthlem  31340  bcs2  31605  pjhthlem1  31814  nmfnsetre  32300  nmfnleub2  32349  nmfnge0  32350  nmbdfnlbi  32472  nmcfnexi  32474  nmcfnlbi  32475  lnfnconi  32478  cnlnadjlem2  32491  cnlnadjlem7  32496  nmopcoadji  32524  leopnmid  32561  constrdircl  34219  iconstr  34220  constrremulcl  34221  constrimcl  34224  constrmulcl  34225  constrinvcl  34227  constrabscl  34232  constrsqrtcl  34233  sqsscirc2  34363  subfaclim  35717  subfacval3  35718  sinccvglem  36201  dnicld1  37118  dnibndlem2  37125  dnibndlem6  37129  dnibndlem9  37132  dnibndlem12  37135  dnicn  37138  knoppcnlem4  37142  knoppcnlem6  37144  unblimceq0lem  37152  unblimceq0  37153  unbdqndv2lem1  37155  unbdqndv2lem2  37156  knoppndvlem11  37168  knoppndvlem12  37169  knoppndvlem14  37171  knoppndvlem15  37172  knoppndvlem17  37174  knoppndvlem18  37175  knoppndvlem20  37177  knoppndvlem21  37178  poimirlem29  38357  poimir  38361  iblabsnclem  38391  iblabsnc  38392  iblmulc2nc  38393  itgabsnc  38397  ftc1cnnclem  38399  ftc1anclem1  38401  ftc1anclem2  38402  ftc1anclem4  38404  ftc1anclem5  38405  ftc1anclem6  38406  ftc1anclem7  38407  ftc1anclem8  38408  ftc1anc  38409  ftc2nc  38410  dvasin  38412  areacirclem1  38416  areacirclem2  38417  areacirclem4  38419  areacirclem5  38420  areacirc  38421  geomcau  38468  cntotbnd  38505  rrndstprj1  38539  rrndstprj2  38540  ismrer1  38547  readvrec  43181  readvcot  43183  dffltz  43424  rencldnfilem  43605  irrapxlem2  43608  irrapxlem4  43610  irrapxlem5  43611  pellexlem2  43615  pellexlem6  43619  pell14qrgt0  43644  congabseq  43759  acongeq  43768  modabsdifz  43771  jm2.26lem3  43786  sqrtcvallem4  44423  extoimad  44948  imo72b2lem0  44949  imo72b2  44956  dvgrat  45080  cvgdvgrat  45081  radcnvrat  45082  dvconstbi  45102  binomcxplemnotnn0  45124  dstregt0  46059  absnpncan2d  46079  absnpncan3d  46084  abslt2sqd  46134  rexabslelem  46190  cvgcaule  46263  fprodabs2  46369  mullimc  46390  mullimcf  46397  limcrecl  46403  lptre2pt  46412  limcleqr  46416  addlimc  46420  0ellimcdiv  46421  limclner  46423  climleltrp  46448  climisp  46518  climxrrelem  46521  cnrefiisplem  46601  climxlim2lem  46617  cncficcgt0  46660  dvdivbd  46695  dvbdfbdioolem1  46700  dvbdfbdioolem2  46701  dvbdfbdioo  46702  ioodvbdlimc1lem1  46703  ioodvbdlimc1lem2  46704  ioodvbdlimc2lem  46706  stoweid  46835  fourierdlem30  46909  fourierdlem39  46918  fourierdlem42  46921  fourierdlem47  46925  fourierdlem68  46946  fourierdlem70  46948  fourierdlem71  46949  fourierdlem73  46951  fourierdlem77  46955  fourierdlem80  46958  fourierdlem83  46961  fourierdlem87  46965  fourierdlem103  46981  fourierdlem104  46982  etransclem23  47029  etransclem48  47054  rrndistlt  47062  ioorrnopnlem  47076  sge0isum  47199  hoicvr  47320  smflimlem4  47546  smfmullem1  47563  smfmullem2  47564  smfmullem3  47565  modlt0b  48164  itsclc0yqsol  49601