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	Could not format assertion : No typesetting found for |- ( ph -> ( A /R B ) = ( iota_ x e. RR ( B x. x ) = A ) ) with typecode |-

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	Could not format /R = ( z e. RR , y e. ( RR \ { 0 } ) |-> ( iota_ x e. RR ( y x. x ) = z ) ) : No typesetting found for |- /R = ( z e. RR , y e. ( RR \ { 0 } ) |-> ( iota_ x e. RR ( y x. x ) = z ) ) with typecode |-
11		riotaex	$$⊢\left(\iota x\in ℝ|Bx=A\right)\in \mathrm{V}$$
12	6 9 10 11	ovmpo	Could not format ( ( A e. RR /\ B e. ( RR \ { 0 } ) ) -> ( A /R B ) = ( iota_ x e. RR ( B x. x ) = A ) ) : No typesetting found for |- ( ( A e. RR /\ B e. ( RR \ { 0 } ) ) -> ( A /R B ) = ( iota_ x e. RR ( B x. x ) = A ) ) with typecode |-
13	1 4 12	syl2anc	Could not format ( ph -> ( A /R B ) = ( iota_ x e. RR ( B x. x ) = A ) ) : No typesetting found for |- ( ph -> ( A /R B ) = ( iota_ x e. RR ( B x. x ) = A ) ) with typecode |-