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 ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) ↔ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) )

Proof

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