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

Proof

Step	Hyp	Ref	Expression
1		pw2gt0divsd.1	$$⊢\phi \to A\in \mathrm{No}$$
2		pw2gt0divsd.2	$$⊢\phi \to N\in {\mathbb{N}}_{\mathrm{0s}}$$
3		0sno	$$⊢0_s\in \mathrm{No}$$
4	3	a1i	$$⊢\phi \to 0_s\in \mathrm{No}$$
5	1 2	pw2divscld	Could not format ( ph -> ( A /su ( 2s ^su N ) ) e. No ) : No typesetting found for |- ( ph -> ( A /su ( 2s ^su N ) ) e. No ) with typecode |-
6		2sno	Could not format 2s e. No : No typesetting found for |- 2s e. No with typecode |-
7		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 |-
8	6 2 7	sylancr	Could not format ( ph -> ( 2s ^su N ) e. No ) : No typesetting found for |- ( ph -> ( 2s ^su N ) e. No ) with typecode |-
9		2nns	Could not format 2s e. NN_s : No typesetting found for |- 2s e. NN_s with typecode |-
10		nnsgt0	Could not format ( 2s e. NN_s -> 0s 0s
11	9 10	ax-mp	Could not format 0s
12		expsgt0	Could not format ( ( 2s e. No /\ N e. NN0_s /\ 0s 0s 0s
13	6 11 12	mp3an13	Could not format ( N e. NN0_s -> 0s 0s
14	2 13	syl	Could not format ( ph -> 0s 0s
15	4 5 8 14	slemul2d	Could not format ( ph -> ( 0s <_s ( A /su ( 2s ^su N ) ) <-> ( ( 2s ^su N ) x.s 0s ) <_s ( ( 2s ^su N ) x.s ( A /su ( 2s ^su N ) ) ) ) ) : No typesetting found for |- ( ph -> ( 0s <_s ( A /su ( 2s ^su N ) ) <-> ( ( 2s ^su N ) x.s 0s ) <_s ( ( 2s ^su N ) x.s ( A /su ( 2s ^su N ) ) ) ) ) with typecode |-
16		muls01	Could not format ( ( 2s ^su N ) e. No -> ( ( 2s ^su N ) x.s 0s ) = 0s ) : No typesetting found for |- ( ( 2s ^su N ) e. No -> ( ( 2s ^su N ) x.s 0s ) = 0s ) with typecode |-
17	8 16	syl	Could not format ( ph -> ( ( 2s ^su N ) x.s 0s ) = 0s ) : No typesetting found for |- ( ph -> ( ( 2s ^su N ) x.s 0s ) = 0s ) with typecode |-
18	1 2	pw2divscan2d	Could not format ( ph -> ( ( 2s ^su N ) x.s ( A /su ( 2s ^su N ) ) ) = A ) : No typesetting found for |- ( ph -> ( ( 2s ^su N ) x.s ( A /su ( 2s ^su N ) ) ) = A ) with typecode |-
19	17 18	breq12d	Could not format ( ph -> ( ( ( 2s ^su N ) x.s 0s ) <_s ( ( 2s ^su N ) x.s ( A /su ( 2s ^su N ) ) ) <-> 0s <_s A ) ) : No typesetting found for |- ( ph -> ( ( ( 2s ^su N ) x.s 0s ) <_s ( ( 2s ^su N ) x.s ( A /su ( 2s ^su N ) ) ) <-> 0s <_s A ) ) with typecode |-
20	15 19	bitr2d	Could not format ( ph -> ( 0s <_s A <-> 0s <_s ( A /su ( 2s ^su N ) ) ) ) : No typesetting found for |- ( ph -> ( 0s <_s A <-> 0s <_s ( A /su ( 2s ^su N ) ) ) ) with typecode |-