Theorem divsubdird 12102

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 11980	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 − 𝐵) / 𝐶) = ((𝐴 / 𝐶) − (𝐵 / 𝐶)))
6	1, 2, 3, 4, 5	syl112anc 1401	1 ⊢ (𝜑 → ((𝐴 − 𝐵) / 𝐶) = ((𝐴 / 𝐶) − (𝐵 / 𝐶)))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145   ≠ wne 2955  (class class class)co 7408  ℂcc 11170  0cc0 11172   − cmin 11513   / cdiv 11943

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 2213  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7734  ax-resscn 11229  ax-1cn 11230  ax-icn 11231  ax-addcl 11232  ax-addrcl 11233  ax-mulcl 11234  ax-mulrcl 11235  ax-mulcom 11236  ax-addass 11237  ax-mulass 11238  ax-distr 11239  ax-i2m1 11240  ax-1ne0 11241  ax-1rid 11242  ax-rnegex 11243  ax-rrecex 11244  ax-cnre 11245  ax-pre-lttri 11246  ax-pre-lttrn 11247  ax-pre-ltadd 11248  ax-pre-mulgt0 11249

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5542  df-po 5555  df-so 5556  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6483  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535  df-riota 7365  df-ov 7411  df-oprab 7412  df-mpo 7413  df-er 8695  df-en 8952  df-dom 8953  df-sdom 8954  df-pnf 11317  df-mnf 11318  df-xr 11319  df-ltxr 11320  df-le 11321  df-sub 11515  df-neg 11516  df-div 11944

This theorem is used by:  xov1plusxeqvd  13599  discr  14352  crre  15249  reccn2  15732  iseralt  15820  trireciplem  15999  geolim  16007  geolim2  16008  georeclim  16009  bpolydiflem  16188  bitsinv1lem  16579  fldivp1  17037  mul4sqlem  17093  lebnumii  25249  dyadovol  25876  mbfi1fseqlem6  26003  dvmptdiv  26256  dveflem  26261  dvsincos  26263  dvlip  26275  ulmdvlem1  26691  efeq1  26820  tanarg  26911  logcnlem4  26937  ang180lem1  27101  angpieqvdlem  27120  chordthmlem2  27125  chordthmlem4  27127  dcubic1lem  27135  dcubic2  27136  mcubic  27139  cubic2  27140  dquartlem1  27143  dquartlem2  27144  dquart  27145  2efiatan  27210  tanatan  27211  atantan  27215  dvatan  27227  atantayl  27229  atantayl2  27230  birthdaylem2  27244  jensenlem2  27279  logdiflbnd  27286  emcllem2  27288  lgamgulmlem2  27321  basellem8  27379  lgseisenlem1  27666  lgsquadlem2  27672  vmalogdivsum2  27829  vmalogdivsum  27830  2vmadivsumlem  27831  selberg3lem1  27848  selberg4lem1  27851  selberg4  27852  pntrmax  27855  pntrsumo1  27856  selberg3r  27860  selberg4r  27861  selberg34r  27862  pntrlog2bndlem4  27871  pntpbnd2  27878  pntibndlem2  27882  pntlemo  27898  pntlem3  27900  brbtwn2  29417  axsegconlem9  29437  axsegconlem10  29438  axpaschlem  29452  axcontlem8  29483  constrrtcclem  34300  dya2icoseg  34844  itg2addnclem  38509  pellexlem2  43775  pellexlem6  43779  areaquad  44161  sqrtcval  44585  hashnzfzclim  45250  binomcxplemrat  45278  oddfl  46215  sumnnodd  46564  itgcoscmulx  46901  itgsincmulx  46906  stirlinglem1  47006  stirlinglem6  47011  dirkercncflem1  47035  fourierdlem26  47065  fourierdlem30  47069  fourierdlem65  47103  ppivalnnprm  48632  quad1  48640  requad1  48642  1subrec1sub  49739  eenglngeehlnmlem1  49771  eenglngeehlnmlem2  49772  itscnhlc0xyqsol  49799