Theorem abscld 15489

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

Syntax hints:   → wi 4   ∈ wcel 2149  ‘cfv 6537  ℂcc 11097  ℝcr 11098  abscabs 15284

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-cnex 11155  ax-resscn 11156  ax-1cn 11157  ax-icn 11158  ax-addcl 11159  ax-addrcl 11160  ax-mulcl 11161  ax-mulrcl 11162  ax-mulcom 11163  ax-addass 11164  ax-mulass 11165  ax-distr 11166  ax-i2m1 11167  ax-1ne0 11168  ax-1rid 11169  ax-rnegex 11170  ax-rrecex 11171  ax-cnre 11172  ax-pre-lttri 11173  ax-pre-lttrn 11174  ax-pre-ltadd 11175  ax-pre-mulgt0 11176  ax-pre-sup 11177

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rmo 3376  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  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 7368  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7862  df-2nd 7986  df-frecs 8277  df-wrecs 8308  df-recs 8357  df-rdg 8396  df-er 8693  df-en 8943  df-dom 8944  df-sdom 8945  df-sup 9401  df-pnf 11244  df-mnf 11245  df-xr 11246  df-ltxr 11247  df-le 11248  df-sub 11442  df-neg 11443  df-div 11871  df-nn 12233  df-2 12302  df-3 12303  df-n0 12504  df-z 12591  df-uz 12862  df-rp 13016  df-seq 14037  df-exp 14097  df-cj 15149  df-re 15150  df-im 15151  df-sqrt 15285  df-abs 15286

