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	⊢ ( 𝜑 → ( 𝐴 /ℝ 𝐵 ) = ( ℩ 𝑥 ∈ ℝ ( 𝐵 · 𝑥 ) = 𝐴 ) )