Metamath Proof Explorer

Theorem recsex

Description: A non-zero surreal has a reciprocal. (Contributed by Scott Fenton, 15-Mar-2025)

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

Proof

Step Hyp Ref Expression
1 0sno 
 |-  0s e. No
2 slttrine 
 |-  ( ( A e. No /\ 0s e. No ) -> ( A =/= 0s <-> ( A
3 1 2 mpan2 
 |-  ( A e. No -> ( A =/= 0s <-> ( A
4 sltneg 
 |-  ( ( A e. No /\ 0s e. No ) -> ( A  ( -us ` 0s )
5 1 4 mpan2 
 |-  ( A e. No -> ( A  ( -us ` 0s )
6 negs0s 
 |-  ( -us ` 0s ) = 0s
7 6 breq1i 
 |-  ( ( -us ` 0s )  0s
8 5 7 bitrdi 
 |-  ( A e. No -> ( A  0s
9 negscl 
 |-  ( A e. No -> ( -us ` A ) e. No )
10 precsex 
 |-  ( ( ( -us ` A ) e. No /\ 0s  E. y e. No ( ( -us ` A ) x.s y ) = 1s )
11 9 10 sylan 
 |-  ( ( A e. No /\ 0s  E. y e. No ( ( -us ` A ) x.s y ) = 1s )
12 simprl 
 |-  ( ( ( A e. No /\ 0s  y e. No )
13 12 negscld 
 |-  ( ( ( A e. No /\ 0s  ( -us ` y ) e. No )
14 simpll 
 |-  ( ( ( A e. No /\ 0s  A e. No )
15 simpr 
 |-  ( ( ( A e. No /\ 0s  y e. No )
16 14 15 mulnegs1d 
 |-  ( ( ( A e. No /\ 0s  ( ( -us ` A ) x.s y ) = ( -us ` ( A x.s y ) ) )
17 14 15 mulnegs2d 
 |-  ( ( ( A e. No /\ 0s  ( A x.s ( -us ` y ) ) = ( -us ` ( A x.s y ) ) )
18 16 17 eqtr4d 
 |-  ( ( ( A e. No /\ 0s  ( ( -us ` A ) x.s y ) = ( A x.s ( -us ` y ) ) )
19 18 eqeq1d 
 |-  ( ( ( A e. No /\ 0s  ( ( ( -us ` A ) x.s y ) = 1s <-> ( A x.s ( -us ` y ) ) = 1s ) )
20 19 biimpd 
 |-  ( ( ( A e. No /\ 0s  ( ( ( -us ` A ) x.s y ) = 1s -> ( A x.s ( -us ` y ) ) = 1s ) )
21 20 impr 
 |-  ( ( ( A e. No /\ 0s  ( A x.s ( -us ` y ) ) = 1s )
22 oveq2 
 |-  ( x = ( -us ` y ) -> ( A x.s x ) = ( A x.s ( -us ` y ) ) )
23 22 eqeq1d 
 |-  ( x = ( -us ` y ) -> ( ( A x.s x ) = 1s <-> ( A x.s ( -us ` y ) ) = 1s ) )
24 23 rspcev 
 |-  ( ( ( -us ` y ) e. No /\ ( A x.s ( -us ` y ) ) = 1s ) -> E. x e. No ( A x.s x ) = 1s )
25 13 21 24 syl2anc 
 |-  ( ( ( A e. No /\ 0s  E. x e. No ( A x.s x ) = 1s )
26 11 25 rexlimddv 
 |-  ( ( A e. No /\ 0s  E. x e. No ( A x.s x ) = 1s )
27 26 ex 
 |-  ( A e. No -> ( 0s  E. x e. No ( A x.s x ) = 1s ) )
28 8 27 sylbid 
 |-  ( A e. No -> ( A  E. x e. No ( A x.s x ) = 1s ) )
29 precsex 
 |-  ( ( A e. No /\ 0s  E. x e. No ( A x.s x ) = 1s )
30 29 ex 
 |-  ( A e. No -> ( 0s  E. x e. No ( A x.s x ) = 1s ) )
31 28 30 jaod 
 |-  ( A e. No -> ( ( A  E. x e. No ( A x.s x ) = 1s ) )
32 3 31 sylbid 
 |-  ( A e. No -> ( A =/= 0s -> E. x e. No ( A x.s x ) = 1s ) )
33 32 imp 
 |-  ( ( A e. No /\ A =/= 0s ) -> E. x e. No ( A x.s x ) = 1s )