Metamath Proof Explorer

Theorem zs12negscl

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

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

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( z = ( -us ` x ) -> ( z /su ( 2s ^su y ) ) = ( ( -us ` x ) /su ( 2s ^su y ) ) )
2 1 eqeq2d 
 |-  ( 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 ) ) ) )
3 znegscl 
 |-  ( x e. ZZ_s -> ( -us ` x ) e. ZZ_s )
4 3 adantl 
 |-  ( ( y e. NN0_s /\ x e. ZZ_s ) -> ( -us ` x ) e. ZZ_s )
5 zno 
 |-  ( x e. ZZ_s -> x e. No )
6 5 adantl 
 |-  ( ( y e. NN0_s /\ x e. ZZ_s ) -> x e. No )
7 simpl 
 |-  ( ( y e. NN0_s /\ x e. ZZ_s ) -> y e. NN0_s )
8 6 7 pw2divsnegd 
 |-  ( ( y e. NN0_s /\ x e. ZZ_s ) -> ( -us ` ( x /su ( 2s ^su y ) ) ) = ( ( -us ` x ) /su ( 2s ^su y ) ) )
9 2 4 8 rspcedvdw 
 |-  ( ( y e. NN0_s /\ x e. ZZ_s ) -> E. z e. ZZ_s ( -us ` ( x /su ( 2s ^su y ) ) ) = ( z /su ( 2s ^su y ) ) )
10 fveq2 
 |-  ( A = ( x /su ( 2s ^su y ) ) -> ( -us ` A ) = ( -us ` ( x /su ( 2s ^su y ) ) ) )
11 10 eqeq1d 
 |-  ( A = ( x /su ( 2s ^su y ) ) -> ( ( -us ` A ) = ( z /su ( 2s ^su y ) ) <-> ( -us ` ( x /su ( 2s ^su y ) ) ) = ( z /su ( 2s ^su y ) ) ) )
12 11 rexbidv 
 |-  ( 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 ) ) ) )
13 9 12 syl5ibrcom 
 |-  ( ( 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 ) ) ) )
14 13 rexlimdva 
 |-  ( 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 ) ) ) )
15 14 reximia 
 |-  ( 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 ) ) )
16 elzs12 
 |-  ( A e. ZZ_s[1/2] <-> E. x e. ZZ_s E. y e. NN0_s A = ( x /su ( 2s ^su y ) ) )
17 rexcom 
 |-  ( 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 ) ) )
18 16 17 bitri 
 |-  ( A e. ZZ_s[1/2] <-> E. y e. NN0_s E. x e. ZZ_s A = ( x /su ( 2s ^su y ) ) )
19 elzs12 
 |-  ( ( -us ` A ) e. ZZ_s[1/2] <-> E. z e. ZZ_s E. y e. NN0_s ( -us ` A ) = ( z /su ( 2s ^su y ) ) )
20 rexcom 
 |-  ( 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 ) ) )
21 19 20 bitri 
 |-  ( ( -us ` A ) e. ZZ_s[1/2] <-> E. y e. NN0_s E. z e. ZZ_s ( -us ` A ) = ( z /su ( 2s ^su y ) ) )
22 15 18 21 3imtr4i 
 |-  ( A e. ZZ_s[1/2] -> ( -us ` A ) e. ZZ_s[1/2] )