Metamath Proof Explorer

Theorem xdivmul

Description: Relationship between division and multiplication. (Contributed by Thierry Arnoux, 24-Dec-2016)

Ref Expression
Assertion xdivmul ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ ∧ C ≠ 0 → A ÷ 𝑒 C = B ↔ C ⋅ 𝑒 B = A

Proof

Step Hyp Ref Expression
1 xdivval ⊢ 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 xreceu ⊢ A ∈ ℝ * ∧ C ∈ ℝ ∧ C ≠ 0 → ∃! x ∈ ℝ * C ⋅ 𝑒 x = A
7 6 3expb ⊢ A ∈ ℝ * ∧ C ∈ ℝ ∧ C ≠ 0 → ∃! x ∈ ℝ * C ⋅ 𝑒 x = A
8 7 3adant2 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ ∧ C ≠ 0 → ∃! x ∈ ℝ * C ⋅ 𝑒 x = A
9 oveq2 ⊢ x = B → C ⋅ 𝑒 x = C ⋅ 𝑒 B
10 9 eqeq1d ⊢ x = B → C ⋅ 𝑒 x = A ↔ C ⋅ 𝑒 B = A
11 10 riota2 ⊢ B ∈ ℝ * ∧ ∃! x ∈ ℝ * C ⋅ 𝑒 x = A → C ⋅ 𝑒 B = A ↔ ι x ∈ ℝ * | C ⋅ 𝑒 x = A = B
12 5 8 11 syl2anc ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ ∧ C ≠ 0 → C ⋅ 𝑒 B = A ↔ ι x ∈ ℝ * | C ⋅ 𝑒 x = A = B
13 4 12 bitr4d ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ ∧ C ≠ 0 → A ÷ 𝑒 C = B ↔ C ⋅ 𝑒 B = A