Description: Swap denominators of two ratios. (Contributed by NM, 6-Aug-1999)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | divclz.1 | ⊢ 𝐴 ∈ ℂ | |
| divclz.2 | ⊢ 𝐵 ∈ ℂ | ||
| divmulz.3 | ⊢ 𝐶 ∈ ℂ | ||
| divmuldiv.4 | ⊢ 𝐷 ∈ ℂ | ||
| divmuldiv.5 | ⊢ 𝐵 ≠ 0 | ||
| divmuldiv.6 | ⊢ 𝐷 ≠ 0 | ||
| Assertion | divmul13i | ⊢ ( ( 𝐴 / 𝐵 ) · ( 𝐶 / 𝐷 ) ) = ( ( 𝐶 / 𝐵 ) · ( 𝐴 / 𝐷 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | divclz.1 | ⊢ 𝐴 ∈ ℂ | |
| 2 | divclz.2 | ⊢ 𝐵 ∈ ℂ | |
| 3 | divmulz.3 | ⊢ 𝐶 ∈ ℂ | |
| 4 | divmuldiv.4 | ⊢ 𝐷 ∈ ℂ | |
| 5 | divmuldiv.5 | ⊢ 𝐵 ≠ 0 | |
| 6 | divmuldiv.6 | ⊢ 𝐷 ≠ 0 | |
| 7 | 3 1 | mulcomi | ⊢ ( 𝐶 · 𝐴 ) = ( 𝐴 · 𝐶 ) |
| 8 | 7 | oveq1i | ⊢ ( ( 𝐶 · 𝐴 ) / ( 𝐵 · 𝐷 ) ) = ( ( 𝐴 · 𝐶 ) / ( 𝐵 · 𝐷 ) ) |
| 9 | 3 2 1 4 5 6 | divmuldivi | ⊢ ( ( 𝐶 / 𝐵 ) · ( 𝐴 / 𝐷 ) ) = ( ( 𝐶 · 𝐴 ) / ( 𝐵 · 𝐷 ) ) |
| 10 | 1 2 3 4 5 6 | divmuldivi | ⊢ ( ( 𝐴 / 𝐵 ) · ( 𝐶 / 𝐷 ) ) = ( ( 𝐴 · 𝐶 ) / ( 𝐵 · 𝐷 ) ) |
| 11 | 8 9 10 | 3eqtr4ri | ⊢ ( ( 𝐴 / 𝐵 ) · ( 𝐶 / 𝐷 ) ) = ( ( 𝐶 / 𝐵 ) · ( 𝐴 / 𝐷 ) ) |