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	$⊢ φ \to A \in ℝ$
	redivvald.b	$⊢ φ \to B \in ℝ$
	redivvald.z	$⊢ φ \to B \neq 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 \|-

Step	Hyp	Ref	Expression
1		redivvald.a	$⊢ φ \to A \in ℝ$
2		redivvald.b	$⊢ φ \to B \in ℝ$
3		redivvald.z	$⊢ φ \to B \neq 0$
4	2 3	eldifsnd	$⊢ φ \to B \in (ℝ ∖ \{0\})$
5		eqeq2	$⊢ z = A \to (y x = z \leftrightarrow y x = A)$
6	5	riotabidv	$⊢ z = A \to (ι x \in ℝ \| y x = z) = (ι x \in ℝ \| y x = A)$
7		oveq1	$⊢ y = B \to y x = B x$
8	7	eqeq1d	$⊢ y = B \to (y x = A \leftrightarrow B x = A)$
9	8	riotabidv	$⊢ y = B \to (ι x \in ℝ \| y x = A) = (ι x \in ℝ \| B x = A)$
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	$⊢ (ι x \in ℝ \| B x = A) \in 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 \|-

Metamath Proof Explorer