Metamath Proof Explorer

Theorem bitsfzo

Description: The bits of a number are all less than M iff the number is nonnegative and less than 2 ^ M . (Contributed by Mario Carneiro, 5-Sep-2016) (Proof shortened by AV, 1-Oct-2020)

Ref Expression
Assertion bitsfzo 
|- ( ( N e. ZZ /\ M e. NN0 ) -> ( N e. ( 0 ..^ ( 2 ^ M ) ) <-> ( bits ` N ) C_ ( 0 ..^ M ) ) )

Proof

Step Hyp Ref Expression
1 bitsval 
 |-  ( m e. ( bits ` N ) <-> ( N e. ZZ /\ m e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) )
2 simp32 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ N e. ( 0 ..^ ( 2 ^ M ) ) /\ ( N e. ZZ /\ m e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) ) -> m e. NN0 )
3 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
4 2 3 eleqtrdi 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ N e. ( 0 ..^ ( 2 ^ M ) ) /\ ( N e. ZZ /\ m e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) ) -> m e. ( ZZ>= ` 0 ) )
5 simp1r 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ N e. ( 0 ..^ ( 2 ^ M ) ) /\ ( N e. ZZ /\ m e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) ) -> M e. NN0 )
6 5 nn0zd 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ N e. ( 0 ..^ ( 2 ^ M ) ) /\ ( N e. ZZ /\ m e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) ) -> M e. ZZ )
7 2re 
 |-  2 e. RR
8 7 a1i 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ N e. ( 0 ..^ ( 2 ^ M ) ) /\ ( N e. ZZ /\ m e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) ) -> 2 e. RR )
9 8 2 reexpcld 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ N e. ( 0 ..^ ( 2 ^ M ) ) /\ ( N e. ZZ /\ m e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) ) -> ( 2 ^ m ) e. RR )
10 simp1l 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ N e. ( 0 ..^ ( 2 ^ M ) ) /\ ( N e. ZZ /\ m e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) ) -> N e. ZZ )
11 10 zred 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ N e. ( 0 ..^ ( 2 ^ M ) ) /\ ( N e. ZZ /\ m e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) ) -> N e. RR )
12 8 5 reexpcld 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ N e. ( 0 ..^ ( 2 ^ M ) ) /\ ( N e. ZZ /\ m e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) ) -> ( 2 ^ M ) e. RR )
13 9 recnd 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ N e. ( 0 ..^ ( 2 ^ M ) ) /\ ( N e. ZZ /\ m e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) ) -> ( 2 ^ m ) e. CC )
14 13 mulid2d 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ N e. ( 0 ..^ ( 2 ^ M ) ) /\ ( N e. ZZ /\ m e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) ) -> ( 1 x. ( 2 ^ m ) ) = ( 2 ^ m ) )
15 simp33 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ N e. ( 0 ..^ ( 2 ^ M ) ) /\ ( N e. ZZ /\ m e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) ) -> -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) )
16 2rp 
 |-  2 e. RR+
17 16 a1i 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ N e. ( 0 ..^ ( 2 ^ M ) ) /\ ( N e. ZZ /\ m e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) ) -> 2 e. RR+ )
18 2 nn0zd 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ N e. ( 0 ..^ ( 2 ^ M ) ) /\ ( N e. ZZ /\ m e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) ) -> m e. ZZ )
19 17 18 rpexpcld 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ N e. ( 0 ..^ ( 2 ^ M ) ) /\ ( N e. ZZ /\ m e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) ) -> ( 2 ^ m ) e. RR+ )
20 11 19 rerpdivcld 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ N e. ( 0 ..^ ( 2 ^ M ) ) /\ ( N e. ZZ /\ m e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) ) -> ( N / ( 2 ^ m ) ) e. RR )
21 1red 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ N e. ( 0 ..^ ( 2 ^ M ) ) /\ ( N e. ZZ /\ m e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) ) -> 1 e. RR )
22 20 21 ltnled 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ N e. ( 0 ..^ ( 2 ^ M ) ) /\ ( N e. ZZ /\ m e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) ) -> ( ( N / ( 2 ^ m ) ) < 1 <-> -. 1 <_ ( N / ( 2 ^ m ) ) ) )
23 0p1e1 
 |-  ( 0 + 1 ) = 1
24 23 breq2i 
 |-  ( ( N / ( 2 ^ m ) ) < ( 0 + 1 ) <-> ( N / ( 2 ^ m ) ) < 1 )
25 elfzole1 
 |-  ( N e. ( 0 ..^ ( 2 ^ M ) ) -> 0 <_ N )
26 25 3ad2ant2 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ N e. ( 0 ..^ ( 2 ^ M ) ) /\ ( N e. ZZ /\ m e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) ) -> 0 <_ N )
27 11 19 26 divge0d 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ N e. ( 0 ..^ ( 2 ^ M ) ) /\ ( N e. ZZ /\ m e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) ) -> 0 <_ ( N / ( 2 ^ m ) ) )
28 0z 
 |-  0 e. ZZ
29 flbi 
 |-  ( ( ( N / ( 2 ^ m ) ) e. RR /\ 0 e. ZZ ) -> ( ( |_ ` ( N / ( 2 ^ m ) ) ) = 0 <-> ( 0 <_ ( N / ( 2 ^ m ) ) /\ ( N / ( 2 ^ m ) ) < ( 0 + 1 ) ) ) )
