Theorem pw2sltdiv1d

Description: Surreal less-than relationship for division by a power of two. (Contributed by Scott Fenton, 18-Jan-2026)

	Ref	Expression
Hypotheses	pw2sltdivmuld.1	|- ( ph -> A e. No )
	pw2sltdivmuld.2	|- ( ph -> B e. No )
	pw2sltdivmuld.3	|- ( ph -> N e. NN0_s )
Assertion	pw2sltdiv1d	|- ( ph -> ( A ( A /su ( 2s ^su N ) )

Proof

Step	Hyp	Ref	Expression
1		pw2sltdivmuld.1	|- ( ph -> A e. No )
2		pw2sltdivmuld.2	|- ( ph -> B e. No )
3		pw2sltdivmuld.3	|- ( ph -> N e. NN0_s )
4	2 3	pw2divscld	|- ( ph -> ( B /su ( 2s ^su N ) ) e. No )
5	1 4 3	pw2sltdivmuld	|- ( ph -> ( ( A /su ( 2s ^su N ) ) A
6	2 3	pw2divscan2d	|- ( ph -> ( ( 2s ^su N ) x.s ( B /su ( 2s ^su N ) ) ) = B )
7	6	breq2d	|- ( ph -> ( A A
8	5 7	bitr2d	|- ( ph -> ( A ( A /su ( 2s ^su N ) )