Theorem subdid 11698

Description: Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
mulm1d.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
mulnegd.2	⊢ (𝜑 → 𝐵 ∈ ℂ)
subdid.3	⊢ (𝜑 → 𝐶 ∈ ℂ)

Assertion

Ref	Expression
subdid	⊢ (𝜑 → (𝐴 · (𝐵 − 𝐶)) = ((𝐴 · 𝐵) − (𝐴 · 𝐶)))

Proof of Theorem subdid

Step	Hyp	Ref	Expression
1		mulm1d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		mulnegd.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		subdid.3	. 2 ⊢ (𝜑 → 𝐶 ∈ ℂ)
4		subdi 11675	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 − 𝐶)) = ((𝐴 · 𝐵) − (𝐴 · 𝐶)))
5	1, 2, 3, 4	syl3anc 1398	1 ⊢ (𝜑 → (𝐴 · (𝐵 − 𝐶)) = ((𝐴 · 𝐵) − (𝐴 · 𝐶)))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  (class class class)co 7417  ℂcc 11126   · cmul 11133   − cmin 11469

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 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7740  ax-resscn 11185  ax-1cn 11186  ax-icn 11187  ax-addcl 11188  ax-addrcl 11189  ax-mulcl 11190  ax-mulrcl 11191  ax-mulcom 11192  ax-addass 11193  ax-mulass 11194  ax-distr 11195  ax-i2m1 11196  ax-1ne0 11197  ax-1rid 11198  ax-rnegex 11199  ax-rrecex 11200  ax-cnre 11201  ax-pre-lttri 11202  ax-pre-lttrn 11203  ax-pre-ltadd 11204

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 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-po 5567  df-so 5568  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  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 7374  df-ov 7420  df-oprab 7421  df-mpo 7422  df-er 8700  df-en 8957  df-dom 8958  df-sdom 8959  df-pnf 11273  df-mnf 11274  df-ltxr 11276  df-sub 11471

This theorem is used by:  muls1d  11702  addmulsub  11704  recextlem1  11872  cru  12238  cju  12242  zneo  12708  qbtwnre  13255  lincmb01cmp  13552  iccf1o  13553  intfracq  13924  modlt  13945  moddi  14007  modsubdir  14008  subsq  14278  expmulnbnd  14303  crre  15205  remullem  15219  mulcn2  15687  iseraltlem3  15775  fsumparts  15897  geoserg  15959  mertens  15979  bpolydiflem  16146  bpoly4  16151  fsumcube  16152  tanval3  16228  tanadd  16261  eirrlem  16298  bezoutlem3  16637  cncongr1  16763  eulerthlem2  16879  prmdiv  16882  prmdiveq  16883  4sqlem10  17045  mul4sqlem  17051  4sqlem17  17059  blcvx  25030  icopnfhmeo  25177  pcoass  25258  cphipval  25477  pjthlem1  25671  itgmulc2lem2  26067  dvmulbr  26173  cmvth  26225  dvcvx  26254  dvfsumle  26255  dvfsumabs  26257  dvfsumlem2  26261  aaliou3lem8  26588  abelthlem2  26675  tangtx  26750  tanregt0  26784  efif1olem2  26788  efif1olem4  26790  ang180lem5  27058  isosctrlem2  27064  isosctrlem3  27065  affineequiv  27068  heron  27083  dcubic1  27090  dquart  27098  quartlem1  27102  asinsin  27137  efiatan  27157  atanlogsublem  27160  efiatan2  27162  2efiatan  27163  tanatan  27164  atantayl2  27183  lgamgulmlem2  27274  lgamgulmlem3  27275  ftalem5  27321  basellem3  27327  basellem5  27329  logfaclbnd  27466  lgseisenlem2  27620  lgsquadlem1  27624  2sqlem4  27665  2sqmod  27680  vmadivsum  27726  rplogsumlem1  27728  dchrmusum2  27738  dchrvmasumiflem2  27746  rpvmasum2  27756  dchrisum0lem2a  27761  dchrisum0lem2  27762  rplogsum  27771  mulogsumlem  27775  mulogsum  27776  mulog2sumlem1  27778  mulog2sumlem2  27779  mulog2sumlem3  27780  vmalogdivsum2  27782  vmalogdivsum  27783  2vmadivsumlem  27784  logsqvma  27786  selberglem1  27789  selberglem2  27790  selberg2lem  27794  chpdifbndlem1  27797  selberg3lem1  27801  selberg4lem1  27804  selberg4  27805  pntrsumo1  27809  selbergr  27812  selberg3r  27813  selberg4r  27814  selberg34r  27815  pntrlog2bndlem4  27824  pntrlog2bndlem5  27825  pntrlog2bndlem6  27827  pntlemo  27851  ttgcontlem1  29349  brbtwn2  29370  colinearalglem1  29371  axcontlem8  29436  pjhthlem1  31880  constrrtll  34249  constrrtlc1  34250  constrrtcclem  34252  constrremulcl  34285  constrrecl  34287  constrreinvcl  34290  cos9thpiminplylem1  34300  cos9thpiminplylem2  34301  knoppndvlem11  37227  knoppndvlem14  37230  knoppndvlem15  37231  knoppndvlem16  37232  bj-bary1lem  38070  bj-bary1lem1  38071  qdiff  38087  itgmulc2nclem2  38444  areacirclem1  38465  areacirclem4  38468  areacirc  38470  cntotbnd  38554  posbezout  42974  hashscontpow1  42995  nicomachus  43195  irrapxlem2  43672  irrapxlem3  43673  irrapxlem5  43675  pellexlem6  43683  pell1qrgaplem  43722  qirropth  43757  jm2.17a  43809  congmul  43816  jm2.18  43837  areaquad  44065  itgsinexp  46791  stoweidlem26  46862  stirlinglem7  46916  fourierdlem83  47025  etransclem46  47116  smfmullem1  47627  sin3t  47743  cos3t  47744  sin5tlem4  47748  cos5t  47751  fmtnorec3  48459  fmtnorec4  48460  fppr2odd  48655  itcovalt2lem2lem2  49612  submuladdmuld  49639  affinecomb2  49641  itsclc0yqsollem1  49700  itsclc0yqsol  49702  itscnhlc0xyqsol  49703  itsclc0xyqsolr  49707  2itscplem3  49718  itscnhlinecirc02plem1  49720  crosspdotd  50806  crossp3d  50808