Theorem pw2divscan2d

Description: A cancellation law for surreal division by powers of two. (Contributed by Scott Fenton, 7-Nov-2025)

	Ref	Expression
Hypotheses	pw2divscan2d.1	$$⊢\phi \to A\in \mathrm{No}$$
	pw2divscan2d.2	$$⊢\phi \to N\in {\mathbb{N}}_{\mathrm{0s}}$$
Assertion	pw2divscan2d	Could not format assertion : No typesetting found for |- ( ph -> ( ( 2s ^su N ) x.s ( A /su ( 2s ^su N ) ) ) = A ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		pw2divscan2d.1	$$⊢\phi \to A\in \mathrm{No}$$
2		pw2divscan2d.2	$$⊢\phi \to N\in {\mathbb{N}}_{\mathrm{0s}}$$
3		2sno	Could not format 2s e. No : No typesetting found for |- 2s e. No with typecode |-
4		expscl	Could not format ( ( 2s e. No /\ N e. NN0_s ) -> ( 2s ^su N ) e. No ) : No typesetting found for |- ( ( 2s e. No /\ N e. NN0_s ) -> ( 2s ^su N ) e. No ) with typecode |-
5	3 2 4	sylancr	Could not format ( ph -> ( 2s ^su N ) e. No ) : No typesetting found for |- ( ph -> ( 2s ^su N ) e. No ) with typecode |-
6		2ne0s	Could not format 2s =/= 0s : No typesetting found for |- 2s =/= 0s with typecode |-
7		expsne0	Could not format ( ( 2s e. No /\ 2s =/= 0s /\ N e. NN0_s ) -> ( 2s ^su N ) =/= 0s ) : No typesetting found for |- ( ( 2s e. No /\ 2s =/= 0s /\ N e. NN0_s ) -> ( 2s ^su N ) =/= 0s ) with typecode |-
8	3 6 2 7	mp3an12i	Could not format ( ph -> ( 2s ^su N ) =/= 0s ) : No typesetting found for |- ( ph -> ( 2s ^su N ) =/= 0s ) with typecode |-
9		pw2recs	Could not format ( N e. NN0_s -> E. x e. No ( ( 2s ^su N ) x.s x ) = 1s ) : No typesetting found for |- ( N e. NN0_s -> E. x e. No ( ( 2s ^su N ) x.s x ) = 1s ) with typecode |-
10	2 9	syl	Could not format ( ph -> E. x e. No ( ( 2s ^su N ) x.s x ) = 1s ) : No typesetting found for |- ( ph -> E. x e. No ( ( 2s ^su N ) x.s x ) = 1s ) with typecode |-
11	1 5 8 10	divscan2wd	Could not format ( ph -> ( ( 2s ^su N ) x.s ( A /su ( 2s ^su N ) ) ) = A ) : No typesetting found for |- ( ph -> ( ( 2s ^su N ) x.s ( A /su ( 2s ^su N ) ) ) = A ) with typecode |-