Step | Hyp | Ref
| Expression |
1 | | bitsval 15146 |
. . . 4
⊢ (𝑚 ∈ (bits‘𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑚 ∈ ℕ0 ∧ ¬ 2
∥ (⌊‘(𝑁 /
(2↑𝑚))))) |
2 | | simp32 1098 |
. . . . . . 7
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 𝑚 ∈ ℕ0) |
3 | | nn0uz 11722 |
. . . . . . 7
⊢
ℕ0 = (ℤ≥‘0) |
4 | 2, 3 | syl6eleq 2711 |
. . . . . 6
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 𝑚 ∈
(ℤ≥‘0)) |
5 | | simp1r 1086 |
. . . . . . 7
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 𝑀 ∈
ℕ0) |
6 | 5 | nn0zd 11480 |
. . . . . 6
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 𝑀 ∈ ℤ) |
7 | | 2re 11090 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ |
8 | 7 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 2 ∈
ℝ) |
9 | 8, 2 | reexpcld 13025 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → (2↑𝑚) ∈ ℝ) |
10 | | simp1l 1085 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 𝑁 ∈ ℤ) |
11 | 10 | zred 11482 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 𝑁 ∈ ℝ) |
12 | 8, 5 | reexpcld 13025 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → (2↑𝑀) ∈ ℝ) |
13 | 9 | recnd 10068 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → (2↑𝑚) ∈ ℂ) |
14 | 13 | mulid2d 10058 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → (1 · (2↑𝑚)) = (2↑𝑚)) |
15 | | simp33 1099 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → ¬ 2 ∥
(⌊‘(𝑁 /
(2↑𝑚)))) |
16 | | 2rp 11837 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℝ+ |
17 | 16 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 2 ∈
ℝ+) |
18 | 2 | nn0zd 11480 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 𝑚 ∈ ℤ) |
19 | 17, 18 | rpexpcld 13032 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → (2↑𝑚) ∈
ℝ+) |
20 | 11, 19 | rerpdivcld 11903 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → (𝑁 / (2↑𝑚)) ∈ ℝ) |
21 | | 1red 10055 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 1 ∈
ℝ) |
22 | 20, 21 | ltnled 10184 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → ((𝑁 / (2↑𝑚)) < 1 ↔ ¬ 1 ≤ (𝑁 / (2↑𝑚)))) |
23 | | 0p1e1 11132 |
. . . . . . . . . . . . . 14
⊢ (0 + 1) =
1 |
24 | 23 | breq2i 4661 |
. . . . . . . . . . . . 13
⊢ ((𝑁 / (2↑𝑚)) < (0 + 1) ↔ (𝑁 / (2↑𝑚)) < 1) |
25 | | elfzole1 12478 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ (0..^(2↑𝑀)) → 0 ≤ 𝑁) |
26 | 25 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 0 ≤ 𝑁) |
27 | 11, 19, 26 | divge0d 11912 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 0 ≤ (𝑁 / (2↑𝑚))) |
28 | | 0z 11388 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℤ |
29 | | flbi 12617 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 / (2↑𝑚)) ∈ ℝ ∧ 0 ∈ ℤ)
→ ((⌊‘(𝑁 /
(2↑𝑚))) = 0 ↔ (0
≤ (𝑁 / (2↑𝑚)) ∧ (𝑁 / (2↑𝑚)) < (0 + 1)))) |
30 | 20, 28, 29 | sylancl 694 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → ((⌊‘(𝑁 / (2↑𝑚))) = 0 ↔ (0 ≤ (𝑁 / (2↑𝑚)) ∧ (𝑁 / (2↑𝑚)) < (0 + 1)))) |
31 | | 2z 11409 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℤ |
32 | | dvds0 14997 |
. . . . . . . . . . . . . . . . 17
⊢ (2 ∈
ℤ → 2 ∥ 0) |
33 | 31, 32 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∥
0 |
34 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢
((⌊‘(𝑁 /
(2↑𝑚))) = 0 →
(⌊‘(𝑁 /
(2↑𝑚))) =
0) |
35 | 33, 34 | syl5breqr 4691 |
. . . . . . . . . . . . . . 15
⊢
((⌊‘(𝑁 /
(2↑𝑚))) = 0 → 2
∥ (⌊‘(𝑁 /
(2↑𝑚)))) |
36 | 30, 35 | syl6bir 244 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → ((0 ≤ (𝑁 / (2↑𝑚)) ∧ (𝑁 / (2↑𝑚)) < (0 + 1)) → 2 ∥
(⌊‘(𝑁 /
(2↑𝑚))))) |
37 | 27, 36 | mpand 711 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → ((𝑁 / (2↑𝑚)) < (0 + 1) → 2 ∥
(⌊‘(𝑁 /
(2↑𝑚))))) |
38 | 24, 37 | syl5bir 233 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → ((𝑁 / (2↑𝑚)) < 1 → 2 ∥
(⌊‘(𝑁 /
(2↑𝑚))))) |
39 | 22, 38 | sylbird 250 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → (¬ 1 ≤ (𝑁 / (2↑𝑚)) → 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) |
40 | 15, 39 | mt3d 140 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 1 ≤ (𝑁 / (2↑𝑚))) |
41 | 21, 11, 19 | lemuldivd 11921 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → ((1 · (2↑𝑚)) ≤ 𝑁 ↔ 1 ≤ (𝑁 / (2↑𝑚)))) |
42 | 40, 41 | mpbird 247 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → (1 · (2↑𝑚)) ≤ 𝑁) |
43 | 14, 42 | eqbrtrrd 4677 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → (2↑𝑚) ≤ 𝑁) |
44 | | elfzolt2 12479 |
. . . . . . . . 9
⊢ (𝑁 ∈ (0..^(2↑𝑀)) → 𝑁 < (2↑𝑀)) |
45 | 44 | 3ad2ant2 1083 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 𝑁 < (2↑𝑀)) |
46 | 9, 11, 12, 43, 45 | lelttrd 10195 |
. . . . . . 7
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → (2↑𝑚) < (2↑𝑀)) |
47 | | 1lt2 11194 |
. . . . . . . . 9
⊢ 1 <
2 |
48 | 47 | a1i 11 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 1 < 2) |
49 | 8, 18, 6, 48 | ltexp2d 13038 |
. . . . . . 7
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → (𝑚 < 𝑀 ↔ (2↑𝑚) < (2↑𝑀))) |
50 | 46, 49 | mpbird 247 |
. . . . . 6
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 𝑚 < 𝑀) |
51 | | elfzo2 12473 |
. . . . . 6
⊢ (𝑚 ∈ (0..^𝑀) ↔ (𝑚 ∈ (ℤ≥‘0)
∧ 𝑀 ∈ ℤ
∧ 𝑚 < 𝑀)) |
52 | 4, 6, 50, 51 | syl3anbrc 1246 |
. . . . 5
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 𝑚 ∈ (0..^𝑀)) |
53 | 52 | 3expia 1267 |
. . . 4
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀))) →
((𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚)))) → 𝑚 ∈ (0..^𝑀))) |
54 | 1, 53 | syl5bi 232 |
. . 3
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀))) →
(𝑚 ∈ (bits‘𝑁) → 𝑚 ∈ (0..^𝑀))) |
55 | 54 | ssrdv 3609 |
. 2
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀))) →
(bits‘𝑁) ⊆
(0..^𝑀)) |
56 | | simpr 477 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
-𝑁 ∈
ℕ) |
57 | 56 | nnred 11035 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
-𝑁 ∈
ℝ) |
58 | | simpllr 799 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
𝑀 ∈
ℕ0) |
59 | 58 | nn0red 11352 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
𝑀 ∈
ℝ) |
60 | | max2 12018 |
. . . . . . 7
⊢ ((-𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ) → 𝑀 ≤ if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)) |
61 | 57, 59, 60 | syl2anc 693 |
. . . . . 6
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
𝑀 ≤ if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)) |
62 | | simplr 792 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
(bits‘𝑁) ⊆
(0..^𝑀)) |
63 | | n2dvds1 15104 |
. . . . . . . . . . . 12
⊢ ¬ 2
∥ 1 |
64 | | 1z 11407 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℤ |
65 | | dvdsnegb 14999 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℤ ∧ 1 ∈ ℤ) → (2 ∥ 1 ↔ 2 ∥
-1)) |
66 | 31, 64, 65 | mp2an 708 |
. . . . . . . . . . . 12
⊢ (2
∥ 1 ↔ 2 ∥ -1) |
67 | 63, 66 | mtbi 312 |
. . . . . . . . . . 11
⊢ ¬ 2
∥ -1 |
68 | | simplll 798 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
𝑁 ∈
ℤ) |
69 | 68 | zred 11482 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
𝑁 ∈
ℝ) |
70 | | 2nn 11185 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℕ |
71 | 70 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) → 2
∈ ℕ) |
72 | 56 | nnnn0d 11351 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
-𝑁 ∈
ℕ0) |
73 | 58, 72 | ifcld 4131 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) ∈
ℕ0) |
74 | 71, 73 | nnexpcld 13030 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
(2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)) ∈ ℕ) |
75 | 69, 74 | nndivred 11069 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
(𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) ∈ ℝ) |
76 | | 1red 10055 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) → 1
∈ ℝ) |
77 | 68 | zcnd 11483 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
𝑁 ∈
ℂ) |
78 | 74 | nncnd 11036 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
(2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)) ∈ ℂ) |
79 | | 2cnd 11093 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) → 2
∈ ℂ) |
80 | | 2ne0 11113 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ≠
0 |
81 | 80 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) → 2
≠ 0) |
82 | 73 | nn0zd 11480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) ∈ ℤ) |
83 | 79, 81, 82 | expne0d 13014 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
(2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)) ≠ 0) |
84 | 77, 78, 83 | divnegd 10814 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
-(𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) = (-𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)))) |
85 | 73 | nn0red 11352 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) ∈ ℝ) |
86 | 74 | nnred 11035 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
(2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)) ∈ ℝ) |
87 | | max1 12016 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((-𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ) → -𝑁 ≤ if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)) |
88 | 57, 59, 87 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
-𝑁 ≤ if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)) |
89 | | uzid 11702 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (2 ∈
ℤ → 2 ∈ (ℤ≥‘2)) |
90 | 31, 89 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
(ℤ≥‘2) |
91 | | bernneq3 12992 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((2
∈ (ℤ≥‘2) ∧ if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) ∈ ℕ0) →
if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) < (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) |
92 | 90, 73, 91 | sylancr 695 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) < (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) |
93 | 85, 86, 92 | ltled 10185 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) ≤ (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) |
94 | 57, 85, 86, 88, 93 | letrd 10194 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
-𝑁 ≤ (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) |
95 | 78 | mulid1d 10057 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
((2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)) · 1) = (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) |
96 | 94, 95 | breqtrrd 4681 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
-𝑁 ≤ ((2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)) · 1)) |
97 | 74 | nnrpd 11870 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
(2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)) ∈
ℝ+) |
98 | 57, 76, 97 | ledivmuld 11925 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
((-𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) ≤ 1 ↔ -𝑁 ≤ ((2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)) · 1))) |
99 | 96, 98 | mpbird 247 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
(-𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) ≤ 1) |
100 | 84, 99 | eqbrtrd 4675 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
-(𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) ≤ 1) |
101 | 75, 76, 100 | lenegcon1d 10609 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
-1 ≤ (𝑁 /
(2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)))) |
102 | 56 | nngt0d 11064 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) → 0
< -𝑁) |
103 | 74 | nngt0d 11064 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) → 0
< (2↑if(-𝑁 ≤
𝑀, 𝑀, -𝑁))) |
104 | 57, 86, 102, 103 | divgt0d 10959 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) → 0
< (-𝑁 /
(2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)))) |
105 | 104, 84 | breqtrrd 4681 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) → 0
< -(𝑁 /
(2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)))) |
106 | 75 | lt0neg1d 10597 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
((𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) < 0 ↔ 0 < -(𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))))) |
107 | 105, 106 | mpbird 247 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
(𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) < 0) |
108 | | ax-1cn 9994 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℂ |
109 | | neg1cn 11124 |
. . . . . . . . . . . . . . 15
⊢ -1 ∈
ℂ |
110 | | 1pneg1e0 11129 |
. . . . . . . . . . . . . . 15
⊢ (1 + -1)
= 0 |
111 | 108, 109,
110 | addcomli 10228 |
. . . . . . . . . . . . . 14
⊢ (-1 + 1)
= 0 |
112 | 107, 111 | syl6breqr 4695 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
(𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) < (-1 + 1)) |
113 | | neg1z 11413 |
. . . . . . . . . . . . . 14
⊢ -1 ∈
ℤ |
114 | | flbi 12617 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) ∈ ℝ ∧ -1 ∈ ℤ)
→ ((⌊‘(𝑁 /
(2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)))) = -1 ↔ (-1 ≤ (𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) ∧ (𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) < (-1 + 1)))) |
115 | 75, 113, 114 | sylancl 694 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
((⌊‘(𝑁 /
(2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)))) = -1 ↔ (-1 ≤ (𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) ∧ (𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) < (-1 + 1)))) |
116 | 101, 112,
115 | mpbir2and 957 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
(⌊‘(𝑁 /
(2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)))) = -1) |
117 | 116 | breq2d 4665 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
(2 ∥ (⌊‘(𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)))) ↔ 2 ∥ -1)) |
118 | 67, 117 | mtbiri 317 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
¬ 2 ∥ (⌊‘(𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))))) |
119 | | bitsval2 15147 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) ∈ ℕ0) →
(if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) ∈ (bits‘𝑁) ↔ ¬ 2 ∥
(⌊‘(𝑁 /
(2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)))))) |
120 | 68, 73, 119 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
(if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) ∈ (bits‘𝑁) ↔ ¬ 2 ∥
(⌊‘(𝑁 /
(2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)))))) |
121 | 118, 120 | mpbird 247 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) ∈ (bits‘𝑁)) |
122 | 62, 121 | sseldd 3604 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) ∈ (0..^𝑀)) |
123 | | elfzolt2 12479 |
. . . . . . . 8
⊢
(if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) ∈ (0..^𝑀) → if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) < 𝑀) |
124 | 122, 123 | syl 17 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) < 𝑀) |
125 | 85, 59 | ltnled 10184 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
(if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) < 𝑀 ↔ ¬ 𝑀 ≤ if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) |
126 | 124, 125 | mpbid 222 |
. . . . . 6
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
¬ 𝑀 ≤ if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)) |
127 | 61, 126 | pm2.65da 600 |
. . . . 5
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) →
¬ -𝑁 ∈
ℕ) |
128 | 127 | intnand 962 |
. . . 4
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) →
¬ (𝑁 ∈ ℝ
∧ -𝑁 ∈
ℕ)) |
129 | | simpll 790 |
. . . . . 6
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) →
𝑁 ∈
ℤ) |
130 | | elznn0nn 11391 |
. . . . . 6
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℕ0 ∨
(𝑁 ∈ ℝ ∧
-𝑁 ∈
ℕ))) |
131 | 129, 130 | sylib 208 |
. . . . 5
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) →
(𝑁 ∈
ℕ0 ∨ (𝑁
∈ ℝ ∧ -𝑁
∈ ℕ))) |
132 | 131 | ord 392 |
. . . 4
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) →
(¬ 𝑁 ∈
ℕ0 → (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ))) |
133 | 128, 132 | mt3d 140 |
. . 3
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) →
𝑁 ∈
ℕ0) |
134 | | simplr 792 |
. . 3
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) →
𝑀 ∈
ℕ0) |
135 | | simpr 477 |
. . 3
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) →
(bits‘𝑁) ⊆
(0..^𝑀)) |
136 | | eqid 2622 |
. . 3
⊢
inf({𝑛 ∈
ℕ0 ∣ 𝑁 < (2↑𝑛)}, ℝ, < ) = inf({𝑛 ∈ ℕ0 ∣ 𝑁 < (2↑𝑛)}, ℝ, < ) |
137 | 133, 134,
135, 136 | bitsfzolem 15156 |
. 2
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) →
𝑁 ∈ (0..^(2↑𝑀))) |
138 | 55, 137 | impbida 877 |
1
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
→ (𝑁 ∈
(0..^(2↑𝑀)) ↔
(bits‘𝑁) ⊆
(0..^𝑀))) |