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 ) ) ) → ( ( 𝐴 / 𝐶 ) · ( 𝐵 / 𝐷 ) ) = ( ( 𝐴 · 𝐵 ) / ( 𝐶 · 𝐷 ) ) )