Metamath Proof Explorer

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