Theorem absmuld 14806

Description: Absolute value distributes over multiplication. Proposition 10-3.7(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)

Hypotheses

Ref	Expression
abscld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
abssubd.2	⊢ (𝜑 → 𝐵 ∈ ℂ)

Assertion

Ref	Expression
absmuld	⊢ (𝜑 → (abs‘(𝐴 · 𝐵)) = ((abs‘𝐴) · (abs‘𝐵)))

Proof of Theorem absmuld

Step	Hyp	Ref	Expression
1		abscld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		abssubd.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		absmul 14646	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (abs‘(𝐴 · 𝐵)) = ((abs‘𝐴) · (abs‘𝐵)))
4	1, 2, 3	syl2anc 587	1 ⊢ (𝜑 → (abs‘(𝐴 · 𝐵)) = ((abs‘𝐴) · (abs‘𝐵)))

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  ‘cfv 6324  (class class class)co 7135  ℂcc 10524   · cmul 10531  abscabs 14585

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604

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 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-om 7561  df-2nd 7672  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-er 8272  df-en 8493  df-dom 8494  df-sdom 8495  df-sup 8890  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11626  df-2 11688  df-3 11689  df-n0 11886  df-z 11970  df-uz 12232  df-rp 12378  df-seq 13365  df-exp 13426  df-cj 14450  df-re 14451  df-im 14452  df-sqrt 14586  df-abs 14587

This theorem is referenced by:  bhmafibid1  14817  mulcn2  14944  reccn2  14945  o1mul  14963  o1rlimmul  14967  iseraltlem3  15032  geomulcvg  15224  mertenslem1  15232  fprodabs  15320  absef  15542  efieq1re  15544  lcmgcd  15941  lcmid  15943  mulgcddvds  15989  prmirredlem  20186  blcvx  23403  iblmulc2  24434  itgabs  24438  bddmulibl  24442  dveflem  24582  dvlip  24596  dvlipcn  24597  plyeq0lem  24807  aalioulem4  24931  radcnvlem1  25008  dvradcnv  25016  pserulm  25017  abelthlem5  25030  abelthlem7  25033  abslogle  25209  logtayllem  25250  abscxpbnd  25342  chordthmlem4  25421  divsqrtsumo1  25569  lgamgulmlem2  25615  lgamgulmlem3  25616  lgamgulmlem5  25618  ftalem1  25658  ftalem2  25659  ftalem5  25662  logexprlim  25809  lgsdilem2  25917  2sqlem3  26004  dchrisumlem2  26074  dchrmusum2  26078  dchrvmasumlem3  26083  dchrvmasumiflem1  26085  dchrisum0lem2a  26101  dchrisum0lem2  26102  mudivsum  26114  mulogsumlem  26115  mulog2sumlem1  26118  mulog2sumlem2  26119  2vmadivsumlem  26124  selberglem2  26130  selberg3lem1  26141  selberg4lem1  26144  pntrlog2bndlem1  26161  pntrlog2bndlem3  26163  pntibndlem2  26175  pntlemn  26184  pntlemj  26187  nmbdfnlbi  29832  nmcfnlbi  29835  cnzh  31321  rezh  31322  subfaclim  32548  knoppcnlem4  33948  knoppndvlem11  33974  knoppndvlem14  33977  iblmulc2nc  35122  itgabsnc  35126  cntotbnd  35234  irrapxlem2  39764  irrapxlem5  39767  pellexlem2  39771  absmulrposd  40862  imo72b2lem0  40869  radcnvrat  41018  fprodabs2  42237  dvdivbd  42565  dvbdfbdioolem1  42570  fourierdlem30  42779  fourierdlem39  42788  fourierdlem47  42795  fourierdlem68  42816  fourierdlem73  42821  fourierdlem77  42825  fourierdlem87  42835  etransclem23  42899  smfmullem1  43423