Theorem divdird 11978

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106   ≠ wne 2939  (class class class)co 7362  ℂcc 11058  0cc0 11060   + caddc 11063   / cdiv 11821

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 2702  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-resscn 11117  ax-1cn 11118  ax-icn 11119  ax-addcl 11120  ax-addrcl 11121  ax-mulcl 11122  ax-mulrcl 11123  ax-mulcom 11124  ax-addass 11125  ax-mulass 11126  ax-distr 11127  ax-i2m1 11128  ax-1ne0 11129  ax-1rid 11130  ax-rnegex 11131  ax-rrecex 11132  ax-cnre 11133  ax-pre-lttri 11134  ax-pre-lttrn 11135  ax-pre-ltadd 11136  ax-pre-mulgt0 11137

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 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3448  df-sbc 3743  df-csb 3859  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-po 5550  df-so 5551  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-er 8655  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11200  df-mnf 11201  df-xr 11202  df-ltxr 11203  df-le 11204  df-sub 11396  df-neg 11397  df-div 11822

This theorem is referenced by:  zesq  14139  sqreulem  15256  bitsp1o  16324  bitsmod  16327  lcmgcdlem  16493  pythagtriplem19  16716  fldivp1  16780  mul4sqlem  16836  4sqlem17  16844  metnrmlem3  24261  pcoass  24424  ovollb2lem  24889  opnmbllem  25002  dvaddbr  25339  dvmulbr  25340  ftc1lem4  25440  vieta1lem2  25708  cosargd  26000  tanarg  26011  cxpaddle  26142  cxpeq  26147  dcubic1lem  26230  dcubic2  26231  mcubic  26234  cubic2  26235  dquartlem1  26238  dquart  26240  cosatan  26308  atantan  26310  dvatan  26322  jensenlem2  26374  logdifbnd  26380  emcllem3  26384  emcllem5  26386  dmgmdivn0  26414  lgamgulmlem2  26416  lgamgulmlem5  26419  lgamcvg2  26441  lgam1  26450  basellem3  26469  basellem8  26474  perfectlem2  26615  bclbnd  26665  lgseisenlem1  26760  lgsquad2lem1  26769  dchrvmasum2if  26882  selberg3  26944  selberg4  26946  selberg34r  26956  pntrlog2bndlem2  26963  pntrlog2bndlem4  26965  pntrlog2bndlem5  26966  pntrlog2bndlem6  26968  pntibndlem2  26976  brbtwn2  27917  axsegconlem10  27938  axeuclidlem  27974  axcontlem8  27983  dya2icoseg  32966  divcnvlin  34391  iprodgam  34401  knoppndvlem9  35059  bj-bary1lem  35854  bj-bary1  35856  poimirlem29  36180  opnmbllem0  36187  dvtan  36201  ftc1cnnclem  36222  dvasin  36235  areacirclem1  36239  aks4d1p1p2  40600  aks4d1p1p4  40601  aks4d1p1p7  40604  fltdiv  41032  flt4lem6  41054  3cubeslem4  41070  reglogmul  41274  binomcxplemwb  42750  clim1fr1  43962  coseq0  44225  stirlinglem4  44438  stirlinglem6  44440  dirkerper  44457  dirkertrigeqlem3  44461  dirkercncflem1  44464  dirkercncflem2  44465  fourierdlem4  44472  fourierdlem26  44494  fourierdlem42  44510  fourierdlem83  44550  fourierdlem112  44579  sqwvfourb  44590  etransclem44  44639  quad1  45932  requad1  45934  perfectALTVlem2  46034  eenglngeehlnmlem1  46943  line2  46958  itsclc0xyqsolr  46975  itsclquadb  46982  cotsqcscsq  47327