Metamath Proof Explorer

Theorem bitsinv1lem

Description: Lemma for bitsinv1 . (Contributed by Mario Carneiro, 22-Sep-2016)

Ref Expression
Assertion bitsinv1lem 
|- ( ( N e. ZZ /\ M e. NN0 ) -> ( N mod ( 2 ^ ( M + 1 ) ) ) = ( ( N mod ( 2 ^ M ) ) + if ( M e. ( bits ` N ) , ( 2 ^ M ) , 0 ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( ( 2 ^ M ) = if ( M e. ( bits ` N ) , ( 2 ^ M ) , 0 ) -> ( ( N mod ( 2 ^ M ) ) + ( 2 ^ M ) ) = ( ( N mod ( 2 ^ M ) ) + if ( M e. ( bits ` N ) , ( 2 ^ M ) , 0 ) ) )
2 1 eqeq2d 
 |-  ( ( 2 ^ M ) = if ( M e. ( bits ` N ) , ( 2 ^ M ) , 0 ) -> ( ( N mod ( 2 ^ ( M + 1 ) ) ) = ( ( N mod ( 2 ^ M ) ) + ( 2 ^ M ) ) <-> ( N mod ( 2 ^ ( M + 1 ) ) ) = ( ( N mod ( 2 ^ M ) ) + if ( M e. ( bits ` N ) , ( 2 ^ M ) , 0 ) ) ) )
3 oveq2 
 |-  ( 0 = if ( M e. ( bits ` N ) , ( 2 ^ M ) , 0 ) -> ( ( N mod ( 2 ^ M ) ) + 0 ) = ( ( N mod ( 2 ^ M ) ) + if ( M e. ( bits ` N ) , ( 2 ^ M ) , 0 ) ) )
4 3 eqeq2d 
 |-  ( 0 = if ( M e. ( bits ` N ) , ( 2 ^ M ) , 0 ) -> ( ( N mod ( 2 ^ ( M + 1 ) ) ) = ( ( N mod ( 2 ^ M ) ) + 0 ) <-> ( N mod ( 2 ^ ( M + 1 ) ) ) = ( ( N mod ( 2 ^ M ) ) + if ( M e. ( bits ` N ) , ( 2 ^ M ) , 0 ) ) ) )
5 simpl 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> N e. ZZ )
6 2nn 
 |-  2 e. NN
7 6 a1i 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> 2 e. NN )
8 simpr 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> M e. NN0 )
9 7 8 nnexpcld 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( 2 ^ M ) e. NN )
10 5 9 zmodcld 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( N mod ( 2 ^ M ) ) e. NN0 )
11 10 nn0cnd 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( N mod ( 2 ^ M ) ) e. CC )
12 11 adantr 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ M e. ( bits ` N ) ) -> ( N mod ( 2 ^ M ) ) e. CC )
13 1nn0 
 |-  1 e. NN0
14 13 a1i 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> 1 e. NN0 )
15 8 14 nn0addcld 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( M + 1 ) e. NN0 )
16 7 15 nnexpcld 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( 2 ^ ( M + 1 ) ) e. NN )
17 5 16 zmodcld 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( N mod ( 2 ^ ( M + 1 ) ) ) e. NN0 )
18 17 nn0cnd 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( N mod ( 2 ^ ( M + 1 ) ) ) e. CC )
19 18 adantr 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ M e. ( bits ` N ) ) -> ( N mod ( 2 ^ ( M + 1 ) ) ) e. CC )
20 12 19 pncan3d 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ M e. ( bits ` N ) ) -> ( ( N mod ( 2 ^ M ) ) + ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) ) = ( N mod ( 2 ^ ( M + 1 ) ) ) )
21 18 11 subcld 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) e. CC )
22 21 adantr 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ M e. ( bits ` N ) ) -> ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) e. CC )
23 6 a1i 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ M e. ( bits ` N ) ) -> 2 e. NN )
24 simplr 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ M e. ( bits ` N ) ) -> M e. NN0 )
25 23 24 nnexpcld 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ M e. ( bits ` N ) ) -> ( 2 ^ M ) e. NN )
26 25 nncnd 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ M e. ( bits ` N ) ) -> ( 2 ^ M ) e. CC )
27 2cnd 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> 2 e. CC )
28 2ne0 
 |-  2 =/= 0
29 28 a1i 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> 2 =/= 0 )
30 8 nn0zd 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> M e. ZZ )
31 27 29 30 expne0d 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( 2 ^ M ) =/= 0 )
32 31 adantr 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ M e. ( bits ` N ) ) -> ( 2 ^ M ) =/= 0 )
33 z0even 
 |-  2 || 0
