Theorem pw2ltdivmuls2d

Description: Surreal less-than relationship between division and multiplication for powers of two. (Contributed by Scott Fenton, 23-Feb-2026)

	Ref	Expression
Hypotheses	pw2ltdivmuls2d.1	⊢ ( 𝜑 → 𝐴 ∈ No )
	pw2ltdivmuls2d.2	⊢ ( 𝜑 → 𝐵 ∈ No )
	pw2ltdivmuls2d.3	⊢ ( 𝜑 → 𝑁 ∈ ℕ0s )
Assertion	pw2ltdivmuls2d	⊢ ( 𝜑 → ( ( 𝐴 /su ( 2s ↑s 𝑁 ) ) <s 𝐵 ↔ 𝐴 <s ( 𝐵 ·s ( 2s ↑s 𝑁 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		pw2ltdivmuls2d.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		pw2ltdivmuls2d.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3		pw2ltdivmuls2d.3	⊢ ( 𝜑 → 𝑁 ∈ ℕ0s )
4		2no	⊢ 2s ∈ No
5		expscl	⊢ ( ( 2s ∈ No ∧ 𝑁 ∈ ℕ0s ) → ( 2s ↑s 𝑁 ) ∈ No )
6	4 3 5	sylancr	⊢ ( 𝜑 → ( 2s ↑s 𝑁 ) ∈ No )
7		2nns	⊢ 2s ∈ ℕs
8		nnsgt0	⊢ ( 2s ∈ ℕs → 0s <s 2s )
9	7 8	ax-mp	⊢ 0s <s 2s
10		expsgt0	⊢ ( ( 2s ∈ No ∧ 𝑁 ∈ ℕ0s ∧ 0s <s 2s ) → 0s <s ( 2s ↑s 𝑁 ) )
11	4 9 10	mp3an13	⊢ ( 𝑁 ∈ ℕ0s → 0s <s ( 2s ↑s 𝑁 ) )
12	3 11	syl	⊢ ( 𝜑 → 0s <s ( 2s ↑s 𝑁 ) )
13		pw2recs	⊢ ( 𝑁 ∈ ℕ0s → ∃ 𝑥 ∈ No ( ( 2s ↑s 𝑁 ) ·s 𝑥 ) = 1s )
14	3 13	syl	⊢ ( 𝜑 → ∃ 𝑥 ∈ No ( ( 2s ↑s 𝑁 ) ·s 𝑥 ) = 1s )
15	1 2 6 12 14	ltdivmuls2wd	⊢ ( 𝜑 → ( ( 𝐴 /su ( 2s ↑s 𝑁 ) ) <s 𝐵 ↔ 𝐴 <s ( 𝐵 ·s ( 2s ↑s 𝑁 ) ) ) )