Metamath Proof Explorer

Theorem precsex

Description: Every positive surreal has a reciprocal. Theorem 10(iv) of Conway p. 21. (Contributed by Scott Fenton, 15-Mar-2025)

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

Proof

Step Hyp Ref Expression
1 breq2 
 |-  ( z = xO -> ( 0s  0s
2 oveq1 
 |-  ( z = xO -> ( z x.s y ) = ( xO x.s y ) )
3 2 eqeq1d 
 |-  ( z = xO -> ( ( z x.s y ) = 1s <-> ( xO x.s y ) = 1s ) )
4 3 rexbidv 
 |-  ( z = xO -> ( E. y e. No ( z x.s y ) = 1s <-> E. y e. No ( xO x.s y ) = 1s ) )
5 1 4 imbi12d 
 |-  ( z = xO -> ( ( 0s  E. y e. No ( z x.s y ) = 1s ) <-> ( 0s  E. y e. No ( xO x.s y ) = 1s ) ) )
6 breq2 
 |-  ( z = A -> ( 0s  0s
7 oveq1 
 |-  ( z = A -> ( z x.s y ) = ( A x.s y ) )
8 7 eqeq1d 
 |-  ( z = A -> ( ( z x.s y ) = 1s <-> ( A x.s y ) = 1s ) )
9 8 rexbidv 
 |-  ( z = A -> ( E. y e. No ( z x.s y ) = 1s <-> E. y e. No ( A x.s y ) = 1s ) )
10 6 9 imbi12d 
 |-  ( z = A -> ( ( 0s  E. y e. No ( z x.s y ) = 1s ) <-> ( 0s  E. y e. No ( A x.s y ) = 1s ) ) )
11 eqid 
 |-  rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) = rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. )
12 11 precsexlemcbv 
 |-  rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) = rec ( ( p e. _V |-> [_ ( 1st ` p ) / l ]_ [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` z ) E. yL e. l a = ( ( 1s +s ( ( xR -s z ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. )
13 eqid 
 |-  ( 1st o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) = ( 1st o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) )
14 eqid 
 |-  ( 2nd o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) = ( 2nd o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) )
15 simp1 
 |-  ( ( z e. No /\ 0s  E. y e. No ( xO x.s y ) = 1s ) ) -> z e. No )
16 simp2 
 |-  ( ( z e. No /\ 0s  E. y e. No ( xO x.s y ) = 1s ) ) -> 0s
17 simp3 
 |-  ( ( z e. No /\ 0s  E. y e. No ( xO x.s y ) = 1s ) ) -> A. xO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( 0s  E. y e. No ( xO x.s y ) = 1s ) )
18 12 13 14 15 16 17 precsexlem10 
 |-  ( ( z e. No /\ 0s  E. y e. No ( xO x.s y ) = 1s ) ) -> U. ( ( 1st o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) < [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) )
19 18 scutcld 
 |-  ( ( z e. No /\ 0s  E. y e. No ( xO x.s y ) = 1s ) ) -> ( U. ( ( 1st o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) |s U. ( ( 2nd o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) ) e. No )
20 eqid 
 |-  ( U. ( ( 1st o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) |s U. ( ( 2nd o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) ) = ( U. ( ( 1st o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) |s U. ( ( 2nd o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) )
21 12 13 14 15 16 17 20 precsexlem11 
 |-  ( ( z e. No /\ 0s  E. y e. No ( xO x.s y ) = 1s ) ) -> ( z x.s ( U. ( ( 1st o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) |s U. ( ( 2nd o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) ) ) = 1s )
22 oveq2 
 |-  ( y = ( U. ( ( 1st o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) |s U. ( ( 2nd o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) ) -> ( z x.s y ) = ( z x.s ( U. ( ( 1st o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) |s U. ( ( 2nd o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) ) ) )
23 22 eqeq1d 
 |-  ( y = ( U. ( ( 1st o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) |s U. ( ( 2nd o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) ) -> ( ( z x.s y ) = 1s <-> ( z x.s ( U. ( ( 1st o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) |s U. ( ( 2nd o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) ) ) = 1s ) )
24 23 rspcev 
 |-  ( ( ( U. ( ( 1st o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) |s U. ( ( 2nd o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) ) e. No /\ ( z x.s ( U. ( ( 1st o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) |s U. ( ( 2nd o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) ) ) = 1s ) -> E. y e. No ( z x.s y ) = 1s )
25 19 21 24 syl2anc 
 |-  ( ( z e. No /\ 0s  E. y e. No ( xO x.s y ) = 1s ) ) -> E. y e. No ( z x.s y ) = 1s )
26 25 3exp 
 |-  ( z e. No -> ( 0s  ( A. xO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( 0s  E. y e. No ( xO x.s y ) = 1s ) -> E. y e. No ( z x.s y ) = 1s ) ) )
27 26 com23 
 |-  ( z e. No -> ( A. xO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( 0s  E. y e. No ( xO x.s y ) = 1s ) -> ( 0s  E. y e. No ( z x.s y ) = 1s ) ) )
28 5 10 27 noinds 
 |-  ( A e. No -> ( 0s  E. y e. No ( A x.s y ) = 1s ) )
29 28 imp 
 |-  ( ( A e. No /\ 0s  E. y e. No ( A x.s y ) = 1s )