Metamath Proof Explorer

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 
|- ( ph -> A e. No )
pw2divsrecd.2 
|- ( ph -> N e. NN0_s )
Assertion pw2divsrecd 
|- ( ph -> ( A /su ( 2s ^su N ) ) = ( A x.s ( 1s /su ( 2s ^su N ) ) ) )

Proof

Step Hyp Ref Expression
1 pw2divsrecd.1 
 |-  ( ph -> A e. No )
2 pw2divsrecd.2 
 |-  ( ph -> N e. NN0_s )
3 1 mulsridd 
 |-  ( ph -> ( A x.s 1s ) = A )
4 2sno 
 |-  2s e. No
5 expscl 
 |-  ( ( 2s e. No /\ N e. NN0_s ) -> ( 2s ^su N ) e. No )
6 4 2 5 sylancr 
 |-  ( ph -> ( 2s ^su N ) e. No )
7 1sno 
 |-  1s e. No
8 7 a1i 
 |-  ( ph -> 1s e. No )
9 8 2 pw2divscld 
 |-  ( ph -> ( 1s /su ( 2s ^su N ) ) e. No )
10 6 1 9 muls12d 
 |-  ( 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 ) ) ) ) )
11 8 2 pw2divscan2d 
 |-  ( ph -> ( ( 2s ^su N ) x.s ( 1s /su ( 2s ^su N ) ) ) = 1s )
12 11 oveq2d 
 |-  ( ph -> ( A x.s ( ( 2s ^su N ) x.s ( 1s /su ( 2s ^su N ) ) ) ) = ( A x.s 1s ) )
13 10 12 eqtrd 
 |-  ( ph -> ( ( 2s ^su N ) x.s ( A x.s ( 1s /su ( 2s ^su N ) ) ) ) = ( A x.s 1s ) )
14 1 2 pw2divscan2d 
 |-  ( ph -> ( ( 2s ^su N ) x.s ( A /su ( 2s ^su N ) ) ) = A )
15 3 13 14 3eqtr4rd 
 |-  ( ph -> ( ( 2s ^su N ) x.s ( A /su ( 2s ^su N ) ) ) = ( ( 2s ^su N ) x.s ( A x.s ( 1s /su ( 2s ^su N ) ) ) ) )
16 1 2 pw2divscld 
 |-  ( ph -> ( A /su ( 2s ^su N ) ) e. No )
17 1 9 mulscld 
 |-  ( ph -> ( A x.s ( 1s /su ( 2s ^su N ) ) ) e. No )
18 2ne0s 
 |-  2s =/= 0s
19 expsne0 
 |-  ( ( 2s e. No /\ 2s =/= 0s /\ N e. NN0_s ) -> ( 2s ^su N ) =/= 0s )
20 4 18 2 19 mp3an12i 
 |-  ( ph -> ( 2s ^su N ) =/= 0s )
21 16 17 6 20 mulscan1d 
 |-  ( 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 ) ) ) ) )
22 15 21 mpbid 
 |-  ( ph -> ( A /su ( 2s ^su N ) ) = ( A x.s ( 1s /su ( 2s ^su N ) ) ) )