Theorem pw2divscan3d

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

	Ref	Expression
Hypotheses	pw2divscan3d.1	⊢ ( 𝜑 → 𝐴 ∈ No )
	pw2divscan3d.2	⊢ ( 𝜑 → 𝑁 ∈ ℕ0s )
Assertion	pw2divscan3d	⊢ ( 𝜑 → ( ( ( 2s ↑s 𝑁 ) ·s 𝐴 ) /su ( 2s ↑s 𝑁 ) ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		pw2divscan3d.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		pw2divscan3d.2	⊢ ( 𝜑 → 𝑁 ∈ ℕ0s )
3		eqid	⊢ ( ( 2s ↑s 𝑁 ) ·s 𝐴 ) = ( ( 2s ↑s 𝑁 ) ·s 𝐴 )
4		2no	⊢ 2s ∈ No
5		expscl	⊢ ( ( 2s ∈ No ∧ 𝑁 ∈ ℕ0s ) → ( 2s ↑s 𝑁 ) ∈ No )
6	4 2 5	sylancr	⊢ ( 𝜑 → ( 2s ↑s 𝑁 ) ∈ No )
7	6 1	mulscld	⊢ ( 𝜑 → ( ( 2s ↑s 𝑁 ) ·s 𝐴 ) ∈ No )
8	7 1 2	pw2divmulsd	⊢ ( 𝜑 → ( ( ( ( 2s ↑s 𝑁 ) ·s 𝐴 ) /su ( 2s ↑s 𝑁 ) ) = 𝐴 ↔ ( ( 2s ↑s 𝑁 ) ·s 𝐴 ) = ( ( 2s ↑s 𝑁 ) ·s 𝐴 ) ) )
9	3 8	mpbiri	⊢ ( 𝜑 → ( ( ( 2s ↑s 𝑁 ) ·s 𝐴 ) /su ( 2s ↑s 𝑁 ) ) = 𝐴 )