Metamath Proof Explorer

Theorem norecdiv

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

Ref Expression
Assertion norecdiv 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 simprl Could not format ( ( ( A e. No /\ A =/= 0s /\ B e. No ) /\ ( w e. No /\ ( A x.s w ) = 1s ) ) -> w e. No ) : No typesetting found for |- ( ( ( A e. No /\ A =/= 0s /\ B e. No ) /\ ( w e. No /\ ( A x.s w ) = 1s ) ) -> w e. No ) with typecode |-
2 simpl3 Could not format ( ( ( A e. No /\ A =/= 0s /\ B e. No ) /\ ( w e. No /\ ( A x.s w ) = 1s ) ) -> B e. No ) : No typesetting found for |- ( ( ( A e. No /\ A =/= 0s /\ B e. No ) /\ ( w e. No /\ ( A x.s w ) = 1s ) ) -> B e. No ) with typecode |-
3 1 2 mulscld Could not format ( ( ( A e. No /\ A =/= 0s /\ B e. No ) /\ ( w e. No /\ ( A x.s w ) = 1s ) ) -> ( w x.s B ) e. No ) : No typesetting found for |- ( ( ( A e. No /\ A =/= 0s /\ B e. No ) /\ ( w e. No /\ ( A x.s w ) = 1s ) ) -> ( w x.s B ) e. No ) with typecode |-
4 oveq1 Could not format ( ( A x.s w ) = 1s -> ( ( A x.s w ) x.s B ) = ( 1s x.s B ) ) : No typesetting found for |- ( ( A x.s w ) = 1s -> ( ( A x.s w ) x.s B ) = ( 1s x.s B ) ) with typecode |-
5 4 adantl Could not format ( ( w e. No /\ ( A x.s w ) = 1s ) -> ( ( A x.s w ) x.s B ) = ( 1s x.s B ) ) : No typesetting found for |- ( ( w e. No /\ ( A x.s w ) = 1s ) -> ( ( A x.s w ) x.s B ) = ( 1s x.s B ) ) with typecode |-
6 5 adantl Could not format ( ( ( A e. No /\ A =/= 0s /\ B e. No ) /\ ( w e. No /\ ( A x.s w ) = 1s ) ) -> ( ( A x.s w ) x.s B ) = ( 1s x.s B ) ) : No typesetting found for |- ( ( ( A e. No /\ A =/= 0s /\ B e. No ) /\ ( w e. No /\ ( A x.s w ) = 1s ) ) -> ( ( A x.s w ) x.s B ) = ( 1s x.s B ) ) with typecode |-
7 simpl1 Could not format ( ( ( A e. No /\ A =/= 0s /\ B e. No ) /\ ( w e. No /\ ( A x.s w ) = 1s ) ) -> A e. No ) : No typesetting found for |- ( ( ( A e. No /\ A =/= 0s /\ B e. No ) /\ ( w e. No /\ ( A x.s w ) = 1s ) ) -> A e. No ) with typecode |-
8 7 1 2 mulsassd Could not format ( ( ( A e. No /\ A =/= 0s /\ B e. No ) /\ ( w e. No /\ ( A x.s w ) = 1s ) ) -> ( ( A x.s w ) x.s B ) = ( A x.s ( w x.s B ) ) ) : No typesetting found for |- ( ( ( A e. No /\ A =/= 0s /\ B e. No ) /\ ( w e. No /\ ( A x.s w ) = 1s ) ) -> ( ( A x.s w ) x.s B ) = ( A x.s ( w x.s B ) ) ) with typecode |-
9 2 mulslidd Could not format ( ( ( A e. No /\ A =/= 0s /\ B e. No ) /\ ( w e. No /\ ( A x.s w ) = 1s ) ) -> ( 1s x.s B ) = B ) : No typesetting found for |- ( ( ( A e. No /\ A =/= 0s /\ B e. No ) /\ ( w e. No /\ ( A x.s w ) = 1s ) ) -> ( 1s x.s B ) = B ) with typecode |-
10 6 8 9 3eqtr3d Could not format ( ( ( A e. No /\ A =/= 0s /\ B e. No ) /\ ( w e. No /\ ( A x.s w ) = 1s ) ) -> ( A x.s ( w x.s B ) ) = B ) : No typesetting found for |- ( ( ( A e. No /\ A =/= 0s /\ B e. No ) /\ ( w e. No /\ ( A x.s w ) = 1s ) ) -> ( A x.s ( w x.s B ) ) = B ) with typecode |-
11 oveq2 Could not format ( z = ( w x.s B ) -> ( A x.s z ) = ( A x.s ( w x.s B ) ) ) : No typesetting found for |- ( z = ( w x.s B ) -> ( A x.s z ) = ( A x.s ( w x.s B ) ) ) with typecode |-
12 11 eqeq1d Could not format ( z = ( w x.s B ) -> ( ( A x.s z ) = B <-> ( A x.s ( w x.s B ) ) = B ) ) : No typesetting found for |- ( z = ( w x.s B ) -> ( ( A x.s z ) = B <-> ( A x.s ( w x.s B ) ) = B ) ) with typecode |-
13 12 rspcev Could not format ( ( ( w x.s B ) e. No /\ ( A x.s ( w x.s B ) ) = B ) -> E. z e. No ( A x.s z ) = B ) : No typesetting found for |- ( ( ( w x.s B ) e. No /\ ( A x.s ( w x.s B ) ) = B ) -> E. z e. No ( A x.s z ) = B ) with typecode |-
14 3 10 13 syl2anc Could not format ( ( ( A e. No /\ A =/= 0s /\ B e. No ) /\ ( w e. No /\ ( A x.s w ) = 1s ) ) -> E. z e. No ( A x.s z ) = B ) : No typesetting found for |- ( ( ( A e. No /\ A =/= 0s /\ B e. No ) /\ ( w e. No /\ ( A x.s w ) = 1s ) ) -> E. z e. No ( A x.s z ) = B ) with typecode |-
15 14 rexlimdvaa Could not format ( ( A e. No /\ A =/= 0s /\ B e. No ) -> ( E. w e. No ( A x.s w ) = 1s -> E. z e. No ( A x.s z ) = B ) ) : No typesetting found for |- ( ( A e. No /\ A =/= 0s /\ B e. No ) -> ( E. w e. No ( A x.s w ) = 1s -> E. z e. No ( A x.s z ) = B ) ) with typecode |-
16 15 imp Could not format ( ( ( A e. No /\ A =/= 0s /\ B e. No ) /\ E. w e. No ( A x.s w ) = 1s ) -> E. z e. No ( A x.s z ) = B ) : No typesetting found for |- ( ( ( A e. No /\ A =/= 0s /\ B e. No ) /\ E. w e. No ( A x.s w ) = 1s ) -> E. z e. No ( A x.s z ) = B ) with typecode |-
17 oveq2 Could not format ( x = w -> ( A x.s x ) = ( A x.s w ) ) : No typesetting found for |- ( x = w -> ( A x.s x ) = ( A x.s w ) ) with typecode |-
18 17 eqeq1d Could not format ( x = w -> ( ( A x.s x ) = 1s <-> ( A x.s w ) = 1s ) ) : No typesetting found for |- ( x = w -> ( ( A x.s x ) = 1s <-> ( A x.s w ) = 1s ) ) with typecode |-
19 18 cbvrexvw Could not format ( E. x e. No ( A x.s x ) = 1s <-> E. w e. No ( A x.s w ) = 1s ) : No typesetting found for |- ( E. x e. No ( A x.s x ) = 1s <-> E. w e. No ( A x.s w ) = 1s ) with typecode |-
20 19 anbi2i Could not format ( ( ( A e. No /\ A =/= 0s /\ B e. No ) /\ E. x e. No ( A x.s x ) = 1s ) <-> ( ( A e. No /\ A =/= 0s /\ B e. No ) /\ E. w e. No ( A x.s w ) = 1s ) ) : No typesetting found for |- ( ( ( A e. No /\ A =/= 0s /\ B e. No ) /\ E. x e. No ( A x.s x ) = 1s ) <-> ( ( A e. No /\ A =/= 0s /\ B e. No ) /\ E. w e. No ( A x.s w ) = 1s ) ) with typecode |-
21 oveq2 Could not format ( y = z -> ( A x.s y ) = ( A x.s z ) ) : No typesetting found for |- ( y = z -> ( A x.s y ) = ( A x.s z ) ) with typecode |-
22 21 eqeq1d Could not format ( y = z -> ( ( A x.s y ) = B <-> ( A x.s z ) = B ) ) : No typesetting found for |- ( y = z -> ( ( A x.s y ) = B <-> ( A x.s z ) = B ) ) with typecode |-
23 22 cbvrexvw Could not format ( E. y e. No ( A x.s y ) = B <-> E. z e. No ( A x.s z ) = B ) : No typesetting found for |- ( E. y e. No ( A x.s y ) = B <-> E. z e. No ( A x.s z ) = B ) with typecode |-
24 16 20 23 3imtr4i 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 |-