30 20 28 29 sylancl 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ N e. ( 0 ..^ ( 2 ^ M ) ) /\ ( N e. ZZ /\ m e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) ) -> ( ( |_ ` ( N / ( 2 ^ m ) ) ) = 0 <-> ( 0 <_ ( N / ( 2 ^ m ) ) /\ ( N / ( 2 ^ m ) ) < ( 0 + 1 ) ) ) )
31 z0even 
 |-  2 || 0
32 id 
 |-  ( ( |_ ` ( N / ( 2 ^ m ) ) ) = 0 -> ( |_ ` ( N / ( 2 ^ m ) ) ) = 0 )
33 31 32 breqtrrid 
 |-  ( ( |_ ` ( N / ( 2 ^ m ) ) ) = 0 -> 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) )
34 30 33 syl6bir 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ N e. ( 0 ..^ ( 2 ^ M ) ) /\ ( N e. ZZ /\ m e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) ) -> ( ( 0 <_ ( N / ( 2 ^ m ) ) /\ ( N / ( 2 ^ m ) ) < ( 0 + 1 ) ) -> 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) )
35 27 34 mpand 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ N e. ( 0 ..^ ( 2 ^ M ) ) /\ ( N e. ZZ /\ m e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) ) -> ( ( N / ( 2 ^ m ) ) < ( 0 + 1 ) -> 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) )
36 24 35 syl5bir 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ N e. ( 0 ..^ ( 2 ^ M ) ) /\ ( N e. ZZ /\ m e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) ) -> ( ( N / ( 2 ^ m ) ) < 1 -> 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) )
37 22 36 sylbird 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ N e. ( 0 ..^ ( 2 ^ M ) ) /\ ( N e. ZZ /\ m e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) ) -> ( -. 1 <_ ( N / ( 2 ^ m ) ) -> 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) )
38 15 37 mt3d 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ N e. ( 0 ..^ ( 2 ^ M ) ) /\ ( N e. ZZ /\ m e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) ) -> 1 <_ ( N / ( 2 ^ m ) ) )
39 21 11 19 lemuldivd 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ N e. ( 0 ..^ ( 2 ^ M ) ) /\ ( N e. ZZ /\ m e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) ) -> ( ( 1 x. ( 2 ^ m ) ) <_ N <-> 1 <_ ( N / ( 2 ^ m ) ) ) )
40 38 39 mpbird 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ N e. ( 0 ..^ ( 2 ^ M ) ) /\ ( N e. ZZ /\ m e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) ) -> ( 1 x. ( 2 ^ m ) ) <_ N )
41 14 40 eqbrtrrd 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ N e. ( 0 ..^ ( 2 ^ M ) ) /\ ( N e. ZZ /\ m e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) ) -> ( 2 ^ m ) <_ N )
42 elfzolt2 
 |-  ( N e. ( 0 ..^ ( 2 ^ M ) ) -> N < ( 2 ^ M ) )
