Metamath Proof Explorer

Theorem elzs12i

Description: Inference form of membership in the dyadic fractions. (Contributed by Scott Fenton, 21-Feb-2026)

Ref Expression
Assertion elzs12i 
|- ( ( A e. ZZ_s /\ N e. NN0_s ) -> ( A /su ( 2s ^su N ) ) e. ZZ_s[1/2] )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( A /su ( 2s ^su N ) ) = ( A /su ( 2s ^su N ) )
2 oveq1 
 |-  ( x = A -> ( x /su ( 2s ^su n ) ) = ( A /su ( 2s ^su n ) ) )
3 2 eqeq2d 
 |-  ( x = A -> ( ( A /su ( 2s ^su N ) ) = ( x /su ( 2s ^su n ) ) <-> ( A /su ( 2s ^su N ) ) = ( A /su ( 2s ^su n ) ) ) )
4 oveq2 
 |-  ( n = N -> ( 2s ^su n ) = ( 2s ^su N ) )
5 4 oveq2d 
 |-  ( n = N -> ( A /su ( 2s ^su n ) ) = ( A /su ( 2s ^su N ) ) )
6 5 eqeq2d 
 |-  ( n = N -> ( ( A /su ( 2s ^su N ) ) = ( A /su ( 2s ^su n ) ) <-> ( A /su ( 2s ^su N ) ) = ( A /su ( 2s ^su N ) ) ) )
7 3 6 rspc2ev 
 |-  ( ( A e. ZZ_s /\ N e. NN0_s /\ ( A /su ( 2s ^su N ) ) = ( A /su ( 2s ^su N ) ) ) -> E. x e. ZZ_s E. n e. NN0_s ( A /su ( 2s ^su N ) ) = ( x /su ( 2s ^su n ) ) )
8 1 7 mp3an3 
 |-  ( ( A e. ZZ_s /\ N e. NN0_s ) -> E. x e. ZZ_s E. n e. NN0_s ( A /su ( 2s ^su N ) ) = ( x /su ( 2s ^su n ) ) )
9 elzs12 
 |-  ( ( A /su ( 2s ^su N ) ) e. ZZ_s[1/2] <-> E. x e. ZZ_s E. n e. NN0_s ( A /su ( 2s ^su N ) ) = ( x /su ( 2s ^su n ) ) )
10 8 9 sylibr 
 |-  ( ( A e. ZZ_s /\ N e. NN0_s ) -> ( A /su ( 2s ^su N ) ) e. ZZ_s[1/2] )