Theorem elzs12

Description: Membership in the dyadic fractions. (Contributed by Scott Fenton, 7-Aug-2025)

	Ref	Expression
Assertion	elzs12	Could not format assertion : 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 |-

Proof

Step	Hyp	Ref	Expression
1		elex	Could not format ( A e. ZZ_s[1/2] -> A e. _V ) : No typesetting found for |- ( A e. ZZ_s[1/2] -> A e. _V ) with typecode |-
2		id	Could not format ( A = ( x /su ( 2s ^su y ) ) -> A = ( x /su ( 2s ^su y ) ) ) : No typesetting found for |- ( A = ( x /su ( 2s ^su y ) ) -> A = ( x /su ( 2s ^su y ) ) ) with typecode |-
3		ovex	Could not format ( x /su ( 2s ^su y ) ) e. _V : No typesetting found for |- ( x /su ( 2s ^su y ) ) e. _V with typecode |-
4	2 3	eqeltrdi	Could not format ( A = ( x /su ( 2s ^su y ) ) -> A e. _V ) : No typesetting found for |- ( A = ( x /su ( 2s ^su y ) ) -> A e. _V ) with typecode |-
5	4	a1i	Could not format ( ( x e. ZZ_s /\ y e. NN0_s ) -> ( A = ( x /su ( 2s ^su y ) ) -> A e. _V ) ) : No typesetting found for |- ( ( x e. ZZ_s /\ y e. NN0_s ) -> ( A = ( x /su ( 2s ^su y ) ) -> A e. _V ) ) with typecode |-
6	5	rexlimivv	Could not format ( E. x e. ZZ_s E. y e. NN0_s A = ( x /su ( 2s ^su y ) ) -> A e. _V ) : No typesetting found for |- ( E. x e. ZZ_s E. y e. NN0_s A = ( x /su ( 2s ^su y ) ) -> A e. _V ) with typecode |-
7		eqeq1	Could not format ( z = A -> ( z = ( x /su ( 2s ^su y ) ) <-> A = ( x /su ( 2s ^su y ) ) ) ) : No typesetting found for |- ( z = A -> ( z = ( x /su ( 2s ^su y ) ) <-> A = ( x /su ( 2s ^su y ) ) ) ) with typecode |-
8	7	2rexbidv	Could not format ( z = A -> ( E. x e. ZZ_s E. y e. NN0_s z = ( x /su ( 2s ^su y ) ) <-> E. x e. ZZ_s E. y e. NN0_s A = ( x /su ( 2s ^su y ) ) ) ) : No typesetting found for |- ( z = A -> ( E. x e. ZZ_s E. y e. NN0_s z = ( x /su ( 2s ^su y ) ) <-> E. x e. ZZ_s E. y e. NN0_s A = ( x /su ( 2s ^su y ) ) ) ) with typecode |-
9		df-zs12	Could not format ZZ_s[1/2] = { z | E. x e. ZZ_s E. y e. NN0_s z = ( x /su ( 2s ^su y ) ) } : No typesetting found for |- ZZ_s[1/2] = { z | E. x e. ZZ_s E. y e. NN0_s z = ( x /su ( 2s ^su y ) ) } with typecode |-
10	8 9	elab2g	Could not format ( A e. _V -> ( 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. _V -> ( A e. ZZ_s[1/2] <-> E. x e. ZZ_s E. y e. NN0_s A = ( x /su ( 2s ^su y ) ) ) ) with typecode |-
11	1 6 10	pm5.21nii	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 |-