Theorem abscld 15599

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 15438	. 2 ⊢ (𝐴 ∈ ℂ → (abs‘𝐴) ∈ ℝ)
3	1, 2	syl 18	1 ⊢ (𝜑 → (abs‘𝐴) ∈ ℝ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ‘cfv 6537  ℂcc 11191  ℝcr 11192  abscabs 15394

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-cnex 11249  ax-resscn 11250  ax-1cn 11251  ax-icn 11252  ax-addcl 11253  ax-addrcl 11254  ax-mulcl 11255  ax-mulrcl 11256  ax-mulcom 11257  ax-addass 11258  ax-mulass 11259  ax-distr 11260  ax-i2m1 11261  ax-1ne0 11262  ax-1rid 11263  ax-rnegex 11264  ax-rrecex 11265  ax-cnre 11266  ax-pre-lttri 11267  ax-pre-lttrn 11268  ax-pre-ltadd 11269  ax-pre-mulgt0 11270  ax-pre-sup 11271

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7375  df-ov 7421  df-oprab 7422  df-mpo 7423  df-om 7876  df-2nd 8000  df-frecs 8292  df-wrecs 8323  df-recs 8372  df-rdg 8411  df-er 8710  df-en 8967  df-dom 8968  df-sdom 8969  df-sup 9427  df-pnf 11338  df-mnf 11339  df-xr 11340  df-ltxr 11341  df-le 11342  df-sub 11536  df-neg 11537  df-div 11967  df-nn 12329  df-2 12398  df-3 12399  df-n0 12600  df-z 12687  df-uz 12959  df-rp 13114  df-seq 14138  df-exp 14198  df-cj 15259  df-re 15260  df-im 15261  df-sqrt 15395  df-abs 15396

This theorem is used by:  bhmafibid1  15628  lo1bddrp  15685  elo1mpt  15694  elo1mpt2  15695  elo1d  15696  o1bdd2  15701  o1bddrp  15702  rlimuni  15710  climuni  15712  o1eq  15730  rlimcld2  15738  rlimrege0  15739  climabs0  15745  mulcn2  15756  reccn2  15757  cn1lem  15758  cjcn2  15760  o1add  15774  o1mul  15775  o1sub  15776  rlimo1  15777  o1rlimmul  15779  climsqz  15801  climsqz2  15802  rlimsqzlem  15809  o1le  15813  climbdd  15832  caucvgrlem  15833  caucvgrlem2  15835  iseraltlem3  15844  iseralt  15845  fsumabs  15961  o1fsum  15973  iserabs  15975  cvgcmpce  15978  abscvgcvg  15979  divrcnv  16014  explecnv  16027  geomulcvg  16038  cvgrat  16045  mertenslem1  16046  mertenslem2  16047  fprodabs  16134  efcllem  16236  efaddlem  16252  eftlub  16270  ef01bndlem  16345  sin01bnd  16346  cos01bnd  16347  absef  16358  dvdsabseq  16476  alzdvds  16483  sqnprm  16871  pclem  17009  mul4sqlem  17124  xrsdsreclb  21713  gzrngunitlem  21731  gzrngunit  21732  prmirredlem  21771  nm2dif  24937  blcvx  25110  recld2  25127  addcnlem  25177  cnheiborlem  25268  cnheibor  25269  cnllycmp  25270  cphsqrtcl2  25500  ipcau2  25548  tcphcphlem1  25549  ipcnlem2  25558  cncmet  25636  trirn  25714  rrxdstprj1  25723  pjthlem1  25751  volsup2  25919  mbfi1fseqlem6  26034  iblabslem  26141  iblabs  26142  iblabsr  26143  iblmulc2  26144  itgabs  26148  bddmulibl  26152  bddiblnc  26155  itgcn  26158  dveflem  26292  dvlip  26306  dvlipcn  26307  c1liplem1  26309  dveq0  26313  dv11cn  26314  lhop1lem  26326  dvfsumabs  26336  dvfsumrlim  26344  dvfsumrlim2  26345  ftc1a  26350  ftc1lem4  26352  plyeq0lem  26522  aalioulem2  26653  aalioulem3  26654  aalioulem4  26655  aalioulem5  26656  aalioulem6  26657  aaliou  26658  geolim3  26659  aaliou2b  26661  aaliou3lem9  26670  ulmbdd  26718  ulmcn  26719  ulmdvlem1  26720  mtest  26724  mtestbdd  26725  iblulm  26727  itgulm  26728  radcnvlem1  26733  radcnvlem2  26734  radcnvlt1  26738  radcnvle  26740  dvradcnv  26741  pserulm  26742  psercnlem2  26744  psercnlem1  26745  psercn  26746  pserdvlem1  26747  pserdvlem2  26748  pserdv  26749  abelthlem2  26752  abelthlem3  26753  abelthlem5  26755  abelthlem7  26758  abelthlem8  26759  tanregt0  26860  efif1olem3  26865  efif1olem4  26866  eff1olem  26869  cosargd  26929  cosarg0d  26930  argregt0  26931  argrege0  26932  abslogle  26939  logcnlem3  26965  logcnlem4  26966  efopnlem1  26977  logtayl  26981  abscxp2  27014  cxpcn3lem  27068  abscxpbnd  27074  cosangneg2d  27128  lawcoslem1  27136  lawcos  27137  pythag  27138  isosctrlem3  27141  ssscongptld  27143  chordthmlem3  27155  chordthmlem4  27156  chordthmlem5  27157  heron  27159  bndatandm  27250  efrlim  27290  rlimcxp  27294  o1cxp  27295  cxploglim2  27299  divsqrtsumo1  27304  fsumharmonic  27332  lgamgulmlem2  27350  lgamgulmlem3  27351  lgamgulmlem5  27353  lgambdd  27357  lgamucov  27358  lgamcvg2  27375  ftalem1  27393  ftalem2  27394  ftalem3  27395  ftalem4  27396  ftalem5  27397  ftalem7  27399  logfacbnd3  27543  logfacrlim  27544  logexprlim  27545  dchrabs  27580  lgsdirprm  27651  lgsdilem2  27653  lgsne0  27655  lgsabs1  27656  mul2sq  27739  2sqlem3  27740  2sqblem  27751  vmadivsumb  27803  rplogsumlem2  27805  dchrisumlem2  27810  dchrisumlem3  27811  dchrisum  27812  dchrmusum2  27814  dchrvmasumlem2  27818  dchrvmasumlem3  27819  dchrvmasumiflem1  27821  dchrvmasumiflem2  27822  dchrisum0flblem1  27828  dchrisum0fno1  27831  dchrisum0lem1b  27835  dchrisum0lem1  27836  dchrisum0lem2a  27837  dchrisum0lem2  27838  dchrisum0lem3  27839  mudivsum  27850  mulogsumlem  27851  mulog2sumlem1  27854  mulog2sumlem2  27855  2vmadivsumlem  27860  log2sumbnd  27864  selberglem2  27866  selbergb  27869  selberg2b  27872  chpdifbndlem1  27873  selberg3lem1  27877  selberg3lem2  27878  selberg4lem1  27880  pntrsumo1  27885  pntrsumbnd  27886  pntrsumbnd2  27887  pntrlog2bndlem1  27897  pntrlog2bndlem2  27898  pntrlog2bndlem3  27899  pntrlog2bndlem4  27900  pntrlog2bndlem5  27901  pntrlog2bndlem6  27903  pntrlog2bnd  27904  pntpbnd1a  27905  pntpbnd2  27907  pntibndlem2  27911  pntlemn  27920  pntlemj  27923  pntlemf  27925  pntlemo  27927  pntlem3  27929  pntleml  27931  smcnlem  31292  nmoub3i  31368  isblo3i  31396  htthlem  31512  bcs2  31777  pjhthlem1  31986  nmfnsetre  32472  nmfnleub2  32521  nmfnge0  32522  nmbdfnlbi  32644  nmcfnexi  32646  nmcfnlbi  32647  lnfnconi  32650  cnlnadjlem2  32663  cnlnadjlem7  32668  nmopcoadji  32696  leopnmid  32733  constrdircl  34390  iconstr  34391  constrremulcl  34392  constrimcl  34395  constrmulcl  34396  constrinvcl  34398  constrabscl  34403  constrsqrtcl  34404  sqsscirc2  34534  subfaclim  35932  subfacval3  35933  sinccvglem  36416  dnicld1  37318  dnibndlem2  37325  dnibndlem6  37329  dnibndlem9  37332  dnibndlem12  37335  dnicn  37338  knoppcnlem4  37342  knoppcnlem6  37344  unblimceq0lem  37352  unblimceq0  37353  unbdqndv2lem1  37355  unbdqndv2lem2  37356  knoppndvlem11  37368  knoppndvlem12  37369  knoppndvlem14  37371  knoppndvlem15  37372  knoppndvlem17  37374  knoppndvlem18  37375  knoppndvlem20  37377  knoppndvlem21  37378  poimirlem29  38547  poimir  38551  iblabsnclem  38581  iblabsnc  38582  iblmulc2nc  38583  itgabsnc  38587  ftc1cnnclem  38589  ftc1anclem1  38591  ftc1anclem2  38592  ftc1anclem4  38594  ftc1anclem5  38595  ftc1anclem6  38596  ftc1anclem7  38597  ftc1anclem8  38598  ftc1anc  38599  ftc2nc  38600  dvasin  38602  areacirclem1  38606  areacirclem2  38607  areacirclem4  38609  areacirclem5  38610  areacirc  38611  geomcau  38673  cntotbnd  38710  rrndstprj1  38744  rrndstprj2  38745  ismrer1  38752  readvrec  43393  readvcot  43395  dffltz  43650  rencldnfilem  43806  irrapxlem2  43809  irrapxlem4  43811  irrapxlem5  43812  pellexlem2  43816  pellexlem6  43820  pell14qrgt0  43845  congabseq  43960  acongeq  43969  modabsdifz  43972  jm2.26lem3  43987  sqrtcvallem4  44624  extoimad  45149  imo72b2lem0  45150  imo72b2  45157  dvgrat  45281  cvgdvgrat  45282  radcnvrat  45283  dvconstbi  45303  binomcxplemnotnn0  45325  dstregt0  46267  absnpncan2d  46287  absnpncan3d  46292  abslt2sqd  46341  rexabslelem  46397  cvgcaule  46470  fprodabs2  46576  mullimc  46597  mullimcf  46604  limcrecl  46610  lptre2pt  46619  limcleqr  46623  addlimc  46627  0ellimcdiv  46628  limclner  46630  climleltrp  46655  climisp  46725  climxrrelem  46728  cnrefiisplem  46808  climxlim2lem  46824  cncficcgt0  46867  dvdivbd  46902  dvbdfbdioolem1  46907  dvbdfbdioolem2  46908  dvbdfbdioo  46909  ioodvbdlimc1lem1  46910  ioodvbdlimc1lem2  46911  ioodvbdlimc2lem  46913  stoweid  47042  fourierdlem30  47116  fourierdlem39  47125  fourierdlem42  47128  fourierdlem47  47132  fourierdlem68  47153  fourierdlem70  47155  fourierdlem71  47156  fourierdlem73  47158  fourierdlem77  47162  fourierdlem80  47165  fourierdlem83  47168  fourierdlem87  47172  fourierdlem103  47188  fourierdlem104  47189  etransclem23  47236  etransclem48  47261  rrndistlt  47269  ioorrnopnlem  47283  sge0isum  47406  hoicvr  47527  smflimlem4  47753  smfmullem1  47770  smfmullem2  47771  smfmullem3  47772  modlt0b  48408  itsclc0yqsol  49845