This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 → A C = B ↔ C ⁢ B = A

Proof

Step Hyp Ref Expression
1 divval ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A C = ι x ∈ ℂ | C ⁢ x = A
2 1 3expb ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A C = ι x ∈ ℂ | C ⁢ x = A
3 2 3adant2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A C = ι x ∈ ℂ | C ⁢ x = A
4 3 eqeq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A C = 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 → A C = B ↔ C ⁢ B = A