Theorem pw2gt0divsd

Description: Division of a positive 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	pw2gt0divsd	Could not format assertion : No typesetting found for |- ( ph -> ( 0s 0s

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	sltmul2d	Could not format ( ph -> ( 0s ( ( 2s ^su N ) x.s 0s ) ( 0s ( ( 2s ^su N ) x.s 0s )
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 ) 0s ( ( ( 2s ^su N ) x.s 0s ) 0s
20	15 19	bitr2d	Could not format ( ph -> ( 0s 0s ( 0s 0s