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