Metamath Proof Explorer

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 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0→AC=B↔C⁢B=A

Proof

Step Hyp Ref Expression
1 divval ⊢A∈ℂ∧C∈ℂ∧C≠0→AC=ιx∈ℂ|C⁢x=A
2 1 3expb ⊢A∈ℂ∧C∈ℂ∧C≠0→AC=ιx∈ℂ|C⁢x=A
3 2 3adant2 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0→AC=ιx∈ℂ|C⁢x=A
4 3 eqeq1d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0→AC=B↔ιx∈ℂ|C⁢x=A=B
5 simp2 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0→B∈ℂ
6 receu ⊢A∈ℂ∧C∈ℂ∧C≠0→∃!x∈ℂC⁢x=A
7 6 3expb ⊢A∈ℂ∧C∈ℂ∧C≠0→∃!x∈ℂC⁢x=A
8 oveq2 ⊢x=B→C⁢x=C⁢B
9 8 eqeq1d ⊢x=B→C⁢x=A↔C⁢B=A
10 9 riota2 ⊢B∈ℂ∧∃!x∈ℂC⁢x=A→C⁢B=A↔ιx∈ℂ|C⁢x=A=B
11 5 7 10 3imp3i2an ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0→C⁢B=A↔ιx∈ℂ|C⁢x=A=B
12 4 11 bitr4d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0→AC=B↔C⁢B=A