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	$$⊢\phi \to A\in \mathrm{No}$$
	pw2sltdivmuld.2	$$⊢\phi \to B\in \mathrm{No}$$
	pw2sltdivmuld.3	$$⊢\phi \to N\in {\mathbb{N}}_{\mathrm{0s}}$$
Assertion	pw2sltdivmuld	Could not format assertion : No typesetting found for |- ( ph -> ( ( A /su ( 2s ^su N ) ) A

Proof

Step	Hyp	Ref	Expression
1		pw2sltdivmuld.1	$$⊢\phi \to A\in \mathrm{No}$$
2		pw2sltdivmuld.2	$$⊢\phi \to B\in \mathrm{No}$$
3		pw2sltdivmuld.3	$$⊢\phi \to N\in {\mathbb{N}}_{\mathrm{0s}}$$
4		2sno	Could not format 2s e. No : No typesetting found for |- 2s e. No with typecode |-
5		expscl	Could not format ( ( 2s e. No /\ N e. NN0_s ) -> ( 2s ^su N ) e. No ) : No typesetting found for |- ( ( 2s e. No /\ N e. NN0_s ) -> ( 2s ^su N ) e. No ) with typecode |-
6	4 3 5	sylancr	Could not format ( ph -> ( 2s ^su N ) e. No ) : No typesetting found for |- ( ph -> ( 2s ^su N ) e. No ) with typecode |-
7		2nns	Could not format 2s e. NN_s : No typesetting found for |- 2s e. NN_s with typecode |-
8		nnsgt0	Could not format ( 2s e. NN_s -> 0s 0s
9	7 8	ax-mp	Could not format 0s
10		expsgt0	Could not format ( ( 2s e. No /\ N e. NN0_s /\ 0s 0s 0s
11	4 9 10	mp3an13	Could not format ( N e. NN0_s -> 0s 0s
12	3 11	syl	Could not format ( ph -> 0s 0s
13		pw2recs	Could not format ( N e. NN0_s -> E. x e. No ( ( 2s ^su N ) x.s x ) = 1s ) : No typesetting found for |- ( N e. NN0_s -> E. x e. No ( ( 2s ^su N ) x.s x ) = 1s ) with typecode |-
14	3 13	syl	Could not format ( ph -> E. x e. No ( ( 2s ^su N ) x.s x ) = 1s ) : No typesetting found for |- ( ph -> E. x e. No ( ( 2s ^su N ) x.s x ) = 1s ) with typecode |-
15	1 2 6 12 14	sltdivmulwd	Could not format ( ph -> ( ( A /su ( 2s ^su N ) ) A ( ( A /su ( 2s ^su N ) ) A