Theorem abscld 14175

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

Syntax hints:   → wi 4   ∈ wcel 1990  ‘cfv 5888  ℂcc 9934  ℝcr 9935  abscabs 13974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-sup 8348  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-n0 11293  df-z 11378  df-uz 11688  df-rp 11833  df-seq 12802  df-exp 12861  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976

This theorem is referenced by:  lo1bddrp  14256  elo1mpt  14265  elo1mpt2  14266  elo1d  14267  o1bdd2  14272  o1bddrp  14273  rlimuni  14281  climuni  14283  o1eq  14301  rlimcld2  14309  rlimrege0  14310  climabs0  14316  mulcn2  14326  reccn2  14327  cn1lem  14328  cjcn2  14330  o1add  14344  o1mul  14345  o1sub  14346  rlimo1  14347  o1rlimmul  14349  climsqz  14371  climsqz2  14372  rlimsqzlem  14379  o1le  14383  climbdd  14402  caucvgrlem  14403  caucvgrlem2  14405  iseraltlem3  14414  iseralt  14415  fsumabs  14533  o1fsum  14545  iserabs  14547  cvgcmpce  14550  abscvgcvg  14551  divrcnv  14584  explecnv  14597  geomulcvg  14607  cvgrat  14615  mertenslem1  14616  mertenslem2  14617  fprodabs  14704  efcllem  14808  efaddlem  14823  eftlub  14839  ef01bndlem  14914  sin01bnd  14915  cos01bnd  14916  absef  14927  dvdsabseq  15035  alzdvds  15042  sqnprm  15414  pclem  15543  mul4sqlem  15657  xrsdsreclb  19793  gzrngunitlem  19811  gzrngunit  19812  prmirredlem  19841  nm2dif  22429  blcvx  22601  recld2  22617  addcnlem  22667  cnheiborlem  22753  cnheibor  22754  cnllycmp  22755  cphsqrtcl2  22986  ipcau2  23033  tchcphlem1  23034  ipcnlem2  23043  cncmet  23119  trirn  23183  rrxdstprj1  23192  pjthlem1  23208  volsup2  23373  mbfi1fseqlem6  23487  iblabslem  23594  iblabs  23595  iblabsr  23596  iblmulc2  23597  itgabs  23601  bddmulibl  23605  itgcn  23609  dveflem  23742  dvlip  23756  dvlipcn  23757  c1liplem1  23759  dveq0  23763  dv11cn  23764  lhop1lem  23776  dvfsumabs  23786  dvfsumrlim  23794  dvfsumrlim2  23795  ftc1a  23800  ftc1lem4  23802  plyeq0lem  23966  aalioulem2  24088  aalioulem3  24089  aalioulem4  24090  aalioulem5  24091  aalioulem6  24092  aaliou  24093  geolim3  24094  aaliou2b  24096  aaliou3lem9  24105  ulmbdd  24152  ulmcn  24153  ulmdvlem1  24154  mtest  24158  mtestbdd  24159  iblulm  24161  itgulm  24162  radcnvlem1  24167  radcnvlem2  24168  radcnvlt1  24172  radcnvle  24174  dvradcnv  24175  pserulm  24176  psercnlem2  24178  psercnlem1  24179  psercn  24180  pserdvlem1  24181  pserdvlem2  24182  pserdv  24183  abelthlem2  24186  abelthlem3  24187  abelthlem5  24189  abelthlem7  24192  abelthlem8  24193  tanregt0  24285  efif1olem3  24290  efif1olem4  24291  eff1olem  24294  cosargd  24354  cosarg0d  24355  argrege0  24357  abslogle  24364  logcnlem3  24390  logcnlem4  24391  efopnlem1  24402  logtayl  24406  abscxp2  24439  cxpcn3lem  24488  abscxpbnd  24494  cosangneg2d  24537  lawcoslem1  24545  lawcos  24546  pythag  24547  isosctrlem3  24550  ssscongptld  24552  chordthmlem3  24561  chordthmlem4  24562  chordthmlem5  24563  heron  24565  bndatandm  24656  efrlim  24696  rlimcxp  24700  o1cxp  24701  cxploglim2  24705  divsqrtsumo1  24710  fsumharmonic  24738  lgamgulmlem2  24756  lgamgulmlem3  24757  lgamgulmlem5  24759  lgambdd  24763  lgamucov  24764  lgamcvg2  24781  ftalem1  24799  ftalem2  24800  ftalem3  24801  ftalem4  24802  ftalem5  24803  ftalem7  24805  logfacbnd3  24948  logfacrlim  24949  logexprlim  24950  dchrabs  24985  lgsdirprm  25056  lgsdilem2  25058  lgsne0  25060  lgsabs1  25061  mul2sq  25144  2sqlem3  25145  2sqblem  25156  vmadivsumb  25172  rplogsumlem2  25174  dchrisumlem2  25179  dchrisumlem3  25180  dchrisum  25181  dchrmusum2  25183  dchrvmasumlem2  25187  dchrvmasumlem3  25188  dchrvmasumiflem1  25190  dchrvmasumiflem2  25191  dchrisum0flblem1  25197  dchrisum0fno1  25200  dchrisum0lem1b  25204  dchrisum0lem1  25205  dchrisum0lem2a  25206  dchrisum0lem2  25207  dchrisum0lem3  25208  mudivsum  25219  mulogsumlem  25220  mulog2sumlem1  25223  mulog2sumlem2  25224  2vmadivsumlem  25229  log2sumbnd  25233  selberglem2  25235  selbergb  25238  selberg2b  25241  chpdifbndlem1  25242  selberg3lem1  25246  selberg3lem2  25247  selberg4lem1  25249  pntrsumo1  25254  pntrsumbnd  25255  pntrsumbnd2  25256  pntrlog2bndlem1  25266  pntrlog2bndlem2  25267  pntrlog2bndlem3  25268  pntrlog2bndlem4  25269  pntrlog2bndlem5  25270  pntrlog2bndlem6  25272  pntrlog2bnd  25273  pntpbnd1a  25274  pntpbnd2  25276  pntibndlem2  25280  pntlemn  25289  pntlemj  25292  pntlemf  25294  pntlemo  25296  pntlem3  25298  pntleml  25300  smcnlem  27552  nmoub3i  27628  isblo3i  27656  htthlem  27774  bcs2  28039  pjhthlem1  28250  nmfnsetre  28736  nmfnleub2  28785  nmfnge0  28786  nmbdfnlbi  28908  nmcfnexi  28910  nmcfnlbi  28911  lnfnconi  28914  cnlnadjlem2  28927  cnlnadjlem7  28932  nmopcoadji  28960  leopnmid  28997  bhmafibid1  29644  sqsscirc2  29955  subfaclim  31170  subfacval3  31171  sinccvglem  31566  dnicld1  32462  dnibndlem2  32469  dnibndlem6  32473  dnibndlem9  32476  dnibndlem12  32479  dnicn  32482  knoppcnlem4  32486  knoppcnlem6  32488  unblimceq0lem  32497  unblimceq0  32498  unbdqndv2lem1  32500  unbdqndv2lem2  32501  knoppndvlem11  32513  knoppndvlem12  32514  knoppndvlem14  32516  knoppndvlem15  32517  knoppndvlem17  32519  knoppndvlem18  32520  knoppndvlem20  32522  knoppndvlem21  32523  poimirlem29  33438  poimir  33442  iblabsnclem  33473  iblabsnc  33474  iblmulc2nc  33475  itgabsnc  33479  bddiblnc  33480  ftc1cnnclem  33483  ftc1anclem1  33485  ftc1anclem2  33486  ftc1anclem4  33488  ftc1anclem5  33489  ftc1anclem6  33490  ftc1anclem7  33491  ftc1anclem8  33492  ftc1anc  33493  ftc2nc  33494  dvasin  33496  areacirclem1  33500  areacirclem2  33501  areacirclem4  33503  areacirclem5  33504  areacirc  33505  geomcau  33555  cntotbnd  33595  rrndstprj1  33629  rrndstprj2  33630  ismrer1  33637  rencldnfilem  37384  irrapxlem2  37387  irrapxlem4  37389  irrapxlem5  37390  pellexlem2  37394  pellexlem6  37398  pell14qrgt0  37423  congabseq  37541  acongeq  37550  modabsdifz  37553  jm2.26lem3  37568  extoimad  38464  imo72b2lem0  38465  imo72b2  38475  dvgrat  38511  cvgdvgrat  38512  radcnvrat  38513  dvconstbi  38533  binomcxplemnotnn0  38555  dstregt0  39493  absnpncan2d  39516  absnpncan3d  39521  abslt2sqd  39576  rexabslelem  39645  fprodabs2  39827  mullimc  39848  mullimcf  39855  limcrecl  39861  lptre2pt  39872  limcleqr  39876  addlimc  39880  0ellimcdiv  39881  limclner  39883  climleltrp  39908  climisp  39978  climxrrelem  39981  cnrefiisplem  40055  climxlim2lem  40071  cncficcgt0  40101  dvdivbd  40138  dvbdfbdioolem1  40143  dvbdfbdioolem2  40144  dvbdfbdioo  40145  ioodvbdlimc1lem1  40146  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  stoweid  40280  fourierdlem30  40354  fourierdlem39  40363  fourierdlem42  40366  fourierdlem47  40370  fourierdlem68  40391  fourierdlem70  40393  fourierdlem71  40394  fourierdlem73  40396  fourierdlem77  40400  fourierdlem80  40403  fourierdlem83  40406  fourierdlem87  40410  fourierdlem103  40426  fourierdlem104  40427  etransclem23  40474  etransclem48  40499  rrndistlt  40510  ioorrnopnlem  40524  sge0isum  40644  hoicvr  40762  smflimlem4  40982  smfmullem1  40998  smfmullem2  40999  smfmullem3  41000