Theorem divassd 11965

Description: An associative law for division. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

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

Assertion

Ref	Expression
divassd	⊢ (𝜑 → ((𝐴 · 𝐵) / 𝐶) = (𝐴 · (𝐵 / 𝐶)))

Proof of Theorem divassd

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106   ≠ wne 2943  (class class class)co 7356  ℂcc 11048  0cc0 11050   · cmul 11055   / cdiv 11811

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 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7671  ax-resscn 11107  ax-1cn 11108  ax-icn 11109  ax-addcl 11110  ax-addrcl 11111  ax-mulcl 11112  ax-mulrcl 11113  ax-mulcom 11114  ax-addass 11115  ax-mulass 11116  ax-distr 11117  ax-i2m1 11118  ax-1ne0 11119  ax-1rid 11120  ax-rnegex 11121  ax-rrecex 11122  ax-cnre 11123  ax-pre-lttri 11124  ax-pre-lttrn 11125  ax-pre-ltadd 11126  ax-pre-mulgt0 11127

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 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-po 5545  df-so 5546  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7312  df-ov 7359  df-oprab 7360  df-mpo 7361  df-er 8647  df-en 8883  df-dom 8884  df-sdom 8885  df-pnf 11190  df-mnf 11191  df-xr 11192  df-ltxr 11193  df-le 11194  df-sub 11386  df-neg 11387  df-div 11812

This theorem is referenced by:  zesq  14128  discr  14142  crre  14998  abs1m  15219  sqreulem  15243  o1rlimmul  15500  geoisum1c  15764  mertenslem1  15768  eftlub  15990  lcmgcdlem  16481  cncongr2  16543  isprm5  16582  pcaddlem  16759  pockthlem  16776  mul4sqlem  16824  4sqlem17  16832  odadd1  19624  nmoleub3  24480  ipcau2  24596  pjthlem1  24799  dvrec  25317  plyeq0lem  25569  aareccl  25684  dvradcnv  25778  abelthlem7  25795  tangtx  25860  tanarg  25972  logcnlem4  25998  mcubic  26195  cubic2  26196  dquart  26201  quart1lem  26203  quart1  26204  tanatan  26267  atantan  26271  dvatan  26283  atantayl  26285  log2cnv  26292  lgamgulmlem4  26379  basellem3  26430  perfectlem2  26576  bposlem1  26630  bposlem2  26631  lgsquad2lem1  26730  chebbnd1lem2  26816  selberg3lem1  26903  selberg4lem1  26906  selberg4  26907  selberg4r  26916  pntrlog2bndlem2  26924  pntrlog2bndlem3  26925  pntrlog2bndlem4  26926  pntrlog2bndlem5  26927  pntrlog2bndlem6  26929  pntibndlem2  26937  pntlemo  26953  ostth2lem3  26981  axeuclidlem  27909  pjhthlem1  30331  signsplypnf  33153  hgt750leme  33262  subfaclim  33773  circum  34253  faclimlem1  34307  faclimlem3  34309  knoppndvlem2  34967  knoppndvlem7  34972  knoppndvlem17  34982  itg2addnclem  36120  dvasin  36153  areacirclem1  36157  lcmineqlem11  40487  lcmineqlem18  40494  dvrelogpow2b  40516  aks4d1p1p7  40522  pellexlem6  41135  reglogexp  41195  sqrtcval  41895  binomcxplemwb  42610  binomcxplemnotnn0  42618  0ellimcdiv  43862  stoweidlem1  44214  wallispilem4  44281  stirlinglem3  44289  stirlinglem4  44290  stirlinglem7  44293  dirkertrigeq  44314  dirkercncflem2  44317  fourierdlem30  44350  fourierdlem83  44402  elaa2lem  44446  etransclem23  44470  etransclem24  44471  etransclem44  44491  etransclem45  44492  perfectALTVlem2  45886  itscnhlc0xyqsol  46823  itsclc0xyqsolr  46827  itsclquadb  46834