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

Theorem divdivdiv 10575
Description: Division of two ratios. Theorem I.15 of [Apostol] p. 18. (Contributed by NM, 2-Aug-2004.)
Assertion
Ref Expression
divdivdiv (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → ((𝐴 / 𝐵) / (𝐶 / 𝐷)) = ((𝐴 · 𝐷) / (𝐵 · 𝐶)))

Proof of Theorem divdivdiv
StepHypRef Expression
1 simprrl 799 . . . . . . 7 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → 𝐷 ∈ ℂ)
2 simprll 797 . . . . . . 7 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → 𝐶 ∈ ℂ)
3 simprlr 798 . . . . . . 7 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → 𝐶 ≠ 0)
4 divcl 10540 . . . . . . 7 ((𝐷 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) → (𝐷 / 𝐶) ∈ ℂ)
51, 2, 3, 4syl3anc 1317 . . . . . 6 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → (𝐷 / 𝐶) ∈ ℂ)
6 simpll 785 . . . . . . 7 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → 𝐴 ∈ ℂ)
7 simplrl 795 . . . . . . 7 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → 𝐵 ∈ ℂ)
8 simplrr 796 . . . . . . 7 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → 𝐵 ≠ 0)
9 divcl 10540 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) ∈ ℂ)
106, 7, 8, 9syl3anc 1317 . . . . . 6 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → (𝐴 / 𝐵) ∈ ℂ)
115, 10mulcomd 9917 . . . . 5 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → ((𝐷 / 𝐶) · (𝐴 / 𝐵)) = ((𝐴 / 𝐵) · (𝐷 / 𝐶)))
12 simplr 787 . . . . . 6 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0))
13 simprl 789 . . . . . 6 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0))
14 divmuldiv 10574 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝐷 ∈ ℂ) ∧ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0))) → ((𝐴 / 𝐵) · (𝐷 / 𝐶)) = ((𝐴 · 𝐷) / (𝐵 · 𝐶)))
156, 1, 12, 13, 14syl22anc 1318 . . . . 5 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → ((𝐴 / 𝐵) · (𝐷 / 𝐶)) = ((𝐴 · 𝐷) / (𝐵 · 𝐶)))
1611, 15eqtrd 2643 . . . 4 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → ((𝐷 / 𝐶) · (𝐴 / 𝐵)) = ((𝐴 · 𝐷) / (𝐵 · 𝐶)))
1716oveq2d 6543 . . 3 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → ((𝐶 / 𝐷) · ((𝐷 / 𝐶) · (𝐴 / 𝐵))) = ((𝐶 / 𝐷) · ((𝐴 · 𝐷) / (𝐵 · 𝐶))))
18 simprr 791 . . . . . . 7 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))
19 divmuldiv 10574 . . . . . . 7 (((𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ) ∧ ((𝐷 ∈ ℂ ∧ 𝐷 ≠ 0) ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0))) → ((𝐶 / 𝐷) · (𝐷 / 𝐶)) = ((𝐶 · 𝐷) / (𝐷 · 𝐶)))
202, 1, 18, 13, 19syl22anc 1318 . . . . . 6 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → ((𝐶 / 𝐷) · (𝐷 / 𝐶)) = ((𝐶 · 𝐷) / (𝐷 · 𝐶)))
212, 1mulcomd 9917 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → (𝐶 · 𝐷) = (𝐷 · 𝐶))
2221oveq1d 6542 . . . . . . 7 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → ((𝐶 · 𝐷) / (𝐷 · 𝐶)) = ((𝐷 · 𝐶) / (𝐷 · 𝐶)))
231, 2mulcld 9916 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → (𝐷 · 𝐶) ∈ ℂ)
24 simprrr 800 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → 𝐷 ≠ 0)
251, 2, 24, 3mulne0d 10528 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → (𝐷 · 𝐶) ≠ 0)
26 divid 10563 . . . . . . . 8 (((𝐷 · 𝐶) ∈ ℂ ∧ (𝐷 · 𝐶) ≠ 0) → ((𝐷 · 𝐶) / (𝐷 · 𝐶)) = 1)
2723, 25, 26syl2anc 690 . . . . . . 7 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → ((𝐷 · 𝐶) / (𝐷 · 𝐶)) = 1)
2822, 27eqtrd 2643 . . . . . 6 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → ((𝐶 · 𝐷) / (𝐷 · 𝐶)) = 1)
2920, 28eqtrd 2643 . . . . 5 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → ((𝐶 / 𝐷) · (𝐷 / 𝐶)) = 1)
3029oveq1d 6542 . . . 4 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → (((𝐶 / 𝐷) · (𝐷 / 𝐶)) · (𝐴 / 𝐵)) = (1 · (𝐴 / 𝐵)))
31 divcl 10540 . . . . . 6 ((𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0) → (𝐶 / 𝐷) ∈ ℂ)
322, 1, 24, 31syl3anc 1317 . . . . 5 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → (𝐶 / 𝐷) ∈ ℂ)
3332, 5, 10mulassd 9919 . . . 4 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → (((𝐶 / 𝐷) · (𝐷 / 𝐶)) · (𝐴 / 𝐵)) = ((𝐶 / 𝐷) · ((𝐷 / 𝐶) · (𝐴 / 𝐵))))
3410mulid2d 9914 . . . 4 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → (1 · (𝐴 / 𝐵)) = (𝐴 / 𝐵))
3530, 33, 343eqtr3d 2651 . . 3 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → ((𝐶 / 𝐷) · ((𝐷 / 𝐶) · (𝐴 / 𝐵))) = (𝐴 / 𝐵))
3617, 35eqtr3d 2645 . 2 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → ((𝐶 / 𝐷) · ((𝐴 · 𝐷) / (𝐵 · 𝐶))) = (𝐴 / 𝐵))
376, 1mulcld 9916 . . . 4 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → (𝐴 · 𝐷) ∈ ℂ)
387, 2mulcld 9916 . . . 4 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → (𝐵 · 𝐶) ∈ ℂ)
39 mulne0 10518 . . . . 5 (((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → (𝐵 · 𝐶) ≠ 0)
4039ad2ant2lr 779 . . . 4 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → (𝐵 · 𝐶) ≠ 0)
41 divcl 10540 . . . 4 (((𝐴 · 𝐷) ∈ ℂ ∧ (𝐵 · 𝐶) ∈ ℂ ∧ (𝐵 · 𝐶) ≠ 0) → ((𝐴 · 𝐷) / (𝐵 · 𝐶)) ∈ ℂ)
4237, 38, 40, 41syl3anc 1317 . . 3 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → ((𝐴 · 𝐷) / (𝐵 · 𝐶)) ∈ ℂ)
43 divne0 10546 . . . 4 (((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0)) → (𝐶 / 𝐷) ≠ 0)
4443adantl 480 . . 3 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → (𝐶 / 𝐷) ≠ 0)
45 divmul 10537 . . 3 (((𝐴 / 𝐵) ∈ ℂ ∧ ((𝐴 · 𝐷) / (𝐵 · 𝐶)) ∈ ℂ ∧ ((𝐶 / 𝐷) ∈ ℂ ∧ (𝐶 / 𝐷) ≠ 0)) → (((𝐴 / 𝐵) / (𝐶 / 𝐷)) = ((𝐴 · 𝐷) / (𝐵 · 𝐶)) ↔ ((𝐶 / 𝐷) · ((𝐴 · 𝐷) / (𝐵 · 𝐶))) = (𝐴 / 𝐵)))
4610, 42, 32, 44, 45syl112anc 1321 . 2 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → (((𝐴 / 𝐵) / (𝐶 / 𝐷)) = ((𝐴 · 𝐷) / (𝐵 · 𝐶)) ↔ ((𝐶 / 𝐷) · ((𝐴 · 𝐷) / (𝐵 · 𝐶))) = (𝐴 / 𝐵)))
4736, 46mpbird 245 1 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → ((𝐴 / 𝐵) / (𝐶 / 𝐷)) = ((𝐴 · 𝐷) / (𝐵 · 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  wcel 1976  wne 2779  (class class class)co 6527  cc 9790  0cc0 9792  1c1 9793   · cmul 9797   / cdiv 10533
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4943  df-po 4949  df-so 4950  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-er 7606  df-en 7819  df-dom 7820  df-sdom 7821  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-div 10534
This theorem is referenced by:  recdiv  10580  divcan7  10583  divdiv1  10585  divdiv2  10586  divdivdivi  10637  divdivdivd  10697  qreccl  11640  pnt2  25019
  Copyright terms: Public domain W3C validator