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