Theorem noreceuw

Description: If a surreal has a reciprocal, then it has unique division. (Contributed by Scott Fenton, 12-Mar-2025)

	Ref	Expression
Assertion	noreceuw	|- ( ( ( A e. No /\ A =/= 0s /\ B e. No ) /\ E. x e. No ( A x.s x ) = 1s ) -> E! y e. No ( A x.s y ) = B )

Proof

Step	Hyp	Ref	Expression
1		norecdiv	|- ( ( ( A e. No /\ A =/= 0s /\ B e. No ) /\ E. x e. No ( A x.s x ) = 1s ) -> E. y e. No ( A x.s y ) = B )
2		divsmo	|- ( ( A e. No /\ A =/= 0s ) -> E* y e. No ( A x.s y ) = B )
3	2	3adant3	|- ( ( A e. No /\ A =/= 0s /\ B e. No ) -> E* y e. No ( A x.s y ) = B )
4	3	adantr	|- ( ( ( A e. No /\ A =/= 0s /\ B e. No ) /\ E. x e. No ( A x.s x ) = 1s ) -> E* y e. No ( A x.s y ) = B )
5		reu5	|- ( E! y e. No ( A x.s y ) = B <-> ( E. y e. No ( A x.s y ) = B /\ E* y e. No ( A x.s y ) = B ) )
6	1 4 5	sylanbrc	|- ( ( ( A e. No /\ A =/= 0s /\ B e. No ) /\ E. x e. No ( A x.s x ) = 1s ) -> E! y e. No ( A x.s y ) = B )