Theorem rediveud

Description: Existential uniqueness of real quotients. (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	rediveud	$$⊢\phi \to \exists !x\in ℝBx=A$$

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		ax-rrecex	$$⊢\left(B\in ℝ\wedge B\ne 0\right)\to \exists y\in ℝBy=1$$
5	2 3 4	syl2anc	$$⊢\phi \to \exists y\in ℝBy=1$$
6		oveq2	$$⊢x=yA\to Bx=ByA$$
7	6	eqeq1d	$$⊢x=yA\to \left(Bx=A\leftrightarrow ByA=A\right)$$
8		simprl	$$⊢\left(\phi \wedge \left(y\in ℝ\wedge By=1\right)\right)\to y\in ℝ$$
9	1	adantr	$$⊢\left(\phi \wedge \left(y\in ℝ\wedge By=1\right)\right)\to A\in ℝ$$
10	8 9	remulcld	$$⊢\left(\phi \wedge \left(y\in ℝ\wedge By=1\right)\right)\to yA\in ℝ$$
11		simprr	$$⊢\left(\phi \wedge \left(y\in ℝ\wedge By=1\right)\right)\to By=1$$
12	11	oveq1d	$$⊢\left(\phi \wedge \left(y\in ℝ\wedge By=1\right)\right)\to ByA=1A$$
13	2	recnd	$$⊢\phi \to B\in ℂ$$
14	13	adantr	$$⊢\left(\phi \wedge \left(y\in ℝ\wedge By=1\right)\right)\to B\in ℂ$$
15	8	recnd	$$⊢\left(\phi \wedge \left(y\in ℝ\wedge By=1\right)\right)\to y\in ℂ$$
16	1	recnd	$$⊢\phi \to A\in ℂ$$
17	16	adantr	$$⊢\left(\phi \wedge \left(y\in ℝ\wedge By=1\right)\right)\to A\in ℂ$$
18	14 15 17	mulassd	$$⊢\left(\phi \wedge \left(y\in ℝ\wedge By=1\right)\right)\to ByA=ByA$$
19		remullid	$$⊢A\in ℝ\to 1A=A$$
20	1 19	syl	$$⊢\phi \to 1A=A$$
21	20	adantr	$$⊢\left(\phi \wedge \left(y\in ℝ\wedge By=1\right)\right)\to 1A=A$$
22	12 18 21	3eqtr3d	$$⊢\left(\phi \wedge \left(y\in ℝ\wedge By=1\right)\right)\to ByA=A$$
23	7 10 22	rspcedvdw	$$⊢\left(\phi \wedge \left(y\in ℝ\wedge By=1\right)\right)\to \exists x\in ℝBx=A$$
24	5 23	rexlimddv	$$⊢\phi \to \exists x\in ℝBx=A$$
25		eqtr3	$$⊢\left(Bx=A\wedge By=A\right)\to Bx=By$$
26		simprl	$$⊢\left(\phi \wedge \left(x\in ℝ\wedge y\in ℝ\right)\right)\to x\in ℝ$$
27		simprr	$$⊢\left(\phi \wedge \left(x\in ℝ\wedge y\in ℝ\right)\right)\to y\in ℝ$$
28	2	adantr	$$⊢\left(\phi \wedge \left(x\in ℝ\wedge y\in ℝ\right)\right)\to B\in ℝ$$
29	3	adantr	$$⊢\left(\phi \wedge \left(x\in ℝ\wedge y\in ℝ\right)\right)\to B\ne 0$$
30	26 27 28 29	remulcand	$$⊢\left(\phi \wedge \left(x\in ℝ\wedge y\in ℝ\right)\right)\to \left(Bx=By\leftrightarrow x=y\right)$$
31	25 30	imbitrid	$$⊢\left(\phi \wedge \left(x\in ℝ\wedge y\in ℝ\right)\right)\to \left(\left(Bx=A\wedge By=A\right)\to x=y\right)$$
32	31	ralrimivva	$$⊢\phi \to \forall x\in ℝ\forall y\in ℝ\left(\left(Bx=A\wedge By=A\right)\to x=y\right)$$
33		oveq2	$$⊢x=y\to Bx=By$$
34	33	eqeq1d	$$⊢x=y\to \left(Bx=A\leftrightarrow By=A\right)$$
35	34	reu4	$$⊢\exists !x\in ℝBx=A\leftrightarrow \left(\exists x\in ℝBx=A\wedge \forall x\in ℝ\forall y\in ℝ\left(\left(Bx=A\wedge By=A\right)\to x=y\right)\right)$$
36	24 32 35	sylanbrc	$$⊢\phi \to \exists !x\in ℝBx=A$$