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	⊢ ( 𝜑 → 𝐴 ∈ No )
	pw2divscan2d.2	⊢ ( 𝜑 → 𝑁 ∈ ℕ0s )
Assertion	pw2divscan2d	⊢ ( 𝜑 → ( ( 2s ↑s 𝑁 ) ·s ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		pw2divscan2d.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		pw2divscan2d.2	⊢ ( 𝜑 → 𝑁 ∈ ℕ0s )
3		2no	⊢ 2s ∈ No
4		expscl	⊢ ( ( 2s ∈ No ∧ 𝑁 ∈ ℕ0s ) → ( 2s ↑s 𝑁 ) ∈ No )
5	3 2 4	sylancr	⊢ ( 𝜑 → ( 2s ↑s 𝑁 ) ∈ No )
6		2ne0s	⊢ 2s ≠ 0s
7		expsne0	⊢ ( ( 2s ∈ No ∧ 2s ≠ 0s ∧ 𝑁 ∈ ℕ0s ) → ( 2s ↑s 𝑁 ) ≠ 0s )
8	3 6 2 7	mp3an12i	⊢ ( 𝜑 → ( 2s ↑s 𝑁 ) ≠ 0s )
9		pw2recs	⊢ ( 𝑁 ∈ ℕ0s → ∃ 𝑥 ∈ No ( ( 2s ↑s 𝑁 ) ·s 𝑥 ) = 1s )
10	2 9	syl	⊢ ( 𝜑 → ∃ 𝑥 ∈ No ( ( 2s ↑s 𝑁 ) ·s 𝑥 ) = 1s )
11	1 5 8 10	divscan2wd	⊢ ( 𝜑 → ( ( 2s ↑s 𝑁 ) ·s ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ) = 𝐴 )