Theorem pw2divscan3d

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

	Ref	Expression
Hypotheses	pw2divscan3d.1	|- ( ph -> A e. No )
	pw2divscan3d.2	|- ( ph -> N e. NN0_s )
Assertion	pw2divscan3d	|- ( ph -> ( ( ( 2s ^su N ) x.s A ) /su ( 2s ^su N ) ) = A )

Proof

Step	Hyp	Ref	Expression
1		pw2divscan3d.1	|- ( ph -> A e. No )
2		pw2divscan3d.2	|- ( ph -> N e. NN0_s )
3		eqid	|- ( ( 2s ^su N ) x.s A ) = ( ( 2s ^su N ) x.s A )
4		2sno	|- 2s e. No
5		expscl	|- ( ( 2s e. No /\ N e. NN0_s ) -> ( 2s ^su N ) e. No )
6	4 2 5	sylancr	|- ( ph -> ( 2s ^su N ) e. No )
7	6 1	mulscld	|- ( ph -> ( ( 2s ^su N ) x.s A ) e. No )
8	7 1 2	pw2divsmuld	|- ( ph -> ( ( ( ( 2s ^su N ) x.s A ) /su ( 2s ^su N ) ) = A <-> ( ( 2s ^su N ) x.s A ) = ( ( 2s ^su N ) x.s A ) ) )
9	3 8	mpbiri	|- ( ph -> ( ( ( 2s ^su N ) x.s A ) /su ( 2s ^su N ) ) = A )