Theorem pw2divsdird

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

	Ref	Expression
Hypotheses	pw2divsdird.1	⊢ ( 𝜑 → 𝐴 ∈ No )
	pw2divsdird.2	⊢ ( 𝜑 → 𝐵 ∈ No )
	pw2divsdird.3	⊢ ( 𝜑 → 𝑁 ∈ ℕ0s )
Assertion	pw2divsdird	⊢ ( 𝜑 → ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s 𝑁 ) ) = ( ( 𝐴 /su ( 2s ↑s 𝑁 ) ) +s ( 𝐵 /su ( 2s ↑s 𝑁 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		pw2divsdird.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		pw2divsdird.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3		pw2divsdird.3	⊢ ( 𝜑 → 𝑁 ∈ ℕ0s )
4		1sno	⊢ 1s ∈ No
5	4	a1i	⊢ ( 𝜑 → 1s ∈ No )
6	5 3	pw2divscld	⊢ ( 𝜑 → ( 1s /su ( 2s ↑s 𝑁 ) ) ∈ No )
7	1 2 6	addsdird	⊢ ( 𝜑 → ( ( 𝐴 +s 𝐵 ) ·s ( 1s /su ( 2s ↑s 𝑁 ) ) ) = ( ( 𝐴 ·s ( 1s /su ( 2s ↑s 𝑁 ) ) ) +s ( 𝐵 ·s ( 1s /su ( 2s ↑s 𝑁 ) ) ) ) )
8	1 2	addscld	⊢ ( 𝜑 → ( 𝐴 +s 𝐵 ) ∈ No )
9	8 3	pw2divsrecd	⊢ ( 𝜑 → ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s 𝑁 ) ) = ( ( 𝐴 +s 𝐵 ) ·s ( 1s /su ( 2s ↑s 𝑁 ) ) ) )
10	1 3	pw2divsrecd	⊢ ( 𝜑 → ( 𝐴 /su ( 2s ↑s 𝑁 ) ) = ( 𝐴 ·s ( 1s /su ( 2s ↑s 𝑁 ) ) ) )
11	2 3	pw2divsrecd	⊢ ( 𝜑 → ( 𝐵 /su ( 2s ↑s 𝑁 ) ) = ( 𝐵 ·s ( 1s /su ( 2s ↑s 𝑁 ) ) ) )
12	10 11	oveq12d	⊢ ( 𝜑 → ( ( 𝐴 /su ( 2s ↑s 𝑁 ) ) +s ( 𝐵 /su ( 2s ↑s 𝑁 ) ) ) = ( ( 𝐴 ·s ( 1s /su ( 2s ↑s 𝑁 ) ) ) +s ( 𝐵 ·s ( 1s /su ( 2s ↑s 𝑁 ) ) ) ) )
13	7 9 12	3eqtr4d	⊢ ( 𝜑 → ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s 𝑁 ) ) = ( ( 𝐴 /su ( 2s ↑s 𝑁 ) ) +s ( 𝐵 /su ( 2s ↑s 𝑁 ) ) ) )