Metamath Proof Explorer

Theorem bitsfzolem

Description: Lemma for bitsfzo . (Contributed by Mario Carneiro, 5-Sep-2016) (Revised by AV, 1-Oct-2020)

Ref Expression
Hypotheses bitsfzo.1 
|- ( ph -> N e. NN0 )
bitsfzo.2 
|- ( ph -> M e. NN0 )
bitsfzo.3 
|- ( ph -> ( bits ` N ) C_ ( 0 ..^ M ) )
bitsfzo.4 
|- S = inf ( { n e. NN0 | N < ( 2 ^ n ) } , RR , < )
Assertion bitsfzolem 
|- ( ph -> N e. ( 0 ..^ ( 2 ^ M ) ) )

Proof

Step Hyp Ref Expression
1 bitsfzo.1 
 |-  ( ph -> N e. NN0 )
2 bitsfzo.2 
 |-  ( ph -> M e. NN0 )
3 bitsfzo.3 
 |-  ( ph -> ( bits ` N ) C_ ( 0 ..^ M ) )
4 bitsfzo.4 
 |-  S = inf ( { n e. NN0 | N < ( 2 ^ n ) } , RR , < )
5 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
6 1 5 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` 0 ) )
7 2nn 
 |-  2 e. NN
8 7 a1i 
 |-  ( ph -> 2 e. NN )
9 8 2 nnexpcld 
 |-  ( ph -> ( 2 ^ M ) e. NN )
10 9 nnzd 
 |-  ( ph -> ( 2 ^ M ) e. ZZ )
11 3 adantr 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> ( bits ` N ) C_ ( 0 ..^ M ) )
12 n2dvds1 
 |-  -. 2 || 1
13 7 a1i 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> 2 e. NN )
14 ssrab2 
 |-  { n e. NN0 | N < ( 2 ^ n ) } C_ NN0
15 14 5 sseqtri 
 |-  { n e. NN0 | N < ( 2 ^ n ) } C_ ( ZZ>= ` 0 )
16 nnssnn0 
 |-  NN C_ NN0
17 1 nn0red 
 |-  ( ph -> N e. RR )
18 2re 
 |-  2 e. RR
19 18 a1i 
 |-  ( ph -> 2 e. RR )
20 1lt2 
 |-  1 < 2
21 20 a1i 
 |-  ( ph -> 1 < 2 )
22 expnbnd 
 |-  ( ( N e. RR /\ 2 e. RR /\ 1 < 2 ) -> E. n e. NN N < ( 2 ^ n ) )
23 17 19 21 22 syl3anc 
 |-  ( ph -> E. n e. NN N < ( 2 ^ n ) )
24 ssrexv 
 |-  ( NN C_ NN0 -> ( E. n e. NN N < ( 2 ^ n ) -> E. n e. NN0 N < ( 2 ^ n ) ) )
25 16 23 24 mpsyl 
 |-  ( ph -> E. n e. NN0 N < ( 2 ^ n ) )
26 rabn0 
 |-  ( { n e. NN0 | N < ( 2 ^ n ) } =/= (/) <-> E. n e. NN0 N < ( 2 ^ n ) )
27 25 26 sylibr 
 |-  ( ph -> { n e. NN0 | N < ( 2 ^ n ) } =/= (/) )
28 infssuzcl 
 |-  ( ( { n e. NN0 | N < ( 2 ^ n ) } C_ ( ZZ>= ` 0 ) /\ { n e. NN0 | N < ( 2 ^ n ) } =/= (/) ) -> inf ( { n e. NN0 | N < ( 2 ^ n ) } , RR , < ) e. { n e. NN0 | N < ( 2 ^ n ) } )
29 15 27 28 sylancr 
 |-  ( ph -> inf ( { n e. NN0 | N < ( 2 ^ n ) } , RR , < ) e. { n e. NN0 | N < ( 2 ^ n ) } )
30 4 29 eqeltrid 
 |-  ( ph -> S e. { n e. NN0 | N < ( 2 ^ n ) } )
31 14 30 sselid 
 |-  ( ph -> S e. NN0 )
32 31 nn0zd 
 |-  ( ph -> S e. ZZ )
33 32 adantr 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> S e. ZZ )
34 0red 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> 0 e. RR )
35 2 nn0zd 
 |-  ( ph -> M e. ZZ )
36 35 adantr 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> M e. ZZ )
37 36 zred 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> M e. RR )
38 33 zred 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> S e. RR )
39 2 adantr 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> M e. NN0 )
40 39 nn0ge0d 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> 0 <_ M )
41 18 a1i 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> 2 e. RR )
42 41 39 reexpcld 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> ( 2 ^ M ) e. RR )
43 17 adantr 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> N e. RR )
44 8 31 nnexpcld 
 |-  ( ph -> ( 2 ^ S ) e. NN )
45 44 adantr 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> ( 2 ^ S ) e. NN )
46 45 nnred 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> ( 2 ^ S ) e. RR )
47 simpr 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> ( 2 ^ M ) <_ N )
48 30 adantr 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> S e. { n e. NN0 | N < ( 2 ^ n ) } )
49 oveq2 
 |-  ( m = S -> ( 2 ^ m ) = ( 2 ^ S ) )
