Metamath Proof Explorer

Theorem zs12negsclb

Description: A surreal is a dyadic fraction iff its negative is. (Contributed by Scott Fenton, 9-Nov-2025)

Ref Expression
Assertion zs12negsclb 
|- ( A e. No -> ( A e. ZZ_s[1/2] <-> ( -us ` A ) e. ZZ_s[1/2] ) )

Proof

Step Hyp Ref Expression
1 zs12negscl 
 |-  ( A e. ZZ_s[1/2] -> ( -us ` A ) e. ZZ_s[1/2] )
2 zs12negscl 
 |-  ( ( -us ` A ) e. ZZ_s[1/2] -> ( -us ` ( -us ` A ) ) e. ZZ_s[1/2] )
3 negnegs 
 |-  ( A e. No -> ( -us ` ( -us ` A ) ) = A )
4 3 eleq1d 
 |-  ( A e. No -> ( ( -us ` ( -us ` A ) ) e. ZZ_s[1/2] <-> A e. ZZ_s[1/2] ) )
5 2 4 imbitrid 
 |-  ( A e. No -> ( ( -us ` A ) e. ZZ_s[1/2] -> A e. ZZ_s[1/2] ) )
6 1 5 impbid2 
 |-  ( A e. No -> ( A e. ZZ_s[1/2] <-> ( -us ` A ) e. ZZ_s[1/2] ) )