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	Could not format assertion : No typesetting found for |- ( ( ( 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 ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		norecdiv	Could not format ( ( ( 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 ) : No typesetting found for |- ( ( ( 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 ) with typecode |-
2		divsmo	Could not format ( ( A e. No /\ A =/= 0s ) -> E* y e. No ( A x.s y ) = B ) : No typesetting found for |- ( ( A e. No /\ A =/= 0s ) -> E* y e. No ( A x.s y ) = B ) with typecode |-
3	2	3adant3	Could not format ( ( A e. No /\ A =/= 0s /\ B e. No ) -> E* y e. No ( A x.s y ) = B ) : No typesetting found for |- ( ( A e. No /\ A =/= 0s /\ B e. No ) -> E* y e. No ( A x.s y ) = B ) with typecode |-
4	3	adantr	Could not format ( ( ( 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 ) : No typesetting found for |- ( ( ( 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 ) with typecode |-
5		reu5	Could not format ( 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 ) ) : No typesetting found for |- ( 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 ) ) with typecode |-
6	1 4 5	sylanbrc	Could not format ( ( ( 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 ) : No typesetting found for |- ( ( ( 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 ) with typecode |-