Proof of Theorem fllog2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nn0z 12640 | . . . 4
⊢ (𝐼 ∈ ℕ0
→ 𝐼 ∈
ℤ) | 
| 2 | 1 | adantr 480 | . . 3
⊢ ((𝐼 ∈ ℕ0
∧ 𝑁 ∈
((2↑𝐼)..^(2↑(𝐼 + 1)))) → 𝐼 ∈ ℤ) | 
| 3 |  | 2rp 13040 | . . . . 5
⊢ 2 ∈
ℝ+ | 
| 4 |  | elfzoelz 13700 | . . . . . . . 8
⊢ (𝑁 ∈ ((2↑𝐼)..^(2↑(𝐼 + 1))) → 𝑁 ∈ ℤ) | 
| 5 | 4 | zred 12724 | . . . . . . 7
⊢ (𝑁 ∈ ((2↑𝐼)..^(2↑(𝐼 + 1))) → 𝑁 ∈ ℝ) | 
| 6 | 5 | adantl 481 | . . . . . 6
⊢ ((𝐼 ∈ ℕ0
∧ 𝑁 ∈
((2↑𝐼)..^(2↑(𝐼 + 1)))) → 𝑁 ∈ ℝ) | 
| 7 |  | elfzo2 13703 | . . . . . . . 8
⊢ (𝑁 ∈ ((2↑𝐼)..^(2↑(𝐼 + 1))) ↔ (𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ (2↑(𝐼 + 1)) ∈ ℤ ∧ 𝑁 < (2↑(𝐼 + 1)))) | 
| 8 |  | eluz2 12885 | . . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘(2↑𝐼)) ↔ ((2↑𝐼) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (2↑𝐼) ≤ 𝑁)) | 
| 9 |  | 2re 12341 | . . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℝ | 
| 10 |  | 2pos 12370 | . . . . . . . . . . . . . . . . 17
⊢ 0 <
2 | 
| 11 | 10 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ (𝐼 ∈ ℕ0
→ 0 < 2) | 
| 12 |  | expgt0 14137 | . . . . . . . . . . . . . . . 16
⊢ ((2
∈ ℝ ∧ 𝐼
∈ ℤ ∧ 0 < 2) → 0 < (2↑𝐼)) | 
| 13 | 9, 1, 11, 12 | mp3an2i 1467 | . . . . . . . . . . . . . . 15
⊢ (𝐼 ∈ ℕ0
→ 0 < (2↑𝐼)) | 
| 14 | 13 | adantl 481 | . . . . . . . . . . . . . 14
⊢
((((2↑𝐼) ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ 𝐼 ∈
ℕ0) → 0 < (2↑𝐼)) | 
| 15 |  | 0red 11265 | . . . . . . . . . . . . . . 15
⊢
((((2↑𝐼) ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ 𝐼 ∈
ℕ0) → 0 ∈ ℝ) | 
| 16 |  | zre 12619 | . . . . . . . . . . . . . . . . 17
⊢
((2↑𝐼) ∈
ℤ → (2↑𝐼)
∈ ℝ) | 
| 17 | 16 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢
(((2↑𝐼) ∈
ℤ ∧ 𝑁 ∈
ℤ) → (2↑𝐼)
∈ ℝ) | 
| 18 | 17 | adantr 480 | . . . . . . . . . . . . . . 15
⊢
((((2↑𝐼) ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ 𝐼 ∈
ℕ0) → (2↑𝐼) ∈ ℝ) | 
| 19 |  | zre 12619 | . . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) | 
| 20 | 19 | ad2antlr 727 | . . . . . . . . . . . . . . 15
⊢
((((2↑𝐼) ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ 𝐼 ∈
ℕ0) → 𝑁 ∈ ℝ) | 
| 21 |  | ltletr 11354 | . . . . . . . . . . . . . . 15
⊢ ((0
∈ ℝ ∧ (2↑𝐼) ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((0 <
(2↑𝐼) ∧
(2↑𝐼) ≤ 𝑁) → 0 < 𝑁)) | 
| 22 | 15, 18, 20, 21 | syl3anc 1372 | . . . . . . . . . . . . . 14
⊢
((((2↑𝐼) ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ 𝐼 ∈
ℕ0) → ((0 < (2↑𝐼) ∧ (2↑𝐼) ≤ 𝑁) → 0 < 𝑁)) | 
| 23 | 14, 22 | mpand 695 | . . . . . . . . . . . . 13
⊢
((((2↑𝐼) ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ 𝐼 ∈
ℕ0) → ((2↑𝐼) ≤ 𝑁 → 0 < 𝑁)) | 
| 24 | 23 | ex 412 | . . . . . . . . . . . 12
⊢
(((2↑𝐼) ∈
ℤ ∧ 𝑁 ∈
ℤ) → (𝐼 ∈
ℕ0 → ((2↑𝐼) ≤ 𝑁 → 0 < 𝑁))) | 
| 25 | 24 | com23 86 | . . . . . . . . . . 11
⊢
(((2↑𝐼) ∈
ℤ ∧ 𝑁 ∈
ℤ) → ((2↑𝐼)
≤ 𝑁 → (𝐼 ∈ ℕ0
→ 0 < 𝑁))) | 
| 26 | 25 | 3impia 1117 | . . . . . . . . . 10
⊢
(((2↑𝐼) ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ (2↑𝐼)
≤ 𝑁) → (𝐼 ∈ ℕ0
→ 0 < 𝑁)) | 
| 27 | 8, 26 | sylbi 217 | . . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘(2↑𝐼)) → (𝐼 ∈ ℕ0 → 0 <
𝑁)) | 
| 28 | 27 | 3ad2ant1 1133 | . . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ (2↑(𝐼 + 1)) ∈ ℤ ∧ 𝑁 < (2↑(𝐼 + 1))) → (𝐼 ∈ ℕ0 → 0 <
𝑁)) | 
| 29 | 7, 28 | sylbi 217 | . . . . . . 7
⊢ (𝑁 ∈ ((2↑𝐼)..^(2↑(𝐼 + 1))) → (𝐼 ∈ ℕ0 → 0 <
𝑁)) | 
| 30 | 29 | impcom 407 | . . . . . 6
⊢ ((𝐼 ∈ ℕ0
∧ 𝑁 ∈
((2↑𝐼)..^(2↑(𝐼 + 1)))) → 0 < 𝑁) | 
| 31 | 6, 30 | elrpd 13075 | . . . . 5
⊢ ((𝐼 ∈ ℕ0
∧ 𝑁 ∈
((2↑𝐼)..^(2↑(𝐼 + 1)))) → 𝑁 ∈
ℝ+) | 
| 32 |  | 1ne2 12475 | . . . . . . 7
⊢ 1 ≠
2 | 
| 33 | 32 | necomi 2994 | . . . . . 6
⊢ 2 ≠
1 | 
| 34 | 33 | a1i 11 | . . . . 5
⊢ ((𝐼 ∈ ℕ0
∧ 𝑁 ∈
((2↑𝐼)..^(2↑(𝐼 + 1)))) → 2 ≠ 1) | 
| 35 |  | relogbcl 26817 | . . . . 5
⊢ ((2
∈ ℝ+ ∧ 𝑁 ∈ ℝ+ ∧ 2 ≠ 1)
→ (2 logb 𝑁) ∈ ℝ) | 
| 36 | 3, 31, 34, 35 | mp3an2i 1467 | . . . 4
⊢ ((𝐼 ∈ ℕ0
∧ 𝑁 ∈
((2↑𝐼)..^(2↑(𝐼 + 1)))) → (2 logb 𝑁) ∈
ℝ) | 
| 37 | 36 | flcld 13839 | . . 3
⊢ ((𝐼 ∈ ℕ0
∧ 𝑁 ∈
((2↑𝐼)..^(2↑(𝐼 + 1)))) → (⌊‘(2
logb 𝑁)) ∈
ℤ) | 
| 38 |  | eluzelz 12889 | . . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘(2↑𝐼)) → 𝑁 ∈ ℤ) | 
| 39 |  | zltlem1 12672 | . . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧
(2↑(𝐼 + 1)) ∈
ℤ) → (𝑁 <
(2↑(𝐼 + 1)) ↔
𝑁 ≤ ((2↑(𝐼 + 1)) −
1))) | 
| 40 | 38, 39 | sylan 580 | . . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ (2↑(𝐼 + 1)) ∈ ℤ) → (𝑁 < (2↑(𝐼 + 1)) ↔ 𝑁 ≤ ((2↑(𝐼 + 1)) − 1))) | 
| 41 |  | 2z 12651 | . . . . . . . . . . . 12
⊢ 2 ∈
ℤ | 
| 42 |  | uzid 12894 | . . . . . . . . . . . 12
⊢ (2 ∈
ℤ → 2 ∈ (ℤ≥‘2)) | 
| 43 | 41, 42 | ax-mp 5 | . . . . . . . . . . 11
⊢ 2 ∈
(ℤ≥‘2) | 
| 44 |  | eluzelre 12890 | . . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘(2↑𝐼)) → 𝑁 ∈ ℝ) | 
| 45 | 44 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ 𝐼 ∈ ℕ0) → 𝑁 ∈
ℝ) | 
| 46 | 9 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐼 ∈ ℕ0
→ 2 ∈ ℝ) | 
| 47 | 46, 1, 11 | 3jca 1128 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐼 ∈ ℕ0
→ (2 ∈ ℝ ∧ 𝐼 ∈ ℤ ∧ 0 <
2)) | 
| 48 | 47 | 3ad2ant3 1135 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((2↑𝐼) ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝐼 ∈
ℕ0) → (2 ∈ ℝ ∧ 𝐼 ∈ ℤ ∧ 0 <
2)) | 
| 49 | 48, 12 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢
(((2↑𝐼) ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝐼 ∈
ℕ0) → 0 < (2↑𝐼)) | 
| 50 |  | 0red 11265 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((2↑𝐼) ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝐼 ∈
ℕ0) → 0 ∈ ℝ) | 
| 51 | 16 | 3ad2ant1 1133 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((2↑𝐼) ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝐼 ∈
ℕ0) → (2↑𝐼) ∈ ℝ) | 
| 52 | 19 | 3ad2ant2 1134 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((2↑𝐼) ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝐼 ∈
ℕ0) → 𝑁 ∈ ℝ) | 
| 53 | 50, 51, 52, 21 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . 19
⊢
(((2↑𝐼) ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝐼 ∈
ℕ0) → ((0 < (2↑𝐼) ∧ (2↑𝐼) ≤ 𝑁) → 0 < 𝑁)) | 
| 54 | 49, 53 | mpand 695 | . . . . . . . . . . . . . . . . . 18
⊢
(((2↑𝐼) ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝐼 ∈
ℕ0) → ((2↑𝐼) ≤ 𝑁 → 0 < 𝑁)) | 
| 55 | 54 | 3exp 1119 | . . . . . . . . . . . . . . . . 17
⊢
((2↑𝐼) ∈
ℤ → (𝑁 ∈
ℤ → (𝐼 ∈
ℕ0 → ((2↑𝐼) ≤ 𝑁 → 0 < 𝑁)))) | 
| 56 | 55 | com34 91 | . . . . . . . . . . . . . . . 16
⊢
((2↑𝐼) ∈
ℤ → (𝑁 ∈
ℤ → ((2↑𝐼)
≤ 𝑁 → (𝐼 ∈ ℕ0
→ 0 < 𝑁)))) | 
| 57 | 56 | 3imp 1110 | . . . . . . . . . . . . . . 15
⊢
(((2↑𝐼) ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ (2↑𝐼)
≤ 𝑁) → (𝐼 ∈ ℕ0
→ 0 < 𝑁)) | 
| 58 | 8, 57 | sylbi 217 | . . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘(2↑𝐼)) → (𝐼 ∈ ℕ0 → 0 <
𝑁)) | 
| 59 | 58 | imp 406 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ 𝐼 ∈ ℕ0) → 0 <
𝑁) | 
| 60 | 45, 59 | elrpd 13075 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ 𝐼 ∈ ℕ0) → 𝑁 ∈
ℝ+) | 
| 61 | 60 | adantlr 715 | . . . . . . . . . . 11
⊢ (((𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ (2↑(𝐼 + 1)) ∈ ℤ) ∧ 𝐼 ∈ ℕ0)
→ 𝑁 ∈
ℝ+) | 
| 62 | 9 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ (2↑(𝐼 + 1)) ∈ ℤ) ∧ 𝐼 ∈ ℕ0)
→ 2 ∈ ℝ) | 
| 63 |  | peano2nn0 12568 | . . . . . . . . . . . . . . 15
⊢ (𝐼 ∈ ℕ0
→ (𝐼 + 1) ∈
ℕ0) | 
| 64 | 63 | adantl 481 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ (2↑(𝐼 + 1)) ∈ ℤ) ∧ 𝐼 ∈ ℕ0)
→ (𝐼 + 1) ∈
ℕ0) | 
| 65 | 62, 64 | reexpcld 14204 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ (2↑(𝐼 + 1)) ∈ ℤ) ∧ 𝐼 ∈ ℕ0)
→ (2↑(𝐼 + 1))
∈ ℝ) | 
| 66 |  | peano2rem 11577 | . . . . . . . . . . . . 13
⊢
((2↑(𝐼 + 1))
∈ ℝ → ((2↑(𝐼 + 1)) − 1) ∈
ℝ) | 
| 67 | 65, 66 | syl 17 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ (2↑(𝐼 + 1)) ∈ ℤ) ∧ 𝐼 ∈ ℕ0)
→ ((2↑(𝐼 + 1))
− 1) ∈ ℝ) | 
| 68 |  | nn0p1nn 12567 | . . . . . . . . . . . . . . . 16
⊢ (𝐼 ∈ ℕ0
→ (𝐼 + 1) ∈
ℕ) | 
| 69 |  | 1lt2 12438 | . . . . . . . . . . . . . . . . 17
⊢ 1 <
2 | 
| 70 | 69 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ (𝐼 ∈ ℕ0
→ 1 < 2) | 
| 71 | 46, 68, 70 | 3jca 1128 | . . . . . . . . . . . . . . 15
⊢ (𝐼 ∈ ℕ0
→ (2 ∈ ℝ ∧ (𝐼 + 1) ∈ ℕ ∧ 1 <
2)) | 
| 72 | 71 | adantl 481 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ (2↑(𝐼 + 1)) ∈ ℤ) ∧ 𝐼 ∈ ℕ0)
→ (2 ∈ ℝ ∧ (𝐼 + 1) ∈ ℕ ∧ 1 <
2)) | 
| 73 |  | expgt1 14142 | . . . . . . . . . . . . . 14
⊢ ((2
∈ ℝ ∧ (𝐼 +
1) ∈ ℕ ∧ 1 < 2) → 1 < (2↑(𝐼 + 1))) | 
| 74 | 72, 73 | syl 17 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ (2↑(𝐼 + 1)) ∈ ℤ) ∧ 𝐼 ∈ ℕ0)
→ 1 < (2↑(𝐼 +
1))) | 
| 75 |  | 1red 11263 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ (2↑(𝐼 + 1)) ∈ ℤ) ∧ 𝐼 ∈ ℕ0)
→ 1 ∈ ℝ) | 
| 76 |  | zre 12619 | . . . . . . . . . . . . . . 15
⊢
((2↑(𝐼 + 1))
∈ ℤ → (2↑(𝐼 + 1)) ∈ ℝ) | 
| 77 | 76 | ad2antlr 727 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ (2↑(𝐼 + 1)) ∈ ℤ) ∧ 𝐼 ∈ ℕ0)
→ (2↑(𝐼 + 1))
∈ ℝ) | 
| 78 | 75, 77 | posdifd 11851 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ (2↑(𝐼 + 1)) ∈ ℤ) ∧ 𝐼 ∈ ℕ0)
→ (1 < (2↑(𝐼 +
1)) ↔ 0 < ((2↑(𝐼 + 1)) − 1))) | 
| 79 | 74, 78 | mpbid 232 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ (2↑(𝐼 + 1)) ∈ ℤ) ∧ 𝐼 ∈ ℕ0)
→ 0 < ((2↑(𝐼 +
1)) − 1)) | 
| 80 | 67, 79 | elrpd 13075 | . . . . . . . . . . 11
⊢ (((𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ (2↑(𝐼 + 1)) ∈ ℤ) ∧ 𝐼 ∈ ℕ0)
→ ((2↑(𝐼 + 1))
− 1) ∈ ℝ+) | 
| 81 |  | logbleb 26827 | . . . . . . . . . . 11
⊢ ((2
∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℝ+ ∧
((2↑(𝐼 + 1)) −
1) ∈ ℝ+) → (𝑁 ≤ ((2↑(𝐼 + 1)) − 1) ↔ (2 logb
𝑁) ≤ (2 logb
((2↑(𝐼 + 1)) −
1)))) | 
| 82 | 43, 61, 80, 81 | mp3an2i 1467 | . . . . . . . . . 10
⊢ (((𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ (2↑(𝐼 + 1)) ∈ ℤ) ∧ 𝐼 ∈ ℕ0)
→ (𝑁 ≤
((2↑(𝐼 + 1)) −
1) ↔ (2 logb 𝑁) ≤ (2 logb ((2↑(𝐼 + 1)) −
1)))) | 
| 83 | 44 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ (2↑(𝐼 + 1)) ∈ ℤ) → 𝑁 ∈
ℝ) | 
| 84 | 83 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ (2↑(𝐼 + 1)) ∈ ℤ) ∧ 𝐼 ∈ ℕ0)
→ 𝑁 ∈
ℝ) | 
| 85 | 59 | adantlr 715 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ (2↑(𝐼 + 1)) ∈ ℤ) ∧ 𝐼 ∈ ℕ0)
→ 0 < 𝑁) | 
| 86 | 84, 85 | elrpd 13075 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ (2↑(𝐼 + 1)) ∈ ℤ) ∧ 𝐼 ∈ ℕ0)
→ 𝑁 ∈
ℝ+) | 
| 87 | 33 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ (2↑(𝐼 + 1)) ∈ ℤ) ∧ 𝐼 ∈ ℕ0)
→ 2 ≠ 1) | 
| 88 | 3, 86, 87, 35 | mp3an2i 1467 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ (2↑(𝐼 + 1)) ∈ ℤ) ∧ 𝐼 ∈ ℕ0)
→ (2 logb 𝑁) ∈ ℝ) | 
| 89 | 88 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((((𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ (2↑(𝐼 + 1)) ∈ ℤ) ∧ 𝐼 ∈ ℕ0)
∧ (2 logb 𝑁)
≤ (2 logb ((2↑(𝐼 + 1)) − 1))) → (2
logb 𝑁) ∈
ℝ) | 
| 90 | 43 | a1i 11 | . . . . . . . . . . . . . . . . 17
⊢ (𝐼 ∈ ℕ0
→ 2 ∈ (ℤ≥‘2)) | 
| 91 | 46, 63 | reexpcld 14204 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐼 ∈ ℕ0
→ (2↑(𝐼 + 1))
∈ ℝ) | 
| 92 | 91, 66 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐼 ∈ ℕ0
→ ((2↑(𝐼 + 1))
− 1) ∈ ℝ) | 
| 93 | 9, 68, 70, 73 | mp3an2i 1467 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐼 ∈ ℕ0
→ 1 < (2↑(𝐼 +
1))) | 
| 94 |  | 1red 11263 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝐼 ∈ ℕ0
→ 1 ∈ ℝ) | 
| 95 | 94, 91 | posdifd 11851 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐼 ∈ ℕ0
→ (1 < (2↑(𝐼 +
1)) ↔ 0 < ((2↑(𝐼 + 1)) − 1))) | 
| 96 | 93, 95 | mpbid 232 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐼 ∈ ℕ0
→ 0 < ((2↑(𝐼 +
1)) − 1)) | 
| 97 | 92, 96 | elrpd 13075 | . . . . . . . . . . . . . . . . 17
⊢ (𝐼 ∈ ℕ0
→ ((2↑(𝐼 + 1))
− 1) ∈ ℝ+) | 
| 98 | 90, 97 | jca 511 | . . . . . . . . . . . . . . . 16
⊢ (𝐼 ∈ ℕ0
→ (2 ∈ (ℤ≥‘2) ∧ ((2↑(𝐼 + 1)) − 1) ∈
ℝ+)) | 
| 99 | 98 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ (2↑(𝐼 + 1)) ∈ ℤ) ∧ 𝐼 ∈ ℕ0)
→ (2 ∈ (ℤ≥‘2) ∧ ((2↑(𝐼 + 1)) − 1) ∈
ℝ+)) | 
| 100 |  | relogbzcl 26818 | . . . . . . . . . . . . . . 15
⊢ ((2
∈ (ℤ≥‘2) ∧ ((2↑(𝐼 + 1)) − 1) ∈
ℝ+) → (2 logb ((2↑(𝐼 + 1)) − 1)) ∈
ℝ) | 
| 101 | 99, 100 | syl 17 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ (2↑(𝐼 + 1)) ∈ ℤ) ∧ 𝐼 ∈ ℕ0)
→ (2 logb ((2↑(𝐼 + 1)) − 1)) ∈
ℝ) | 
| 102 | 101 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((((𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ (2↑(𝐼 + 1)) ∈ ℤ) ∧ 𝐼 ∈ ℕ0)
∧ (2 logb 𝑁)
≤ (2 logb ((2↑(𝐼 + 1)) − 1))) → (2
logb ((2↑(𝐼
+ 1)) − 1)) ∈ ℝ) | 
| 103 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ ((((𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ (2↑(𝐼 + 1)) ∈ ℤ) ∧ 𝐼 ∈ ℕ0)
∧ (2 logb 𝑁)
≤ (2 logb ((2↑(𝐼 + 1)) − 1))) → (2
logb 𝑁) ≤ (2
logb ((2↑(𝐼
+ 1)) − 1))) | 
| 104 |  | flwordi 13853 | . . . . . . . . . . . . 13
⊢ (((2
logb 𝑁) ∈
ℝ ∧ (2 logb ((2↑(𝐼 + 1)) − 1)) ∈ ℝ ∧ (2
logb 𝑁) ≤ (2
logb ((2↑(𝐼
+ 1)) − 1))) → (⌊‘(2 logb 𝑁)) ≤ (⌊‘(2 logb
((2↑(𝐼 + 1)) −
1)))) | 
| 105 | 89, 102, 103, 104 | syl3anc 1372 | . . . . . . . . . . . 12
⊢ ((((𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ (2↑(𝐼 + 1)) ∈ ℤ) ∧ 𝐼 ∈ ℕ0)
∧ (2 logb 𝑁)
≤ (2 logb ((2↑(𝐼 + 1)) − 1))) → (⌊‘(2
logb 𝑁)) ≤
(⌊‘(2 logb ((2↑(𝐼 + 1)) − 1)))) | 
| 106 | 105 | ex 412 | . . . . . . . . . . 11
⊢ (((𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ (2↑(𝐼 + 1)) ∈ ℤ) ∧ 𝐼 ∈ ℕ0)
→ ((2 logb 𝑁) ≤ (2 logb ((2↑(𝐼 + 1)) − 1)) →
(⌊‘(2 logb 𝑁)) ≤ (⌊‘(2 logb
((2↑(𝐼 + 1)) −
1))))) | 
| 107 | 68 | adantl 481 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ (2↑(𝐼 + 1)) ∈ ℤ) ∧ 𝐼 ∈ ℕ0)
→ (𝐼 + 1) ∈
ℕ) | 
| 108 |  | logbpw2m1 48493 | . . . . . . . . . . . . . 14
⊢ ((𝐼 + 1) ∈ ℕ →
(⌊‘(2 logb ((2↑(𝐼 + 1)) − 1))) = ((𝐼 + 1) − 1)) | 
| 109 | 107, 108 | syl 17 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ (2↑(𝐼 + 1)) ∈ ℤ) ∧ 𝐼 ∈ ℕ0)
→ (⌊‘(2 logb ((2↑(𝐼 + 1)) − 1))) = ((𝐼 + 1) − 1)) | 
| 110 |  | nn0cn 12538 | . . . . . . . . . . . . . . 15
⊢ (𝐼 ∈ ℕ0
→ 𝐼 ∈
ℂ) | 
| 111 |  | pncan1 11688 | . . . . . . . . . . . . . . 15
⊢ (𝐼 ∈ ℂ → ((𝐼 + 1) − 1) = 𝐼) | 
| 112 | 110, 111 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝐼 ∈ ℕ0
→ ((𝐼 + 1) − 1)
= 𝐼) | 
| 113 | 112 | adantl 481 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ (2↑(𝐼 + 1)) ∈ ℤ) ∧ 𝐼 ∈ ℕ0)
→ ((𝐼 + 1) − 1)
= 𝐼) | 
| 114 | 109, 113 | eqtrd 2776 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ (2↑(𝐼 + 1)) ∈ ℤ) ∧ 𝐼 ∈ ℕ0)
→ (⌊‘(2 logb ((2↑(𝐼 + 1)) − 1))) = 𝐼) | 
| 115 | 114 | breq2d 5154 | . . . . . . . . . . 11
⊢ (((𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ (2↑(𝐼 + 1)) ∈ ℤ) ∧ 𝐼 ∈ ℕ0)
→ ((⌊‘(2 logb 𝑁)) ≤ (⌊‘(2 logb
((2↑(𝐼 + 1)) −
1))) ↔ (⌊‘(2 logb 𝑁)) ≤ 𝐼)) | 
| 116 | 106, 115 | sylibd 239 | . . . . . . . . . 10
⊢ (((𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ (2↑(𝐼 + 1)) ∈ ℤ) ∧ 𝐼 ∈ ℕ0)
→ ((2 logb 𝑁) ≤ (2 logb ((2↑(𝐼 + 1)) − 1)) →
(⌊‘(2 logb 𝑁)) ≤ 𝐼)) | 
| 117 | 82, 116 | sylbid 240 | . . . . . . . . 9
⊢ (((𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ (2↑(𝐼 + 1)) ∈ ℤ) ∧ 𝐼 ∈ ℕ0)
→ (𝑁 ≤
((2↑(𝐼 + 1)) −
1) → (⌊‘(2 logb 𝑁)) ≤ 𝐼)) | 
| 118 | 117 | ex 412 | . . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ (2↑(𝐼 + 1)) ∈ ℤ) → (𝐼 ∈ ℕ0
→ (𝑁 ≤
((2↑(𝐼 + 1)) −
1) → (⌊‘(2 logb 𝑁)) ≤ 𝐼))) | 
| 119 | 118 | com23 86 | . . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ (2↑(𝐼 + 1)) ∈ ℤ) → (𝑁 ≤ ((2↑(𝐼 + 1)) − 1) → (𝐼 ∈ ℕ0
→ (⌊‘(2 logb 𝑁)) ≤ 𝐼))) | 
| 120 | 40, 119 | sylbid 240 | . . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ (2↑(𝐼 + 1)) ∈ ℤ) → (𝑁 < (2↑(𝐼 + 1)) → (𝐼 ∈ ℕ0 →
(⌊‘(2 logb 𝑁)) ≤ 𝐼))) | 
| 121 | 120 | 3impia 1117 | . . . . 5
⊢ ((𝑁 ∈
(ℤ≥‘(2↑𝐼)) ∧ (2↑(𝐼 + 1)) ∈ ℤ ∧ 𝑁 < (2↑(𝐼 + 1))) → (𝐼 ∈ ℕ0 →
(⌊‘(2 logb 𝑁)) ≤ 𝐼)) | 
| 122 | 7, 121 | sylbi 217 | . . . 4
⊢ (𝑁 ∈ ((2↑𝐼)..^(2↑(𝐼 + 1))) → (𝐼 ∈ ℕ0 →
(⌊‘(2 logb 𝑁)) ≤ 𝐼)) | 
| 123 | 122 | impcom 407 | . . 3
⊢ ((𝐼 ∈ ℕ0
∧ 𝑁 ∈
((2↑𝐼)..^(2↑(𝐼 + 1)))) → (⌊‘(2
logb 𝑁)) ≤
𝐼) | 
| 124 |  | nn0re 12537 | . . . . . . . 8
⊢ (𝐼 ∈ ℕ0
→ 𝐼 ∈
ℝ) | 
| 125 |  | nn0ge0 12553 | . . . . . . . 8
⊢ (𝐼 ∈ ℕ0
→ 0 ≤ 𝐼) | 
| 126 |  | flge0nn0 13861 | . . . . . . . 8
⊢ ((𝐼 ∈ ℝ ∧ 0 ≤
𝐼) →
(⌊‘𝐼) ∈
ℕ0) | 
| 127 | 124, 125,
126 | syl2anc 584 | . . . . . . 7
⊢ (𝐼 ∈ ℕ0
→ (⌊‘𝐼)
∈ ℕ0) | 
| 128 | 127 | nn0red 12590 | . . . . . 6
⊢ (𝐼 ∈ ℕ0
→ (⌊‘𝐼)
∈ ℝ) | 
| 129 | 128 | adantr 480 | . . . . 5
⊢ ((𝐼 ∈ ℕ0
∧ 𝑁 ∈
((2↑𝐼)..^(2↑(𝐼 + 1)))) → (⌊‘𝐼) ∈
ℝ) | 
| 130 | 124 | adantr 480 | . . . . 5
⊢ ((𝐼 ∈ ℕ0
∧ 𝑁 ∈
((2↑𝐼)..^(2↑(𝐼 + 1)))) → 𝐼 ∈ ℝ) | 
| 131 |  | flle 13840 | . . . . . . 7
⊢ (𝐼 ∈ ℝ →
(⌊‘𝐼) ≤
𝐼) | 
| 132 | 124, 131 | syl 17 | . . . . . 6
⊢ (𝐼 ∈ ℕ0
→ (⌊‘𝐼)
≤ 𝐼) | 
| 133 | 132 | adantr 480 | . . . . 5
⊢ ((𝐼 ∈ ℕ0
∧ 𝑁 ∈
((2↑𝐼)..^(2↑(𝐼 + 1)))) → (⌊‘𝐼) ≤ 𝐼) | 
| 134 | 3 | a1i 11 | . . . . . . . . 9
⊢ (𝐼 ∈ ℕ0
→ 2 ∈ ℝ+) | 
| 135 | 134, 1 | rpexpcld 14287 | . . . . . . . 8
⊢ (𝐼 ∈ ℕ0
→ (2↑𝐼) ∈
ℝ+) | 
| 136 | 33 | a1i 11 | . . . . . . . 8
⊢ (𝐼 ∈ ℕ0
→ 2 ≠ 1) | 
| 137 |  | relogbcl 26817 | . . . . . . . 8
⊢ ((2
∈ ℝ+ ∧ (2↑𝐼) ∈ ℝ+ ∧ 2 ≠ 1)
→ (2 logb (2↑𝐼)) ∈ ℝ) | 
| 138 | 3, 135, 136, 137 | mp3an2i 1467 | . . . . . . 7
⊢ (𝐼 ∈ ℕ0
→ (2 logb (2↑𝐼)) ∈ ℝ) | 
| 139 | 138 | adantr 480 | . . . . . 6
⊢ ((𝐼 ∈ ℕ0
∧ 𝑁 ∈
((2↑𝐼)..^(2↑(𝐼 + 1)))) → (2 logb
(2↑𝐼)) ∈
ℝ) | 
| 140 |  | nnlogbexp 26825 | . . . . . . . . . 10
⊢ ((2
∈ (ℤ≥‘2) ∧ 𝐼 ∈ ℤ) → (2 logb
(2↑𝐼)) = 𝐼) | 
| 141 | 90, 1, 140 | syl2anc 584 | . . . . . . . . 9
⊢ (𝐼 ∈ ℕ0
→ (2 logb (2↑𝐼)) = 𝐼) | 
| 142 | 141 | eqcomd 2742 | . . . . . . . 8
⊢ (𝐼 ∈ ℕ0
→ 𝐼 = (2
logb (2↑𝐼))) | 
| 143 | 124, 142 | eqled 11365 | . . . . . . 7
⊢ (𝐼 ∈ ℕ0
→ 𝐼 ≤ (2
logb (2↑𝐼))) | 
| 144 | 143 | adantr 480 | . . . . . 6
⊢ ((𝐼 ∈ ℕ0
∧ 𝑁 ∈
((2↑𝐼)..^(2↑(𝐼 + 1)))) → 𝐼 ≤ (2 logb (2↑𝐼))) | 
| 145 |  | elfzole1 13708 | . . . . . . . 8
⊢ (𝑁 ∈ ((2↑𝐼)..^(2↑(𝐼 + 1))) → (2↑𝐼) ≤ 𝑁) | 
| 146 | 145 | adantl 481 | . . . . . . 7
⊢ ((𝐼 ∈ ℕ0
∧ 𝑁 ∈
((2↑𝐼)..^(2↑(𝐼 + 1)))) → (2↑𝐼) ≤ 𝑁) | 
| 147 | 135 | adantr 480 | . . . . . . . 8
⊢ ((𝐼 ∈ ℕ0
∧ 𝑁 ∈
((2↑𝐼)..^(2↑(𝐼 + 1)))) → (2↑𝐼) ∈
ℝ+) | 
| 148 |  | logbleb 26827 | . . . . . . . 8
⊢ ((2
∈ (ℤ≥‘2) ∧ (2↑𝐼) ∈ ℝ+ ∧ 𝑁 ∈ ℝ+)
→ ((2↑𝐼) ≤
𝑁 ↔ (2 logb
(2↑𝐼)) ≤ (2
logb 𝑁))) | 
| 149 | 43, 147, 31, 148 | mp3an2i 1467 | . . . . . . 7
⊢ ((𝐼 ∈ ℕ0
∧ 𝑁 ∈
((2↑𝐼)..^(2↑(𝐼 + 1)))) → ((2↑𝐼) ≤ 𝑁 ↔ (2 logb (2↑𝐼)) ≤ (2 logb 𝑁))) | 
| 150 | 146, 149 | mpbid 232 | . . . . . 6
⊢ ((𝐼 ∈ ℕ0
∧ 𝑁 ∈
((2↑𝐼)..^(2↑(𝐼 + 1)))) → (2 logb
(2↑𝐼)) ≤ (2
logb 𝑁)) | 
| 151 | 130, 139,
36, 144, 150 | letrd 11419 | . . . . 5
⊢ ((𝐼 ∈ ℕ0
∧ 𝑁 ∈
((2↑𝐼)..^(2↑(𝐼 + 1)))) → 𝐼 ≤ (2 logb 𝑁)) | 
| 152 | 129, 130,
36, 133, 151 | letrd 11419 | . . . 4
⊢ ((𝐼 ∈ ℕ0
∧ 𝑁 ∈
((2↑𝐼)..^(2↑(𝐼 + 1)))) → (⌊‘𝐼) ≤ (2 logb 𝑁)) | 
| 153 |  | flflp1 13848 | . . . . 5
⊢ ((𝐼 ∈ ℝ ∧ (2
logb 𝑁) ∈
ℝ) → ((⌊‘𝐼) ≤ (2 logb 𝑁) ↔ 𝐼 < ((⌊‘(2 logb
𝑁)) + 1))) | 
| 154 | 130, 36, 153 | syl2anc 584 | . . . 4
⊢ ((𝐼 ∈ ℕ0
∧ 𝑁 ∈
((2↑𝐼)..^(2↑(𝐼 + 1)))) → ((⌊‘𝐼) ≤ (2 logb 𝑁) ↔ 𝐼 < ((⌊‘(2 logb
𝑁)) + 1))) | 
| 155 | 152, 154 | mpbid 232 | . . 3
⊢ ((𝐼 ∈ ℕ0
∧ 𝑁 ∈
((2↑𝐼)..^(2↑(𝐼 + 1)))) → 𝐼 < ((⌊‘(2 logb
𝑁)) + 1)) | 
| 156 |  | zgeltp1eq 47326 | . . . 4
⊢ ((𝐼 ∈ ℤ ∧
(⌊‘(2 logb 𝑁)) ∈ ℤ) →
(((⌊‘(2 logb 𝑁)) ≤ 𝐼 ∧ 𝐼 < ((⌊‘(2 logb
𝑁)) + 1)) → 𝐼 = (⌊‘(2
logb 𝑁)))) | 
| 157 | 156 | imp 406 | . . 3
⊢ (((𝐼 ∈ ℤ ∧
(⌊‘(2 logb 𝑁)) ∈ ℤ) ∧ ((⌊‘(2
logb 𝑁)) ≤
𝐼 ∧ 𝐼 < ((⌊‘(2 logb
𝑁)) + 1))) → 𝐼 = (⌊‘(2
logb 𝑁))) | 
| 158 | 2, 37, 123, 155, 157 | syl22anc 838 | . 2
⊢ ((𝐼 ∈ ℕ0
∧ 𝑁 ∈
((2↑𝐼)..^(2↑(𝐼 + 1)))) → 𝐼 = (⌊‘(2 logb 𝑁))) | 
| 159 | 158 | eqcomd 2742 | 1
⊢ ((𝐼 ∈ ℕ0
∧ 𝑁 ∈
((2↑𝐼)..^(2↑(𝐼 + 1)))) → (⌊‘(2
logb 𝑁)) = 𝐼) |