Theorem divdird 12054

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

Hypotheses

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

Assertion

Ref	Expression
divdird	⊢ (𝜑 → ((𝐴 + 𝐵) / 𝐶) = ((𝐴 / 𝐶) + (𝐵 / 𝐶)))

Proof of Theorem divdird

Step	Hyp	Ref	Expression
1		div1d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		divcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		divmuld.3	. 2 ⊢ (𝜑 → 𝐶 ∈ ℂ)
4		divassd.4	. 2 ⊢ (𝜑 → 𝐶 ≠ 0)
5		divdir 11922	. 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 7414  ℂcc 11123  0cc0 11125   + caddc 11128   / cdiv 11896

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 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7737  ax-resscn 11182  ax-1cn 11183  ax-icn 11184  ax-addcl 11185  ax-addrcl 11186  ax-mulcl 11187  ax-mulrcl 11188  ax-mulcom 11189  ax-addass 11190  ax-mulass 11191  ax-distr 11192  ax-i2m1 11193  ax-1ne0 11194  ax-1rid 11195  ax-rnegex 11196  ax-rrecex 11197  ax-cnre 11198  ax-pre-lttri 11199  ax-pre-lttrn 11200  ax-pre-ltadd 11201  ax-pre-mulgt0 11202

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 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-po 5563  df-so 5564  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7371  df-ov 7417  df-oprab 7418  df-mpo 7419  df-er 8697  df-en 8954  df-dom 8955  df-sdom 8956  df-pnf 11270  df-mnf 11271  df-xr 11272  df-ltxr 11273  df-le 11274  df-sub 11468  df-neg 11469  df-div 11897

This theorem is used by:  zesq  14291  sqreulem  15448  bitsp1o  16524  bitsmod  16527  lcmgcdlem  16697  pythagtriplem19  16926  fldivp1  16990  mul4sqlem  17046  4sqlem17  17054  metnrmlem3  25089  pcoass  25253  ovollb2lem  25717  opnmbllem  25830  dvaddbr  26166  dvmulbr  26167  ftc1lem4  26267  vieta1lem2  26544  cosargd  26846  tanarg  26857  cxpaddle  26990  cxpeq  26995  dcubic1lem  27081  dcubic2  27082  mcubic  27085  cubic2  27086  dquartlem1  27089  dquart  27091  cosatan  27159  atantan  27161  dvatan  27173  jensenlem2  27225  logdifbnd  27231  emcllem3  27235  emcllem5  27237  dmgmdivn0  27265  lgamgulmlem2  27267  lgamgulmlem5  27270  lgamcvg2  27292  lgam1  27301  basellem3  27320  basellem8  27325  perfectlem2  27467  bclbnd  27517  lgseisenlem1  27612  lgsquad2lem1  27621  dchrvmasum2if  27734  selberg3  27796  selberg4  27798  selberg34r  27808  pntrlog2bndlem2  27815  pntrlog2bndlem4  27817  pntrlog2bndlem5  27818  pntrlog2bndlem6  27820  pntibndlem2  27828  brbtwn2  29363  axsegconlem10  29384  axeuclidlem  29420  axcontlem8  29429  quad3d  33221  constrrtlc1  34243  constrresqrtcl  34288  dya2icoseg  34789  divcnvlin  36313  iprodgam  36322  knoppndvlem9  37218  bj-bary1lem  38063  bj-bary1  38065  poimirlem29  38399  opnmbllem0  38406  dvtan  38420  ftc1cnnclem  38441  dvasin  38454  areacirclem1  38458  aks4d1p1p2  42937  aks4d1p1p4  42938  aks4d1p1p7  42941  cxp112d  43217  cxp111d  43218  fltdiv  43483  flt4lem6  43505  3cubeslem4  43535  reglogmul  43735  binomcxplemwb  45173  clim1fr1  46432  coseq0  46693  stirlinglem4  46906  stirlinglem6  46908  dirkerper  46925  dirkertrigeqlem3  46929  dirkercncflem1  46932  dirkercncflem2  46933  fourierdlem4  46940  fourierdlem26  46962  fourierdlem42  46978  fourierdlem83  47018  fourierdlem112  47047  sqwvfourb  47058  etransclem44  47107  quad1  48537  requad1  48539  perfectALTVlem2  48639  eenglngeehlnmlem1  49668  line2  49683  itsclc0xyqsolr  49700  itsclquadb  49707  cotsqcscsq  50689