50 49 breq2d 
 |-  ( m = S -> ( N < ( 2 ^ m ) <-> N < ( 2 ^ S ) ) )
51 oveq2 
 |-  ( n = m -> ( 2 ^ n ) = ( 2 ^ m ) )
52 51 breq2d 
 |-  ( n = m -> ( N < ( 2 ^ n ) <-> N < ( 2 ^ m ) ) )
53 52 cbvrabv 
 |-  { n e. NN0 | N < ( 2 ^ n ) } = { m e. NN0 | N < ( 2 ^ m ) }
54 50 53 elrab2 
 |-  ( S e. { n e. NN0 | N < ( 2 ^ n ) } <-> ( S e. NN0 /\ N < ( 2 ^ S ) ) )
55 54 simprbi 
 |-  ( S e. { n e. NN0 | N < ( 2 ^ n ) } -> N < ( 2 ^ S ) )
56 48 55 syl 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> N < ( 2 ^ S ) )
57 42 43 46 47 56 lelttrd 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> ( 2 ^ M ) < ( 2 ^ S ) )
58 20 a1i 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> 1 < 2 )
59 41 36 33 58 ltexp2d 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> ( M < S <-> ( 2 ^ M ) < ( 2 ^ S ) ) )
60 57 59 mpbird 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> M < S )
61 34 37 38 40 60 lelttrd 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> 0 < S )
62 elnnz 
 |-  ( S e. NN <-> ( S e. ZZ /\ 0 < S ) )
63 33 61 62 sylanbrc 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> S e. NN )
64 nnm1nn0 
 |-  ( S e. NN -> ( S - 1 ) e. NN0 )
65 63 64 syl 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> ( S - 1 ) e. NN0 )
66 13 65 nnexpcld 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> ( 2 ^ ( S - 1 ) ) e. NN )
67 66 nncnd 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> ( 2 ^ ( S - 1 ) ) e. CC )
68 67 mullidd 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> ( 1 x. ( 2 ^ ( S - 1 ) ) ) = ( 2 ^ ( S - 1 ) ) )
69 66 nnred 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> ( 2 ^ ( S - 1 ) ) e. RR )
70 38 ltm1d 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> ( S - 1 ) < S )
71 65 nn0red 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> ( S - 1 ) e. RR )
72 71 38 ltnled 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> ( ( S - 1 ) < S <-> -. S <_ ( S - 1 ) ) )
73 70 72 mpbid 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> -. S <_ ( S - 1 ) )
74 oveq2 
 |-  ( m = ( S - 1 ) -> ( 2 ^ m ) = ( 2 ^ ( S - 1 ) ) )
75 74 breq2d 
 |-  ( m = ( S - 1 ) -> ( N < ( 2 ^ m ) <-> N < ( 2 ^ ( S - 1 ) ) ) )
76 75 53 elrab2 
 |-  ( ( S - 1 ) e. { n e. NN0 | N < ( 2 ^ n ) } <-> ( ( S - 1 ) e. NN0 /\ N < ( 2 ^ ( S - 1 ) ) ) )
