| Step | Hyp | Ref
| Expression |
| 1 | | bitsval 16461 |
. . . 4
⊢ (𝑚 ∈ (bits‘𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑚 ∈ ℕ0 ∧ ¬ 2
∥ (⌊‘(𝑁 /
(2↑𝑚))))) |
| 2 | | simp32 1211 |
. . . . . . 7
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 𝑚 ∈ ℕ0) |
| 3 | | nn0uz 12920 |
. . . . . . 7
⊢
ℕ0 = (ℤ≥‘0) |
| 4 | 2, 3 | eleqtrdi 2851 |
. . . . . 6
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 𝑚 ∈
(ℤ≥‘0)) |
| 5 | | simp1r 1199 |
. . . . . . 7
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 𝑀 ∈
ℕ0) |
| 6 | 5 | nn0zd 12639 |
. . . . . 6
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 𝑀 ∈ ℤ) |
| 7 | | 2re 12340 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ |
| 8 | 7 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 2 ∈
ℝ) |
| 9 | 8, 2 | reexpcld 14203 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → (2↑𝑚) ∈ ℝ) |
| 10 | | simp1l 1198 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 𝑁 ∈ ℤ) |
| 11 | 10 | zred 12722 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 𝑁 ∈ ℝ) |
| 12 | 8, 5 | reexpcld 14203 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → (2↑𝑀) ∈ ℝ) |
| 13 | 9 | recnd 11289 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → (2↑𝑚) ∈ ℂ) |
| 14 | 13 | mullidd 11279 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → (1 · (2↑𝑚)) = (2↑𝑚)) |
| 15 | | simp33 1212 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → ¬ 2 ∥
(⌊‘(𝑁 /
(2↑𝑚)))) |
| 16 | | 2rp 13039 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℝ+ |
| 17 | 16 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 2 ∈
ℝ+) |
| 18 | 2 | nn0zd 12639 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 𝑚 ∈ ℤ) |
| 19 | 17, 18 | rpexpcld 14286 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → (2↑𝑚) ∈
ℝ+) |
| 20 | 11, 19 | rerpdivcld 13108 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → (𝑁 / (2↑𝑚)) ∈ ℝ) |
| 21 | | 1red 11262 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 1 ∈
ℝ) |
| 22 | 20, 21 | ltnled 11408 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → ((𝑁 / (2↑𝑚)) < 1 ↔ ¬ 1 ≤ (𝑁 / (2↑𝑚)))) |
| 23 | | 0p1e1 12388 |
. . . . . . . . . . . . . 14
⊢ (0 + 1) =
1 |
| 24 | 23 | breq2i 5151 |
. . . . . . . . . . . . 13
⊢ ((𝑁 / (2↑𝑚)) < (0 + 1) ↔ (𝑁 / (2↑𝑚)) < 1) |
| 25 | | elfzole1 13707 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ (0..^(2↑𝑀)) → 0 ≤ 𝑁) |
| 26 | 25 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 0 ≤ 𝑁) |
| 27 | 11, 19, 26 | divge0d 13117 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 0 ≤ (𝑁 / (2↑𝑚))) |
| 28 | | 0z 12624 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℤ |
| 29 | | flbi 13856 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 / (2↑𝑚)) ∈ ℝ ∧ 0 ∈ ℤ)
→ ((⌊‘(𝑁 /
(2↑𝑚))) = 0 ↔ (0
≤ (𝑁 / (2↑𝑚)) ∧ (𝑁 / (2↑𝑚)) < (0 + 1)))) |
| 30 | 20, 28, 29 | sylancl 586 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → ((⌊‘(𝑁 / (2↑𝑚))) = 0 ↔ (0 ≤ (𝑁 / (2↑𝑚)) ∧ (𝑁 / (2↑𝑚)) < (0 + 1)))) |
| 31 | | z0even 16404 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∥
0 |
| 32 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢
((⌊‘(𝑁 /
(2↑𝑚))) = 0 →
(⌊‘(𝑁 /
(2↑𝑚))) =
0) |
| 33 | 31, 32 | breqtrrid 5181 |
. . . . . . . . . . . . . . 15
⊢
((⌊‘(𝑁 /
(2↑𝑚))) = 0 → 2
∥ (⌊‘(𝑁 /
(2↑𝑚)))) |
| 34 | 30, 33 | biimtrrdi 254 |
. . . . . . . . . . . . . 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 | biimtrrid 243 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → ((𝑁 / (2↑𝑚)) < 1 → 2 ∥
(⌊‘(𝑁 /
(2↑𝑚))))) |
| 37 | 22, 36 | sylbird 260 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → (¬ 1 ≤ (𝑁 / (2↑𝑚)) → 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) |
| 38 | 15, 37 | mt3d 148 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 1 ≤ (𝑁 / (2↑𝑚))) |
| 39 | 21, 11, 19 | lemuldivd 13126 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → ((1 · (2↑𝑚)) ≤ 𝑁 ↔ 1 ≤ (𝑁 / (2↑𝑚)))) |
| 40 | 38, 39 | mpbird 257 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → (1 · (2↑𝑚)) ≤ 𝑁) |
| 41 | 14, 40 | eqbrtrrd 5167 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → (2↑𝑚) ≤ 𝑁) |
| 42 | | elfzolt2 13708 |
. . . . . . . . 9
⊢ (𝑁 ∈ (0..^(2↑𝑀)) → 𝑁 < (2↑𝑀)) |
| 43 | 42 | 3ad2ant2 1135 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 𝑁 < (2↑𝑀)) |
| 44 | 9, 11, 12, 41, 43 | lelttrd 11419 |
. . . . . . 7
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → (2↑𝑚) < (2↑𝑀)) |
| 45 | | 1lt2 12437 |
. . . . . . . . 9
⊢ 1 <
2 |
| 46 | 45 | a1i 11 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 1 < 2) |
| 47 | 8, 18, 6, 46 | ltexp2d 14290 |
. . . . . . 7
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → (𝑚 < 𝑀 ↔ (2↑𝑚) < (2↑𝑀))) |
| 48 | 44, 47 | mpbird 257 |
. . . . . 6
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 𝑚 < 𝑀) |
| 49 | | elfzo2 13702 |
. . . . . 6
⊢ (𝑚 ∈ (0..^𝑀) ↔ (𝑚 ∈ (ℤ≥‘0)
∧ 𝑀 ∈ ℤ
∧ 𝑚 < 𝑀)) |
| 50 | 4, 6, 48, 49 | syl3anbrc 1344 |
. . . . 5
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀)) ∧
(𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚))))) → 𝑚 ∈ (0..^𝑀)) |
| 51 | 50 | 3expia 1122 |
. . . 4
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀))) →
((𝑁 ∈ ℤ ∧
𝑚 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚)))) → 𝑚 ∈ (0..^𝑀))) |
| 52 | 1, 51 | biimtrid 242 |
. . 3
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀))) →
(𝑚 ∈ (bits‘𝑁) → 𝑚 ∈ (0..^𝑀))) |
| 53 | 52 | ssrdv 3989 |
. 2
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
(0..^(2↑𝑀))) →
(bits‘𝑁) ⊆
(0..^𝑀)) |
| 54 | | simpr 484 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
-𝑁 ∈
ℕ) |
| 55 | 54 | nnred 12281 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
-𝑁 ∈
ℝ) |
| 56 | | simpllr 776 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
𝑀 ∈
ℕ0) |
| 57 | 56 | nn0red 12588 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
𝑀 ∈
ℝ) |
| 58 | | max2 13229 |
. . . . . . 7
⊢ ((-𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ) → 𝑀 ≤ if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)) |
| 59 | 55, 57, 58 | syl2anc 584 |
. . . . . 6
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
𝑀 ≤ if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)) |
| 60 | | simplr 769 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
(bits‘𝑁) ⊆
(0..^𝑀)) |
| 61 | | n2dvdsm1 16406 |
. . . . . . . . . . 11
⊢ ¬ 2
∥ -1 |
| 62 | | simplll 775 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
𝑁 ∈
ℤ) |
| 63 | 62 | zred 12722 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
𝑁 ∈
ℝ) |
| 64 | | 2nn 12339 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℕ |
| 65 | 64 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) → 2
∈ ℕ) |
| 66 | 54 | nnnn0d 12587 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
-𝑁 ∈
ℕ0) |
| 67 | 56, 66 | ifcld 4572 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) ∈
ℕ0) |
| 68 | 65, 67 | nnexpcld 14284 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
(2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)) ∈ ℕ) |
| 69 | 63, 68 | nndivred 12320 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
(𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) ∈ ℝ) |
| 70 | | 1red 11262 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) → 1
∈ ℝ) |
| 71 | 62 | zcnd 12723 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
𝑁 ∈
ℂ) |
| 72 | 68 | nncnd 12282 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
(2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)) ∈ ℂ) |
| 73 | | 2cnd 12344 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) → 2
∈ ℂ) |
| 74 | | 2ne0 12370 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ≠
0 |
| 75 | 74 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) → 2
≠ 0) |
| 76 | 67 | nn0zd 12639 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) ∈ ℤ) |
| 77 | 73, 75, 76 | expne0d 14192 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
(2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)) ≠ 0) |
| 78 | 71, 72, 77 | divnegd 12056 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
-(𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) = (-𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)))) |
| 79 | 67 | nn0red 12588 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) ∈ ℝ) |
| 80 | 68 | nnred 12281 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
(2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)) ∈ ℝ) |
| 81 | | max1 13227 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((-𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ) → -𝑁 ≤ if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)) |
| 82 | 55, 57, 81 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
-𝑁 ≤ if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)) |
| 83 | | 2z 12649 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 2 ∈
ℤ |
| 84 | | uzid 12893 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (2 ∈
ℤ → 2 ∈ (ℤ≥‘2)) |
| 85 | 83, 84 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
(ℤ≥‘2) |
| 86 | | bernneq3 14270 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((2
∈ (ℤ≥‘2) ∧ if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) ∈ ℕ0) →
if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) < (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) |
| 87 | 85, 67, 86 | sylancr 587 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) < (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) |
| 88 | 79, 80, 87 | ltled 11409 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) ≤ (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) |
| 89 | 55, 79, 80, 82, 88 | letrd 11418 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
-𝑁 ≤ (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) |
| 90 | 72 | mulridd 11278 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
((2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)) · 1) = (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) |
| 91 | 89, 90 | breqtrrd 5171 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
-𝑁 ≤ ((2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)) · 1)) |
| 92 | 68 | nnrpd 13075 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
(2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)) ∈
ℝ+) |
| 93 | 55, 70, 92 | ledivmuld 13130 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
((-𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) ≤ 1 ↔ -𝑁 ≤ ((2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)) · 1))) |
| 94 | 91, 93 | mpbird 257 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
(-𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) ≤ 1) |
| 95 | 78, 94 | eqbrtrd 5165 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
-(𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) ≤ 1) |
| 96 | 69, 70, 95 | lenegcon1d 11845 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
-1 ≤ (𝑁 /
(2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)))) |
| 97 | 54 | nngt0d 12315 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) → 0
< -𝑁) |
| 98 | 68 | nngt0d 12315 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) → 0
< (2↑if(-𝑁 ≤
𝑀, 𝑀, -𝑁))) |
| 99 | 55, 80, 97, 98 | divgt0d 12203 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) → 0
< (-𝑁 /
(2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)))) |
| 100 | 99, 78 | breqtrrd 5171 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) → 0
< -(𝑁 /
(2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)))) |
| 101 | 69 | lt0neg1d 11832 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
((𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) < 0 ↔ 0 < -(𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))))) |
| 102 | 100, 101 | mpbird 257 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
(𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) < 0) |
| 103 | | ax-1cn 11213 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℂ |
| 104 | | neg1cn 12380 |
. . . . . . . . . . . . . . 15
⊢ -1 ∈
ℂ |
| 105 | | 1pneg1e0 12385 |
. . . . . . . . . . . . . . 15
⊢ (1 + -1)
= 0 |
| 106 | 103, 104,
105 | addcomli 11453 |
. . . . . . . . . . . . . 14
⊢ (-1 + 1)
= 0 |
| 107 | 102, 106 | breqtrrdi 5185 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
(𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) < (-1 + 1)) |
| 108 | | neg1z 12653 |
. . . . . . . . . . . . . 14
⊢ -1 ∈
ℤ |
| 109 | | flbi 13856 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) ∈ ℝ ∧ -1 ∈ ℤ)
→ ((⌊‘(𝑁 /
(2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)))) = -1 ↔ (-1 ≤ (𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) ∧ (𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) < (-1 + 1)))) |
| 110 | 69, 108, 109 | sylancl 586 |
. . . . . . . . . . . . 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 5155 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
(2 ∥ (⌊‘(𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)))) ↔ 2 ∥ -1)) |
| 113 | 61, 112 | mtbiri 327 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
¬ 2 ∥ (⌊‘(𝑁 / (2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))))) |
| 114 | | bitsval2 16462 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) ∈ ℕ0) →
(if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) ∈ (bits‘𝑁) ↔ ¬ 2 ∥
(⌊‘(𝑁 /
(2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)))))) |
| 115 | 62, 67, 114 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
(if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) ∈ (bits‘𝑁) ↔ ¬ 2 ∥
(⌊‘(𝑁 /
(2↑if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)))))) |
| 116 | 113, 115 | mpbird 257 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) ∈ (bits‘𝑁)) |
| 117 | 60, 116 | sseldd 3984 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) ∈ (0..^𝑀)) |
| 118 | | elfzolt2 13708 |
. . . . . . . 8
⊢
(if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) ∈ (0..^𝑀) → if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) < 𝑀) |
| 119 | 117, 118 | syl 17 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) < 𝑀) |
| 120 | 79, 57 | ltnled 11408 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
(if(-𝑁 ≤ 𝑀, 𝑀, -𝑁) < 𝑀 ↔ ¬ 𝑀 ≤ if(-𝑁 ≤ 𝑀, 𝑀, -𝑁))) |
| 121 | 119, 120 | mpbid 232 |
. . . . . 6
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) ∧
-𝑁 ∈ ℕ) →
¬ 𝑀 ≤ if(-𝑁 ≤ 𝑀, 𝑀, -𝑁)) |
| 122 | 59, 121 | pm2.65da 817 |
. . . . 5
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) →
¬ -𝑁 ∈
ℕ) |
| 123 | 122 | intnand 488 |
. . . 4
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) →
¬ (𝑁 ∈ ℝ
∧ -𝑁 ∈
ℕ)) |
| 124 | | simpll 767 |
. . . . . 6
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) →
𝑁 ∈
ℤ) |
| 125 | | elznn0nn 12627 |
. . . . . 6
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℕ0 ∨
(𝑁 ∈ ℝ ∧
-𝑁 ∈
ℕ))) |
| 126 | 124, 125 | sylib 218 |
. . . . 5
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) →
(𝑁 ∈
ℕ0 ∨ (𝑁
∈ ℝ ∧ -𝑁
∈ ℕ))) |
| 127 | 126 | ord 865 |
. . . 4
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) →
(¬ 𝑁 ∈
ℕ0 → (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ))) |
| 128 | 123, 127 | mt3d 148 |
. . 3
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) →
𝑁 ∈
ℕ0) |
| 129 | | simplr 769 |
. . 3
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) →
𝑀 ∈
ℕ0) |
| 130 | | simpr 484 |
. . 3
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) →
(bits‘𝑁) ⊆
(0..^𝑀)) |
| 131 | | eqid 2737 |
. . 3
⊢
inf({𝑛 ∈
ℕ0 ∣ 𝑁 < (2↑𝑛)}, ℝ, < ) = inf({𝑛 ∈ ℕ0 ∣ 𝑁 < (2↑𝑛)}, ℝ, < ) |
| 132 | 128, 129,
130, 131 | bitsfzolem 16471 |
. 2
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ (bits‘𝑁)
⊆ (0..^𝑀)) →
𝑁 ∈ (0..^(2↑𝑀))) |
| 133 | 53, 132 | impbida 801 |
1
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
→ (𝑁 ∈
(0..^(2↑𝑀)) ↔
(bits‘𝑁) ⊆
(0..^𝑀))) |