Metamath Proof Explorer

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 
|- ( ph -> A e. No )
pw2gt0divsd.2 
|- ( ph -> N e. NN0_s )
Assertion pw2gt0divsd 
|- ( ph -> ( 0s  0s

Proof

Step Hyp Ref Expression
1 pw2gt0divsd.1 
 |-  ( ph -> A e. No )
2 pw2gt0divsd.2 
 |-  ( ph -> N e. NN0_s )
3 0sno 
 |-  0s e. No
4 3 a1i 
 |-  ( ph -> 0s e. No )
5 1 2 pw2divscld 
 |-  ( ph -> ( A /su ( 2s ^su N ) ) e. No )
6 2sno 
 |-  2s e. No
7 expscl 
 |-  ( ( 2s e. No /\ N e. NN0_s ) -> ( 2s ^su N ) e. No )
8 6 2 7 sylancr 
 |-  ( ph -> ( 2s ^su N ) e. No )
9 2nns 
 |-  2s e. NN_s
10 nnsgt0 
 |-  ( 2s e. NN_s -> 0s
11 9 10 ax-mp 
 |-  0s
12 expsgt0 
 |-  ( ( 2s e. No /\ N e. NN0_s /\ 0s  0s
13 6 11 12 mp3an13 
 |-  ( N e. NN0_s -> 0s
14 2 13 syl 
 |-  ( ph -> 0s
15 4 5 8 14 sltmul2d 
 |-  ( ph -> ( 0s  ( ( 2s ^su N ) x.s 0s )
16 muls01 
 |-  ( ( 2s ^su N ) e. No -> ( ( 2s ^su N ) x.s 0s ) = 0s )
17 8 16 syl 
 |-  ( ph -> ( ( 2s ^su N ) x.s 0s ) = 0s )
18 1 2 pw2divscan2d 
 |-  ( ph -> ( ( 2s ^su N ) x.s ( A /su ( 2s ^su N ) ) ) = A )
19 17 18 breq12d 
 |-  ( ph -> ( ( ( 2s ^su N ) x.s 0s )  0s
20 15 19 bitr2d 
 |-  ( ph -> ( 0s  0s