Metamath Proof Explorer

Theorem divmuldiv

Description: Multiplication of two ratios. Theorem I.14 of Apostol p. 18. (Contributed by NM, 1-Aug-2004)

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

Proof

Step Hyp Ref Expression
1 3anass ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ↔ ( 𝐴 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) )
2 3anass ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ↔ ( 𝐵 ∈ ℂ ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) )
3 divcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) → ( 𝐴 / 𝐶 ) ∈ ℂ )
4 divcl ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) → ( 𝐵 / 𝐷 ) ∈ ℂ )
5 mulcl ⊢ ( ( ( 𝐴 / 𝐶 ) ∈ ℂ ∧ ( 𝐵 / 𝐷 ) ∈ ℂ ) → ( ( 𝐴 / 𝐶 ) · ( 𝐵 / 𝐷 ) ) ∈ ℂ )
6 3 4 5 syl2an ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( ( 𝐴 / 𝐶 ) · ( 𝐵 / 𝐷 ) ) ∈ ℂ )
7 mulcl ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( 𝐶 · 𝐷 ) ∈ ℂ )
8 7 ad2ant2r ⊢ ( ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( 𝐶 · 𝐷 ) ∈ ℂ )
9 8 3adantr1 ⊢ ( ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( 𝐶 · 𝐷 ) ∈ ℂ )
10 9 3adantl1 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( 𝐶 · 𝐷 ) ∈ ℂ )
11 mulne0 ⊢ ( ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( 𝐶 · 𝐷 ) ≠ 0 )
12 11 3adantr1 ⊢ ( ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( 𝐶 · 𝐷 ) ≠ 0 )
13 12 3adantl1 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( 𝐶 · 𝐷 ) ≠ 0 )
14 divcan3 ⊢ ( ( ( ( 𝐴 / 𝐶 ) · ( 𝐵 / 𝐷 ) ) ∈ ℂ ∧ ( 𝐶 · 𝐷 ) ∈ ℂ ∧ ( 𝐶 · 𝐷 ) ≠ 0 ) → ( ( ( 𝐶 · 𝐷 ) · ( ( 𝐴 / 𝐶 ) · ( 𝐵 / 𝐷 ) ) ) / ( 𝐶 · 𝐷 ) ) = ( ( 𝐴 / 𝐶 ) · ( 𝐵 / 𝐷 ) ) )
15 6 10 13 14 syl3anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( ( ( 𝐶 · 𝐷 ) · ( ( 𝐴 / 𝐶 ) · ( 𝐵 / 𝐷 ) ) ) / ( 𝐶 · 𝐷 ) ) = ( ( 𝐴 / 𝐶 ) · ( 𝐵 / 𝐷 ) ) )
16 simp2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) → 𝐶 ∈ ℂ )
17 16 3 jca ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) → ( 𝐶 ∈ ℂ ∧ ( 𝐴 / 𝐶 ) ∈ ℂ ) )
18 simp2 ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) → 𝐷 ∈ ℂ )
19 18 4 jca ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) → ( 𝐷 ∈ ℂ ∧ ( 𝐵 / 𝐷 ) ∈ ℂ ) )
20 mul4 ⊢ ( ( ( 𝐶 ∈ ℂ ∧ ( 𝐴 / 𝐶 ) ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ ( 𝐵 / 𝐷 ) ∈ ℂ ) ) → ( ( 𝐶 · ( 𝐴 / 𝐶 ) ) · ( 𝐷 · ( 𝐵 / 𝐷 ) ) ) = ( ( 𝐶 · 𝐷 ) · ( ( 𝐴 / 𝐶 ) · ( 𝐵 / 𝐷 ) ) ) )
21 17 19 20 syl2an ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( ( 𝐶 · ( 𝐴 / 𝐶 ) ) · ( 𝐷 · ( 𝐵 / 𝐷 ) ) ) = ( ( 𝐶 · 𝐷 ) · ( ( 𝐴 / 𝐶 ) · ( 𝐵 / 𝐷 ) ) ) )
22 divcan2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) → ( 𝐶 · ( 𝐴 / 𝐶 ) ) = 𝐴 )
23 divcan2 ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) → ( 𝐷 · ( 𝐵 / 𝐷 ) ) = 𝐵 )
24 22 23 oveqan12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( ( 𝐶 · ( 𝐴 / 𝐶 ) ) · ( 𝐷 · ( 𝐵 / 𝐷 ) ) ) = ( 𝐴 · 𝐵 ) )
25 21 24 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( ( 𝐶 · 𝐷 ) · ( ( 𝐴 / 𝐶 ) · ( 𝐵 / 𝐷 ) ) ) = ( 𝐴 · 𝐵 ) )
26 25 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( ( ( 𝐶 · 𝐷 ) · ( ( 𝐴 / 𝐶 ) · ( 𝐵 / 𝐷 ) ) ) / ( 𝐶 · 𝐷 ) ) = ( ( 𝐴 · 𝐵 ) / ( 𝐶 · 𝐷 ) ) )
27 15 26 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( ( 𝐴 / 𝐶 ) · ( 𝐵 / 𝐷 ) ) = ( ( 𝐴 · 𝐵 ) / ( 𝐶 · 𝐷 ) ) )
28 1 2 27 syl2anbr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) ∧ ( 𝐵 ∈ ℂ ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( ( 𝐴 / 𝐶 ) · ( 𝐵 / 𝐷 ) ) = ( ( 𝐴 · 𝐵 ) / ( 𝐶 · 𝐷 ) ) )
29 28 an4s ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( ( 𝐴 / 𝐶 ) · ( 𝐵 / 𝐷 ) ) = ( ( 𝐴 · 𝐵 ) / ( 𝐶 · 𝐷 ) ) )