Theorem zs12negsclb

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

	Ref	Expression
Assertion	zs12negsclb	Could not format assertion : No typesetting found for |- ( A e. No -> ( A e. ZZ_s[1/2] <-> ( -us ` A ) e. ZZ_s[1/2] ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		zs12negscl	Could not format ( A e. ZZ_s[1/2] -> ( -us ` A ) e. ZZ_s[1/2] ) : No typesetting found for |- ( A e. ZZ_s[1/2] -> ( -us ` A ) e. ZZ_s[1/2] ) with typecode |-
2		zs12negscl	Could not format ( ( -us ` A ) e. ZZ_s[1/2] -> ( -us ` ( -us ` A ) ) e. ZZ_s[1/2] ) : No typesetting found for |- ( ( -us ` A ) e. ZZ_s[1/2] -> ( -us ` ( -us ` A ) ) e. ZZ_s[1/2] ) with typecode |-
3		negnegs	$$⊢A\in \mathrm{No}\to {+}_s\left({+}_s\left(A\right)\right)=A$$
4	3	eleq1d	Could not format ( A e. No -> ( ( -us ` ( -us ` A ) ) e. ZZ_s[1/2] <-> A e. ZZ_s[1/2] ) ) : No typesetting found for |- ( A e. No -> ( ( -us ` ( -us ` A ) ) e. ZZ_s[1/2] <-> A e. ZZ_s[1/2] ) ) with typecode |-
5	2 4	imbitrid	Could not format ( A e. No -> ( ( -us ` A ) e. ZZ_s[1/2] -> A e. ZZ_s[1/2] ) ) : No typesetting found for |- ( A e. No -> ( ( -us ` A ) e. ZZ_s[1/2] -> A e. ZZ_s[1/2] ) ) with typecode |-
6	1 5	impbid2	Could not format ( A e. No -> ( A e. ZZ_s[1/2] <-> ( -us ` A ) e. ZZ_s[1/2] ) ) : No typesetting found for |- ( A e. No -> ( A e. ZZ_s[1/2] <-> ( -us ` A ) e. ZZ_s[1/2] ) ) with typecode |-