43 42 3ad2ant2 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ N e. ( 0 ..^ ( 2 ^ M ) ) /\ ( N e. ZZ /\ m e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) ) -> N < ( 2 ^ M ) )
44 9 11 12 41 43 lelttrd 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ N e. ( 0 ..^ ( 2 ^ M ) ) /\ ( N e. ZZ /\ m e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) ) -> ( 2 ^ m ) < ( 2 ^ M ) )
45 1lt2 
 |-  1 < 2
46 45 a1i 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ N e. ( 0 ..^ ( 2 ^ M ) ) /\ ( N e. ZZ /\ m e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) ) -> 1 < 2 )
47 8 18 6 46 ltexp2d 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ N e. ( 0 ..^ ( 2 ^ M ) ) /\ ( N e. ZZ /\ m e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) ) -> ( m < M <-> ( 2 ^ m ) < ( 2 ^ M ) ) )
48 44 47 mpbird 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ N e. ( 0 ..^ ( 2 ^ M ) ) /\ ( N e. ZZ /\ m e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) ) -> m < M )
49 elfzo2 
 |-  ( m e. ( 0 ..^ M ) <-> ( m e. ( ZZ>= ` 0 ) /\ M e. ZZ /\ m < M ) )
50 4 6 48 49 syl3anbrc 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ N e. ( 0 ..^ ( 2 ^ M ) ) /\ ( N e. ZZ /\ m e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) ) -> m e. ( 0 ..^ M ) )
51 50 3expia 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ N e. ( 0 ..^ ( 2 ^ M ) ) ) -> ( ( N e. ZZ /\ m e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) -> m e. ( 0 ..^ M ) ) )
52 1 51 syl5bi 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ N e. ( 0 ..^ ( 2 ^ M ) ) ) -> ( m e. ( bits ` N ) -> m e. ( 0 ..^ M ) ) )
53 52 ssrdv 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ N e. ( 0 ..^ ( 2 ^ M ) ) ) -> ( bits ` N ) C_ ( 0 ..^ M ) )
54 simpr 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> -u N e. NN )
55 54 nnred 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> -u N e. RR )
56 simpllr 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> M e. NN0 )
57 56 nn0red 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> M e. RR )
58 max2 
 |-  ( ( -u N e. RR /\ M e. RR ) -> M <_ if ( -u N <_ M , M , -u N ) )
59 55 57 58 syl2anc 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> M <_ if ( -u N <_ M , M , -u N ) )
60 simplr 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> ( bits ` N ) C_ ( 0 ..^ M ) )
61 n2dvdsm1 
 |-  -. 2 || -u 1
62 simplll 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> N e. ZZ )
63 62 zred 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> N e. RR )
64 2nn 
 |-  2 e. NN
65 64 a1i 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> 2 e. NN )
66 54 nnnn0d 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> -u N e. NN0 )
67 56 66 ifcld 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> if ( -u N <_ M , M , -u N ) e. NN0 )
68 65 67 nnexpcld 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> ( 2 ^ if ( -u N <_ M , M , -u N ) ) e. NN )
69 63 68 nndivred 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> ( N / ( 2 ^ if ( -u N <_ M , M , -u N ) ) ) e. RR )
70 1red 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> 1 e. RR )
71 62 zcnd 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> N e. CC )
72 68 nncnd 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> ( 2 ^ if ( -u N <_ M , M , -u N ) ) e. CC )
73 2cnd 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> 2 e. CC )
74 2ne0 
 |-  2 =/= 0
75 74 a1i 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> 2 =/= 0 )
76 67 nn0zd 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> if ( -u N <_ M , M , -u N ) e. ZZ )
77 73 75 76 expne0d 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> ( 2 ^ if ( -u N <_ M , M , -u N ) ) =/= 0 )
78 71 72 77 divnegd 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> -u ( N / ( 2 ^ if ( -u N <_ M , M , -u N ) ) ) = ( -u N / ( 2 ^ if ( -u N <_ M , M , -u N ) ) ) )
79 67 nn0red 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> if ( -u N <_ M , M , -u N ) e. RR )
80 68 nnred 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> ( 2 ^ if ( -u N <_ M , M , -u N ) ) e. RR )
81 max1 
 |-  ( ( -u N e. RR /\ M e. RR ) -> -u N <_ if ( -u N <_ M , M , -u N ) )
