Metamath Proof Explorer

Theorem zs12half

Description: Half of a dyadic is a dyadic. (Contributed by Scott Fenton, 11-Dec-2025)

Ref Expression
Assertion zs12half 
|- ( A e. ZZ_s[1/2] -> ( A /su 2s ) e. ZZ_s[1/2] )

Proof

Step Hyp Ref Expression
1 elzs12 
 |-  ( A e. ZZ_s[1/2] <-> E. a e. ZZ_s E. n e. NN0_s A = ( a /su ( 2s ^su n ) ) )
2 2sno 
 |-  2s e. No
3 exps1 
 |-  ( 2s e. No -> ( 2s ^su 1s ) = 2s )
4 2 3 ax-mp 
 |-  ( 2s ^su 1s ) = 2s
5 4 oveq2i 
 |-  ( ( a /su ( 2s ^su n ) ) /su ( 2s ^su 1s ) ) = ( ( a /su ( 2s ^su n ) ) /su 2s )
6 zno 
 |-  ( a e. ZZ_s -> a e. No )
7 6 adantr 
 |-  ( ( a e. ZZ_s /\ n e. NN0_s ) -> a e. No )
8 simpr 
 |-  ( ( a e. ZZ_s /\ n e. NN0_s ) -> n e. NN0_s )
9 1n0s 
 |-  1s e. NN0_s
10 9 a1i 
 |-  ( ( a e. ZZ_s /\ n e. NN0_s ) -> 1s e. NN0_s )
11 7 8 10 pw2divscan4d 
 |-  ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( a /su ( 2s ^su n ) ) = ( ( ( 2s ^su 1s ) x.s a ) /su ( 2s ^su ( n +s 1s ) ) ) )
12 4 2 eqeltri 
 |-  ( 2s ^su 1s ) e. No
13 12 a1i 
 |-  ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( 2s ^su 1s ) e. No )
14 peano2n0s 
 |-  ( n e. NN0_s -> ( n +s 1s ) e. NN0_s )
15 14 adantl 
 |-  ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( n +s 1s ) e. NN0_s )
16 13 7 15 pw2divsassd 
 |-  ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( ( ( 2s ^su 1s ) x.s a ) /su ( 2s ^su ( n +s 1s ) ) ) = ( ( 2s ^su 1s ) x.s ( a /su ( 2s ^su ( n +s 1s ) ) ) ) )
17 11 16 eqtr2d 
 |-  ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( ( 2s ^su 1s ) x.s ( a /su ( 2s ^su ( n +s 1s ) ) ) ) = ( a /su ( 2s ^su n ) ) )
18 7 8 pw2divscld 
 |-  ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( a /su ( 2s ^su n ) ) e. No )
19 7 15 pw2divscld 
 |-  ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( a /su ( 2s ^su ( n +s 1s ) ) ) e. No )
20 18 19 10 pw2divsmuld 
 |-  ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( ( ( a /su ( 2s ^su n ) ) /su ( 2s ^su 1s ) ) = ( a /su ( 2s ^su ( n +s 1s ) ) ) <-> ( ( 2s ^su 1s ) x.s ( a /su ( 2s ^su ( n +s 1s ) ) ) ) = ( a /su ( 2s ^su n ) ) ) )
21 17 20 mpbird 
 |-  ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( ( a /su ( 2s ^su n ) ) /su ( 2s ^su 1s ) ) = ( a /su ( 2s ^su ( n +s 1s ) ) ) )
22 5 21 eqtr3id 
 |-  ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( ( a /su ( 2s ^su n ) ) /su 2s ) = ( a /su ( 2s ^su ( n +s 1s ) ) ) )
23 oveq1 
 |-  ( b = a -> ( b /su ( 2s ^su m ) ) = ( a /su ( 2s ^su m ) ) )
24 23 eqeq2d 
 |-  ( b = a -> ( ( a /su ( 2s ^su ( n +s 1s ) ) ) = ( b /su ( 2s ^su m ) ) <-> ( a /su ( 2s ^su ( n +s 1s ) ) ) = ( a /su ( 2s ^su m ) ) ) )
25 oveq2 
 |-  ( m = ( n +s 1s ) -> ( 2s ^su m ) = ( 2s ^su ( n +s 1s ) ) )
26 25 oveq2d 
 |-  ( m = ( n +s 1s ) -> ( a /su ( 2s ^su m ) ) = ( a /su ( 2s ^su ( n +s 1s ) ) ) )
27 26 eqeq2d 
 |-  ( m = ( n +s 1s ) -> ( ( a /su ( 2s ^su ( n +s 1s ) ) ) = ( a /su ( 2s ^su m ) ) <-> ( a /su ( 2s ^su ( n +s 1s ) ) ) = ( a /su ( 2s ^su ( n +s 1s ) ) ) ) )
28 simpl 
 |-  ( ( a e. ZZ_s /\ n e. NN0_s ) -> a e. ZZ_s )
29 eqidd 
 |-  ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( a /su ( 2s ^su ( n +s 1s ) ) ) = ( a /su ( 2s ^su ( n +s 1s ) ) ) )
30 24 27 28 15 29 2rspcedvdw 
 |-  ( ( a e. ZZ_s /\ n e. NN0_s ) -> E. b e. ZZ_s E. m e. NN0_s ( a /su ( 2s ^su ( n +s 1s ) ) ) = ( b /su ( 2s ^su m ) ) )
31 elzs12 
 |-  ( ( a /su ( 2s ^su ( n +s 1s ) ) ) e. ZZ_s[1/2] <-> E. b e. ZZ_s E. m e. NN0_s ( a /su ( 2s ^su ( n +s 1s ) ) ) = ( b /su ( 2s ^su m ) ) )
32 30 31 sylibr 
 |-  ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( a /su ( 2s ^su ( n +s 1s ) ) ) e. ZZ_s[1/2] )
33 22 32 eqeltrd 
 |-  ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( ( a /su ( 2s ^su n ) ) /su 2s ) e. ZZ_s[1/2] )
34 oveq1 
 |-  ( A = ( a /su ( 2s ^su n ) ) -> ( A /su 2s ) = ( ( a /su ( 2s ^su n ) ) /su 2s ) )
35 34 eleq1d 
 |-  ( A = ( a /su ( 2s ^su n ) ) -> ( ( A /su 2s ) e. ZZ_s[1/2] <-> ( ( a /su ( 2s ^su n ) ) /su 2s ) e. ZZ_s[1/2] ) )
36 33 35 syl5ibrcom 
 |-  ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( A = ( a /su ( 2s ^su n ) ) -> ( A /su 2s ) e. ZZ_s[1/2] ) )
37 36 rexlimivv 
 |-  ( E. a e. ZZ_s E. n e. NN0_s A = ( a /su ( 2s ^su n ) ) -> ( A /su 2s ) e. ZZ_s[1/2] )
38 1 37 sylbi 
 |-  ( A e. ZZ_s[1/2] -> ( A /su 2s ) e. ZZ_s[1/2] )