Step | Hyp | Ref
| Expression |
1 | | bitsval 15983 |
. . . 4
⊢ (𝑚 ∈ (bits‘𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑚 ∈ ℕ0 ∧ ¬ 2
∥ (⌊‘(𝑁 /
(2↑𝑚))))) |
2 | | simp32 1212 |
. . . . . . 7
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 𝑚 ∈ ℕ0) |
3 | | nn0uz 12476 |
. . . . . . 7
⊢
ℕ0 = (ℤ≥‘0) |
4 | 2, 3 | eleqtrdi 2848 |
. . . . . 6
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 𝑚 ∈
(ℤ≥‘0)) |
5 | | simp1r 1200 |
. . . . . . 7
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 𝑀 ∈
ℕ0) |
6 | 5 | nn0zd 12280 |
. . . . . 6
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 𝑀 ∈ ℤ) |
7 | | 2re 11904 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ |
8 | 7 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 2 ∈
ℝ) |
9 | 8, 2 | reexpcld 13733 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → (2↑𝑚) ∈ ℝ) |
10 | | simp1l 1199 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 𝑁 ∈ ℤ) |
11 | 10 | zred 12282 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 𝑁 ∈ ℝ) |
12 | 8, 5 | reexpcld 13733 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → (2↑𝑀) ∈ ℝ) |
13 | 9 | recnd 10861 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → (2↑𝑚) ∈ ℂ) |
14 | 13 | mulid2d 10851 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → (1 · (2↑𝑚)) = (2↑𝑚)) |
15 | | simp33 1213 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → ¬ 2 ∥
(⌊‘(𝑁 /
(2↑𝑚)))) |
16 | | 2rp 12591 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℝ+ |
17 | 16 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 2 ∈
ℝ+) |
18 | 2 | nn0zd 12280 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 𝑚 ∈ ℤ) |
19 | 17, 18 | rpexpcld 13814 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → (2↑𝑚) ∈
ℝ+) |
20 | 11, 19 | rerpdivcld 12659 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → (𝑁 / (2↑𝑚)) ∈ ℝ) |
21 | | 1red 10834 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 1 ∈
ℝ) |
22 | 20, 21 | ltnled 10979 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → ((𝑁 / (2↑𝑚)) < 1 ↔ ¬ 1 ≤ (𝑁 / (2↑𝑚)))) |
23 | | 0p1e1 11952 |
. . . . . . . . . . . . . 14
⊢ (0 + 1) =
1 |
24 | 23 | breq2i 5061 |
. . . . . . . . . . . . 13
⊢ ((𝑁 / (2↑𝑚)) < (0 + 1) ↔ (𝑁 / (2↑𝑚)) < 1) |
25 | | elfzole1 13251 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ (0..^(2↑𝑀)) → 0 ≤ 𝑁) |
26 | 25 | 3ad2ant2 1136 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 0 ≤ 𝑁) |
27 | 11, 19, 26 | divge0d 12668 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 0 ≤ (𝑁 / (2↑𝑚))) |
28 | | 0z 12187 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℤ |
29 | | flbi 13391 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 / (2↑𝑚)) ∈ ℝ ∧ 0 ∈ ℤ)
→ ((⌊‘(𝑁 /
(2↑𝑚))) = 0 ↔ (0
≤ (𝑁 / (2↑𝑚)) ∧ (𝑁 / (2↑𝑚)) < (0 + 1)))) |
30 | 20, 28, 29 | sylancl 589 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → ((⌊‘(𝑁 / (2↑𝑚))) = 0 ↔ (0 ≤ (𝑁 / (2↑𝑚)) ∧ (𝑁 / (2↑𝑚)) < (0 + 1)))) |
31 | | z0even 15928 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∥
0 |
32 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢
((⌊‘(𝑁 /
(2↑𝑚))) = 0 →
(⌊‘(𝑁 /
(2↑𝑚))) =
0) |
33 | 31, 32 | breqtrrid 5091 |
. . . . . . . . . . . . . . 15
⊢
((⌊‘(𝑁 /
(2↑𝑚))) = 0 → 2
∥ (⌊‘(𝑁 /
(2↑𝑚)))) |
34 | 30, 33 | syl6bir 257 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → ((0 ≤ (𝑁 / (2↑𝑚)) ∧ (𝑁 / (2↑𝑚)) < (0 + 1)) → 2 ∥
(⌊‘(𝑁 /
(2↑𝑚))))) |
35 | 27, 34 | mpand 695 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → ((𝑁 / (2↑𝑚)) < (0 + 1) → 2 ∥
(⌊‘(𝑁 /
(2↑𝑚))))) |
36 | 24, 35 | syl5bir 246 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → ((𝑁 / (2↑𝑚)) < 1 → 2 ∥
(⌊‘(𝑁 /
(2↑𝑚))))) |
37 | 22, 36 | sylbird 263 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → (¬ 1 ≤ (𝑁 / (2↑𝑚)) → 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) |
38 | 15, 37 | mt3d 150 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 1 ≤ (𝑁 / (2↑𝑚))) |
39 | 21, 11, 19 | lemuldivd 12677 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → ((1 · (2↑𝑚)) ≤ 𝑁 ↔ 1 ≤ (𝑁 / (2↑𝑚)))) |
40 | 38, 39 | mpbird 260 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → (1 · (2↑𝑚)) ≤ 𝑁) |
41 | 14, 40 | eqbrtrrd 5077 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → (2↑𝑚) ≤ 𝑁) |
42 | | elfzolt2 13252 |
. . . . . . . . 9
⊢ (𝑁 ∈ (0..^(2↑𝑀)) → 𝑁 < (2↑𝑀)) |
43 | 42 | 3ad2ant2 1136 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 𝑁 < (2↑𝑀)) |
44 | 9, 11, 12, 41, 43 | lelttrd 10990 |
. . . . . . 7
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → (2↑𝑚) < (2↑𝑀)) |
45 | | 1lt2 12001 |
. . . . . . . . 9
⊢ 1 <
2 |
46 | 45 | a1i 11 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 1 < 2) |
47 | 8, 18, 6, 46 | ltexp2d 13820 |
. . . . . . 7
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → (𝑚 < 𝑀 ↔ (2↑𝑚) < (2↑𝑀))) |
48 | 44, 47 | mpbird 260 |
. . . . . 6
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 𝑚 < 𝑀) |
49 | | elfzo2 13246 |
. . . . . 6
⊢ (𝑚 ∈ (0..^𝑀) ↔ (𝑚 ∈ (ℤ≥‘0)
∧ 𝑀 ∈ ℤ
∧ 𝑚 < 𝑀)) |
50 | 4, 6, 48, 49 | syl3anbrc 1345 |
. . . . 5
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 𝑚 ∈ (0..^𝑀)) |
51 | 50 | 3expia 1123 |
. . . 4
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀))) →
((𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚)))) → 𝑚 ∈ (0..^𝑀))) |
52 | 1, 51 | syl5bi 245 |
. . 3
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀))) →
(𝑚 ∈ (bits‘𝑁) → 𝑚 ∈ (0..^𝑀))) |
53 | 52 | ssrdv 3907 |
. 2
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀))) →
(bits‘𝑁) ⊆
(0..^𝑀)) |
54 | | simpr 488 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
-𝑁 ∈
ℕ) |
55 | 54 | nnred 11845 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
-𝑁 ∈
ℝ) |
56 | | simpllr 776 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
𝑀 ∈
ℕ0) |
57 | 56 | nn0red 12151 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
𝑀 ∈
ℝ) |
58 | | max2 12777 |
. . . . . . 7
⊢ ((-𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ) → 𝑀 ≤ if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)) |
59 | 55, 57, 58 | syl2anc 587 |
. . . . . 6
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
𝑀 ≤ if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)) |
60 | | simplr 769 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
(bits‘𝑁) ⊆
(0..^𝑀)) |
61 | | n2dvdsm1 15930 |
. . . . . . . . . . 11
⊢ ¬ 2
∥ -1 |
62 | | simplll 775 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
𝑁 ∈
ℤ) |
63 | 62 | zred 12282 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
𝑁 ∈
ℝ) |
64 | | 2nn 11903 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℕ |
65 | 64 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) → 2
∈ ℕ) |
66 | 54 | nnnn0d 12150 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
-𝑁 ∈
ℕ0) |
67 | 56, 66 | ifcld 4485 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) ∈
ℕ0) |
68 | 65, 67 | nnexpcld 13812 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
(2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)) ∈ ℕ) |
69 | 63, 68 | nndivred 11884 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
(𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) ∈ ℝ) |
70 | | 1red 10834 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) → 1
∈ ℝ) |
71 | 62 | zcnd 12283 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
𝑁 ∈
ℂ) |
72 | 68 | nncnd 11846 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
(2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)) ∈ ℂ) |
73 | | 2cnd 11908 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) → 2
∈ ℂ) |
74 | | 2ne0 11934 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ≠
0 |
75 | 74 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) → 2
≠ 0) |
76 | 67 | nn0zd 12280 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) ∈ ℤ) |
77 | 73, 75, 76 | expne0d 13722 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
(2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)) ≠ 0) |
78 | 71, 72, 77 | divnegd 11621 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
-(𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) = (-𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)))) |
79 | 67 | nn0red 12151 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) ∈ ℝ) |
80 | 68 | nnred 11845 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
(2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)) ∈ ℝ) |
81 | | max1 12775 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((-𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ) → -𝑁 ≤ if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)) |
82 | 55, 57, 81 | syl2anc 587 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
-𝑁 ≤ if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)) |
83 | | 2z 12209 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 2 ∈
ℤ |
84 | | uzid 12453 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (2 ∈
ℤ → 2 ∈ (ℤ≥‘2)) |
85 | 83, 84 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
(ℤ≥‘2) |
86 | | bernneq3 13798 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((2
∈ (ℤ≥‘2) ∧ if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) ∈ ℕ0) →
if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) < (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) |
87 | 85, 67, 86 | sylancr 590 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) < (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) |
88 | 79, 80, 87 | ltled 10980 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) ≤ (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) |
89 | 55, 79, 80, 82, 88 | letrd 10989 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
-𝑁 ≤ (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) |
90 | 72 | mulid1d 10850 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
((2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)) · 1) = (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) |
91 | 89, 90 | breqtrrd 5081 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
-𝑁 ≤ ((2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)) · 1)) |
92 | 68 | nnrpd 12626 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
(2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)) ∈
ℝ+) |
93 | 55, 70, 92 | ledivmuld 12681 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
((-𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) ≤ 1 ↔ -𝑁 ≤ ((2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)) · 1))) |
94 | 91, 93 | mpbird 260 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
(-𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) ≤ 1) |
95 | 78, 94 | eqbrtrd 5075 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
-(𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) ≤ 1) |
96 | 69, 70, 95 | lenegcon1d 11414 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
-1 ≤ (𝑁 /
(2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)))) |
97 | 54 | nngt0d 11879 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) → 0
< -𝑁) |
98 | 68 | nngt0d 11879 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) → 0
< (2↑if(-𝑁 ≤
𝑀, 𝑀, -𝑁))) |
99 | 55, 80, 97, 98 | divgt0d 11767 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) → 0
< (-𝑁 /
(2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)))) |
100 | 99, 78 | breqtrrd 5081 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) → 0
< -(𝑁 /
(2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)))) |
101 | 69 | lt0neg1d 11401 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
((𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) < 0 ↔ 0 < -(𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))))) |
102 | 100, 101 | mpbird 260 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
(𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) < 0) |
103 | | ax-1cn 10787 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℂ |
104 | | neg1cn 11944 |
. . . . . . . . . . . . . . 15
⊢ -1 ∈
ℂ |
105 | | 1pneg1e0 11949 |
. . . . . . . . . . . . . . 15
⊢ (1 + -1)
= 0 |
106 | 103, 104,
105 | addcomli 11024 |
. . . . . . . . . . . . . 14
⊢ (-1 + 1)
= 0 |
107 | 102, 106 | breqtrrdi 5095 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
(𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) < (-1 + 1)) |
108 | | neg1z 12213 |
. . . . . . . . . . . . . 14
⊢ -1 ∈
ℤ |
109 | | flbi 13391 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) ∈ ℝ ∧ -1 ∈ ℤ)
→ ((⌊‘(𝑁 /
(2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)))) = -1 ↔ (-1 ≤ (𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) ∧ (𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) < (-1 + 1)))) |
110 | 69, 108, 109 | sylancl 589 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
((⌊‘(𝑁 /
(2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)))) = -1 ↔ (-1 ≤ (𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) ∧ (𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) < (-1 + 1)))) |
111 | 96, 107, 110 | mpbir2and 713 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
(⌊‘(𝑁 /
(2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)))) = -1) |
112 | 111 | breq2d 5065 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
(2 ∥ (⌊‘(𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)))) ↔ 2 ∥ -1)) |
113 | 61, 112 | mtbiri 330 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
¬ 2 ∥ (⌊‘(𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))))) |
114 | | bitsval2 15984 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) ∈ ℕ0) →
(if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) ∈ (bits‘𝑁) ↔ ¬ 2 ∥
(⌊‘(𝑁 /
(2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)))))) |
115 | 62, 67, 114 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
(if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) ∈ (bits‘𝑁) ↔ ¬ 2 ∥
(⌊‘(𝑁 /
(2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)))))) |
116 | 113, 115 | mpbird 260 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) ∈ (bits‘𝑁)) |
117 | 60, 116 | sseldd 3902 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) ∈ (0..^𝑀)) |
118 | | elfzolt2 13252 |
. . . . . . . 8
⊢
(if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) ∈ (0..^𝑀) → if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) < 𝑀) |
119 | 117, 118 | syl 17 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) < 𝑀) |
120 | 79, 57 | ltnled 10979 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
(if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) < 𝑀 ↔ ¬ 𝑀 ≤ if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) |
121 | 119, 120 | mpbid 235 |
. . . . . 6
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
¬ 𝑀 ≤ if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)) |
122 | 59, 121 | pm2.65da 817 |
. . . . 5
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) →
¬ -𝑁 ∈
ℕ) |
123 | 122 | intnand 492 |
. . . 4
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) →
¬ (𝑁 ∈ ℝ
∧ -𝑁 ∈
ℕ)) |
124 | | simpll 767 |
. . . . . 6
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) →
𝑁 ∈
ℤ) |
125 | | elznn0nn 12190 |
. . . . . 6
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℕ0 ∨
(𝑁 ∈ ℝ ∧
-𝑁 ∈
ℕ))) |
126 | 124, 125 | sylib 221 |
. . . . 5
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) →
(𝑁 ∈
ℕ0 ∨ (𝑁
∈ ℝ ∧ -𝑁
∈ ℕ))) |
127 | 126 | ord 864 |
. . . 4
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) →
(¬ 𝑁 ∈
ℕ0 → (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ))) |
128 | 123, 127 | mt3d 150 |
. . 3
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) →
𝑁 ∈
ℕ0) |
129 | | simplr 769 |
. . 3
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) →
𝑀 ∈
ℕ0) |
130 | | simpr 488 |
. . 3
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) →
(bits‘𝑁) ⊆
(0..^𝑀)) |
131 | | eqid 2737 |
. . 3
⊢
inf({𝑛 ∈
ℕ0 ∣ 𝑁 < (2↑𝑛)}, ℝ, < ) = inf({𝑛 ∈ ℕ0 ∣ 𝑁 < (2↑𝑛)}, ℝ, < ) |
132 | 128, 129,
130, 131 | bitsfzolem 15993 |
. 2
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) →
𝑁 ∈ (0..^(2↑𝑀))) |
133 | 53, 132 | impbida 801 |
1
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
→ (𝑁 ∈
(0..^(2↑𝑀)) ↔
(bits‘𝑁) ⊆
(0..^𝑀))) |