Proof of Theorem nnolog2flm1
Step | Hyp | Ref
| Expression |
1 | | eluz2nn 12480 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ ℕ) |
2 | | nnpw2blenfzo2 45601 |
. . . 4
⊢ (𝑁 ∈ ℕ → (𝑁 =
(2↑((#b‘𝑁) − 1)) ∨ 𝑁 ∈
(((2↑((#b‘𝑁) − 1)) +
1)..^(2↑(#b‘𝑁))))) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 = (2↑((#b‘𝑁) − 1)) ∨ 𝑁 ∈
(((2↑((#b‘𝑁) − 1)) +
1)..^(2↑(#b‘𝑁))))) |
4 | 1 | adantl 485 |
. . . . . . . . 9
⊢ ((𝑁 =
(2↑((#b‘𝑁) − 1)) ∧ 𝑁 ∈ (ℤ≥‘2))
→ 𝑁 ∈
ℕ) |
5 | | nneo 12261 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → ((𝑁 / 2) ∈ ℕ ↔
¬ ((𝑁 + 1) / 2) ∈
ℕ)) |
6 | 5 | bicomd 226 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (¬
((𝑁 + 1) / 2) ∈
ℕ ↔ (𝑁 / 2)
∈ ℕ)) |
7 | 4, 6 | syl 17 |
. . . . . . . 8
⊢ ((𝑁 =
(2↑((#b‘𝑁) − 1)) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (¬ ((𝑁 + 1) / 2)
∈ ℕ ↔ (𝑁 /
2) ∈ ℕ)) |
8 | | notnotb 318 |
. . . . . . . 8
⊢ ((𝑁 / 2) ∈ ℕ ↔
¬ ¬ (𝑁 / 2) ∈
ℕ) |
9 | 7, 8 | bitrdi 290 |
. . . . . . 7
⊢ ((𝑁 =
(2↑((#b‘𝑁) − 1)) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (¬ ((𝑁 + 1) / 2)
∈ ℕ ↔ ¬ ¬ (𝑁 / 2) ∈ ℕ)) |
10 | 9 | con4bid 320 |
. . . . . 6
⊢ ((𝑁 =
(2↑((#b‘𝑁) − 1)) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (((𝑁 + 1) / 2)
∈ ℕ ↔ ¬ (𝑁 / 2) ∈ ℕ)) |
11 | | simpl 486 |
. . . . . . . . 9
⊢ ((𝑁 =
(2↑((#b‘𝑁) − 1)) ∧ 𝑁 ∈ (ℤ≥‘2))
→ 𝑁 =
(2↑((#b‘𝑁) − 1))) |
12 | 11 | oveq1d 7228 |
. . . . . . . 8
⊢ ((𝑁 =
(2↑((#b‘𝑁) − 1)) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑁 / 2) =
((2↑((#b‘𝑁) − 1)) / 2)) |
13 | | blennnelnn 45595 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ →
(#b‘𝑁)
∈ ℕ) |
14 | 13 | nnnn0d 12150 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ →
(#b‘𝑁)
∈ ℕ0) |
15 | 1, 14 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘2) → (#b‘𝑁) ∈
ℕ0) |
16 | | 2m1e1 11956 |
. . . . . . . . . . . . . 14
⊢ (2
− 1) = 1 |
17 | | 2cn 11905 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℂ |
18 | | 2ne0 11934 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ≠
0 |
19 | | 1ne2 12038 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ≠
2 |
20 | 19 | necomi 2995 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ≠
1 |
21 | | logbid1 25651 |
. . . . . . . . . . . . . . . . 17
⊢ ((2
∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1) → (2 logb 2) =
1) |
22 | 17, 18, 20, 21 | mp3an 1463 |
. . . . . . . . . . . . . . . 16
⊢ (2
logb 2) = 1 |
23 | | eluzle 12451 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈
(ℤ≥‘2) → 2 ≤ 𝑁) |
24 | | 2z 12209 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ∈
ℤ |
25 | | uzid 12453 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2 ∈
ℤ → 2 ∈ (ℤ≥‘2)) |
26 | 24, 25 | mp1i 13 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈
(ℤ≥‘2) → 2 ∈
(ℤ≥‘2)) |
27 | | 2rp 12591 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ∈
ℝ+ |
28 | 27 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈
(ℤ≥‘2) → 2 ∈
ℝ+) |
29 | 1 | nnrpd 12626 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈
ℝ+) |
30 | | logbleb 25666 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2
∈ (ℤ≥‘2) ∧ 2 ∈ ℝ+
∧ 𝑁 ∈
ℝ+) → (2 ≤ 𝑁 ↔ (2 logb 2) ≤ (2
logb 𝑁))) |
31 | 26, 28, 29, 30 | syl3anc 1373 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 ≤ 𝑁 ↔ (2 logb 2) ≤ (2
logb 𝑁))) |
32 | 23, 31 | mpbid 235 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 logb 2) ≤ (2
logb 𝑁)) |
33 | 22, 32 | eqbrtrrid 5089 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘2) → 1 ≤ (2 logb 𝑁)) |
34 | 20 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈
(ℤ≥‘2) → 2 ≠ 1) |
35 | | relogbcl 25656 |
. . . . . . . . . . . . . . . . 17
⊢ ((2
∈ ℝ+ ∧ 𝑁 ∈ ℝ+ ∧ 2 ≠ 1)
→ (2 logb 𝑁) ∈ ℝ) |
36 | 28, 29, 34, 35 | syl3anc 1373 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 logb 𝑁) ∈ ℝ) |
37 | | 1zzd 12208 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘2) → 1 ∈ ℤ) |
38 | | flge 13380 |
. . . . . . . . . . . . . . . 16
⊢ (((2
logb 𝑁) ∈
ℝ ∧ 1 ∈ ℤ) → (1 ≤ (2 logb 𝑁) ↔ 1 ≤
(⌊‘(2 logb 𝑁)))) |
39 | 36, 37, 38 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘2) → (1 ≤ (2 logb 𝑁) ↔ 1 ≤
(⌊‘(2 logb 𝑁)))) |
40 | 33, 39 | mpbid 235 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘2) → 1 ≤ (⌊‘(2
logb 𝑁))) |
41 | 16, 40 | eqbrtrid 5088 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 − 1) ≤ (⌊‘(2
logb 𝑁))) |
42 | | 2re 11904 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℝ |
43 | 42 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘2) → 2 ∈ ℝ) |
44 | | 1red 10834 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘2) → 1 ∈ ℝ) |
45 | 36 | flcld 13373 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘2) → (⌊‘(2 logb 𝑁)) ∈
ℤ) |
46 | 45 | zred 12282 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘2) → (⌊‘(2 logb 𝑁)) ∈
ℝ) |
47 | 43, 44, 46 | lesubaddd 11429 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘2) → ((2 − 1) ≤ (⌊‘(2
logb 𝑁)) ↔
2 ≤ ((⌊‘(2 logb 𝑁)) + 1))) |
48 | 41, 47 | mpbid 235 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘2) → 2 ≤ ((⌊‘(2
logb 𝑁)) +
1)) |
49 | | blennn 45594 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ →
(#b‘𝑁) =
((⌊‘(2 logb 𝑁)) + 1)) |
50 | 1, 49 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘2) → (#b‘𝑁) = ((⌊‘(2 logb 𝑁)) + 1)) |
51 | 48, 50 | breqtrrd 5081 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘2) → 2 ≤ (#b‘𝑁)) |
52 | | nn0ge2m1nn 12159 |
. . . . . . . . . . 11
⊢
(((#b‘𝑁) ∈ ℕ0 ∧ 2 ≤
(#b‘𝑁))
→ ((#b‘𝑁) − 1) ∈
ℕ) |
53 | 15, 51, 52 | syl2anc 587 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘2) → ((#b‘𝑁) − 1) ∈
ℕ) |
54 | 53 | adantl 485 |
. . . . . . . . 9
⊢ ((𝑁 =
(2↑((#b‘𝑁) − 1)) ∧ 𝑁 ∈ (ℤ≥‘2))
→ ((#b‘𝑁) − 1) ∈
ℕ) |
55 | | nnpw2even 45548 |
. . . . . . . . 9
⊢
(((#b‘𝑁) − 1) ∈ ℕ →
((2↑((#b‘𝑁) − 1)) / 2) ∈
ℕ) |
56 | 54, 55 | syl 17 |
. . . . . . . 8
⊢ ((𝑁 =
(2↑((#b‘𝑁) − 1)) ∧ 𝑁 ∈ (ℤ≥‘2))
→ ((2↑((#b‘𝑁) − 1)) / 2) ∈
ℕ) |
57 | 12, 56 | eqeltrd 2838 |
. . . . . . 7
⊢ ((𝑁 =
(2↑((#b‘𝑁) − 1)) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑁 / 2) ∈
ℕ) |
58 | 57 | pm2.24d 154 |
. . . . . 6
⊢ ((𝑁 =
(2↑((#b‘𝑁) − 1)) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (¬ (𝑁 / 2)
∈ ℕ → (⌊‘(2 logb 𝑁)) = (⌊‘(2 logb
(𝑁 −
1))))) |
59 | 10, 58 | sylbid 243 |
. . . . 5
⊢ ((𝑁 =
(2↑((#b‘𝑁) − 1)) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (((𝑁 + 1) / 2)
∈ ℕ → (⌊‘(2 logb 𝑁)) = (⌊‘(2 logb
(𝑁 −
1))))) |
60 | 59 | ex 416 |
. . . 4
⊢ (𝑁 =
(2↑((#b‘𝑁) − 1)) → (𝑁 ∈ (ℤ≥‘2)
→ (((𝑁 + 1) / 2)
∈ ℕ → (⌊‘(2 logb 𝑁)) = (⌊‘(2 logb
(𝑁 −
1)))))) |
61 | 1, 13 | syl 17 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘2) → (#b‘𝑁) ∈ ℕ) |
62 | | nnm1nn0 12131 |
. . . . . . . . 9
⊢
((#b‘𝑁) ∈ ℕ →
((#b‘𝑁)
− 1) ∈ ℕ0) |
63 | 61, 62 | syl 17 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → ((#b‘𝑁) − 1) ∈
ℕ0) |
64 | 63 | ad2antlr 727 |
. . . . . . 7
⊢ (((𝑁 ∈
(((2↑((#b‘𝑁) − 1)) +
1)..^(2↑(#b‘𝑁))) ∧ 𝑁 ∈ (ℤ≥‘2))
∧ ((𝑁 + 1) / 2) ∈
ℕ) → ((#b‘𝑁) − 1) ∈
ℕ0) |
65 | 1 | ad2antlr 727 |
. . . . . . . . 9
⊢ (((𝑁 ∈
(((2↑((#b‘𝑁) − 1)) +
1)..^(2↑(#b‘𝑁))) ∧ 𝑁 ∈ (ℤ≥‘2))
∧ ((𝑁 + 1) / 2) ∈
ℕ) → 𝑁 ∈
ℕ) |
66 | | nnpw2blenfzo 45600 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
((2↑((#b‘𝑁) −
1))..^(2↑(#b‘𝑁)))) |
67 | 65, 66 | syl 17 |
. . . . . . . 8
⊢ (((𝑁 ∈
(((2↑((#b‘𝑁) − 1)) +
1)..^(2↑(#b‘𝑁))) ∧ 𝑁 ∈ (ℤ≥‘2))
∧ ((𝑁 + 1) / 2) ∈
ℕ) → 𝑁 ∈
((2↑((#b‘𝑁) −
1))..^(2↑(#b‘𝑁)))) |
68 | 61 | nncnd 11846 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘2) → (#b‘𝑁) ∈ ℂ) |
69 | 68 | ad2antlr 727 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈
(((2↑((#b‘𝑁) − 1)) +
1)..^(2↑(#b‘𝑁))) ∧ 𝑁 ∈ (ℤ≥‘2))
∧ ((𝑁 + 1) / 2) ∈
ℕ) → (#b‘𝑁) ∈ ℂ) |
70 | | npcan1 11257 |
. . . . . . . . . . 11
⊢
((#b‘𝑁) ∈ ℂ →
(((#b‘𝑁)
− 1) + 1) = (#b‘𝑁)) |
71 | 69, 70 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑁 ∈
(((2↑((#b‘𝑁) − 1)) +
1)..^(2↑(#b‘𝑁))) ∧ 𝑁 ∈ (ℤ≥‘2))
∧ ((𝑁 + 1) / 2) ∈
ℕ) → (((#b‘𝑁) − 1) + 1) =
(#b‘𝑁)) |
72 | 71 | oveq2d 7229 |
. . . . . . . . 9
⊢ (((𝑁 ∈
(((2↑((#b‘𝑁) − 1)) +
1)..^(2↑(#b‘𝑁))) ∧ 𝑁 ∈ (ℤ≥‘2))
∧ ((𝑁 + 1) / 2) ∈
ℕ) → (2↑(((#b‘𝑁) − 1) + 1)) =
(2↑(#b‘𝑁))) |
73 | 72 | oveq2d 7229 |
. . . . . . . 8
⊢ (((𝑁 ∈
(((2↑((#b‘𝑁) − 1)) +
1)..^(2↑(#b‘𝑁))) ∧ 𝑁 ∈ (ℤ≥‘2))
∧ ((𝑁 + 1) / 2) ∈
ℕ) → ((2↑((#b‘𝑁) −
1))..^(2↑(((#b‘𝑁) − 1) + 1))) =
((2↑((#b‘𝑁) −
1))..^(2↑(#b‘𝑁)))) |
74 | 67, 73 | eleqtrrd 2841 |
. . . . . . 7
⊢ (((𝑁 ∈
(((2↑((#b‘𝑁) − 1)) +
1)..^(2↑(#b‘𝑁))) ∧ 𝑁 ∈ (ℤ≥‘2))
∧ ((𝑁 + 1) / 2) ∈
ℕ) → 𝑁 ∈
((2↑((#b‘𝑁) −
1))..^(2↑(((#b‘𝑁) − 1) + 1)))) |
75 | | fllog2 45587 |
. . . . . . 7
⊢
((((#b‘𝑁) − 1) ∈ ℕ0
∧ 𝑁 ∈
((2↑((#b‘𝑁) −
1))..^(2↑(((#b‘𝑁) − 1) + 1)))) →
(⌊‘(2 logb 𝑁)) = ((#b‘𝑁) − 1)) |
76 | 64, 74, 75 | syl2anc 587 |
. . . . . 6
⊢ (((𝑁 ∈
(((2↑((#b‘𝑁) − 1)) +
1)..^(2↑(#b‘𝑁))) ∧ 𝑁 ∈ (ℤ≥‘2))
∧ ((𝑁 + 1) / 2) ∈
ℕ) → (⌊‘(2 logb 𝑁)) = ((#b‘𝑁) − 1)) |
77 | 61 | ad2antlr 727 |
. . . . . . . 8
⊢ (((𝑁 ∈
(((2↑((#b‘𝑁) − 1)) +
1)..^(2↑(#b‘𝑁))) ∧ 𝑁 ∈ (ℤ≥‘2))
∧ ((𝑁 + 1) / 2) ∈
ℕ) → (#b‘𝑁) ∈ ℕ) |
78 | 77, 62 | syl 17 |
. . . . . . 7
⊢ (((𝑁 ∈
(((2↑((#b‘𝑁) − 1)) +
1)..^(2↑(#b‘𝑁))) ∧ 𝑁 ∈ (ℤ≥‘2))
∧ ((𝑁 + 1) / 2) ∈
ℕ) → ((#b‘𝑁) − 1) ∈
ℕ0) |
79 | | elfzo2 13246 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(((2↑((#b‘𝑁) − 1)) +
1)..^(2↑(#b‘𝑁))) ↔ (𝑁 ∈
(ℤ≥‘((2↑((#b‘𝑁) − 1)) + 1)) ∧
(2↑(#b‘𝑁)) ∈ ℤ ∧ 𝑁 < (2↑(#b‘𝑁)))) |
80 | | eluz2 12444 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘((2↑((#b‘𝑁) − 1)) + 1)) ↔
(((2↑((#b‘𝑁) − 1)) + 1) ∈ ℤ ∧
𝑁 ∈ ℤ ∧
((2↑((#b‘𝑁) − 1)) + 1) ≤ 𝑁)) |
81 | 80 | 3anbi1i 1159 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈
(ℤ≥‘((2↑((#b‘𝑁) − 1)) + 1)) ∧
(2↑(#b‘𝑁)) ∈ ℤ ∧ 𝑁 < (2↑(#b‘𝑁))) ↔
((((2↑((#b‘𝑁) − 1)) + 1) ∈ ℤ ∧
𝑁 ∈ ℤ ∧
((2↑((#b‘𝑁) − 1)) + 1) ≤ 𝑁) ∧ (2↑(#b‘𝑁)) ∈ ℤ ∧ 𝑁 <
(2↑(#b‘𝑁)))) |
82 | 79, 81 | bitri 278 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(((2↑((#b‘𝑁) − 1)) +
1)..^(2↑(#b‘𝑁))) ↔
((((2↑((#b‘𝑁) − 1)) + 1) ∈ ℤ ∧
𝑁 ∈ ℤ ∧
((2↑((#b‘𝑁) − 1)) + 1) ≤ 𝑁) ∧ (2↑(#b‘𝑁)) ∈ ℤ ∧ 𝑁 <
(2↑(#b‘𝑁)))) |
83 | | 2nn 11903 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
ℕ |
84 | 83 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈
(ℤ≥‘2) → 2 ∈ ℕ) |
85 | 84, 63 | jca 515 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 ∈ ℕ ∧
((#b‘𝑁)
− 1) ∈ ℕ0)) |
86 | 85 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢
((((((2↑((#b‘𝑁) − 1)) + 1) ∈ ℤ ∧
𝑁 ∈ ℤ ∧
((2↑((#b‘𝑁) − 1)) + 1) ≤ 𝑁) ∧ 𝑁 < (2↑(#b‘𝑁))) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (2 ∈ ℕ ∧ ((#b‘𝑁) − 1) ∈
ℕ0)) |
87 | | nnexpcl 13648 |
. . . . . . . . . . . . . . . . 17
⊢ ((2
∈ ℕ ∧ ((#b‘𝑁) − 1) ∈ ℕ0)
→ (2↑((#b‘𝑁) − 1)) ∈
ℕ) |
88 | 86, 87 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
((((((2↑((#b‘𝑁) − 1)) + 1) ∈ ℤ ∧
𝑁 ∈ ℤ ∧
((2↑((#b‘𝑁) − 1)) + 1) ≤ 𝑁) ∧ 𝑁 < (2↑(#b‘𝑁))) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (2↑((#b‘𝑁) − 1)) ∈
ℕ) |
89 | 88 | nnzd 12281 |
. . . . . . . . . . . . . . 15
⊢
((((((2↑((#b‘𝑁) − 1)) + 1) ∈ ℤ ∧
𝑁 ∈ ℤ ∧
((2↑((#b‘𝑁) − 1)) + 1) ≤ 𝑁) ∧ 𝑁 < (2↑(#b‘𝑁))) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (2↑((#b‘𝑁) − 1)) ∈
ℤ) |
90 | | peano2zm 12220 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
91 | 90 | 3ad2ant2 1136 |
. . . . . . . . . . . . . . . . 17
⊢
((((2↑((#b‘𝑁) − 1)) + 1) ∈ ℤ ∧
𝑁 ∈ ℤ ∧
((2↑((#b‘𝑁) − 1)) + 1) ≤ 𝑁) → (𝑁 − 1) ∈ ℤ) |
92 | 91 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢
(((((2↑((#b‘𝑁) − 1)) + 1) ∈ ℤ ∧
𝑁 ∈ ℤ ∧
((2↑((#b‘𝑁) − 1)) + 1) ≤ 𝑁) ∧ 𝑁 < (2↑(#b‘𝑁))) → (𝑁 − 1) ∈ ℤ) |
93 | 92 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢
((((((2↑((#b‘𝑁) − 1)) + 1) ∈ ℤ ∧
𝑁 ∈ ℤ ∧
((2↑((#b‘𝑁) − 1)) + 1) ≤ 𝑁) ∧ 𝑁 < (2↑(#b‘𝑁))) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑁 − 1) ∈
ℤ) |
94 | 84, 63 | nnexpcld 13812 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈
(ℤ≥‘2) → (2↑((#b‘𝑁) − 1)) ∈
ℕ) |
95 | 94 | nnred 11845 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈
(ℤ≥‘2) → (2↑((#b‘𝑁) − 1)) ∈
ℝ) |
96 | 1 | nnred 11845 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ ℝ) |
97 | | leaddsub 11308 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((2↑((#b‘𝑁) − 1)) ∈ ℝ ∧ 1 ∈
ℝ ∧ 𝑁 ∈
ℝ) → (((2↑((#b‘𝑁) − 1)) + 1) ≤ 𝑁 ↔ (2↑((#b‘𝑁) − 1)) ≤ (𝑁 − 1))) |
98 | 95, 44, 96, 97 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈
(ℤ≥‘2) → (((2↑((#b‘𝑁) − 1)) + 1) ≤ 𝑁 ↔
(2↑((#b‘𝑁) − 1)) ≤ (𝑁 − 1))) |
99 | 98 | biimpcd 252 |
. . . . . . . . . . . . . . . . . 18
⊢
(((2↑((#b‘𝑁) − 1)) + 1) ≤ 𝑁 → (𝑁 ∈ (ℤ≥‘2)
→ (2↑((#b‘𝑁) − 1)) ≤ (𝑁 − 1))) |
100 | 99 | 3ad2ant3 1137 |
. . . . . . . . . . . . . . . . 17
⊢
((((2↑((#b‘𝑁) − 1)) + 1) ∈ ℤ ∧
𝑁 ∈ ℤ ∧
((2↑((#b‘𝑁) − 1)) + 1) ≤ 𝑁) → (𝑁 ∈ (ℤ≥‘2)
→ (2↑((#b‘𝑁) − 1)) ≤ (𝑁 − 1))) |
101 | 100 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢
(((((2↑((#b‘𝑁) − 1)) + 1) ∈ ℤ ∧
𝑁 ∈ ℤ ∧
((2↑((#b‘𝑁) − 1)) + 1) ≤ 𝑁) ∧ 𝑁 < (2↑(#b‘𝑁))) → (𝑁 ∈ (ℤ≥‘2)
→ (2↑((#b‘𝑁) − 1)) ≤ (𝑁 − 1))) |
102 | 101 | imp 410 |
. . . . . . . . . . . . . . 15
⊢
((((((2↑((#b‘𝑁) − 1)) + 1) ∈ ℤ ∧
𝑁 ∈ ℤ ∧
((2↑((#b‘𝑁) − 1)) + 1) ≤ 𝑁) ∧ 𝑁 < (2↑(#b‘𝑁))) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (2↑((#b‘𝑁) − 1)) ≤ (𝑁 − 1)) |
103 | | eluz2 12444 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 − 1) ∈
(ℤ≥‘(2↑((#b‘𝑁) − 1))) ↔
((2↑((#b‘𝑁) − 1)) ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ ∧
(2↑((#b‘𝑁) − 1)) ≤ (𝑁 − 1))) |
104 | 89, 93, 102, 103 | syl3anbrc 1345 |
. . . . . . . . . . . . . 14
⊢
((((((2↑((#b‘𝑁) − 1)) + 1) ∈ ℤ ∧
𝑁 ∈ ℤ ∧
((2↑((#b‘𝑁) − 1)) + 1) ≤ 𝑁) ∧ 𝑁 < (2↑(#b‘𝑁))) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑁 − 1) ∈
(ℤ≥‘(2↑((#b‘𝑁) − 1)))) |
105 | 70 | eleq1d 2822 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#b‘𝑁) ∈ ℂ →
((((#b‘𝑁)
− 1) + 1) ∈ ℕ0 ↔ (#b‘𝑁) ∈
ℕ0)) |
106 | 68, 105 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈
(ℤ≥‘2) → ((((#b‘𝑁) − 1) + 1) ∈
ℕ0 ↔ (#b‘𝑁) ∈
ℕ0)) |
107 | 15, 106 | mpbird 260 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈
(ℤ≥‘2) → (((#b‘𝑁) − 1) + 1) ∈
ℕ0) |
108 | 84, 107 | jca 515 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 ∈ ℕ ∧
(((#b‘𝑁)
− 1) + 1) ∈ ℕ0)) |
109 | 108 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢
((((((2↑((#b‘𝑁) − 1)) + 1) ∈ ℤ ∧
𝑁 ∈ ℤ ∧
((2↑((#b‘𝑁) − 1)) + 1) ≤ 𝑁) ∧ 𝑁 < (2↑(#b‘𝑁))) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (2 ∈ ℕ ∧ (((#b‘𝑁) − 1) + 1) ∈
ℕ0)) |
110 | | nnexpcl 13648 |
. . . . . . . . . . . . . . . 16
⊢ ((2
∈ ℕ ∧ (((#b‘𝑁) − 1) + 1) ∈
ℕ0) → (2↑(((#b‘𝑁) − 1) + 1)) ∈
ℕ) |
111 | 109, 110 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
((((((2↑((#b‘𝑁) − 1)) + 1) ∈ ℤ ∧
𝑁 ∈ ℤ ∧
((2↑((#b‘𝑁) − 1)) + 1) ≤ 𝑁) ∧ 𝑁 < (2↑(#b‘𝑁))) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (2↑(((#b‘𝑁) − 1) + 1)) ∈
ℕ) |
112 | 111 | nnzd 12281 |
. . . . . . . . . . . . . 14
⊢
((((((2↑((#b‘𝑁) − 1)) + 1) ∈ ℤ ∧
𝑁 ∈ ℤ ∧
((2↑((#b‘𝑁) − 1)) + 1) ≤ 𝑁) ∧ 𝑁 < (2↑(#b‘𝑁))) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (2↑(((#b‘𝑁) − 1) + 1)) ∈
ℤ) |
113 | | ltle 10921 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℝ ∧
(2↑(#b‘𝑁)) ∈ ℝ) → (𝑁 < (2↑(#b‘𝑁)) → 𝑁 ≤ (2↑(#b‘𝑁)))) |
114 | | nnre 11837 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
115 | 42 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℕ → 2 ∈
ℝ) |
116 | 115, 14 | reexpcld 13733 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ →
(2↑(#b‘𝑁)) ∈ ℝ) |
117 | 114, 116 | jca 515 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℝ ∧
(2↑(#b‘𝑁)) ∈ ℝ)) |
118 | 1, 117 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 ∈ ℝ ∧
(2↑(#b‘𝑁)) ∈ ℝ)) |
119 | 113, 118 | syl11 33 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 <
(2↑(#b‘𝑁)) → (𝑁 ∈ (ℤ≥‘2)
→ 𝑁 ≤
(2↑(#b‘𝑁)))) |
120 | 119 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢
(((((2↑((#b‘𝑁) − 1)) + 1) ∈ ℤ ∧
𝑁 ∈ ℤ ∧
((2↑((#b‘𝑁) − 1)) + 1) ≤ 𝑁) ∧ 𝑁 < (2↑(#b‘𝑁))) → (𝑁 ∈ (ℤ≥‘2)
→ 𝑁 ≤
(2↑(#b‘𝑁)))) |
121 | 120 | imp 410 |
. . . . . . . . . . . . . . . 16
⊢
((((((2↑((#b‘𝑁) − 1)) + 1) ∈ ℤ ∧
𝑁 ∈ ℤ ∧
((2↑((#b‘𝑁) − 1)) + 1) ≤ 𝑁) ∧ 𝑁 < (2↑(#b‘𝑁))) ∧ 𝑁 ∈ (ℤ≥‘2))
→ 𝑁 ≤
(2↑(#b‘𝑁))) |
122 | | simpll2 1215 |
. . . . . . . . . . . . . . . . 17
⊢
((((((2↑((#b‘𝑁) − 1)) + 1) ∈ ℤ ∧
𝑁 ∈ ℤ ∧
((2↑((#b‘𝑁) − 1)) + 1) ≤ 𝑁) ∧ 𝑁 < (2↑(#b‘𝑁))) ∧ 𝑁 ∈ (ℤ≥‘2))
→ 𝑁 ∈
ℤ) |
123 | 84, 15 | nnexpcld 13812 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈
(ℤ≥‘2) → (2↑(#b‘𝑁)) ∈
ℕ) |
124 | 123 | nnzd 12281 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈
(ℤ≥‘2) → (2↑(#b‘𝑁)) ∈
ℤ) |
125 | 124 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢
((((((2↑((#b‘𝑁) − 1)) + 1) ∈ ℤ ∧
𝑁 ∈ ℤ ∧
((2↑((#b‘𝑁) − 1)) + 1) ≤ 𝑁) ∧ 𝑁 < (2↑(#b‘𝑁))) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (2↑(#b‘𝑁)) ∈ ℤ) |
126 | | zlem1lt 12229 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℤ ∧
(2↑(#b‘𝑁)) ∈ ℤ) → (𝑁 ≤ (2↑(#b‘𝑁)) ↔ (𝑁 − 1) <
(2↑(#b‘𝑁)))) |
127 | 122, 125,
126 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢
((((((2↑((#b‘𝑁) − 1)) + 1) ∈ ℤ ∧
𝑁 ∈ ℤ ∧
((2↑((#b‘𝑁) − 1)) + 1) ≤ 𝑁) ∧ 𝑁 < (2↑(#b‘𝑁))) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑁 ≤
(2↑(#b‘𝑁)) ↔ (𝑁 − 1) <
(2↑(#b‘𝑁)))) |
128 | 121, 127 | mpbid 235 |
. . . . . . . . . . . . . . 15
⊢
((((((2↑((#b‘𝑁) − 1)) + 1) ∈ ℤ ∧
𝑁 ∈ ℤ ∧
((2↑((#b‘𝑁) − 1)) + 1) ≤ 𝑁) ∧ 𝑁 < (2↑(#b‘𝑁))) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑁 − 1) <
(2↑(#b‘𝑁))) |
129 | 68, 70 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈
(ℤ≥‘2) → (((#b‘𝑁) − 1) + 1) =
(#b‘𝑁)) |
130 | 129 | oveq2d 7229 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘2) → (2↑(((#b‘𝑁) − 1) + 1)) =
(2↑(#b‘𝑁))) |
131 | 130 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢
((((((2↑((#b‘𝑁) − 1)) + 1) ∈ ℤ ∧
𝑁 ∈ ℤ ∧
((2↑((#b‘𝑁) − 1)) + 1) ≤ 𝑁) ∧ 𝑁 < (2↑(#b‘𝑁))) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (2↑(((#b‘𝑁) − 1) + 1)) =
(2↑(#b‘𝑁))) |
132 | 128, 131 | breqtrrd 5081 |
. . . . . . . . . . . . . 14
⊢
((((((2↑((#b‘𝑁) − 1)) + 1) ∈ ℤ ∧
𝑁 ∈ ℤ ∧
((2↑((#b‘𝑁) − 1)) + 1) ≤ 𝑁) ∧ 𝑁 < (2↑(#b‘𝑁))) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑁 − 1) <
(2↑(((#b‘𝑁) − 1) + 1))) |
133 | 104, 112,
132 | 3jca 1130 |
. . . . . . . . . . . . 13
⊢
((((((2↑((#b‘𝑁) − 1)) + 1) ∈ ℤ ∧
𝑁 ∈ ℤ ∧
((2↑((#b‘𝑁) − 1)) + 1) ≤ 𝑁) ∧ 𝑁 < (2↑(#b‘𝑁))) ∧ 𝑁 ∈ (ℤ≥‘2))
→ ((𝑁 − 1)
∈ (ℤ≥‘(2↑((#b‘𝑁) − 1))) ∧
(2↑(((#b‘𝑁) − 1) + 1)) ∈ ℤ ∧
(𝑁 − 1) <
(2↑(((#b‘𝑁) − 1) + 1)))) |
134 | 133 | ex 416 |
. . . . . . . . . . . 12
⊢
(((((2↑((#b‘𝑁) − 1)) + 1) ∈ ℤ ∧
𝑁 ∈ ℤ ∧
((2↑((#b‘𝑁) − 1)) + 1) ≤ 𝑁) ∧ 𝑁 < (2↑(#b‘𝑁))) → (𝑁 ∈ (ℤ≥‘2)
→ ((𝑁 − 1)
∈ (ℤ≥‘(2↑((#b‘𝑁) − 1))) ∧
(2↑(((#b‘𝑁) − 1) + 1)) ∈ ℤ ∧
(𝑁 − 1) <
(2↑(((#b‘𝑁) − 1) + 1))))) |
135 | 134 | 3adant2 1133 |
. . . . . . . . . . 11
⊢
(((((2↑((#b‘𝑁) − 1)) + 1) ∈ ℤ ∧
𝑁 ∈ ℤ ∧
((2↑((#b‘𝑁) − 1)) + 1) ≤ 𝑁) ∧ (2↑(#b‘𝑁)) ∈ ℤ ∧ 𝑁 <
(2↑(#b‘𝑁))) → (𝑁 ∈ (ℤ≥‘2)
→ ((𝑁 − 1)
∈ (ℤ≥‘(2↑((#b‘𝑁) − 1))) ∧
(2↑(((#b‘𝑁) − 1) + 1)) ∈ ℤ ∧
(𝑁 − 1) <
(2↑(((#b‘𝑁) − 1) + 1))))) |
136 | 82, 135 | sylbi 220 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(((2↑((#b‘𝑁) − 1)) +
1)..^(2↑(#b‘𝑁))) → (𝑁 ∈ (ℤ≥‘2)
→ ((𝑁 − 1)
∈ (ℤ≥‘(2↑((#b‘𝑁) − 1))) ∧
(2↑(((#b‘𝑁) − 1) + 1)) ∈ ℤ ∧
(𝑁 − 1) <
(2↑(((#b‘𝑁) − 1) + 1))))) |
137 | 136 | imp 410 |
. . . . . . . . 9
⊢ ((𝑁 ∈
(((2↑((#b‘𝑁) − 1)) +
1)..^(2↑(#b‘𝑁))) ∧ 𝑁 ∈ (ℤ≥‘2))
→ ((𝑁 − 1)
∈ (ℤ≥‘(2↑((#b‘𝑁) − 1))) ∧
(2↑(((#b‘𝑁) − 1) + 1)) ∈ ℤ ∧
(𝑁 − 1) <
(2↑(((#b‘𝑁) − 1) + 1)))) |
138 | | elfzo2 13246 |
. . . . . . . . 9
⊢ ((𝑁 − 1) ∈
((2↑((#b‘𝑁) −
1))..^(2↑(((#b‘𝑁) − 1) + 1))) ↔ ((𝑁 − 1) ∈
(ℤ≥‘(2↑((#b‘𝑁) − 1))) ∧
(2↑(((#b‘𝑁) − 1) + 1)) ∈ ℤ ∧
(𝑁 − 1) <
(2↑(((#b‘𝑁) − 1) + 1)))) |
139 | 137, 138 | sylibr 237 |
. . . . . . . 8
⊢ ((𝑁 ∈
(((2↑((#b‘𝑁) − 1)) +
1)..^(2↑(#b‘𝑁))) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑁 − 1) ∈
((2↑((#b‘𝑁) −
1))..^(2↑(((#b‘𝑁) − 1) + 1)))) |
140 | 139 | adantr 484 |
. . . . . . 7
⊢ (((𝑁 ∈
(((2↑((#b‘𝑁) − 1)) +
1)..^(2↑(#b‘𝑁))) ∧ 𝑁 ∈ (ℤ≥‘2))
∧ ((𝑁 + 1) / 2) ∈
ℕ) → (𝑁 −
1) ∈ ((2↑((#b‘𝑁) −
1))..^(2↑(((#b‘𝑁) − 1) + 1)))) |
141 | | fllog2 45587 |
. . . . . . 7
⊢
((((#b‘𝑁) − 1) ∈ ℕ0
∧ (𝑁 − 1) ∈
((2↑((#b‘𝑁) −
1))..^(2↑(((#b‘𝑁) − 1) + 1)))) →
(⌊‘(2 logb (𝑁 − 1))) = ((#b‘𝑁) − 1)) |
142 | 78, 140, 141 | syl2anc 587 |
. . . . . 6
⊢ (((𝑁 ∈
(((2↑((#b‘𝑁) − 1)) +
1)..^(2↑(#b‘𝑁))) ∧ 𝑁 ∈ (ℤ≥‘2))
∧ ((𝑁 + 1) / 2) ∈
ℕ) → (⌊‘(2 logb (𝑁 − 1))) = ((#b‘𝑁) − 1)) |
143 | 76, 142 | eqtr4d 2780 |
. . . . 5
⊢ (((𝑁 ∈
(((2↑((#b‘𝑁) − 1)) +
1)..^(2↑(#b‘𝑁))) ∧ 𝑁 ∈ (ℤ≥‘2))
∧ ((𝑁 + 1) / 2) ∈
ℕ) → (⌊‘(2 logb 𝑁)) = (⌊‘(2 logb
(𝑁 −
1)))) |
144 | 143 | exp31 423 |
. . . 4
⊢ (𝑁 ∈
(((2↑((#b‘𝑁) − 1)) +
1)..^(2↑(#b‘𝑁))) → (𝑁 ∈ (ℤ≥‘2)
→ (((𝑁 + 1) / 2)
∈ ℕ → (⌊‘(2 logb 𝑁)) = (⌊‘(2 logb
(𝑁 −
1)))))) |
145 | 60, 144 | jaoi 857 |
. . 3
⊢ ((𝑁 =
(2↑((#b‘𝑁) − 1)) ∨ 𝑁 ∈
(((2↑((#b‘𝑁) − 1)) +
1)..^(2↑(#b‘𝑁)))) → (𝑁 ∈ (ℤ≥‘2)
→ (((𝑁 + 1) / 2)
∈ ℕ → (⌊‘(2 logb 𝑁)) = (⌊‘(2 logb
(𝑁 −
1)))))) |
146 | 3, 145 | mpcom 38 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘2) → (((𝑁 + 1) / 2) ∈ ℕ →
(⌊‘(2 logb 𝑁)) = (⌊‘(2 logb
(𝑁 −
1))))) |
147 | 146 | imp 410 |
1
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ ((𝑁 + 1) / 2) ∈ ℕ) →
(⌊‘(2 logb 𝑁)) = (⌊‘(2 logb
(𝑁 −
1)))) |