Theorem elzs12i

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

	Ref	Expression
Assertion	elzs12i	Could not format assertion : No typesetting found for |- ( ( A e. ZZ_s /\ N e. NN0_s ) -> ( A /su ( 2s ^su N ) ) e. ZZ_s[1/2] ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		eqid	Could not format ( A /su ( 2s ^su N ) ) = ( A /su ( 2s ^su N ) ) : No typesetting found for |- ( A /su ( 2s ^su N ) ) = ( A /su ( 2s ^su N ) ) with typecode |-
2		oveq1	Could not format ( x = A -> ( x /su ( 2s ^su n ) ) = ( A /su ( 2s ^su n ) ) ) : No typesetting found for |- ( x = A -> ( x /su ( 2s ^su n ) ) = ( A /su ( 2s ^su n ) ) ) with typecode |-
3	2	eqeq2d	Could not format ( x = A -> ( ( A /su ( 2s ^su N ) ) = ( x /su ( 2s ^su n ) ) <-> ( A /su ( 2s ^su N ) ) = ( A /su ( 2s ^su n ) ) ) ) : No typesetting found for |- ( x = A -> ( ( A /su ( 2s ^su N ) ) = ( x /su ( 2s ^su n ) ) <-> ( A /su ( 2s ^su N ) ) = ( A /su ( 2s ^su n ) ) ) ) with typecode |-
4		oveq2	Could not format ( n = N -> ( 2s ^su n ) = ( 2s ^su N ) ) : No typesetting found for |- ( n = N -> ( 2s ^su n ) = ( 2s ^su N ) ) with typecode |-
5	4	oveq2d	Could not format ( n = N -> ( A /su ( 2s ^su n ) ) = ( A /su ( 2s ^su N ) ) ) : No typesetting found for |- ( n = N -> ( A /su ( 2s ^su n ) ) = ( A /su ( 2s ^su N ) ) ) with typecode |-
6	5	eqeq2d	Could not format ( n = N -> ( ( A /su ( 2s ^su N ) ) = ( A /su ( 2s ^su n ) ) <-> ( A /su ( 2s ^su N ) ) = ( A /su ( 2s ^su N ) ) ) ) : No typesetting found for |- ( n = N -> ( ( A /su ( 2s ^su N ) ) = ( A /su ( 2s ^su n ) ) <-> ( A /su ( 2s ^su N ) ) = ( A /su ( 2s ^su N ) ) ) ) with typecode |-
7	3 6	rspc2ev	Could not format ( ( 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 ) ) ) : No typesetting found for |- ( ( 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 ) ) ) with typecode |-
8	1 7	mp3an3	Could not format ( ( 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 ) ) ) : No typesetting found for |- ( ( 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 ) ) ) with typecode |-
9		elzs12	Could not format ( ( 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 ) ) ) : No typesetting found for |- ( ( 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 ) ) ) with typecode |-
10	8 9	sylibr	Could not format ( ( A e. ZZ_s /\ N e. NN0_s ) -> ( A /su ( 2s ^su N ) ) e. ZZ_s[1/2] ) : No typesetting found for |- ( ( A e. ZZ_s /\ N e. NN0_s ) -> ( A /su ( 2s ^su N ) ) e. ZZ_s[1/2] ) with typecode |-