77 infssuzle 
 |-  ( ( { n e. NN0 | N < ( 2 ^ n ) } C_ ( ZZ>= ` 0 ) /\ ( S - 1 ) e. { n e. NN0 | N < ( 2 ^ n ) } ) -> inf ( { n e. NN0 | N < ( 2 ^ n ) } , RR , < ) <_ ( S - 1 ) )
78 15 77 mpan 
 |-  ( ( S - 1 ) e. { n e. NN0 | N < ( 2 ^ n ) } -> inf ( { n e. NN0 | N < ( 2 ^ n ) } , RR , < ) <_ ( S - 1 ) )
79 4 78 eqbrtrid 
 |-  ( ( S - 1 ) e. { n e. NN0 | N < ( 2 ^ n ) } -> S <_ ( S - 1 ) )
80 79 a1i 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> ( ( S - 1 ) e. { n e. NN0 | N < ( 2 ^ n ) } -> S <_ ( S - 1 ) ) )
81 76 80 biimtrrid 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> ( ( ( S - 1 ) e. NN0 /\ N < ( 2 ^ ( S - 1 ) ) ) -> S <_ ( S - 1 ) ) )
82 65 81 mpand 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> ( N < ( 2 ^ ( S - 1 ) ) -> S <_ ( S - 1 ) ) )
83 73 82 mtod 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> -. N < ( 2 ^ ( S - 1 ) ) )
84 69 43 83 nltled 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> ( 2 ^ ( S - 1 ) ) <_ N )
85 68 84 eqbrtrd 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> ( 1 x. ( 2 ^ ( S - 1 ) ) ) <_ N )
86 1red 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> 1 e. RR )
87 2rp 
 |-  2 e. RR+
88 87 a1i 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> 2 e. RR+ )
89 1z 
 |-  1 e. ZZ
90 89 a1i 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> 1 e. ZZ )
91 33 90 zsubcld 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> ( S - 1 ) e. ZZ )
92 88 91 rpexpcld 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> ( 2 ^ ( S - 1 ) ) e. RR+ )
93 86 43 92 lemuldivd 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> ( ( 1 x. ( 2 ^ ( S - 1 ) ) ) <_ N <-> 1 <_ ( N / ( 2 ^ ( S - 1 ) ) ) ) )
94 85 93 mpbid 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> 1 <_ ( N / ( 2 ^ ( S - 1 ) ) ) )
95 2cn 
 |-  2 e. CC
96 expm1t 
 |-  ( ( 2 e. CC /\ S e. NN ) -> ( 2 ^ S ) = ( ( 2 ^ ( S - 1 ) ) x. 2 ) )
97 95 63 96 sylancr 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> ( 2 ^ S ) = ( ( 2 ^ ( S - 1 ) ) x. 2 ) )
98 56 97 breqtrd 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> N < ( ( 2 ^ ( S - 1 ) ) x. 2 ) )
99 43 41 92 ltdivmuld 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> ( ( N / ( 2 ^ ( S - 1 ) ) ) < 2 <-> N < ( ( 2 ^ ( S - 1 ) ) x. 2 ) ) )
100 98 99 mpbird 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> ( N / ( 2 ^ ( S - 1 ) ) ) < 2 )
101 df-2 
 |-  2 = ( 1 + 1 )
102 100 101 breqtrdi 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> ( N / ( 2 ^ ( S - 1 ) ) ) < ( 1 + 1 ) )
103 43 92 rerpdivcld 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> ( N / ( 2 ^ ( S - 1 ) ) ) e. RR )
104 flbi 
 |-  ( ( ( N / ( 2 ^ ( S - 1 ) ) ) e. RR /\ 1 e. ZZ ) -> ( ( |_ ` ( N / ( 2 ^ ( S - 1 ) ) ) ) = 1 <-> ( 1 <_ ( N / ( 2 ^ ( S - 1 ) ) ) /\ ( N / ( 2 ^ ( S - 1 ) ) ) < ( 1 + 1 ) ) ) )
105 103 89 104 sylancl 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> ( ( |_ ` ( N / ( 2 ^ ( S - 1 ) ) ) ) = 1 <-> ( 1 <_ ( N / ( 2 ^ ( S - 1 ) ) ) /\ ( N / ( 2 ^ ( S - 1 ) ) ) < ( 1 + 1 ) ) ) )
106 94 102 105 mpbir2and 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> ( |_ ` ( N / ( 2 ^ ( S - 1 ) ) ) ) = 1 )
107 106 breq2d 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> ( 2 || ( |_ ` ( N / ( 2 ^ ( S - 1 ) ) ) ) <-> 2 || 1 ) )
108 12 107 mtbiri 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> -. 2 || ( |_ ` ( N / ( 2 ^ ( S - 1 ) ) ) ) )
109 1 nn0zd 
 |-  ( ph -> N e. ZZ )
110 bitsval2 
 |-  ( ( N e. ZZ /\ ( S - 1 ) e. NN0 ) -> ( ( S - 1 ) e. ( bits ` N ) <-> -. 2 || ( |_ ` ( N / ( 2 ^ ( S - 1 ) ) ) ) ) )
111 109 65 110 syl2an2r 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> ( ( S - 1 ) e. ( bits ` N ) <-> -. 2 || ( |_ ` ( N / ( 2 ^ ( S - 1 ) ) ) ) ) )
112 108 111 mpbird 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> ( S - 1 ) e. ( bits ` N ) )
113 11 112 sseldd 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> ( S - 1 ) e. ( 0 ..^ M ) )
114 elfzolt2 
 |-  ( ( S - 1 ) e. ( 0 ..^ M ) -> ( S - 1 ) < M )
115 113 114 syl 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> ( S - 1 ) < M )
116 zlem1lt 
 |-  ( ( S e. ZZ /\ M e. ZZ ) -> ( S <_ M <-> ( S - 1 ) < M ) )
117 32 36 116 syl2an2r 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> ( S <_ M <-> ( S - 1 ) < M ) )
118 115 117 mpbird 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> S <_ M )
119 37 38 ltnled 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> ( M < S <-> -. S <_ M ) )
120 60 119 mpbid 
 |-  ( ( ph /\ ( 2 ^ M ) <_ N ) -> -. S <_ M )
121 118 120 pm2.65da 
 |-  ( ph -> -. ( 2 ^ M ) <_ N )
122 9 nnred 
 |-  ( ph -> ( 2 ^ M ) e. RR )
123 17 122 ltnled 
 |-  ( ph -> ( N < ( 2 ^ M ) <-> -. ( 2 ^ M ) <_ N ) )
124 121 123 mpbird 
 |-  ( ph -> N < ( 2 ^ M ) )
125 elfzo2 
 |-  ( N e. ( 0 ..^ ( 2 ^ M ) ) <-> ( N e. ( ZZ>= ` 0 ) /\ ( 2 ^ M ) e. ZZ /\ N < ( 2 ^ M ) ) )
126 6 10 124 125 syl3anbrc 
 |-  ( ph -> N e. ( 0 ..^ ( 2 ^ M ) ) )