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

Metamath Proof Explorer

Theorem redivvald

Description: Value of real division, which is the (unique) real x such that ( B x. x ) = A . (Contributed by SN, 25-Nov-2025)

Ref Expression
Hypotheses redivvald.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
redivvald.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
redivvald.z ⊢ ( 𝜑 → 𝐵 ≠ 0 )
Assertion redivvald ( 𝜑 → ( 𝐴 /ℝ 𝐵 ) = ( ℩ 𝑥 ∈ ℝ ( 𝐵 · 𝑥 ) = 𝐴 ) )

Proof

Step Hyp Ref Expression
1 redivvald.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 redivvald.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 redivvald.z ⊢ ( 𝜑 → 𝐵 ≠ 0 )
4 2 3 eldifsnd ⊢ ( 𝜑 → 𝐵 ∈ ( ℝ ∖ { 0 } ) )
5 eqeq2 ⊢ ( 𝑧 = 𝐴 → ( ( 𝑦 · 𝑥 ) = 𝑧 ↔ ( 𝑦 · 𝑥 ) = 𝐴 ) )
6 5 riotabidv ⊢ ( 𝑧 = 𝐴 → ( ℩ 𝑥 ∈ ℝ ( 𝑦 · 𝑥 ) = 𝑧 ) = ( ℩ 𝑥 ∈ ℝ ( 𝑦 · 𝑥 ) = 𝐴 ) )
7 oveq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 · 𝑥 ) = ( 𝐵 · 𝑥 ) )
8 7 eqeq1d ⊢ ( 𝑦 = 𝐵 → ( ( 𝑦 · 𝑥 ) = 𝐴 ↔ ( 𝐵 · 𝑥 ) = 𝐴 ) )
9 8 riotabidv ⊢ ( 𝑦 = 𝐵 → ( ℩ 𝑥 ∈ ℝ ( 𝑦 · 𝑥 ) = 𝐴 ) = ( ℩ 𝑥 ∈ ℝ ( 𝐵 · 𝑥 ) = 𝐴 ) )
10 df-rediv ⊢ /ℝ = ( 𝑧 ∈ ℝ , 𝑦 ∈ ( ℝ ∖ { 0 } ) ↦ ( ℩ 𝑥 ∈ ℝ ( 𝑦 · 𝑥 ) = 𝑧 ) )
11 riotaex ⊢ ( ℩ 𝑥 ∈ ℝ ( 𝐵 · 𝑥 ) = 𝐴 ) ∈ V
12 6 9 10 11 ovmpo ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ( ℝ ∖ { 0 } ) ) → ( 𝐴 /ℝ 𝐵 ) = ( ℩ 𝑥 ∈ ℝ ( 𝐵 · 𝑥 ) = 𝐴 ) )
13 1 4 12 syl2anc ⊢ ( 𝜑 → ( 𝐴 /ℝ 𝐵 ) = ( ℩ 𝑥 ∈ ℝ ( 𝐵 · 𝑥 ) = 𝐴 ) )