82 55 57 81 syl2anc 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> -u N <_ if ( -u N <_ M , M , -u N ) )
83 2z 
 |-  2 e. ZZ
84 uzid 
 |-  ( 2 e. ZZ -> 2 e. ( ZZ>= ` 2 ) )
85 83 84 ax-mp 
 |-  2 e. ( ZZ>= ` 2 )
86 bernneq3 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ if ( -u N <_ M , M , -u N ) e. NN0 ) -> if ( -u N <_ M , M , -u N ) < ( 2 ^ if ( -u N <_ M , M , -u N ) ) )
87 85 67 86 sylancr 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> if ( -u N <_ M , M , -u N ) < ( 2 ^ if ( -u N <_ M , M , -u N ) ) )
88 79 80 87 ltled 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> if ( -u N <_ M , M , -u N ) <_ ( 2 ^ if ( -u N <_ M , M , -u N ) ) )
89 55 79 80 82 88 letrd 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> -u N <_ ( 2 ^ if ( -u N <_ M , M , -u N ) ) )
90 72 mulid1d 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> ( ( 2 ^ if ( -u N <_ M , M , -u N ) ) x. 1 ) = ( 2 ^ if ( -u N <_ M , M , -u N ) ) )
91 89 90 breqtrrd 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> -u N <_ ( ( 2 ^ if ( -u N <_ M , M , -u N ) ) x. 1 ) )
92 68 nnrpd 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> ( 2 ^ if ( -u N <_ M , M , -u N ) ) e. RR+ )
93 55 70 92 ledivmuld 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> ( ( -u N / ( 2 ^ if ( -u N <_ M , M , -u N ) ) ) <_ 1 <-> -u N <_ ( ( 2 ^ if ( -u N <_ M , M , -u N ) ) x. 1 ) ) )
94 91 93 mpbird 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> ( -u N / ( 2 ^ if ( -u N <_ M , M , -u N ) ) ) <_ 1 )
95 78 94 eqbrtrd 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> -u ( N / ( 2 ^ if ( -u N <_ M , M , -u N ) ) ) <_ 1 )
96 69 70 95 lenegcon1d 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> -u 1 <_ ( N / ( 2 ^ if ( -u N <_ M , M , -u N ) ) ) )
97 54 nngt0d 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> 0 < -u N )
98 68 nngt0d 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> 0 < ( 2 ^ if ( -u N <_ M , M , -u N ) ) )
99 55 80 97 98 divgt0d 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> 0 < ( -u N / ( 2 ^ if ( -u N <_ M , M , -u N ) ) ) )
100 99 78 breqtrrd 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> 0 < -u ( N / ( 2 ^ if ( -u N <_ M , M , -u N ) ) ) )
101 69 lt0neg1d 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> ( ( N / ( 2 ^ if ( -u N <_ M , M , -u N ) ) ) < 0 <-> 0 < -u ( N / ( 2 ^ if ( -u N <_ M , M , -u N ) ) ) ) )
102 100 101 mpbird 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> ( N / ( 2 ^ if ( -u N <_ M , M , -u N ) ) ) < 0 )
103 ax-1cn 
 |-  1 e. CC
104 neg1cn 
 |-  -u 1 e. CC
105 1pneg1e0 
 |-  ( 1 + -u 1 ) = 0
106 103 104 105 addcomli 
 |-  ( -u 1 + 1 ) = 0
107 102 106 breqtrrdi 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> ( N / ( 2 ^ if ( -u N <_ M , M , -u N ) ) ) < ( -u 1 + 1 ) )
108 neg1z 
 |-  -u 1 e. ZZ
