Metamath Proof Explorer

Theorem divmuleq

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

Ref Expression
Assertion divmuleq ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → A C = B D ↔ A ⁢ D = B ⁢ C

Proof

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