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 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
bitsfzo.2 ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
bitsfzo.3 ⊢ ( 𝜑 → ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) )
bitsfzo.4 ⊢ 𝑆 = inf ( { 𝑛 ∈ ℕ0 ∣ 𝑁 < ( 2 ↑ 𝑛 ) } , ℝ , < )
Assertion bitsfzolem ( 𝜑 → 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) )

Proof

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