109 flbi 
 |-  ( ( ( N / ( 2 ^ if ( -u N <_ M , M , -u N ) ) ) e. RR /\ -u 1 e. ZZ ) -> ( ( |_ ` ( N / ( 2 ^ if ( -u N <_ M , M , -u N ) ) ) ) = -u 1 <-> ( -u 1 <_ ( N / ( 2 ^ if ( -u N <_ M , M , -u N ) ) ) /\ ( N / ( 2 ^ if ( -u N <_ M , M , -u N ) ) ) < ( -u 1 + 1 ) ) ) )
110 69 108 109 sylancl 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> ( ( |_ ` ( N / ( 2 ^ if ( -u N <_ M , M , -u N ) ) ) ) = -u 1 <-> ( -u 1 <_ ( N / ( 2 ^ if ( -u N <_ M , M , -u N ) ) ) /\ ( N / ( 2 ^ if ( -u N <_ M , M , -u N ) ) ) < ( -u 1 + 1 ) ) ) )
111 96 107 110 mpbir2and 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> ( |_ ` ( N / ( 2 ^ if ( -u N <_ M , M , -u N ) ) ) ) = -u 1 )
112 111 breq2d 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> ( 2 || ( |_ ` ( N / ( 2 ^ if ( -u N <_ M , M , -u N ) ) ) ) <-> 2 || -u 1 ) )
113 61 112 mtbiri 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> -. 2 || ( |_ ` ( N / ( 2 ^ if ( -u N <_ M , M , -u N ) ) ) ) )
114 bitsval2 
 |-  ( ( N e. ZZ /\ if ( -u N <_ M , M , -u N ) e. NN0 ) -> ( if ( -u N <_ M , M , -u N ) e. ( bits ` N ) <-> -. 2 || ( |_ ` ( N / ( 2 ^ if ( -u N <_ M , M , -u N ) ) ) ) ) )
115 62 67 114 syl2anc 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> ( if ( -u N <_ M , M , -u N ) e. ( bits ` N ) <-> -. 2 || ( |_ ` ( N / ( 2 ^ if ( -u N <_ M , M , -u N ) ) ) ) ) )
116 113 115 mpbird 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> if ( -u N <_ M , M , -u N ) e. ( bits ` N ) )
117 60 116 sseldd 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> if ( -u N <_ M , M , -u N ) e. ( 0 ..^ M ) )
118 elfzolt2 
 |-  ( if ( -u N <_ M , M , -u N ) e. ( 0 ..^ M ) -> if ( -u N <_ M , M , -u N ) < M )
119 117 118 syl 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> if ( -u N <_ M , M , -u N ) < M )
120 79 57 ltnled 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> ( if ( -u N <_ M , M , -u N ) < M <-> -. M <_ if ( -u N <_ M , M , -u N ) ) )
121 119 120 mpbid 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) /\ -u N e. NN ) -> -. M <_ if ( -u N <_ M , M , -u N ) )
122 59 121 pm2.65da 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) -> -. -u N e. NN )
123 122 intnand 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) -> -. ( N e. RR /\ -u N e. NN ) )
124 simpll 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) -> N e. ZZ )
125 elznn0nn 
 |-  ( N e. ZZ <-> ( N e. NN0 \/ ( N e. RR /\ -u N e. NN ) ) )
126 124 125 sylib 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) -> ( N e. NN0 \/ ( N e. RR /\ -u N e. NN ) ) )
127 126 ord 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) -> ( -. N e. NN0 -> ( N e. RR /\ -u N e. NN ) ) )
128 123 127 mt3d 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) -> N e. NN0 )
129 simplr 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) -> M e. NN0 )
130 simpr 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) -> ( bits ` N ) C_ ( 0 ..^ M ) )
131 eqid 
 |-  inf ( { n e. NN0 | N < ( 2 ^ n ) } , RR , < ) = inf ( { n e. NN0 | N < ( 2 ^ n ) } , RR , < )
132 128 129 130 131 bitsfzolem 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ ( bits ` N ) C_ ( 0 ..^ M ) ) -> N e. ( 0 ..^ ( 2 ^ M ) ) )
133 53 132 impbida 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( N e. ( 0 ..^ ( 2 ^ M ) ) <-> ( bits ` N ) C_ ( 0 ..^ M ) ) )