Metamath Proof Explorer

Theorem recsne0

Description: If a surreal has a reciprocal, then it is non-zero. (Contributed by Scott Fenton, 5-Sep-2025)

Ref Expression
Hypotheses recsne0.1 
|- ( ph -> A e. No )
recsne0.2 
|- ( ph -> E. x e. No ( A x.s x ) = 1s )
Assertion recsne0 
|- ( ph -> A =/= 0s )

Proof

Step Hyp Ref Expression
1 recsne0.1 
 |-  ( ph -> A e. No )
2 recsne0.2 
 |-  ( ph -> E. x e. No ( A x.s x ) = 1s )
3 oveq2 
 |-  ( x = y -> ( A x.s x ) = ( A x.s y ) )
4 3 eqeq1d 
 |-  ( x = y -> ( ( A x.s x ) = 1s <-> ( A x.s y ) = 1s ) )
5 4 cbvrexvw 
 |-  ( E. x e. No ( A x.s x ) = 1s <-> E. y e. No ( A x.s y ) = 1s )
6 2 5 sylib 
 |-  ( ph -> E. y e. No ( A x.s y ) = 1s )
7 simprr 
 |-  ( ( ph /\ ( y e. No /\ ( A x.s y ) = 1s ) ) -> ( A x.s y ) = 1s )
8 1sne0s 
 |-  1s =/= 0s
9 8 a1i 
 |-  ( ( ph /\ ( y e. No /\ ( A x.s y ) = 1s ) ) -> 1s =/= 0s )
10 7 9 eqnetrd 
 |-  ( ( ph /\ ( y e. No /\ ( A x.s y ) = 1s ) ) -> ( A x.s y ) =/= 0s )
11 1 adantr 
 |-  ( ( ph /\ ( y e. No /\ ( A x.s y ) = 1s ) ) -> A e. No )
12 simprl 
 |-  ( ( ph /\ ( y e. No /\ ( A x.s y ) = 1s ) ) -> y e. No )
13 11 12 mulsne0bd 
 |-  ( ( ph /\ ( y e. No /\ ( A x.s y ) = 1s ) ) -> ( ( A x.s y ) =/= 0s <-> ( A =/= 0s /\ y =/= 0s ) ) )
14 10 13 mpbid 
 |-  ( ( ph /\ ( y e. No /\ ( A x.s y ) = 1s ) ) -> ( A =/= 0s /\ y =/= 0s ) )
15 14 simpld 
 |-  ( ( ph /\ ( y e. No /\ ( A x.s y ) = 1s ) ) -> A =/= 0s )
16 6 15 rexlimddv 
 |-  ( ph -> A =/= 0s )