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	$$⊢\phi \to A\in \mathrm{No}$$
	pw2sltdivmuld.2	$$⊢\phi \to B\in \mathrm{No}$$
	pw2sltdivmuld.3	$$⊢\phi \to N\in {\mathbb{N}}_{\mathrm{0s}}$$
Assertion	pw2sltdiv1d	Could not format assertion : No typesetting found for |- ( ph -> ( A ( A /su ( 2s ^su N ) )

Proof

Step	Hyp	Ref	Expression
1		pw2sltdivmuld.1	$$⊢\phi \to A\in \mathrm{No}$$
2		pw2sltdivmuld.2	$$⊢\phi \to B\in \mathrm{No}$$
3		pw2sltdivmuld.3	$$⊢\phi \to N\in {\mathbb{N}}_{\mathrm{0s}}$$
4	2 3	pw2divscld	Could not format ( ph -> ( B /su ( 2s ^su N ) ) e. No ) : No typesetting found for |- ( ph -> ( B /su ( 2s ^su N ) ) e. No ) with typecode |-
5	1 4 3	pw2sltdivmuld	Could not format ( ph -> ( ( A /su ( 2s ^su N ) ) A ( ( A /su ( 2s ^su N ) ) A
6	2 3	pw2divscan2d	Could not format ( ph -> ( ( 2s ^su N ) x.s ( B /su ( 2s ^su N ) ) ) = B ) : No typesetting found for |- ( ph -> ( ( 2s ^su N ) x.s ( B /su ( 2s ^su N ) ) ) = B ) with typecode |-
7	6	breq2d	Could not format ( ph -> ( A A ( A A
8	5 7	bitr2d	Could not format ( ph -> ( A ( A /su ( 2s ^su N ) ) ( A ( A /su ( 2s ^su N ) )