MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  divass Structured version   Visualization version   GIF version

Theorem divass 11521
Description: An associative law for division. (Contributed by NM, 2-Aug-2004.)
Assertion
Ref Expression
divass ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 · 𝐵) / 𝐶) = (𝐴 · (𝐵 / 𝐶)))

Proof of Theorem divass
StepHypRef Expression
1 reccl 11510 . . 3 ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) → (1 / 𝐶) ∈ ℂ)
2 mulass 10830 . . 3 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (1 / 𝐶) ∈ ℂ) → ((𝐴 · 𝐵) · (1 / 𝐶)) = (𝐴 · (𝐵 · (1 / 𝐶))))
31, 2syl3an3 1167 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 · 𝐵) · (1 / 𝐶)) = (𝐴 · (𝐵 · (1 / 𝐶))))
4 mulcl 10826 . . . 4 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
543adant3 1134 . . 3 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → (𝐴 · 𝐵) ∈ ℂ)
6 simp3l 1203 . . 3 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → 𝐶 ∈ ℂ)
7 simp3r 1204 . . 3 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → 𝐶 ≠ 0)
8 divrec 11519 . . 3 (((𝐴 · 𝐵) ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) → ((𝐴 · 𝐵) / 𝐶) = ((𝐴 · 𝐵) · (1 / 𝐶)))
95, 6, 7, 8syl3anc 1373 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 · 𝐵) / 𝐶) = ((𝐴 · 𝐵) · (1 / 𝐶)))
10 simp2 1139 . . . 4 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → 𝐵 ∈ ℂ)
11 divrec 11519 . . . 4 ((𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) → (𝐵 / 𝐶) = (𝐵 · (1 / 𝐶)))
1210, 6, 7, 11syl3anc 1373 . . 3 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → (𝐵 / 𝐶) = (𝐵 · (1 / 𝐶)))
1312oveq2d 7238 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → (𝐴 · (𝐵 / 𝐶)) = (𝐴 · (𝐵 · (1 / 𝐶))))
143, 9, 133eqtr4d 2788 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 · 𝐵) / 𝐶) = (𝐴 · (𝐵 / 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1089   = wceq 1543  wcel 2111  wne 2941  (class class class)co 7222  cc 10740  0cc0 10742  1c1 10743   · cmul 10747   / cdiv 11502
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-sep 5201  ax-nul 5208  ax-pow 5267  ax-pr 5331  ax-un 7532  ax-resscn 10799  ax-1cn 10800  ax-icn 10801  ax-addcl 10802  ax-addrcl 10803  ax-mulcl 10804  ax-mulrcl 10805  ax-mulcom 10806  ax-addass 10807  ax-mulass 10808  ax-distr 10809  ax-i2m1 10810  ax-1ne0 10811  ax-1rid 10812  ax-rnegex 10813  ax-rrecex 10814  ax-cnre 10815  ax-pre-lttri 10816  ax-pre-lttrn 10817  ax-pre-ltadd 10818  ax-pre-mulgt0 10819
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3067  df-rex 3068  df-reu 3069  df-rmo 3070  df-rab 3071  df-v 3417  df-sbc 3704  df-csb 3821  df-dif 3878  df-un 3880  df-in 3882  df-ss 3892  df-nul 4247  df-if 4449  df-pw 4524  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4829  df-br 5063  df-opab 5125  df-mpt 5145  df-id 5464  df-po 5477  df-so 5478  df-xp 5566  df-rel 5567  df-cnv 5568  df-co 5569  df-dm 5570  df-rn 5571  df-res 5572  df-ima 5573  df-iota 6347  df-fun 6391  df-fn 6392  df-f 6393  df-f1 6394  df-fo 6395  df-f1o 6396  df-fv 6397  df-riota 7179  df-ov 7225  df-oprab 7226  df-mpo 7227  df-er 8400  df-en 8636  df-dom 8637  df-sdom 8638  df-pnf 10882  df-mnf 10883  df-xr 10884  df-ltxr 10885  df-le 10886  df-sub 11077  df-neg 11078  df-div 11503
This theorem is referenced by:  div23  11522  div32  11523  divmulass  11526  divmulasscom  11527  divasszi  11595  divassd  11656  lt2mul2div  11723  zdivmul  12262  mertenslem1  15461  efi4p  15711  mulsucdiv2z  15927  relogbreexp  25671  divsqrtsumlem  25875  basellem8  25983  logexprlim  26119  bposlem6  26183  lgsquadlem2  26275  chebbnd1lem3  26365  vmadivsum  26376  dchrmusum2  26388  dchrisum0lem1b  26409  dchrisum0lem2  26412  mudivsum  26424  mulog2sumlem2  26429  selberglem1  26439  selberglem2  26440  pntlemb  26491  pntlemr  26496  pntlemj  26497  pntlemf  26499  pntlemk  26500  pntlemo  26501  dvasin  35611  stoweidlem24  43255
  Copyright terms: Public domain W3C validator