Theorem pw2divsmuld

Description: Relationship between surreal division and multiplication for powers of two. (Contributed by Scott Fenton, 7-Nov-2025)

	Ref	Expression
Hypotheses	pw2divsmuld.1	$$⊢\phi \to A\in \mathrm{No}$$
	pw2divsmuld.2	$$⊢\phi \to B\in \mathrm{No}$$
	pw2divsmuld.3	$$⊢\phi \to N\in {\mathbb{N}}_{\mathrm{0s}}$$
Assertion	pw2divsmuld	Could not format assertion : No typesetting found for |- ( ph -> ( ( A /su ( 2s ^su N ) ) = B <-> ( ( 2s ^su N ) x.s B ) = A ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		pw2divsmuld.1	$$⊢\phi \to A\in \mathrm{No}$$
2		pw2divsmuld.2	$$⊢\phi \to B\in \mathrm{No}$$
3		pw2divsmuld.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		2ne0s	Could not format 2s =/= 0s : No typesetting found for |- 2s =/= 0s with typecode |-
8		expsne0	Could not format ( ( 2s e. No /\ 2s =/= 0s /\ N e. NN0_s ) -> ( 2s ^su N ) =/= 0s ) : No typesetting found for |- ( ( 2s e. No /\ 2s =/= 0s /\ N e. NN0_s ) -> ( 2s ^su N ) =/= 0s ) with typecode |-
9	4 7 3 8	mp3an12i	Could not format ( ph -> ( 2s ^su N ) =/= 0s ) : No typesetting found for |- ( ph -> ( 2s ^su N ) =/= 0s ) with typecode |-
10		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 |-
11	3 10	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 |-
12	1 2 6 9 11	divsmulwd	Could not format ( ph -> ( ( A /su ( 2s ^su N ) ) = B <-> ( ( 2s ^su N ) x.s B ) = A ) ) : No typesetting found for |- ( ph -> ( ( A /su ( 2s ^su N ) ) = B <-> ( ( 2s ^su N ) x.s B ) = A ) ) with typecode |-