Theorem divsubdird 12025

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106   ≠ wne 2940  (class class class)co 7405  ℂcc 11104  0cc0 11106   − cmin 11440   / cdiv 11867

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-po 5587  df-so 5588  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868

This theorem is referenced by:  xov1plusxeqvd  13471  discr  14199  crre  15057  reccn2  15537  iseralt  15627  trireciplem  15804  geolim  15812  geolim2  15813  georeclim  15814  bpolydiflem  15994  bitsinv1lem  16378  fldivp1  16826  mul4sqlem  16882  lebnumii  24473  dyadovol  25101  mbfi1fseqlem6  25229  dvmptdiv  25482  dveflem  25487  dvsincos  25489  dvlip  25501  ulmdvlem1  25903  efeq1  26028  tanarg  26118  logcnlem4  26144  ang180lem1  26303  angpieqvdlem  26322  chordthmlem2  26327  chordthmlem4  26329  dcubic1lem  26337  dcubic2  26338  mcubic  26341  cubic2  26342  dquartlem1  26345  dquartlem2  26346  dquart  26347  2efiatan  26412  tanatan  26413  atantan  26417  dvatan  26429  atantayl  26431  atantayl2  26432  birthdaylem2  26446  jensenlem2  26481  logdiflbnd  26488  emcllem2  26490  lgamgulmlem2  26523  basellem8  26581  lgseisenlem1  26867  lgsquadlem2  26873  vmalogdivsum2  27030  vmalogdivsum  27031  2vmadivsumlem  27032  selberg3lem1  27049  selberg4lem1  27052  selberg4  27053  pntrmax  27056  pntrsumo1  27057  selberg3r  27061  selberg4r  27062  selberg34r  27063  pntrlog2bndlem4  27072  pntpbnd2  27079  pntibndlem2  27083  pntlemo  27099  pntlem3  27101  brbtwn2  28152  axsegconlem9  28172  axsegconlem10  28173  axpaschlem  28187  axcontlem8  28218  dya2icoseg  33264  itg2addnclem  36527  pellexlem2  41553  pellexlem6  41557  areaquad  41950  sqrtcval  42377  hashnzfzclim  43066  binomcxplemrat  43094  oddfl  43973  sumnnodd  44332  itgcoscmulx  44671  itgsincmulx  44676  stirlinglem1  44776  stirlinglem6  44781  dirkercncflem1  44805  fourierdlem26  44835  fourierdlem30  44839  fourierdlem65  44873  quad1  46274  requad1  46276  1subrec1sub  47344  eenglngeehlnmlem1  47376  eenglngeehlnmlem2  47377  itscnhlc0xyqsol  47404