Theorem divmuleq

Description: Cross-multiply in an equality of ratios. (Contributed by Mario Carneiro, 23-Feb-2014)

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

Proof

Step	Hyp	Ref	Expression
1		divcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) → ( 𝐴 / 𝐶 ) ∈ ℂ )
2	1	3expb	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( 𝐴 / 𝐶 ) ∈ ℂ )
3	2	ad2ant2r	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( 𝐴 / 𝐶 ) ∈ ℂ )
4		divcl	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) → ( 𝐵 / 𝐷 ) ∈ ℂ )
5	4	3expb	⊢ ( ( 𝐵 ∈ ℂ ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( 𝐵 / 𝐷 ) ∈ ℂ )
6	5	ad2ant2l	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( 𝐵 / 𝐷 ) ∈ ℂ )
7		mulcl	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( 𝐶 · 𝐷 ) ∈ ℂ )
8	7	ad2ant2r	⊢ ( ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( 𝐶 · 𝐷 ) ∈ ℂ )
9		mulne0	⊢ ( ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( 𝐶 · 𝐷 ) ≠ 0 )
10	8 9	jca	⊢ ( ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( ( 𝐶 · 𝐷 ) ∈ ℂ ∧ ( 𝐶 · 𝐷 ) ≠ 0 ) )
11	10	adantl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( ( 𝐶 · 𝐷 ) ∈ ℂ ∧ ( 𝐶 · 𝐷 ) ≠ 0 ) )
12		mulcan2	⊢ ( ( ( 𝐴 / 𝐶 ) ∈ ℂ ∧ ( 𝐵 / 𝐷 ) ∈ ℂ ∧ ( ( 𝐶 · 𝐷 ) ∈ ℂ ∧ ( 𝐶 · 𝐷 ) ≠ 0 ) ) → ( ( ( 𝐴 / 𝐶 ) · ( 𝐶 · 𝐷 ) ) = ( ( 𝐵 / 𝐷 ) · ( 𝐶 · 𝐷 ) ) ↔ ( 𝐴 / 𝐶 ) = ( 𝐵 / 𝐷 ) ) )
13	3 6 11 12	syl3anc	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( ( ( 𝐴 / 𝐶 ) · ( 𝐶 · 𝐷 ) ) = ( ( 𝐵 / 𝐷 ) · ( 𝐶 · 𝐷 ) ) ↔ ( 𝐴 / 𝐶 ) = ( 𝐵 / 𝐷 ) ) )
14		simprll	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → 𝐶 ∈ ℂ )
15		simprrl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → 𝐷 ∈ ℂ )
16	3 14 15	mulassd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( ( ( 𝐴 / 𝐶 ) · 𝐶 ) · 𝐷 ) = ( ( 𝐴 / 𝐶 ) · ( 𝐶 · 𝐷 ) ) )
17		divcan1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) → ( ( 𝐴 / 𝐶 ) · 𝐶 ) = 𝐴 )
18	17	3expb	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐴 / 𝐶 ) · 𝐶 ) = 𝐴 )
19	18	ad2ant2r	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( ( 𝐴 / 𝐶 ) · 𝐶 ) = 𝐴 )
20	19	oveq1d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( ( ( 𝐴 / 𝐶 ) · 𝐶 ) · 𝐷 ) = ( 𝐴 · 𝐷 ) )
21	16 20	eqtr3d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( ( 𝐴 / 𝐶 ) · ( 𝐶 · 𝐷 ) ) = ( 𝐴 · 𝐷 ) )
22	14 15	mulcomd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( 𝐶 · 𝐷 ) = ( 𝐷 · 𝐶 ) )
23	22	oveq2d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( ( 𝐵 / 𝐷 ) · ( 𝐶 · 𝐷 ) ) = ( ( 𝐵 / 𝐷 ) · ( 𝐷 · 𝐶 ) ) )
24	6 15 14	mulassd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( ( ( 𝐵 / 𝐷 ) · 𝐷 ) · 𝐶 ) = ( ( 𝐵 / 𝐷 ) · ( 𝐷 · 𝐶 ) ) )
25		divcan1	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) → ( ( 𝐵 / 𝐷 ) · 𝐷 ) = 𝐵 )
26	25	3expb	⊢ ( ( 𝐵 ∈ ℂ ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( ( 𝐵 / 𝐷 ) · 𝐷 ) = 𝐵 )
27	26	ad2ant2l	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( ( 𝐵 / 𝐷 ) · 𝐷 ) = 𝐵 )
28	27	oveq1d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( ( ( 𝐵 / 𝐷 ) · 𝐷 ) · 𝐶 ) = ( 𝐵 · 𝐶 ) )
29	23 24 28	3eqtr2d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( ( 𝐵 / 𝐷 ) · ( 𝐶 · 𝐷 ) ) = ( 𝐵 · 𝐶 ) )
30	21 29	eqeq12d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( ( ( 𝐴 / 𝐶 ) · ( 𝐶 · 𝐷 ) ) = ( ( 𝐵 / 𝐷 ) · ( 𝐶 · 𝐷 ) ) ↔ ( 𝐴 · 𝐷 ) = ( 𝐵 · 𝐶 ) ) )
31	13 30	bitr3d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( ( 𝐴 / 𝐶 ) = ( 𝐵 / 𝐷 ) ↔ ( 𝐴 · 𝐷 ) = ( 𝐵 · 𝐶 ) ) )