Metamath Proof Explorer

Theorem recsex

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

Ref Expression
Assertion recsex Could not format assertion : No typesetting found for |- ( ( A e. No /\ A =/= 0s ) -> E. x e. No ( A x.s x ) = 1s ) with typecode |-

Proof

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