Description: Relationship between division and multiplication. (Contributed by NM, 7-Feb-2006)
Ref | Expression | ||
---|---|---|---|
Assertion | divmul2 | ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐴 / 𝐶 ) = 𝐵 ↔ 𝐴 = ( 𝐶 · 𝐵 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | divmul | ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐴 / 𝐶 ) = 𝐵 ↔ ( 𝐶 · 𝐵 ) = 𝐴 ) ) | |
2 | eqcom | ⊢ ( ( 𝐶 · 𝐵 ) = 𝐴 ↔ 𝐴 = ( 𝐶 · 𝐵 ) ) | |
3 | 1 2 | bitrdi | ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐴 / 𝐶 ) = 𝐵 ↔ 𝐴 = ( 𝐶 · 𝐵 ) ) ) |