Theorem pw2ge0divsd

Description: Divison of a non-negative surreal by a power of two. (Contributed by Scott Fenton, 7-Nov-2025)

	Ref	Expression
Hypotheses	pw2gt0divsd.1	⊢ ( 𝜑 → 𝐴 ∈ No )
	pw2gt0divsd.2	⊢ ( 𝜑 → 𝑁 ∈ ℕ0s )
Assertion	pw2ge0divsd	⊢ ( 𝜑 → ( 0s ≤s 𝐴 ↔ 0s ≤s ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		pw2gt0divsd.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		pw2gt0divsd.2	⊢ ( 𝜑 → 𝑁 ∈ ℕ0s )
3		0no	⊢ 0s ∈ No
4	3	a1i	⊢ ( 𝜑 → 0s ∈ No )
5	1 2	pw2divscld	⊢ ( 𝜑 → ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ∈ No )
6		2no	⊢ 2s ∈ No
7		expscl	⊢ ( ( 2s ∈ No ∧ 𝑁 ∈ ℕ0s ) → ( 2s ↑s 𝑁 ) ∈ No )
8	6 2 7	sylancr	⊢ ( 𝜑 → ( 2s ↑s 𝑁 ) ∈ No )
9		2nns	⊢ 2s ∈ ℕs
10		nnsgt0	⊢ ( 2s ∈ ℕs → 0s <s 2s )
11	9 10	ax-mp	⊢ 0s <s 2s
12		expsgt0	⊢ ( ( 2s ∈ No ∧ 𝑁 ∈ ℕ0s ∧ 0s <s 2s ) → 0s <s ( 2s ↑s 𝑁 ) )
13	6 11 12	mp3an13	⊢ ( 𝑁 ∈ ℕ0s → 0s <s ( 2s ↑s 𝑁 ) )
14	2 13	syl	⊢ ( 𝜑 → 0s <s ( 2s ↑s 𝑁 ) )
15	4 5 8 14	lemuls2d	⊢ ( 𝜑 → ( 0s ≤s ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ↔ ( ( 2s ↑s 𝑁 ) ·s 0s ) ≤s ( ( 2s ↑s 𝑁 ) ·s ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ) ) )
16		muls01	⊢ ( ( 2s ↑s 𝑁 ) ∈ No → ( ( 2s ↑s 𝑁 ) ·s 0s ) = 0s )
17	8 16	syl	⊢ ( 𝜑 → ( ( 2s ↑s 𝑁 ) ·s 0s ) = 0s )
18	1 2	pw2divscan2d	⊢ ( 𝜑 → ( ( 2s ↑s 𝑁 ) ·s ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ) = 𝐴 )
19	17 18	breq12d	⊢ ( 𝜑 → ( ( ( 2s ↑s 𝑁 ) ·s 0s ) ≤s ( ( 2s ↑s 𝑁 ) ·s ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ) ↔ 0s ≤s 𝐴 ) )
20	15 19	bitr2d	⊢ ( 𝜑 → ( 0s ≤s 𝐴 ↔ 0s ≤s ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ) )