Theorem pw2divsmuld

Description: Relationship between surreal division and multiplication for powers of two. (Contributed by Scott Fenton, 7-Nov-2025)

	Ref	Expression
Hypotheses	pw2divsmuld.1	|- ( ph -> A e. No )
	pw2divsmuld.2	|- ( ph -> B e. No )
	pw2divsmuld.3	|- ( ph -> N e. NN0_s )
Assertion	pw2divsmuld	|- ( ph -> ( ( A /su ( 2s ^su N ) ) = B <-> ( ( 2s ^su N ) x.s B ) = A ) )

Proof

Step	Hyp	Ref	Expression
1		pw2divsmuld.1	|- ( ph -> A e. No )
2		pw2divsmuld.2	|- ( ph -> B e. No )
3		pw2divsmuld.3	|- ( ph -> N e. NN0_s )
4		2sno	|- 2s e. No
5		expscl	|- ( ( 2s e. No /\ N e. NN0_s ) -> ( 2s ^su N ) e. No )
6	4 3 5	sylancr	|- ( ph -> ( 2s ^su N ) e. No )
7		2ne0s	|- 2s =/= 0s
8		expsne0	|- ( ( 2s e. No /\ 2s =/= 0s /\ N e. NN0_s ) -> ( 2s ^su N ) =/= 0s )
9	4 7 3 8	mp3an12i	|- ( ph -> ( 2s ^su N ) =/= 0s )
10		pw2recs	|- ( N e. NN0_s -> E. x e. No ( ( 2s ^su N ) x.s x ) = 1s )
11	3 10	syl	|- ( ph -> E. x e. No ( ( 2s ^su N ) x.s x ) = 1s )
12	1 2 6 9 11	divsmulwd	|- ( ph -> ( ( A /su ( 2s ^su N ) ) = B <-> ( ( 2s ^su N ) x.s B ) = A ) )