Theorem divmul

Description: Relationship between division and multiplication. (Contributed by NM, 2-Aug-2004) (Revised by Mario Carneiro, 17-Feb-2014)

	Ref	Expression
Assertion	divmul	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐴 / 𝐶 ) = 𝐵 ↔ ( 𝐶 · 𝐵 ) = 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		divval	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) → ( 𝐴 / 𝐶 ) = ( ℩ 𝑥 ∈ ℂ ( 𝐶 · 𝑥 ) = 𝐴 ) )
2	1	3expb	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( 𝐴 / 𝐶 ) = ( ℩ 𝑥 ∈ ℂ ( 𝐶 · 𝑥 ) = 𝐴 ) )
3	2	3adant2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( 𝐴 / 𝐶 ) = ( ℩ 𝑥 ∈ ℂ ( 𝐶 · 𝑥 ) = 𝐴 ) )
4	3	eqeq1d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐴 / 𝐶 ) = 𝐵 ↔ ( ℩ 𝑥 ∈ ℂ ( 𝐶 · 𝑥 ) = 𝐴 ) = 𝐵 ) )
5		simp2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → 𝐵 ∈ ℂ )
6		receu	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) → ∃! 𝑥 ∈ ℂ ( 𝐶 · 𝑥 ) = 𝐴 )
7	6	3expb	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ∃! 𝑥 ∈ ℂ ( 𝐶 · 𝑥 ) = 𝐴 )
8		oveq2	⊢ ( 𝑥 = 𝐵 → ( 𝐶 · 𝑥 ) = ( 𝐶 · 𝐵 ) )
9	8	eqeq1d	⊢ ( 𝑥 = 𝐵 → ( ( 𝐶 · 𝑥 ) = 𝐴 ↔ ( 𝐶 · 𝐵 ) = 𝐴 ) )
10	9	riota2	⊢ ( ( 𝐵 ∈ ℂ ∧ ∃! 𝑥 ∈ ℂ ( 𝐶 · 𝑥 ) = 𝐴 ) → ( ( 𝐶 · 𝐵 ) = 𝐴 ↔ ( ℩ 𝑥 ∈ ℂ ( 𝐶 · 𝑥 ) = 𝐴 ) = 𝐵 ) )
11	5 7 10	3imp3i2an	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐶 · 𝐵 ) = 𝐴 ↔ ( ℩ 𝑥 ∈ ℂ ( 𝐶 · 𝑥 ) = 𝐴 ) = 𝐵 ) )
12	4 11	bitr4d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐴 / 𝐶 ) = 𝐵 ↔ ( 𝐶 · 𝐵 ) = 𝐴 ) )