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	$$⊢\phi \to A\in ℝ$$
	redivvald.b	$$⊢\phi \to B\in ℝ$$
	redivvald.z	$$⊢\phi \to B\ne 0$$
Assertion	redivvald	$$⊢\phi \to A{/}_{ℝ}B=\left(\iota x\in ℝ|Bx=A\right)$$

Proof

Step	Hyp	Ref	Expression
1		redivvald.a	$$⊢\phi \to A\in ℝ$$
2		redivvald.b	$$⊢\phi \to B\in ℝ$$
3		redivvald.z	$$⊢\phi \to B\ne 0$$
4	2 3	eldifsnd	$$⊢\phi \to B\in \left(ℝ\setminus \left\{0\right\}\right)$$
5		eqeq2	$$⊢z=A\to \left(yx=z\leftrightarrow yx=A\right)$$
6	5	riotabidv	$$⊢z=A\to \left(\iota x\in ℝ|yx=z\right)=\left(\iota x\in ℝ|yx=A\right)$$
7		oveq1	$$⊢y=B\to yx=Bx$$
8	7	eqeq1d	$$⊢y=B\to \left(yx=A\leftrightarrow Bx=A\right)$$
9	8	riotabidv	$$⊢y=B\to \left(\iota x\in ℝ|yx=A\right)=\left(\iota x\in ℝ|Bx=A\right)$$
10		df-rediv	$$⊢{/}_{ℝ}=\left(z\in ℝ,y\in \left(ℝ\setminus \left\{0\right\}\right)⟼\left(\iota x\in ℝ|yx=z\right)\right)$$
11		riotaex	$$⊢\left(\iota x\in ℝ|Bx=A\right)\in \mathrm{V}$$
12	6 9 10 11	ovmpo	$$⊢\left(A\in ℝ\wedge B\in \left(ℝ\setminus \left\{0\right\}\right)\right)\to A{/}_{ℝ}B=\left(\iota x\in ℝ|Bx=A\right)$$
13	1 4 12	syl2anc	$$⊢\phi \to A{/}_{ℝ}B=\left(\iota x\in ℝ|Bx=A\right)$$