Metamath Proof Explorer

Theorem pw2divscan4d

Description: Cancellation law for divison by powers of two. (Contributed by Scott Fenton, 11-Dec-2025)

Ref Expression
Hypotheses pw2divscan4d.1 
|- ( ph -> A e. No )
pw2divscan4d.2 
|- ( ph -> N e. NN0_s )
pw2divscan4d.3 
|- ( ph -> M e. NN0_s )
Assertion pw2divscan4d 
|- ( ph -> ( A /su ( 2s ^su N ) ) = ( ( ( 2s ^su M ) x.s A ) /su ( 2s ^su ( N +s M ) ) ) )

Proof

Step Hyp Ref Expression
1 pw2divscan4d.1 
 |-  ( ph -> A e. No )
2 pw2divscan4d.2 
 |-  ( ph -> N e. NN0_s )
3 pw2divscan4d.3 
 |-  ( ph -> M e. NN0_s )
4 2sno 
 |-  2s e. No
5 expadds 
 |-  ( ( 2s e. No /\ N e. NN0_s /\ M e. NN0_s ) -> ( 2s ^su ( N +s M ) ) = ( ( 2s ^su N ) x.s ( 2s ^su M ) ) )
6 4 2 3 5 mp3an2i 
 |-  ( ph -> ( 2s ^su ( N +s M ) ) = ( ( 2s ^su N ) x.s ( 2s ^su M ) ) )
7 6 oveq1d 
 |-  ( ph -> ( ( 2s ^su ( N +s M ) ) x.s A ) = ( ( ( 2s ^su N ) x.s ( 2s ^su M ) ) x.s A ) )
8 expscl 
 |-  ( ( 2s e. No /\ N e. NN0_s ) -> ( 2s ^su N ) e. No )
9 4 2 8 sylancr 
 |-  ( ph -> ( 2s ^su N ) e. No )
10 expscl 
 |-  ( ( 2s e. No /\ M e. NN0_s ) -> ( 2s ^su M ) e. No )
11 4 3 10 sylancr 
 |-  ( ph -> ( 2s ^su M ) e. No )
12 9 11 1 mulsassd 
 |-  ( ph -> ( ( ( 2s ^su N ) x.s ( 2s ^su M ) ) x.s A ) = ( ( 2s ^su N ) x.s ( ( 2s ^su M ) x.s A ) ) )
13 7 12 eqtrd 
 |-  ( ph -> ( ( 2s ^su ( N +s M ) ) x.s A ) = ( ( 2s ^su N ) x.s ( ( 2s ^su M ) x.s A ) ) )
14 13 oveq1d 
 |-  ( ph -> ( ( ( 2s ^su ( N +s M ) ) x.s A ) /su ( 2s ^su ( N +s M ) ) ) = ( ( ( 2s ^su N ) x.s ( ( 2s ^su M ) x.s A ) ) /su ( 2s ^su ( N +s M ) ) ) )
15 n0addscl 
 |-  ( ( N e. NN0_s /\ M e. NN0_s ) -> ( N +s M ) e. NN0_s )
16 2 3 15 syl2anc 
 |-  ( ph -> ( N +s M ) e. NN0_s )
17 1 16 pw2divscan3d 
 |-  ( ph -> ( ( ( 2s ^su ( N +s M ) ) x.s A ) /su ( 2s ^su ( N +s M ) ) ) = A )
18 11 1 mulscld 
 |-  ( ph -> ( ( 2s ^su M ) x.s A ) e. No )
19 9 18 16 pw2divsassd 
 |-  ( ph -> ( ( ( 2s ^su N ) x.s ( ( 2s ^su M ) x.s A ) ) /su ( 2s ^su ( N +s M ) ) ) = ( ( 2s ^su N ) x.s ( ( ( 2s ^su M ) x.s A ) /su ( 2s ^su ( N +s M ) ) ) ) )
20 14 17 19 3eqtr3rd 
 |-  ( ph -> ( ( 2s ^su N ) x.s ( ( ( 2s ^su M ) x.s A ) /su ( 2s ^su ( N +s M ) ) ) ) = A )
21 18 16 pw2divscld 
 |-  ( ph -> ( ( ( 2s ^su M ) x.s A ) /su ( 2s ^su ( N +s M ) ) ) e. No )
22 1 21 2 pw2divsmuld 
 |-  ( ph -> ( ( A /su ( 2s ^su N ) ) = ( ( ( 2s ^su M ) x.s A ) /su ( 2s ^su ( N +s M ) ) ) <-> ( ( 2s ^su N ) x.s ( ( ( 2s ^su M ) x.s A ) /su ( 2s ^su ( N +s M ) ) ) ) = A ) )
23 20 22 mpbird 
 |-  ( ph -> ( A /su ( 2s ^su N ) ) = ( ( ( 2s ^su M ) x.s A ) /su ( 2s ^su ( N +s M ) ) ) )