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