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

Metamath Proof Explorer

Theorem redivmuld

Description: Relationship between division and multiplication. (Contributed by SN, 25-Nov-2025)

Ref Expression
Hypotheses redivmuld.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
redivmuld.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
redivmuld.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
redivmuld.z ⊢ ( 𝜑 → 𝐶 ≠ 0 )
Assertion redivmuld ( 𝜑 → ( ( 𝐴 /ℝ 𝐶 ) = 𝐵 ↔ ( 𝐶 · 𝐵 ) = 𝐴 ) )

Proof

Step Hyp Ref Expression
1 redivmuld.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 redivmuld.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 redivmuld.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
4 redivmuld.z ⊢ ( 𝜑 → 𝐶 ≠ 0 )
5 1 3 4 redivvald ⊢ ( 𝜑 → ( 𝐴 /ℝ 𝐶 ) = ( ℩ 𝑥 ∈ ℝ ( 𝐶 · 𝑥 ) = 𝐴 ) )
6 5 eqeq1d ⊢ ( 𝜑 → ( ( 𝐴 /ℝ 𝐶 ) = 𝐵 ↔ ( ℩ 𝑥 ∈ ℝ ( 𝐶 · 𝑥 ) = 𝐴 ) = 𝐵 ) )
7 1 3 4 rediveud ⊢ ( 𝜑 → ∃! 𝑥 ∈ ℝ ( 𝐶 · 𝑥 ) = 𝐴 )
8 oveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝐶 · 𝑥 ) = ( 𝐶 · 𝐵 ) )
9 8 eqeq1d ⊢ ( 𝑥 = 𝐵 → ( ( 𝐶 · 𝑥 ) = 𝐴 ↔ ( 𝐶 · 𝐵 ) = 𝐴 ) )
10 9 riota2 ⊢ ( ( 𝐵 ∈ ℝ ∧ ∃! 𝑥 ∈ ℝ ( 𝐶 · 𝑥 ) = 𝐴 ) → ( ( 𝐶 · 𝐵 ) = 𝐴 ↔ ( ℩ 𝑥 ∈ ℝ ( 𝐶 · 𝑥 ) = 𝐴 ) = 𝐵 ) )
11 2 7 10 syl2anc ⊢ ( 𝜑 → ( ( 𝐶 · 𝐵 ) = 𝐴 ↔ ( ℩ 𝑥 ∈ ℝ ( 𝐶 · 𝑥 ) = 𝐴 ) = 𝐵 ) )
12 6 11 bitr4d ⊢ ( 𝜑 → ( ( 𝐴 /ℝ 𝐶 ) = 𝐵 ↔ ( 𝐶 · 𝐵 ) = 𝐴 ) )