Theorem divsubdird 11996

Description: Distribution of division over subtraction. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
div1d.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
divcld.2	⊢ (𝜑 → 𝐵 ∈ ℂ)
divmuld.3	⊢ (𝜑 → 𝐶 ∈ ℂ)
divassd.4	⊢ (𝜑 → 𝐶 ≠ 0)

Assertion

Ref	Expression
divsubdird	⊢ (𝜑 → ((𝐴 − 𝐵) / 𝐶) = ((𝐴 / 𝐶) − (𝐵 / 𝐶)))

Proof of Theorem divsubdird

Step	Hyp	Ref	Expression
1		div1d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		divcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		divmuld.3	. 2 ⊢ (𝜑 → 𝐶 ∈ ℂ)
4		divassd.4	. 2 ⊢ (𝜑 → 𝐶 ≠ 0)
5		divsubdir 11874	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 − 𝐵) / 𝐶) = ((𝐴 / 𝐶) − (𝐵 / 𝐶)))
6	1, 2, 3, 4, 5	syl112anc 1389	1 ⊢ (𝜑 → ((𝐴 − 𝐵) / 𝐶) = ((𝐴 / 𝐶) − (𝐵 / 𝐶)))

Syntax hints:   → wi 4   = wceq 1554   ∈ wcel 2136   ≠ wne 2951  (class class class)co 7385  ℂcc 11061  0cc0 11063   − cmin 11404   / cdiv 11834

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-10 2169  ax-11 2185  ax-12 2206  ax-ext 2728  ax-sep 5240  ax-nul 5250  ax-pow 5316  ax-pr 5384  ax-un 7707  ax-resscn 11120  ax-1cn 11121  ax-icn 11122  ax-addcl 11123  ax-addrcl 11124  ax-mulcl 11125  ax-mulrcl 11126  ax-mulcom 11127  ax-addass 11128  ax-mulass 11129  ax-distr 11130  ax-i2m1 11131  ax-1ne0 11132  ax-1rid 11133  ax-rnegex 11134  ax-rrecex 11135  ax-cnre 11136  ax-pre-lttri 11137  ax-pre-lttrn 11138  ax-pre-ltadd 11139  ax-pre-mulgt0 11140

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3or 1096  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-nf 1798  df-sb 2085  df-mo 2560  df-eu 2590  df-clab 2735  df-cleq 2748  df-clel 2831  df-nfc 2905  df-ne 2952  df-nel 3056  df-ral 3071  df-rex 3081  df-rmo 3361  df-reu 3362  df-rab 3409  df-v 3450  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4281  df-if 4475  df-pw 4551  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5095  df-opab 5157  df-mpt 5176  df-id 5535  df-po 5548  df-so 5549  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-rn 5651  df-res 5652  df-ima 5653  df-iota 6466  df-fun 6512  df-fn 6513  df-f 6514  df-f1 6515  df-fo 6516  df-f1o 6517  df-fv 6518  df-riota 7342  df-ov 7388  df-oprab 7389  df-mpo 7390  df-er 8666  df-en 8917  df-dom 8918  df-sdom 8919  df-pnf 11208  df-mnf 11209  df-xr 11210  df-ltxr 11211  df-le 11212  df-sub 11406  df-neg 11407  df-div 11835

This theorem is referenced by:  xov1plusxeqvd  13492  discr  14243  crre  15117  reccn2  15600  iseralt  15688  trireciplem  15868  geolim  15876  geolim2  15877  georeclim  15878  bpolydiflem  16060  bitsinv1lem  16451  fldivp1  16909  mul4sqlem  16965  lebnumii  25001  dyadovol  25628  mbfi1fseqlem6  25755  dvmptdiv  26009  dveflem  26014  dvsincos  26016  dvlip  26028  ulmdvlem1  26433  efeq1  26563  tanarg  26654  logcnlem4  26680  ang180lem1  26844  angpieqvdlem  26863  chordthmlem2  26868  chordthmlem4  26870  dcubic1lem  26878  dcubic2  26879  mcubic  26882  cubic2  26883  dquartlem1  26886  dquartlem2  26887  dquart  26888  2efiatan  26953  tanatan  26954  atantan  26958  dvatan  26970  atantayl  26972  atantayl2  26973  birthdaylem2  26987  jensenlem2  27022  logdiflbnd  27029  emcllem2  27031  lgamgulmlem2  27064  basellem8  27122  lgseisenlem1  27409  lgsquadlem2  27415  vmalogdivsum2  27572  vmalogdivsum  27573  2vmadivsumlem  27574  selberg3lem1  27591  selberg4lem1  27594  selberg4  27595  pntrmax  27598  pntrsumo1  27599  selberg3r  27603  selberg4r  27604  selberg34r  27605  pntrlog2bndlem4  27614  pntpbnd2  27621  pntibndlem2  27625  pntlemo  27641  pntlem3  27643  brbtwn2  29045  axsegconlem9  29065  axsegconlem10  29066  axpaschlem  29080  axcontlem8  29111  constrrtcclem  33985  dya2icoseg  34528  itg2addnclem  38118  pellexlem2  43355  pellexlem6  43359  areaquad  43741  sqrtcval  44165  hashnzfzclim  44846  binomcxplemrat  44874  oddfl  45805  sumnnodd  46154  itgcoscmulx  46491  itgsincmulx  46496  stirlinglem1  46596  stirlinglem6  46601  dirkercncflem1  46625  fourierdlem26  46655  fourierdlem30  46659  fourierdlem65  46693  ppivalnnprm  48182  quad1  48190  requad1  48192  1subrec1sub  49275  eenglngeehlnmlem1  49307  eenglngeehlnmlem2  49308  itscnhlc0xyqsol  49335