Theorem zs12negscl

Description: The dyadics are closed under negation. (Contributed by Scott Fenton, 9-Nov-2025)

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

Proof

Step	Hyp	Ref	Expression
1		oveq1	Could not format ( z = ( -us ` x ) -> ( z /su ( 2s ^su y ) ) = ( ( -us ` x ) /su ( 2s ^su y ) ) ) : No typesetting found for |- ( z = ( -us ` x ) -> ( z /su ( 2s ^su y ) ) = ( ( -us ` x ) /su ( 2s ^su y ) ) ) with typecode |-
2	1	eqeq2d	Could not format ( z = ( -us ` x ) -> ( ( -us ` ( x /su ( 2s ^su y ) ) ) = ( z /su ( 2s ^su y ) ) <-> ( -us ` ( x /su ( 2s ^su y ) ) ) = ( ( -us ` x ) /su ( 2s ^su y ) ) ) ) : No typesetting found for |- ( z = ( -us ` x ) -> ( ( -us ` ( x /su ( 2s ^su y ) ) ) = ( z /su ( 2s ^su y ) ) <-> ( -us ` ( x /su ( 2s ^su y ) ) ) = ( ( -us ` x ) /su ( 2s ^su y ) ) ) ) with typecode |-
3		znegscl	$$⊢x\in {\mathbb{Z}}_s\to {+}_s\left(x\right)\in {\mathbb{Z}}_s$$
4	3	adantl	$$⊢\left(y\in {\mathbb{N}}_{\mathrm{0s}}\wedge x\in {\mathbb{Z}}_s\right)\to {+}_s\left(x\right)\in {\mathbb{Z}}_s$$
5		zno	$$⊢x\in {\mathbb{Z}}_s\to x\in \mathrm{No}$$
6	5	adantl	$$⊢\left(y\in {\mathbb{N}}_{\mathrm{0s}}\wedge x\in {\mathbb{Z}}_s\right)\to x\in \mathrm{No}$$
7		simpl	$$⊢\left(y\in {\mathbb{N}}_{\mathrm{0s}}\wedge x\in {\mathbb{Z}}_s\right)\to y\in {\mathbb{N}}_{\mathrm{0s}}$$
8	6 7	pw2divsnegd	Could not format ( ( y e. NN0_s /\ x e. ZZ_s ) -> ( -us ` ( x /su ( 2s ^su y ) ) ) = ( ( -us ` x ) /su ( 2s ^su y ) ) ) : No typesetting found for |- ( ( y e. NN0_s /\ x e. ZZ_s ) -> ( -us ` ( x /su ( 2s ^su y ) ) ) = ( ( -us ` x ) /su ( 2s ^su y ) ) ) with typecode |-
9	2 4 8	rspcedvdw	Could not format ( ( y e. NN0_s /\ x e. ZZ_s ) -> E. z e. ZZ_s ( -us ` ( x /su ( 2s ^su y ) ) ) = ( z /su ( 2s ^su y ) ) ) : No typesetting found for |- ( ( y e. NN0_s /\ x e. ZZ_s ) -> E. z e. ZZ_s ( -us ` ( x /su ( 2s ^su y ) ) ) = ( z /su ( 2s ^su y ) ) ) with typecode |-
10		fveq2	Could not format ( A = ( x /su ( 2s ^su y ) ) -> ( -us ` A ) = ( -us ` ( x /su ( 2s ^su y ) ) ) ) : No typesetting found for |- ( A = ( x /su ( 2s ^su y ) ) -> ( -us ` A ) = ( -us ` ( x /su ( 2s ^su y ) ) ) ) with typecode |-
11	10	eqeq1d	Could not format ( A = ( x /su ( 2s ^su y ) ) -> ( ( -us ` A ) = ( z /su ( 2s ^su y ) ) <-> ( -us ` ( x /su ( 2s ^su y ) ) ) = ( z /su ( 2s ^su y ) ) ) ) : No typesetting found for |- ( A = ( x /su ( 2s ^su y ) ) -> ( ( -us ` A ) = ( z /su ( 2s ^su y ) ) <-> ( -us ` ( x /su ( 2s ^su y ) ) ) = ( z /su ( 2s ^su y ) ) ) ) with typecode |-
12	11	rexbidv	Could not format ( A = ( x /su ( 2s ^su y ) ) -> ( E. z e. ZZ_s ( -us ` A ) = ( z /su ( 2s ^su y ) ) <-> E. z e. ZZ_s ( -us ` ( x /su ( 2s ^su y ) ) ) = ( z /su ( 2s ^su y ) ) ) ) : No typesetting found for |- ( A = ( x /su ( 2s ^su y ) ) -> ( E. z e. ZZ_s ( -us ` A ) = ( z /su ( 2s ^su y ) ) <-> E. z e. ZZ_s ( -us ` ( x /su ( 2s ^su y ) ) ) = ( z /su ( 2s ^su y ) ) ) ) with typecode |-
13	9 12	syl5ibrcom	Could not format ( ( y e. NN0_s /\ x e. ZZ_s ) -> ( A = ( x /su ( 2s ^su y ) ) -> E. z e. ZZ_s ( -us ` A ) = ( z /su ( 2s ^su y ) ) ) ) : No typesetting found for |- ( ( y e. NN0_s /\ x e. ZZ_s ) -> ( A = ( x /su ( 2s ^su y ) ) -> E. z e. ZZ_s ( -us ` A ) = ( z /su ( 2s ^su y ) ) ) ) with typecode |-
14	13	rexlimdva	Could not format ( y e. NN0_s -> ( E. x e. ZZ_s A = ( x /su ( 2s ^su y ) ) -> E. z e. ZZ_s ( -us ` A ) = ( z /su ( 2s ^su y ) ) ) ) : No typesetting found for |- ( y e. NN0_s -> ( E. x e. ZZ_s A = ( x /su ( 2s ^su y ) ) -> E. z e. ZZ_s ( -us ` A ) = ( z /su ( 2s ^su y ) ) ) ) with typecode |-
15	14	reximia	Could not format ( E. y e. NN0_s E. x e. ZZ_s A = ( x /su ( 2s ^su y ) ) -> E. y e. NN0_s E. z e. ZZ_s ( -us ` A ) = ( z /su ( 2s ^su y ) ) ) : No typesetting found for |- ( E. y e. NN0_s E. x e. ZZ_s A = ( x /su ( 2s ^su y ) ) -> E. y e. NN0_s E. z e. ZZ_s ( -us ` A ) = ( z /su ( 2s ^su y ) ) ) with typecode |-
16		elzs12	Could not format ( A e. ZZ_s[1/2] <-> E. x e. ZZ_s E. y e. NN0_s A = ( x /su ( 2s ^su y ) ) ) : No typesetting found for |- ( A e. ZZ_s[1/2] <-> E. x e. ZZ_s E. y e. NN0_s A = ( x /su ( 2s ^su y ) ) ) with typecode |-
17		rexcom	Could not format ( E. x e. ZZ_s E. y e. NN0_s A = ( x /su ( 2s ^su y ) ) <-> E. y e. NN0_s E. x e. ZZ_s A = ( x /su ( 2s ^su y ) ) ) : No typesetting found for |- ( E. x e. ZZ_s E. y e. NN0_s A = ( x /su ( 2s ^su y ) ) <-> E. y e. NN0_s E. x e. ZZ_s A = ( x /su ( 2s ^su y ) ) ) with typecode |-
18	16 17	bitri	Could not format ( A e. ZZ_s[1/2] <-> E. y e. NN0_s E. x e. ZZ_s A = ( x /su ( 2s ^su y ) ) ) : No typesetting found for |- ( A e. ZZ_s[1/2] <-> E. y e. NN0_s E. x e. ZZ_s A = ( x /su ( 2s ^su y ) ) ) with typecode |-
19		elzs12	Could not format ( ( -us ` A ) e. ZZ_s[1/2] <-> E. z e. ZZ_s E. y e. NN0_s ( -us ` A ) = ( z /su ( 2s ^su y ) ) ) : No typesetting found for |- ( ( -us ` A ) e. ZZ_s[1/2] <-> E. z e. ZZ_s E. y e. NN0_s ( -us ` A ) = ( z /su ( 2s ^su y ) ) ) with typecode |-
20		rexcom	Could not format ( E. z e. ZZ_s E. y e. NN0_s ( -us ` A ) = ( z /su ( 2s ^su y ) ) <-> E. y e. NN0_s E. z e. ZZ_s ( -us ` A ) = ( z /su ( 2s ^su y ) ) ) : No typesetting found for |- ( E. z e. ZZ_s E. y e. NN0_s ( -us ` A ) = ( z /su ( 2s ^su y ) ) <-> E. y e. NN0_s E. z e. ZZ_s ( -us ` A ) = ( z /su ( 2s ^su y ) ) ) with typecode |-
21	19 20	bitri	Could not format ( ( -us ` A ) e. ZZ_s[1/2] <-> E. y e. NN0_s E. z e. ZZ_s ( -us ` A ) = ( z /su ( 2s ^su y ) ) ) : No typesetting found for |- ( ( -us ` A ) e. ZZ_s[1/2] <-> E. y e. NN0_s E. z e. ZZ_s ( -us ` A ) = ( z /su ( 2s ^su y ) ) ) with typecode |-
22	15 18 21	3imtr4i	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 |-