Theorem pw2divsrecd

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

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

Proof

Step	Hyp	Ref	Expression
1		pw2divsrecd.1	$$⊢\phi \to A\in \mathrm{No}$$
2		pw2divsrecd.2	$$⊢\phi \to N\in {\mathbb{N}}_{\mathrm{0s}}$$
3	1	mulsridd	$$⊢\phi \to A{\cdot }_s{1}_s=A$$
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 2 5	sylancr	Could not format ( ph -> ( 2s ^su N ) e. No ) : No typesetting found for |- ( ph -> ( 2s ^su N ) e. No ) with typecode |-
7		1sno	$$⊢1_s\in \mathrm{No}$$
8	7	a1i	$$⊢\phi \to 1_s\in \mathrm{No}$$
9	8 2	pw2divscld	Could not format ( ph -> ( 1s /su ( 2s ^su N ) ) e. No ) : No typesetting found for |- ( ph -> ( 1s /su ( 2s ^su N ) ) e. No ) with typecode |-
10	6 1 9	muls12d	Could not format ( ph -> ( ( 2s ^su N ) x.s ( A x.s ( 1s /su ( 2s ^su N ) ) ) ) = ( A x.s ( ( 2s ^su N ) x.s ( 1s /su ( 2s ^su N ) ) ) ) ) : No typesetting found for |- ( ph -> ( ( 2s ^su N ) x.s ( A x.s ( 1s /su ( 2s ^su N ) ) ) ) = ( A x.s ( ( 2s ^su N ) x.s ( 1s /su ( 2s ^su N ) ) ) ) ) with typecode |-
11	8 2	pw2divscan2d	Could not format ( ph -> ( ( 2s ^su N ) x.s ( 1s /su ( 2s ^su N ) ) ) = 1s ) : No typesetting found for |- ( ph -> ( ( 2s ^su N ) x.s ( 1s /su ( 2s ^su N ) ) ) = 1s ) with typecode |-
12	11	oveq2d	Could not format ( ph -> ( A x.s ( ( 2s ^su N ) x.s ( 1s /su ( 2s ^su N ) ) ) ) = ( A x.s 1s ) ) : No typesetting found for |- ( ph -> ( A x.s ( ( 2s ^su N ) x.s ( 1s /su ( 2s ^su N ) ) ) ) = ( A x.s 1s ) ) with typecode |-
13	10 12	eqtrd	Could not format ( ph -> ( ( 2s ^su N ) x.s ( A x.s ( 1s /su ( 2s ^su N ) ) ) ) = ( A x.s 1s ) ) : No typesetting found for |- ( ph -> ( ( 2s ^su N ) x.s ( A x.s ( 1s /su ( 2s ^su N ) ) ) ) = ( A x.s 1s ) ) with typecode |-
14	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 |-
15	3 13 14	3eqtr4rd	Could not format ( ph -> ( ( 2s ^su N ) x.s ( A /su ( 2s ^su N ) ) ) = ( ( 2s ^su N ) x.s ( A x.s ( 1s /su ( 2s ^su N ) ) ) ) ) : No typesetting found for |- ( ph -> ( ( 2s ^su N ) x.s ( A /su ( 2s ^su N ) ) ) = ( ( 2s ^su N ) x.s ( A x.s ( 1s /su ( 2s ^su N ) ) ) ) ) with typecode |-
16	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 |-
17	1 9	mulscld	Could not format ( ph -> ( A x.s ( 1s /su ( 2s ^su N ) ) ) e. No ) : No typesetting found for |- ( ph -> ( A x.s ( 1s /su ( 2s ^su N ) ) ) e. No ) with typecode |-
18		2ne0s	Could not format 2s =/= 0s : No typesetting found for |- 2s =/= 0s with typecode |-
19		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 |-
20	4 18 2 19	mp3an12i	Could not format ( ph -> ( 2s ^su N ) =/= 0s ) : No typesetting found for |- ( ph -> ( 2s ^su N ) =/= 0s ) with typecode |-
21	16 17 6 20	mulscan1d	Could not format ( ph -> ( ( ( 2s ^su N ) x.s ( A /su ( 2s ^su N ) ) ) = ( ( 2s ^su N ) x.s ( A x.s ( 1s /su ( 2s ^su N ) ) ) ) <-> ( A /su ( 2s ^su N ) ) = ( A x.s ( 1s /su ( 2s ^su N ) ) ) ) ) : No typesetting found for |- ( ph -> ( ( ( 2s ^su N ) x.s ( A /su ( 2s ^su N ) ) ) = ( ( 2s ^su N ) x.s ( A x.s ( 1s /su ( 2s ^su N ) ) ) ) <-> ( A /su ( 2s ^su N ) ) = ( A x.s ( 1s /su ( 2s ^su N ) ) ) ) ) with typecode |-
22	15 21	mpbid	Could not format ( ph -> ( A /su ( 2s ^su N ) ) = ( A x.s ( 1s /su ( 2s ^su N ) ) ) ) : No typesetting found for |- ( ph -> ( A /su ( 2s ^su N ) ) = ( A x.s ( 1s /su ( 2s ^su N ) ) ) ) with typecode |-