Description: Cross-multiply in an equality of ratios. (Contributed by Mario Carneiro, 27-May-2016)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | div1d.1 | ⊢ ( 𝜑 → 𝐴 ∈ ℂ ) | |
| divcld.2 | ⊢ ( 𝜑 → 𝐵 ∈ ℂ ) | ||
| divmuld.3 | ⊢ ( 𝜑 → 𝐶 ∈ ℂ ) | ||
| divmuldivd.4 | ⊢ ( 𝜑 → 𝐷 ∈ ℂ ) | ||
| divmuldivd.5 | ⊢ ( 𝜑 → 𝐵 ≠ 0 ) | ||
| divmuldivd.6 | ⊢ ( 𝜑 → 𝐷 ≠ 0 ) | ||
| Assertion | divmuleqd | ⊢ ( 𝜑 → ( ( 𝐴 / 𝐵 ) = ( 𝐶 / 𝐷 ) ↔ ( 𝐴 · 𝐷 ) = ( 𝐶 · 𝐵 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | div1d.1 | ⊢ ( 𝜑 → 𝐴 ∈ ℂ ) | |
| 2 | divcld.2 | ⊢ ( 𝜑 → 𝐵 ∈ ℂ ) | |
| 3 | divmuld.3 | ⊢ ( 𝜑 → 𝐶 ∈ ℂ ) | |
| 4 | divmuldivd.4 | ⊢ ( 𝜑 → 𝐷 ∈ ℂ ) | |
| 5 | divmuldivd.5 | ⊢ ( 𝜑 → 𝐵 ≠ 0 ) | |
| 6 | divmuldivd.6 | ⊢ ( 𝜑 → 𝐷 ≠ 0 ) | |
| 7 | 2 5 | jca | ⊢ ( 𝜑 → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) |
| 8 | 4 6 | jca | ⊢ ( 𝜑 → ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) |
| 9 | divmuleq | ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) ) → ( ( 𝐴 / 𝐵 ) = ( 𝐶 / 𝐷 ) ↔ ( 𝐴 · 𝐷 ) = ( 𝐶 · 𝐵 ) ) ) | |
| 10 | 1 3 7 8 9 | syl22anc | ⊢ ( 𝜑 → ( ( 𝐴 / 𝐵 ) = ( 𝐶 / 𝐷 ) ↔ ( 𝐴 · 𝐷 ) = ( 𝐶 · 𝐵 ) ) ) |