34 id 
 |-  ( ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) = 0 -> ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) = 0 )
35 33 34 breqtrrid 
 |-  ( ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) = 0 -> 2 || ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) )
36 bitsval2 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( M e. ( bits ` N ) <-> -. 2 || ( |_ ` ( N / ( 2 ^ M ) ) ) ) )
37 5 zred 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> N e. RR )
38 9 nnrpd 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( 2 ^ M ) e. RR+ )
39 moddiffl 
 |-  ( ( N e. RR /\ ( 2 ^ M ) e. RR+ ) -> ( ( N - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) = ( |_ ` ( N / ( 2 ^ M ) ) ) )
40 37 38 39 syl2anc 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( N - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) = ( |_ ` ( N / ( 2 ^ M ) ) ) )
41 40 breq2d 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( 2 || ( ( N - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) <-> 2 || ( |_ ` ( N / ( 2 ^ M ) ) ) ) )
42 2z 
 |-  2 e. ZZ
43 42 a1i 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> 2 e. ZZ )
44 moddifz 
 |-  ( ( N e. RR /\ ( 2 ^ M ) e. RR+ ) -> ( ( N - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) e. ZZ )
45 37 38 44 syl2anc 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( N - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) e. ZZ )
46 5 zcnd 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> N e. CC )
47 46 11 18 nnncan1d 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( N - ( N mod ( 2 ^ M ) ) ) - ( N - ( N mod ( 2 ^ ( M + 1 ) ) ) ) ) = ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) )
48 47 oveq1d 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( ( N - ( N mod ( 2 ^ M ) ) ) - ( N - ( N mod ( 2 ^ ( M + 1 ) ) ) ) ) / ( 2 ^ M ) ) = ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) )
49 46 11 subcld 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( N - ( N mod ( 2 ^ M ) ) ) e. CC )
50 46 18 subcld 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( N - ( N mod ( 2 ^ ( M + 1 ) ) ) ) e. CC )
51 9 nncnd 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( 2 ^ M ) e. CC )
52 49 50 51 31 divsubdird 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( ( N - ( N mod ( 2 ^ M ) ) ) - ( N - ( N mod ( 2 ^ ( M + 1 ) ) ) ) ) / ( 2 ^ M ) ) = ( ( ( N - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) - ( ( N - ( N mod ( 2 ^ ( M + 1 ) ) ) ) / ( 2 ^ M ) ) ) )
53 48 52 eqtr3d 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) = ( ( ( N - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) - ( ( N - ( N mod ( 2 ^ ( M + 1 ) ) ) ) / ( 2 ^ M ) ) ) )
54 27 50 mulcomd 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( 2 x. ( N - ( N mod ( 2 ^ ( M + 1 ) ) ) ) ) = ( ( N - ( N mod ( 2 ^ ( M + 1 ) ) ) ) x. 2 ) )
55 27 51 mulcomd 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( 2 x. ( 2 ^ M ) ) = ( ( 2 ^ M ) x. 2 ) )
56 27 8 expp1d 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( 2 ^ ( M + 1 ) ) = ( ( 2 ^ M ) x. 2 ) )
57 55 56 eqtr4d 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( 2 x. ( 2 ^ M ) ) = ( 2 ^ ( M + 1 ) ) )
58 54 57 oveq12d 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( 2 x. ( N - ( N mod ( 2 ^ ( M + 1 ) ) ) ) ) / ( 2 x. ( 2 ^ M ) ) ) = ( ( ( N - ( N mod ( 2 ^ ( M + 1 ) ) ) ) x. 2 ) / ( 2 ^ ( M + 1 ) ) ) )
59 50 51 27 31 29 divcan5d 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( 2 x. ( N - ( N mod ( 2 ^ ( M + 1 ) ) ) ) ) / ( 2 x. ( 2 ^ M ) ) ) = ( ( N - ( N mod ( 2 ^ ( M + 1 ) ) ) ) / ( 2 ^ M ) ) )
60 16 nncnd 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( 2 ^ ( M + 1 ) ) e. CC )
61 30 peano2zd 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( M + 1 ) e. ZZ )
62 27 29 61 expne0d 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( 2 ^ ( M + 1 ) ) =/= 0 )
63 50 27 60 62 div23d 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( ( N - ( N mod ( 2 ^ ( M + 1 ) ) ) ) x. 2 ) / ( 2 ^ ( M + 1 ) ) ) = ( ( ( N - ( N mod ( 2 ^ ( M + 1 ) ) ) ) / ( 2 ^ ( M + 1 ) ) ) x. 2 ) )
64 58 59 63 3eqtr3d 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( N - ( N mod ( 2 ^ ( M + 1 ) ) ) ) / ( 2 ^ M ) ) = ( ( ( N - ( N mod ( 2 ^ ( M + 1 ) ) ) ) / ( 2 ^ ( M + 1 ) ) ) x. 2 ) )
65 16 nnrpd 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( 2 ^ ( M + 1 ) ) e. RR+ )
66 moddifz 
 |-  ( ( N e. RR /\ ( 2 ^ ( M + 1 ) ) e. RR+ ) -> ( ( N - ( N mod ( 2 ^ ( M + 1 ) ) ) ) / ( 2 ^ ( M + 1 ) ) ) e. ZZ )
67 37 65 66 syl2anc 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( N - ( N mod ( 2 ^ ( M + 1 ) ) ) ) / ( 2 ^ ( M + 1 ) ) ) e. ZZ )
68 67 43 zmulcld 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( ( N - ( N mod ( 2 ^ ( M + 1 ) ) ) ) / ( 2 ^ ( M + 1 ) ) ) x. 2 ) e. ZZ )
69 64 68 eqeltrd 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( N - ( N mod ( 2 ^ ( M + 1 ) ) ) ) / ( 2 ^ M ) ) e. ZZ )
70 45 69 zsubcld 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( ( N - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) - ( ( N - ( N mod ( 2 ^ ( M + 1 ) ) ) ) / ( 2 ^ M ) ) ) e. ZZ )
71 53 70 eqeltrd 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) e. ZZ )
72 dvdsmul2 
 |-  ( ( ( ( N - ( N mod ( 2 ^ ( M + 1 ) ) ) ) / ( 2 ^ ( M + 1 ) ) ) e. ZZ /\ 2 e. ZZ ) -> 2 || ( ( ( N - ( N mod ( 2 ^ ( M + 1 ) ) ) ) / ( 2 ^ ( M + 1 ) ) ) x. 2 ) )
73 67 43 72 syl2anc 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> 2 || ( ( ( N - ( N mod ( 2 ^ ( M + 1 ) ) ) ) / ( 2 ^ ( M + 1 ) ) ) x. 2 ) )
74 46 18 11 nnncan2d 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( N - ( N mod ( 2 ^ M ) ) ) - ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) ) = ( N - ( N mod ( 2 ^ ( M + 1 ) ) ) ) )
75 74 oveq1d 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( ( N - ( N mod ( 2 ^ M ) ) ) - ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) ) / ( 2 ^ M ) ) = ( ( N - ( N mod ( 2 ^ ( M + 1 ) ) ) ) / ( 2 ^ M ) ) )
76 49 21 51 31 divsubdird 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( ( N - ( N mod ( 2 ^ M ) ) ) - ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) ) / ( 2 ^ M ) ) = ( ( ( N - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) - ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) ) )
77 75 76 64 3eqtr3d 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( ( N - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) - ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) ) = ( ( ( N - ( N mod ( 2 ^ ( M + 1 ) ) ) ) / ( 2 ^ ( M + 1 ) ) ) x. 2 ) )
78 73 77 breqtrrd 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> 2 || ( ( ( N - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) - ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) ) )
79 dvdssub2 
 |-  ( ( ( 2 e. ZZ /\ ( ( N - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) e. ZZ /\ ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) e. ZZ ) /\ 2 || ( ( ( N - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) - ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) ) ) -> ( 2 || ( ( N - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) <-> 2 || ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) ) )
80 43 45 71 78 79 syl31anc 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( 2 || ( ( N - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) <-> 2 || ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) ) )
81 41 80 bitr3d 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( 2 || ( |_ ` ( N / ( 2 ^ M ) ) ) <-> 2 || ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) ) )
82 81 notbid 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( -. 2 || ( |_ ` ( N / ( 2 ^ M ) ) ) <-> -. 2 || ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) ) )
83 36 82 bitrd 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( M e. ( bits ` N ) <-> -. 2 || ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) ) )
84 83 con2bid 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( 2 || ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) <-> -. M e. ( bits ` N ) ) )
85 35 84 syl5ib 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) = 0 -> -. M e. ( bits ` N ) ) )
86 85 con2d 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( M e. ( bits ` N ) -> -. ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) = 0 ) )
87 df-neg 
 |-  -u 1 = ( 0 - 1 )
88 51 mulm1d 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( -u 1 x. ( 2 ^ M ) ) = -u ( 2 ^ M ) )
89 9 nnred 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( 2 ^ M ) e. RR )
90 89 renegcld 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> -u ( 2 ^ M ) e. RR )
91 37 38 modcld 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( N mod ( 2 ^ M ) ) e. RR )
92 91 renegcld 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> -u ( N mod ( 2 ^ M ) ) e. RR )
93 37 65 modcld 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( N mod ( 2 ^ ( M + 1 ) ) ) e. RR )
94 93 91 resubcld 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) e. RR )
95 modlt 
 |-  ( ( N e. RR /\ ( 2 ^ M ) e. RR+ ) -> ( N mod ( 2 ^ M ) ) < ( 2 ^ M ) )
96 37 38 95 syl2anc 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( N mod ( 2 ^ M ) ) < ( 2 ^ M ) )
97 91 89 ltnegd 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( N mod ( 2 ^ M ) ) < ( 2 ^ M ) <-> -u ( 2 ^ M ) < -u ( N mod ( 2 ^ M ) ) ) )
98 96 97 mpbid 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> -u ( 2 ^ M ) < -u ( N mod ( 2 ^ M ) ) )
99 df-neg 
 |-  -u ( N mod ( 2 ^ M ) ) = ( 0 - ( N mod ( 2 ^ M ) ) )
100 0red 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> 0 e. RR )
101 modge0 
 |-  ( ( N e. RR /\ ( 2 ^ ( M + 1 ) ) e. RR+ ) -> 0 <_ ( N mod ( 2 ^ ( M + 1 ) ) ) )
102 37 65 101 syl2anc 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> 0 <_ ( N mod ( 2 ^ ( M + 1 ) ) ) )
103 100 93 91 102 lesub1dd 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( 0 - ( N mod ( 2 ^ M ) ) ) <_ ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) )
104 99 103 eqbrtrid 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> -u ( N mod ( 2 ^ M ) ) <_ ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) )
105 90 92 94 98 104 ltletrd 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> -u ( 2 ^ M ) < ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) )
106 88 105 eqbrtrd 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( -u 1 x. ( 2 ^ M ) ) < ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) )
107 1red 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> 1 e. RR )
108 107 renegcld 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> -u 1 e. RR )
109 108 94 38 ltmuldivd 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( -u 1 x. ( 2 ^ M ) ) < ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) <-> -u 1 < ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) ) )
110 106 109 mpbid 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> -u 1 < ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) )
111 87 110 eqbrtrrid 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( 0 - 1 ) < ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) )
112 0zd 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> 0 e. ZZ )
113 zlem1lt 
 |-  ( ( 0 e. ZZ /\ ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) e. ZZ ) -> ( 0 <_ ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) <-> ( 0 - 1 ) < ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) ) )
114 112 71 113 syl2anc 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( 0 <_ ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) <-> ( 0 - 1 ) < ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) ) )
115 111 114 mpbird 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> 0 <_ ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) )
116 elnn0z 
 |-  ( ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) e. NN0 <-> ( ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) e. ZZ /\ 0 <_ ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) ) )
117 71 115 116 sylanbrc 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) e. NN0 )
118 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
119 117 118 eleqtrdi 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) e. ( ZZ>= ` 0 ) )
120 16 nnred 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( 2 ^ ( M + 1 ) ) e. RR )
121 modge0 
 |-  ( ( N e. RR /\ ( 2 ^ M ) e. RR+ ) -> 0 <_ ( N mod ( 2 ^ M ) ) )
