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	|- ( ph -> A e. No )
	pw2divscan2d.2	|- ( ph -> N e. NN0_s )
Assertion	pw2divscan2d	|- ( ph -> ( ( 2s ^su N ) x.s ( A /su ( 2s ^su N ) ) ) = A )

Proof

Step	Hyp	Ref	Expression
1		pw2divscan2d.1	|- ( ph -> A e. No )
2		pw2divscan2d.2	|- ( ph -> N e. NN0_s )
3		2sno	|- 2s e. No
4		expscl	|- ( ( 2s e. No /\ N e. NN0_s ) -> ( 2s ^su N ) e. No )
5	3 2 4	sylancr	|- ( ph -> ( 2s ^su N ) e. No )
6		2ne0s	|- 2s =/= 0s
7		expsne0	|- ( ( 2s e. No /\ 2s =/= 0s /\ N e. NN0_s ) -> ( 2s ^su N ) =/= 0s )
8	3 6 2 7	mp3an12i	|- ( ph -> ( 2s ^su N ) =/= 0s )
9		pw2recs	|- ( N e. NN0_s -> E. x e. No ( ( 2s ^su N ) x.s x ) = 1s )
10	2 9	syl	|- ( ph -> E. x e. No ( ( 2s ^su N ) x.s x ) = 1s )
11	1 5 8 10	divscan2wd	|- ( ph -> ( ( 2s ^su N ) x.s ( A /su ( 2s ^su N ) ) ) = A )