Theorem zs12negsclb

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

	Ref	Expression
Assertion	zs12negsclb	⊢ ( 𝐴 ∈ No → ( 𝐴 ∈ ℤs[1/2] ↔ ( -us ‘ 𝐴 ) ∈ ℤs[1/2] ) )

Proof

Step	Hyp	Ref	Expression
1		zs12negscl	⊢ ( 𝐴 ∈ ℤs[1/2] → ( -us ‘ 𝐴 ) ∈ ℤs[1/2] )
2		zs12negscl	⊢ ( ( -us ‘ 𝐴 ) ∈ ℤs[1/2] → ( -us ‘ ( -us ‘ 𝐴 ) ) ∈ ℤs[1/2] )
3		negnegs	⊢ ( 𝐴 ∈ No → ( -us ‘ ( -us ‘ 𝐴 ) ) = 𝐴 )
4	3	eleq1d	⊢ ( 𝐴 ∈ No → ( ( -us ‘ ( -us ‘ 𝐴 ) ) ∈ ℤs[1/2] ↔ 𝐴 ∈ ℤs[1/2] ) )
5	2 4	imbitrid	⊢ ( 𝐴 ∈ No → ( ( -us ‘ 𝐴 ) ∈ ℤs[1/2] → 𝐴 ∈ ℤs[1/2] ) )
6	1 5	impbid2	⊢ ( 𝐴 ∈ No → ( 𝐴 ∈ ℤs[1/2] ↔ ( -us ‘ 𝐴 ) ∈ ℤs[1/2] ) )