Metamath Proof Explorer

Theorem pw2divsnegd

Description: Move negative sign inside of a power of two division. (Contributed by Scott Fenton, 8-Nov-2025)

Ref Expression
Hypotheses pw2divsnegd.1 
|- ( ph -> A e. No )
pw2divsnegd.2 
|- ( ph -> N e. NN0_s )
Assertion pw2divsnegd 
|- ( ph -> ( -us ` ( A /su ( 2s ^su N ) ) ) = ( ( -us ` A ) /su ( 2s ^su N ) ) )

Proof

Step Hyp Ref Expression
1 pw2divsnegd.1 
 |-  ( ph -> A e. No )
2 pw2divsnegd.2 
 |-  ( ph -> N e. NN0_s )
3 1 2 pw2divscld 
 |-  ( ph -> ( A /su ( 2s ^su N ) ) e. No )
4 3 negsidd 
 |-  ( ph -> ( ( A /su ( 2s ^su N ) ) +s ( -us ` ( A /su ( 2s ^su N ) ) ) ) = 0s )
5 2sno 
 |-  2s e. No
6 expscl 
 |-  ( ( 2s e. No /\ N e. NN0_s ) -> ( 2s ^su N ) e. No )
7 5 2 6 sylancr 
 |-  ( ph -> ( 2s ^su N ) e. No )
8 muls01 
 |-  ( ( 2s ^su N ) e. No -> ( ( 2s ^su N ) x.s 0s ) = 0s )
9 7 8 syl 
 |-  ( ph -> ( ( 2s ^su N ) x.s 0s ) = 0s )
10 1 negsidd 
 |-  ( ph -> ( A +s ( -us ` A ) ) = 0s )
11 9 10 eqtr4d 
 |-  ( ph -> ( ( 2s ^su N ) x.s 0s ) = ( A +s ( -us ` A ) ) )
12 1 negscld 
 |-  ( ph -> ( -us ` A ) e. No )
13 1 12 addscld 
 |-  ( ph -> ( A +s ( -us ` A ) ) e. No )
14 0sno 
 |-  0s e. No
15 14 a1i 
 |-  ( ph -> 0s e. No )
16 13 15 2 pw2divsmuld 
 |-  ( ph -> ( ( ( A +s ( -us ` A ) ) /su ( 2s ^su N ) ) = 0s <-> ( ( 2s ^su N ) x.s 0s ) = ( A +s ( -us ` A ) ) ) )
17 11 16 mpbird 
 |-  ( ph -> ( ( A +s ( -us ` A ) ) /su ( 2s ^su N ) ) = 0s )
18 1 12 2 pw2divsdird 
 |-  ( ph -> ( ( A +s ( -us ` A ) ) /su ( 2s ^su N ) ) = ( ( A /su ( 2s ^su N ) ) +s ( ( -us ` A ) /su ( 2s ^su N ) ) ) )
19 4 17 18 3eqtr2rd 
 |-  ( ph -> ( ( A /su ( 2s ^su N ) ) +s ( ( -us ` A ) /su ( 2s ^su N ) ) ) = ( ( A /su ( 2s ^su N ) ) +s ( -us ` ( A /su ( 2s ^su N ) ) ) ) )
20 12 2 pw2divscld 
 |-  ( ph -> ( ( -us ` A ) /su ( 2s ^su N ) ) e. No )
21 3 negscld 
 |-  ( ph -> ( -us ` ( A /su ( 2s ^su N ) ) ) e. No )
22 20 21 3 addscan1d 
 |-  ( ph -> ( ( ( A /su ( 2s ^su N ) ) +s ( ( -us ` A ) /su ( 2s ^su N ) ) ) = ( ( A /su ( 2s ^su N ) ) +s ( -us ` ( A /su ( 2s ^su N ) ) ) ) <-> ( ( -us ` A ) /su ( 2s ^su N ) ) = ( -us ` ( A /su ( 2s ^su N ) ) ) ) )
23 19 22 mpbid 
 |-  ( ph -> ( ( -us ` A ) /su ( 2s ^su N ) ) = ( -us ` ( A /su ( 2s ^su N ) ) ) )
24 23 eqcomd 
 |-  ( ph -> ( -us ` ( A /su ( 2s ^su N ) ) ) = ( ( -us ` A ) /su ( 2s ^su N ) ) )