122 37 38 121 syl2anc 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> 0 <_ ( N mod ( 2 ^ M ) ) )
123 93 91 subge02d 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( 0 <_ ( N mod ( 2 ^ M ) ) <-> ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) <_ ( N mod ( 2 ^ ( M + 1 ) ) ) ) )
124 122 123 mpbid 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) <_ ( N mod ( 2 ^ ( M + 1 ) ) ) )
125 modlt 
 |-  ( ( N e. RR /\ ( 2 ^ ( M + 1 ) ) e. RR+ ) -> ( N mod ( 2 ^ ( M + 1 ) ) ) < ( 2 ^ ( M + 1 ) ) )
126 37 65 125 syl2anc 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( N mod ( 2 ^ ( M + 1 ) ) ) < ( 2 ^ ( M + 1 ) ) )
127 94 93 120 124 126 lelttrd 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) < ( 2 ^ ( M + 1 ) ) )
128 127 56 breqtrd 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) < ( ( 2 ^ M ) x. 2 ) )
129 7 nnred 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> 2 e. RR )
130 94 129 38 ltdivmuld 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) < 2 <-> ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) < ( ( 2 ^ M ) x. 2 ) ) )
131 128 130 mpbird 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) < 2 )
132 elfzo2 
 |-  ( ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) e. ( 0 ..^ 2 ) <-> ( ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) e. ( ZZ>= ` 0 ) /\ 2 e. ZZ /\ ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) < 2 ) )
133 119 43 131 132 syl3anbrc 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) e. ( 0 ..^ 2 ) )
134 fzo0to2pr 
 |-  ( 0 ..^ 2 ) = { 0 , 1 }
135 133 134 eleqtrdi 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) e. { 0 , 1 } )
136 elpri 
 |-  ( ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) e. { 0 , 1 } -> ( ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) = 0 \/ ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) = 1 ) )
137 135 136 syl 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) = 0 \/ ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) = 1 ) )
138 137 ord 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( -. ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) = 0 -> ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) = 1 ) )
139 86 138 syld 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( M e. ( bits ` N ) -> ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) = 1 ) )
140 139 imp 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ M e. ( bits ` N ) ) -> ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) = 1 )
141 22 26 32 140 diveq1d 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ M e. ( bits ` N ) ) -> ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) = ( 2 ^ M ) )
142 141 oveq2d 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ M e. ( bits ` N ) ) -> ( ( N mod ( 2 ^ M ) ) + ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) ) = ( ( N mod ( 2 ^ M ) ) + ( 2 ^ M ) ) )
143 20 142 eqtr3d 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ M e. ( bits ` N ) ) -> ( N mod ( 2 ^ ( M + 1 ) ) ) = ( ( N mod ( 2 ^ M ) ) + ( 2 ^ M ) ) )
144 18 adantr 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ -. M e. ( bits ` N ) ) -> ( N mod ( 2 ^ ( M + 1 ) ) ) e. CC )
145 11 adantr 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ -. M e. ( bits ` N ) ) -> ( N mod ( 2 ^ M ) ) e. CC )
146 21 adantr 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ -. M e. ( bits ` N ) ) -> ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) e. CC )
147 51 adantr 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ -. M e. ( bits ` N ) ) -> ( 2 ^ M ) e. CC )
148 31 adantr 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ -. M e. ( bits ` N ) ) -> ( 2 ^ M ) =/= 0 )
149 n2dvds1 
 |-  -. 2 || 1
150 breq2 
 |-  ( ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) = 1 -> ( 2 || ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) <-> 2 || 1 ) )
151 149 150 mtbiri 
 |-  ( ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) = 1 -> -. 2 || ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) )
152 138 151 syl6 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( -. ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) = 0 -> -. 2 || ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) ) )
153 152 83 sylibrd 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( -. ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) = 0 -> M e. ( bits ` N ) ) )
154 153 con1d 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( -. M e. ( bits ` N ) -> ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) = 0 ) )
155 154 imp 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ -. M e. ( bits ` N ) ) -> ( ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) = 0 )
156 146 147 148 155 diveq0d 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ -. M e. ( bits ` N ) ) -> ( ( N mod ( 2 ^ ( M + 1 ) ) ) - ( N mod ( 2 ^ M ) ) ) = 0 )
157 144 145 156 subeq0d 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ -. M e. ( bits ` N ) ) -> ( N mod ( 2 ^ ( M + 1 ) ) ) = ( N mod ( 2 ^ M ) ) )
158 145 addid1d 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ -. M e. ( bits ` N ) ) -> ( ( N mod ( 2 ^ M ) ) + 0 ) = ( N mod ( 2 ^ M ) ) )
159 157 158 eqtr4d 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ -. M e. ( bits ` N ) ) -> ( N mod ( 2 ^ ( M + 1 ) ) ) = ( ( N mod ( 2 ^ M ) ) + 0 ) )
160 2 4 143 159 ifbothda 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( N mod ( 2 ^ ( M + 1 ) ) ) = ( ( N mod ( 2 ^ M ) ) + if ( M e. ( bits ` N ) , ( 2 ^ M ) , 0 ) ) )