Theorem pw2sltdivmuld

Description: Surreal less-than relationship between division and multiplication for powers of two. (Contributed by Scott Fenton, 11-Dec-2025)

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

Proof

Step	Hyp	Ref	Expression
1		pw2sltdivmuld.1	|- ( ph -> A e. No )
2		pw2sltdivmuld.2	|- ( ph -> B e. No )
3		pw2sltdivmuld.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		2nns	|- 2s e. NN_s
8		nnsgt0	|- ( 2s e. NN_s -> 0s
9	7 8	ax-mp	|- 0s
10		expsgt0	|- ( ( 2s e. No /\ N e. NN0_s /\ 0s 0s
11	4 9 10	mp3an13	|- ( N e. NN0_s -> 0s
12	3 11	syl	|- ( ph -> 0s
13		pw2recs	|- ( N e. NN0_s -> E. x e. No ( ( 2s ^su N ) x.s x ) = 1s )
14	3 13	syl	|- ( ph -> E. x e. No ( ( 2s ^su N ) x.s x ) = 1s )
15	1 2 6 12 14	sltdivmulwd	|- ( ph -> ( ( A /su ( 2s ^su N ) ) A