Metamath Proof Explorer

Theorem divdivdiv

Description: Division of two ratios. Theorem I.15 of Apostol p. 18. (Contributed by NM, 2-Aug-2004)

Ref Expression
Assertion divdivdiv ( ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( ( 𝐴 / 𝐵 ) / ( 𝐶 / 𝐷 ) ) = ( ( 𝐴 · 𝐷 ) / ( 𝐵 · 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 simprrl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → 𝐷 ∈ ℂ )
2 simprll ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → 𝐶 ∈ ℂ )
3 simprlr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → 𝐶 ≠ 0 )
4 divcl ⊢ ( ( 𝐷 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) → ( 𝐷 / 𝐶 ) ∈ ℂ )
5 1 2 3 4 syl3anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( 𝐷 / 𝐶 ) ∈ ℂ )
6 simpll ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → 𝐴 ∈ ℂ )
7 simplrl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → 𝐵 ∈ ℂ )
8 simplrr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → 𝐵 ≠ 0 )
9 divcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( 𝐴 / 𝐵 ) ∈ ℂ )
10 6 7 8 9 syl3anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( 𝐴 / 𝐵 ) ∈ ℂ )
11 5 10 mulcomd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( ( 𝐷 / 𝐶 ) · ( 𝐴 / 𝐵 ) ) = ( ( 𝐴 / 𝐵 ) · ( 𝐷 / 𝐶 ) ) )
12 simplr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
13 simprl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) )
14 divmuldiv ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) ) → ( ( 𝐴 / 𝐵 ) · ( 𝐷 / 𝐶 ) ) = ( ( 𝐴 · 𝐷 ) / ( 𝐵 · 𝐶 ) ) )
15 6 1 12 13 14 syl22anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( ( 𝐴 / 𝐵 ) · ( 𝐷 / 𝐶 ) ) = ( ( 𝐴 · 𝐷 ) / ( 𝐵 · 𝐶 ) ) )
16 11 15 eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( ( 𝐷 / 𝐶 ) · ( 𝐴 / 𝐵 ) ) = ( ( 𝐴 · 𝐷 ) / ( 𝐵 · 𝐶 ) ) )
17 16 oveq2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( ( 𝐶 / 𝐷 ) · ( ( 𝐷 / 𝐶 ) · ( 𝐴 / 𝐵 ) ) ) = ( ( 𝐶 / 𝐷 ) · ( ( 𝐴 · 𝐷 ) / ( 𝐵 · 𝐶 ) ) ) )
18 simprr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) )
19 divmuldiv ⊢ ( ( ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) ) → ( ( 𝐶 / 𝐷 ) · ( 𝐷 / 𝐶 ) ) = ( ( 𝐶 · 𝐷 ) / ( 𝐷 · 𝐶 ) ) )
20 2 1 18 13 19 syl22anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( ( 𝐶 / 𝐷 ) · ( 𝐷 / 𝐶 ) ) = ( ( 𝐶 · 𝐷 ) / ( 𝐷 · 𝐶 ) ) )
21 2 1 mulcomd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( 𝐶 · 𝐷 ) = ( 𝐷 · 𝐶 ) )
22 21 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( ( 𝐶 · 𝐷 ) / ( 𝐷 · 𝐶 ) ) = ( ( 𝐷 · 𝐶 ) / ( 𝐷 · 𝐶 ) ) )
23 1 2 mulcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( 𝐷 · 𝐶 ) ∈ ℂ )
24 simprrr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → 𝐷 ≠ 0 )
25 1 2 24 3 mulne0d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( 𝐷 · 𝐶 ) ≠ 0 )
26 divid ⊢ ( ( ( 𝐷 · 𝐶 ) ∈ ℂ ∧ ( 𝐷 · 𝐶 ) ≠ 0 ) → ( ( 𝐷 · 𝐶 ) / ( 𝐷 · 𝐶 ) ) = 1 )
27 23 25 26 syl2anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( ( 𝐷 · 𝐶 ) / ( 𝐷 · 𝐶 ) ) = 1 )
28 22 27 eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( ( 𝐶 · 𝐷 ) / ( 𝐷 · 𝐶 ) ) = 1 )
29 20 28 eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( ( 𝐶 / 𝐷 ) · ( 𝐷 / 𝐶 ) ) = 1 )
30 29 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( ( ( 𝐶 / 𝐷 ) · ( 𝐷 / 𝐶 ) ) · ( 𝐴 / 𝐵 ) ) = ( 1 · ( 𝐴 / 𝐵 ) ) )
31 divcl ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) → ( 𝐶 / 𝐷 ) ∈ ℂ )
32 2 1 24 31 syl3anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( 𝐶 / 𝐷 ) ∈ ℂ )
33 32 5 10 mulassd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( ( ( 𝐶 / 𝐷 ) · ( 𝐷 / 𝐶 ) ) · ( 𝐴 / 𝐵 ) ) = ( ( 𝐶 / 𝐷 ) · ( ( 𝐷 / 𝐶 ) · ( 𝐴 / 𝐵 ) ) ) )
34 10 mulid2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( 1 · ( 𝐴 / 𝐵 ) ) = ( 𝐴 / 𝐵 ) )
35 30 33 34 3eqtr3d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( ( 𝐶 / 𝐷 ) · ( ( 𝐷 / 𝐶 ) · ( 𝐴 / 𝐵 ) ) ) = ( 𝐴 / 𝐵 ) )
36 17 35 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( ( 𝐶 / 𝐷 ) · ( ( 𝐴 · 𝐷 ) / ( 𝐵 · 𝐶 ) ) ) = ( 𝐴 / 𝐵 ) )
37 6 1 mulcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( 𝐴 · 𝐷 ) ∈ ℂ )
38 7 2 mulcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( 𝐵 · 𝐶 ) ∈ ℂ )
39 mulne0 ⊢ ( ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( 𝐵 · 𝐶 ) ≠ 0 )
40 39 ad2ant2lr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( 𝐵 · 𝐶 ) ≠ 0 )
41 divcl ⊢ ( ( ( 𝐴 · 𝐷 ) ∈ ℂ ∧ ( 𝐵 · 𝐶 ) ∈ ℂ ∧ ( 𝐵 · 𝐶 ) ≠ 0 ) → ( ( 𝐴 · 𝐷 ) / ( 𝐵 · 𝐶 ) ) ∈ ℂ )
42 37 38 40 41 syl3anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( ( 𝐴 · 𝐷 ) / ( 𝐵 · 𝐶 ) ) ∈ ℂ )
43 divne0 ⊢ ( ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( 𝐶 / 𝐷 ) ≠ 0 )
44 43 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( 𝐶 / 𝐷 ) ≠ 0 )
45 divmul ⊢ ( ( ( 𝐴 / 𝐵 ) ∈ ℂ ∧ ( ( 𝐴 · 𝐷 ) / ( 𝐵 · 𝐶 ) ) ∈ ℂ ∧ ( ( 𝐶 / 𝐷 ) ∈ ℂ ∧ ( 𝐶 / 𝐷 ) ≠ 0 ) ) → ( ( ( 𝐴 / 𝐵 ) / ( 𝐶 / 𝐷 ) ) = ( ( 𝐴 · 𝐷 ) / ( 𝐵 · 𝐶 ) ) ↔ ( ( 𝐶 / 𝐷 ) · ( ( 𝐴 · 𝐷 ) / ( 𝐵 · 𝐶 ) ) ) = ( 𝐴 / 𝐵 ) ) )
46 10 42 32 44 45 syl112anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( ( ( 𝐴 / 𝐵 ) / ( 𝐶 / 𝐷 ) ) = ( ( 𝐴 · 𝐷 ) / ( 𝐵 · 𝐶 ) ) ↔ ( ( 𝐶 / 𝐷 ) · ( ( 𝐴 · 𝐷 ) / ( 𝐵 · 𝐶 ) ) ) = ( 𝐴 / 𝐵 ) ) )
47 36 46 mpbird ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( ( 𝐴 / 𝐵 ) / ( 𝐶 / 𝐷 ) ) = ( ( 𝐴 · 𝐷 ) / ( 𝐵 · 𝐶 ) ) )