Definition df-zs12

Description: Define the set of dyadic rationals. This is the set of rationals whose denominator is a power of two. Later we will prove that this is precisely the set of surreals with a finite birthday. (Contributed by Scott Fenton, 27-May-2025)

	Ref	Expression
Assertion	df-zs12	|- ZZ_s[1/2] = { x | E. y e. ZZ_s E. z e. NN0_s x = ( y /su ( 2s ^su z ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		czs12	|- ZZ_s[1/2]
1		vx	|- x
2		vy	|- y
3		czs	|- ZZ_s
4		vz	|- z
5		cnn0s	|- NN0_s
6	1	cv	|- x
7	2	cv	|- y
8		cdivs	|- /su
9		c2s	|- 2s
10		cexps	|- ^su
11	4	cv	|- z
12	9 11 10	co	|- ( 2s ^su z )
13	7 12 8	co	|- ( y /su ( 2s ^su z ) )
14	6 13	wceq	|- x = ( y /su ( 2s ^su z ) )
15	14 4 5	wrex	|- E. z e. NN0_s x = ( y /su ( 2s ^su z ) )
16	15 2 3	wrex	|- E. y e. ZZ_s E. z e. NN0_s x = ( y /su ( 2s ^su z ) )
17	16 1	cab	|- { x | E. y e. ZZ_s E. z e. NN0_s x = ( y /su ( 2s ^su z ) ) }
18	0 17	wceq	|- ZZ_s[1/2] = { x | E. y e. ZZ_s E. z e. NN0_s x = ( y /su ( 2s ^su z ) ) }