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	|- ( ph -> A e. No )
	pw2divsdird.2	|- ( ph -> B e. No )
	pw2divsdird.3	|- ( ph -> N e. NN0_s )
Assertion	pw2divsdird	|- ( ph -> ( ( A +s B ) /su ( 2s ^su N ) ) = ( ( A /su ( 2s ^su N ) ) +s ( B /su ( 2s ^su N ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		pw2divsdird.1	|- ( ph -> A e. No )
2		pw2divsdird.2	|- ( ph -> B e. No )
3		pw2divsdird.3	|- ( ph -> N e. NN0_s )
4		1sno	|- 1s e. No
5	4	a1i	|- ( ph -> 1s e. No )
6	5 3	pw2divscld	|- ( ph -> ( 1s /su ( 2s ^su N ) ) e. No )
7	1 2 6	addsdird	|- ( ph -> ( ( A +s B ) x.s ( 1s /su ( 2s ^su N ) ) ) = ( ( A x.s ( 1s /su ( 2s ^su N ) ) ) +s ( B x.s ( 1s /su ( 2s ^su N ) ) ) ) )
8	1 2	addscld	|- ( ph -> ( A +s B ) e. No )
9	8 3	pw2divsrecd	|- ( ph -> ( ( A +s B ) /su ( 2s ^su N ) ) = ( ( A +s B ) x.s ( 1s /su ( 2s ^su N ) ) ) )
10	1 3	pw2divsrecd	|- ( ph -> ( A /su ( 2s ^su N ) ) = ( A x.s ( 1s /su ( 2s ^su N ) ) ) )
11	2 3	pw2divsrecd	|- ( ph -> ( B /su ( 2s ^su N ) ) = ( B x.s ( 1s /su ( 2s ^su N ) ) ) )
12	10 11	oveq12d	|- ( ph -> ( ( A /su ( 2s ^su N ) ) +s ( B /su ( 2s ^su N ) ) ) = ( ( A x.s ( 1s /su ( 2s ^su N ) ) ) +s ( B x.s ( 1s /su ( 2s ^su N ) ) ) ) )
13	7 9 12	3eqtr4d	|- ( ph -> ( ( A +s B ) /su ( 2s ^su N ) ) = ( ( A /su ( 2s ^su N ) ) +s ( B /su ( 2s ^su N ) ) ) )