Theorem pw2divscan3d

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

	Ref	Expression
Hypotheses	pw2divscan3d.1	$$⊢\phi \to A\in \mathrm{No}$$
	pw2divscan3d.2	$$⊢\phi \to N\in {\mathbb{N}}_{\mathrm{0s}}$$
Assertion	pw2divscan3d	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		pw2divscan3d.1	$$⊢\phi \to A\in \mathrm{No}$$
2		pw2divscan3d.2	$$⊢\phi \to N\in {\mathbb{N}}_{\mathrm{0s}}$$
3		eqid	Could not format ( ( 2s ^su N ) x.s A ) = ( ( 2s ^su N ) x.s A ) : No typesetting found for |- ( ( 2s ^su N ) x.s A ) = ( ( 2s ^su N ) x.s A ) with typecode |-
4		2sno	Could not format 2s e. No : No typesetting found for |- 2s e. No with typecode |-
5		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 |-
6	4 2 5	sylancr	Could not format ( ph -> ( 2s ^su N ) e. No ) : No typesetting found for |- ( ph -> ( 2s ^su N ) e. No ) with typecode |-
7	6 1	mulscld	Could not format ( ph -> ( ( 2s ^su N ) x.s A ) e. No ) : No typesetting found for |- ( ph -> ( ( 2s ^su N ) x.s A ) e. No ) with typecode |-
8	7 1 2	pw2divsmuld	Could not format ( ph -> ( ( ( ( 2s ^su N ) x.s A ) /su ( 2s ^su N ) ) = A <-> ( ( 2s ^su N ) x.s A ) = ( ( 2s ^su N ) x.s A ) ) ) : No typesetting found for |- ( ph -> ( ( ( ( 2s ^su N ) x.s A ) /su ( 2s ^su N ) ) = A <-> ( ( 2s ^su N ) x.s A ) = ( ( 2s ^su N ) x.s A ) ) ) with typecode |-
9	3 8	mpbiri	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 |-