This theorem is referenced by:  bhmafibid1  15518  lo1bddrp  15575  elo1mpt  15584  elo1mpt2  15585  elo1d  15586  o1bdd2  15591  o1bddrp  15592  rlimuni  15600  climuni  15602  o1eq  15620  rlimcld2  15628  rlimrege0  15629  climabs0  15635  mulcn2  15646  reccn2  15647  cn1lem  15648  cjcn2  15650  o1add  15664  o1mul  15665  o1sub  15666  rlimo1  15667  o1rlimmul  15669  climsqz  15691  climsqz2  15692  rlimsqzlem  15699  o1le  15703  climbdd  15722  caucvgrlem  15723  caucvgrlem2  15725  iseraltlem3  15734  iseralt  15735  fsumabs  15852  o1fsum  15864  iserabs  15866  cvgcmpce  15869  abscvgcvg  15870  divrcnv  15905  explecnv  15918  geomulcvg  15929  cvgrat  15936  mertenslem1  15937  mertenslem2  15938  fprodabs  16027  efcllem  16130  efaddlem  16146  eftlub  16164  ef01bndlem  16239  sin01bnd  16240  cos01bnd  16241  absef  16252  dvdsabseq  16370  alzdvds  16377  sqnprm  16760  pclem  16897  mul4sqlem  17012  xrsdsreclb  21532  gzrngunitlem  21550  gzrngunit  21551  prmirredlem  21590  nm2dif  24750  blcvx  24923  recld2  24940  addcnlem  24990  cnheiborlem  25081  cnheibor  25082  cnllycmp  25083  cphsqrtcl2  25313  ipcau2  25361  tcphcphlem1  25362  ipcnlem2  25371  cncmet  25449  trirn  25527  rrxdstprj1  25536  pjthlem1  25564  volsup2  25732  mbfi1fseqlem6  25847  iblabslem  25955  iblabs  25956  iblabsr  25957  iblmulc2  25958  itgabs  25962  bddmulibl  25966  bddiblnc  25969  itgcn  25972  dveflem  26106  dvlip  26120  dvlipcn  26121  c1liplem1  26123  dveq0  26127  dv11cn  26128  lhop1lem  26140  dvfsumabs  26150  dvfsumrlim  26158  dvfsumrlim2  26159  ftc1a  26164  ftc1lem4  26166  plyeq0lem  26335  aalioulem2  26462  aalioulem3  26463  aalioulem4  26464  aalioulem5  26465  aalioulem6  26466  aaliou  26467  geolim3  26468  aaliou2b  26470  aaliou3lem9  26479  ulmbdd  26526  ulmcn  26527  ulmdvlem1  26528  mtest  26532  mtestbdd  26533  iblulm  26535  itgulm  26536  radcnvlem1  26541  radcnvlem2  26542  radcnvlt1  26546  radcnvle  26548  dvradcnv  26549  pserulm  26550  psercnlem2  26552  psercnlem1  26553  psercn  26554  pserdvlem1  26555  pserdvlem2  26556  pserdv  26557  abelthlem2  26560  abelthlem3  26561  abelthlem5  26563  abelthlem7  26566  abelthlem8  26567  tanregt0  26669  efif1olem3  26674  efif1olem4  26675  eff1olem  26678  cosargd  26738  cosarg0d  26739  argregt0  26740  argrege0  26741  abslogle  26748  logcnlem3  26774  logcnlem4  26775  efopnlem1  26786  logtayl  26790  abscxp2  26823  cxpcn3lem  26877  abscxpbnd  26883  cosangneg2d  26937  lawcoslem1  26945  lawcos  26946  pythag  26947  isosctrlem3  26950  ssscongptld  26952  chordthmlem3  26964  chordthmlem4  26965  chordthmlem5  26966  heron  26968  bndatandm  27059  efrlim  27099  rlimcxp  27103  o1cxp  27104  cxploglim2  27108  divsqrtsumo1  27113  fsumharmonic  27141  lgamgulmlem2  27159  lgamgulmlem3  27160  lgamgulmlem5  27162  lgambdd  27166  lgamucov  27167  lgamcvg2  27184  ftalem1  27202  ftalem2  27203  ftalem3  27204  ftalem4  27205  ftalem5  27206  ftalem7  27208  logfacbnd3  27352  logfacrlim  27353  logexprlim  27354  dchrabs  27389  lgsdirprm  27460  lgsdilem2  27462  lgsne0  27464  lgsabs1  27465  mul2sq  27548  2sqlem3  27549  2sqblem  27560  vmadivsumb  27612  rplogsumlem2  27614  dchrisumlem2  27619  dchrisumlem3  27620  dchrisum  27621  dchrmusum2  27623  dchrvmasumlem2  27627  dchrvmasumlem3  27628  dchrvmasumiflem1  27630  dchrvmasumiflem2  27631  dchrisum0flblem1  27637  dchrisum0fno1  27640  dchrisum0lem1b  27644  dchrisum0lem1  27645  dchrisum0lem2a  27646  dchrisum0lem2  27647  dchrisum0lem3  27648  mudivsum  27659  mulogsumlem  27660  mulog2sumlem1  27663  mulog2sumlem2  27664  2vmadivsumlem  27669  log2sumbnd  27673  selberglem2  27675  selbergb  27678  selberg2b  27681  chpdifbndlem1  27682  selberg3lem1  27686  selberg3lem2  27687  selberg4lem1  27689  pntrsumo1  27694  pntrsumbnd  27695  pntrsumbnd2  27696  pntrlog2bndlem1  27706  pntrlog2bndlem2  27707  pntrlog2bndlem3  27708  pntrlog2bndlem4  27709  pntrlog2bndlem5  27710  pntrlog2bndlem6  27712  pntrlog2bnd  27713  pntpbnd1a  27714  pntpbnd2  27716  pntibndlem2  27720  pntlemn  27729  pntlemj  27732  pntlemf  27734  pntlemo  27736  pntlem3  27738  pntleml  27740  smcnlem  30989  nmoub3i  31065  isblo3i  31093  htthlem  31209  bcs2  31474  pjhthlem1  31683  nmfnsetre  32169  nmfnleub2  32218  nmfnge0  32219  nmbdfnlbi  32341  nmcfnexi  32343  nmcfnlbi  32344  lnfnconi  32347  cnlnadjlem2  32360  cnlnadjlem7  32365  nmopcoadji  32393  leopnmid  32430  constrdircl  34099  iconstr  34100  constrremulcl  34101  constrimcl  34104  constrmulcl  34105  constrinvcl  34107  constrabscl  34112  constrsqrtcl  34113  sqsscirc2  34243  subfaclim  35578  subfacval3  35579  sinccvglem  36062  dnicld1  36949  dnibndlem2  36956  dnibndlem6  36960  dnibndlem9  36963  dnibndlem12  36966  dnicn  36969  knoppcnlem4  36973  knoppcnlem6  36975  unblimceq0lem  36983  unblimceq0  36984  unbdqndv2lem1  36986  unbdqndv2lem2  36987  knoppndvlem11  36999  knoppndvlem12  37000  knoppndvlem14  37002  knoppndvlem15  37003  knoppndvlem17  37005  knoppndvlem18  37006  knoppndvlem20  37008  knoppndvlem21  37009  poimirlem29  38187  poimir  38191  iblabsnclem  38221  iblabsnc  38222  iblmulc2nc  38223  itgabsnc  38227  ftc1cnnclem  38229  ftc1anclem1  38231  ftc1anclem2  38232  ftc1anclem4  38234  ftc1anclem5  38235  ftc1anclem6  38236  ftc1anclem7  38237  ftc1anclem8  38238  ftc1anc  38239  ftc2nc  38240  dvasin  38242  areacirclem1  38246  areacirclem2  38247  areacirclem4  38249  areacirclem5  38250  areacirc  38251  geomcau  38297  cntotbnd  38334  rrndstprj1  38368  rrndstprj2  38369  ismrer1  38376  readvrec  43012  readvcot  43014  dffltz  43257  rencldnfilem  43438  irrapxlem2  43441  irrapxlem4  43443  irrapxlem5  43444  pellexlem2  43448  pellexlem6  43452  pell14qrgt0  43477  congabseq  43592  acongeq  43601  modabsdifz  43604  jm2.26lem3  43619  sqrtcvallem4  44256  extoimad  44781  imo72b2lem0  44782  imo72b2  44789  dvgrat  44913  cvgdvgrat  44914  radcnvrat  44915  dvconstbi  44935  binomcxplemnotnn0  44957  dstregt0  45892  absnpncan2d  45912  absnpncan3d  45917  abslt2sqd  45967  rexabslelem  46023  cvgcaule  46096  fprodabs2  46202  mullimc  46223  mullimcf  46230  limcrecl  46236  lptre2pt  46245  limcleqr  46249  addlimc  46253  0ellimcdiv  46254  limclner  46256  climleltrp  46281  climisp  46351  climxrrelem  46354  cnrefiisplem  46434  climxlim2lem  46450  cncficcgt0  46493  dvdivbd  46528  dvbdfbdioolem1  46533  dvbdfbdioolem2  46534  dvbdfbdioo  46535  ioodvbdlimc1lem1  46536  ioodvbdlimc1lem2  46537  ioodvbdlimc2lem  46539  stoweid  46668  fourierdlem30  46742  fourierdlem39  46751  fourierdlem42  46754  fourierdlem47  46758  fourierdlem68  46779  fourierdlem70  46781  fourierdlem71  46782  fourierdlem73  46784  fourierdlem77  46788  fourierdlem80  46791  fourierdlem83  46794  fourierdlem87  46798  fourierdlem103  46814  fourierdlem104  46815  etransclem23  46862  etransclem48  46887  rrndistlt  46895  ioorrnopnlem  46909  sge0isum  47032  hoicvr  47153  smflimlem4  47379  smfmullem1  47396  smfmullem2  47397  smfmullem3  47398  modlt0b  47994  itsclc0yqsol  49428