| Step | Hyp | Ref
| Expression |
| 1 | | 2re 12340 |
. . . . . . . . . . 11
⊢ 2 ∈
ℝ |
| 2 | | 1lt2 12437 |
. . . . . . . . . . 11
⊢ 1 <
2 |
| 3 | | rplogcl 26646 |
. . . . . . . . . . 11
⊢ ((2
∈ ℝ ∧ 1 < 2) → (log‘2) ∈
ℝ+) |
| 4 | 1, 2, 3 | mp2an 692 |
. . . . . . . . . 10
⊢
(log‘2) ∈ ℝ+ |
| 5 | | elrp 13036 |
. . . . . . . . . 10
⊢
((log‘2) ∈ ℝ+ ↔ ((log‘2) ∈
ℝ ∧ 0 < (log‘2))) |
| 6 | 4, 5 | mpbi 230 |
. . . . . . . . 9
⊢
((log‘2) ∈ ℝ ∧ 0 <
(log‘2)) |
| 7 | 6 | simpli 483 |
. . . . . . . 8
⊢
(log‘2) ∈ ℝ |
| 8 | 7 | recni 11275 |
. . . . . . 7
⊢
(log‘2) ∈ ℂ |
| 9 | 8 | mulridi 11265 |
. . . . . 6
⊢
((log‘2) · 1) = (log‘2) |
| 10 | | cht2 27215 |
. . . . . 6
⊢
(θ‘2) = (log‘2) |
| 11 | 9, 10 | eqtr4i 2768 |
. . . . 5
⊢
((log‘2) · 1) = (θ‘2) |
| 12 | | fveq2 6906 |
. . . . 5
⊢
((⌊‘𝑁) =
2 → (θ‘(⌊‘𝑁)) = (θ‘2)) |
| 13 | 11, 12 | eqtr4id 2796 |
. . . 4
⊢
((⌊‘𝑁) =
2 → ((log‘2) · 1) = (θ‘(⌊‘𝑁))) |
| 14 | | chtfl 27192 |
. . . . 5
⊢ (𝑁 ∈ ℝ →
(θ‘(⌊‘𝑁)) = (θ‘𝑁)) |
| 15 | 14 | adantr 480 |
. . . 4
⊢ ((𝑁 ∈ ℝ ∧ 2 <
𝑁) →
(θ‘(⌊‘𝑁)) = (θ‘𝑁)) |
| 16 | 13, 15 | sylan9eqr 2799 |
. . 3
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) = 2)
→ ((log‘2) · 1) = (θ‘𝑁)) |
| 17 | | 2t2e4 12430 |
. . . . . . 7
⊢ (2
· 2) = 4 |
| 18 | | df-4 12331 |
. . . . . . 7
⊢ 4 = (3 +
1) |
| 19 | 17, 18 | eqtri 2765 |
. . . . . 6
⊢ (2
· 2) = (3 + 1) |
| 20 | | simplr 769 |
. . . . . . 7
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) = 2)
→ 2 < 𝑁) |
| 21 | | simpl 482 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 2 <
𝑁) → 𝑁 ∈ ℝ) |
| 22 | | 2pos 12369 |
. . . . . . . . . 10
⊢ 0 <
2 |
| 23 | 1, 22 | pm3.2i 470 |
. . . . . . . . 9
⊢ (2 ∈
ℝ ∧ 0 < 2) |
| 24 | 23 | a1i 11 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) = 2)
→ (2 ∈ ℝ ∧ 0 < 2)) |
| 25 | | ltmul2 12118 |
. . . . . . . 8
⊢ ((2
∈ ℝ ∧ 𝑁
∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (2 < 𝑁 ↔ (2 · 2) < (2
· 𝑁))) |
| 26 | 1, 21, 24, 25 | mp3an2ani 1470 |
. . . . . . 7
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) = 2)
→ (2 < 𝑁 ↔ (2
· 2) < (2 · 𝑁))) |
| 27 | 20, 26 | mpbid 232 |
. . . . . 6
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) = 2)
→ (2 · 2) < (2 · 𝑁)) |
| 28 | 19, 27 | eqbrtrrid 5179 |
. . . . 5
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) = 2)
→ (3 + 1) < (2 · 𝑁)) |
| 29 | | 3re 12346 |
. . . . . . 7
⊢ 3 ∈
ℝ |
| 30 | 29 | a1i 11 |
. . . . . 6
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) = 2)
→ 3 ∈ ℝ) |
| 31 | | 1red 11262 |
. . . . . 6
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) = 2)
→ 1 ∈ ℝ) |
| 32 | | remulcl 11240 |
. . . . . . . 8
⊢ ((2
∈ ℝ ∧ 𝑁
∈ ℝ) → (2 · 𝑁) ∈ ℝ) |
| 33 | 1, 21, 32 | sylancr 587 |
. . . . . . 7
⊢ ((𝑁 ∈ ℝ ∧ 2 <
𝑁) → (2 · 𝑁) ∈
ℝ) |
| 34 | 33 | adantr 480 |
. . . . . 6
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) = 2)
→ (2 · 𝑁)
∈ ℝ) |
| 35 | 30, 31, 34 | ltaddsub2d 11864 |
. . . . 5
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) = 2)
→ ((3 + 1) < (2 · 𝑁) ↔ 1 < ((2 · 𝑁) − 3))) |
| 36 | 28, 35 | mpbid 232 |
. . . 4
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) = 2)
→ 1 < ((2 · 𝑁) − 3)) |
| 37 | | resubcl 11573 |
. . . . . . 7
⊢ (((2
· 𝑁) ∈ ℝ
∧ 3 ∈ ℝ) → ((2 · 𝑁) − 3) ∈
ℝ) |
| 38 | 33, 29, 37 | sylancl 586 |
. . . . . 6
⊢ ((𝑁 ∈ ℝ ∧ 2 <
𝑁) → ((2 ·
𝑁) − 3) ∈
ℝ) |
| 39 | 38 | adantr 480 |
. . . . 5
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) = 2)
→ ((2 · 𝑁)
− 3) ∈ ℝ) |
| 40 | 6 | a1i 11 |
. . . . 5
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) = 2)
→ ((log‘2) ∈ ℝ ∧ 0 <
(log‘2))) |
| 41 | | ltmul2 12118 |
. . . . 5
⊢ ((1
∈ ℝ ∧ ((2 · 𝑁) − 3) ∈ ℝ ∧
((log‘2) ∈ ℝ ∧ 0 < (log‘2))) → (1 < ((2
· 𝑁) − 3)
↔ ((log‘2) · 1) < ((log‘2) · ((2 ·
𝑁) −
3)))) |
| 42 | 31, 39, 40, 41 | syl3anc 1373 |
. . . 4
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) = 2)
→ (1 < ((2 · 𝑁) − 3) ↔ ((log‘2) ·
1) < ((log‘2) · ((2 · 𝑁) − 3)))) |
| 43 | 36, 42 | mpbid 232 |
. . 3
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) = 2)
→ ((log‘2) · 1) < ((log‘2) · ((2 ·
𝑁) −
3))) |
| 44 | 16, 43 | eqbrtrrd 5167 |
. 2
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) = 2)
→ (θ‘𝑁)
< ((log‘2) · ((2 · 𝑁) − 3))) |
| 45 | | chtcl 27152 |
. . . 4
⊢ (𝑁 ∈ ℝ →
(θ‘𝑁) ∈
ℝ) |
| 46 | 45 | ad2antrr 726 |
. . 3
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → (θ‘𝑁) ∈ ℝ) |
| 47 | | reflcl 13836 |
. . . . . . 7
⊢ (𝑁 ∈ ℝ →
(⌊‘𝑁) ∈
ℝ) |
| 48 | 47 | ad2antrr 726 |
. . . . . 6
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → (⌊‘𝑁) ∈ ℝ) |
| 49 | | remulcl 11240 |
. . . . . 6
⊢ ((2
∈ ℝ ∧ (⌊‘𝑁) ∈ ℝ) → (2 ·
(⌊‘𝑁)) ∈
ℝ) |
| 50 | 1, 48, 49 | sylancr 587 |
. . . . 5
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → (2 · (⌊‘𝑁)) ∈
ℝ) |
| 51 | | resubcl 11573 |
. . . . 5
⊢ (((2
· (⌊‘𝑁))
∈ ℝ ∧ 3 ∈ ℝ) → ((2 · (⌊‘𝑁)) − 3) ∈
ℝ) |
| 52 | 50, 29, 51 | sylancl 586 |
. . . 4
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → ((2 ·
(⌊‘𝑁)) −
3) ∈ ℝ) |
| 53 | | remulcl 11240 |
. . . 4
⊢
(((log‘2) ∈ ℝ ∧ ((2 · (⌊‘𝑁)) − 3) ∈ ℝ)
→ ((log‘2) · ((2 · (⌊‘𝑁)) − 3)) ∈
ℝ) |
| 54 | 7, 52, 53 | sylancr 587 |
. . 3
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → ((log‘2) · ((2
· (⌊‘𝑁))
− 3)) ∈ ℝ) |
| 55 | 38 | adantr 480 |
. . . 4
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → ((2 · 𝑁) − 3) ∈
ℝ) |
| 56 | | remulcl 11240 |
. . . 4
⊢
(((log‘2) ∈ ℝ ∧ ((2 · 𝑁) − 3) ∈ ℝ) →
((log‘2) · ((2 · 𝑁) − 3)) ∈
ℝ) |
| 57 | 7, 55, 56 | sylancr 587 |
. . 3
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → ((log‘2) · ((2
· 𝑁) − 3))
∈ ℝ) |
| 58 | 15 | adantr 480 |
. . . 4
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) →
(θ‘(⌊‘𝑁)) = (θ‘𝑁)) |
| 59 | | simpr 484 |
. . . . . 6
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → (⌊‘𝑁) ∈ (ℤ≥‘(2 +
1))) |
| 60 | | df-3 12330 |
. . . . . . 7
⊢ 3 = (2 +
1) |
| 61 | 60 | fveq2i 6909 |
. . . . . 6
⊢
(ℤ≥‘3) = (ℤ≥‘(2 +
1)) |
| 62 | 59, 61 | eleqtrrdi 2852 |
. . . . 5
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → (⌊‘𝑁) ∈
(ℤ≥‘3)) |
| 63 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑘 = (⌊‘𝑁) → (θ‘𝑘) =
(θ‘(⌊‘𝑁))) |
| 64 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑘 = (⌊‘𝑁) → (2 · 𝑘) = (2 ·
(⌊‘𝑁))) |
| 65 | 64 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝑘 = (⌊‘𝑁) → ((2 · 𝑘) − 3) = ((2 ·
(⌊‘𝑁)) −
3)) |
| 66 | 65 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑘 = (⌊‘𝑁) → ((log‘2) ·
((2 · 𝑘) − 3))
= ((log‘2) · ((2 · (⌊‘𝑁)) − 3))) |
| 67 | 63, 66 | breq12d 5156 |
. . . . . 6
⊢ (𝑘 = (⌊‘𝑁) → ((θ‘𝑘) < ((log‘2) ·
((2 · 𝑘) − 3))
↔ (θ‘(⌊‘𝑁)) < ((log‘2) · ((2 ·
(⌊‘𝑁)) −
3)))) |
| 68 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑥 = 3 → (3...𝑥) = (3...3)) |
| 69 | 68 | raleqdv 3326 |
. . . . . . 7
⊢ (𝑥 = 3 → (∀𝑘 ∈ (3...𝑥)(θ‘𝑘) < ((log‘2) · ((2 ·
𝑘) − 3)) ↔
∀𝑘 ∈
(3...3)(θ‘𝑘)
< ((log‘2) · ((2 · 𝑘) − 3)))) |
| 70 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑥 = 𝑛 → (3...𝑥) = (3...𝑛)) |
| 71 | 70 | raleqdv 3326 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → (∀𝑘 ∈ (3...𝑥)(θ‘𝑘) < ((log‘2) · ((2 ·
𝑘) − 3)) ↔
∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) ·
((2 · 𝑘) −
3)))) |
| 72 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑥 = (𝑛 + 1) → (3...𝑥) = (3...(𝑛 + 1))) |
| 73 | 72 | raleqdv 3326 |
. . . . . . 7
⊢ (𝑥 = (𝑛 + 1) → (∀𝑘 ∈ (3...𝑥)(θ‘𝑘) < ((log‘2) · ((2 ·
𝑘) − 3)) ↔
∀𝑘 ∈
(3...(𝑛 +
1))(θ‘𝑘) <
((log‘2) · ((2 · 𝑘) − 3)))) |
| 74 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑥 = (⌊‘𝑁) → (3...𝑥) = (3...(⌊‘𝑁))) |
| 75 | 74 | raleqdv 3326 |
. . . . . . 7
⊢ (𝑥 = (⌊‘𝑁) → (∀𝑘 ∈ (3...𝑥)(θ‘𝑘) < ((log‘2) · ((2 ·
𝑘) − 3)) ↔
∀𝑘 ∈
(3...(⌊‘𝑁))(θ‘𝑘) < ((log‘2) · ((2 ·
𝑘) −
3)))) |
| 76 | | 6lt8 12459 |
. . . . . . . . . . 11
⊢ 6 <
8 |
| 77 | | 6re 12356 |
. . . . . . . . . . . . 13
⊢ 6 ∈
ℝ |
| 78 | | 6pos 12376 |
. . . . . . . . . . . . 13
⊢ 0 <
6 |
| 79 | 77, 78 | elrpii 13037 |
. . . . . . . . . . . 12
⊢ 6 ∈
ℝ+ |
| 80 | | 8re 12362 |
. . . . . . . . . . . . 13
⊢ 8 ∈
ℝ |
| 81 | | 8pos 12378 |
. . . . . . . . . . . . 13
⊢ 0 <
8 |
| 82 | 80, 81 | elrpii 13037 |
. . . . . . . . . . . 12
⊢ 8 ∈
ℝ+ |
| 83 | | logltb 26642 |
. . . . . . . . . . . 12
⊢ ((6
∈ ℝ+ ∧ 8 ∈ ℝ+) → (6 < 8
↔ (log‘6) < (log‘8))) |
| 84 | 79, 82, 83 | mp2an 692 |
. . . . . . . . . . 11
⊢ (6 < 8
↔ (log‘6) < (log‘8)) |
| 85 | 76, 84 | mpbi 230 |
. . . . . . . . . 10
⊢
(log‘6) < (log‘8) |
| 86 | 85 | a1i 11 |
. . . . . . . . 9
⊢ (𝑘 ∈ (3...3) →
(log‘6) < (log‘8)) |
| 87 | | elfz1eq 13575 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (3...3) → 𝑘 = 3) |
| 88 | 87 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (3...3) →
(θ‘𝑘) =
(θ‘3)) |
| 89 | | cht3 27216 |
. . . . . . . . . 10
⊢
(θ‘3) = (log‘6) |
| 90 | 88, 89 | eqtrdi 2793 |
. . . . . . . . 9
⊢ (𝑘 ∈ (3...3) →
(θ‘𝑘) =
(log‘6)) |
| 91 | 87 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (3...3) → (2
· 𝑘) = (2 ·
3)) |
| 92 | 91 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (3...3) → ((2
· 𝑘) − 3) =
((2 · 3) − 3)) |
| 93 | | 3cn 12347 |
. . . . . . . . . . . . 13
⊢ 3 ∈
ℂ |
| 94 | 93 | 2timesi 12404 |
. . . . . . . . . . . . 13
⊢ (2
· 3) = (3 + 3) |
| 95 | 93, 93, 94 | mvrraddi 11525 |
. . . . . . . . . . . 12
⊢ ((2
· 3) − 3) = 3 |
| 96 | 92, 95 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (3...3) → ((2
· 𝑘) − 3) =
3) |
| 97 | 96 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (3...3) →
((log‘2) · ((2 · 𝑘) − 3)) = ((log‘2) ·
3)) |
| 98 | | 2rp 13039 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℝ+ |
| 99 | | relogcl 26617 |
. . . . . . . . . . . . . . 15
⊢ (2 ∈
ℝ+ → (log‘2) ∈ ℝ) |
| 100 | 98, 99 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
(log‘2) ∈ ℝ |
| 101 | 100 | recni 11275 |
. . . . . . . . . . . . 13
⊢
(log‘2) ∈ ℂ |
| 102 | 101, 93 | mulcomi 11269 |
. . . . . . . . . . . 12
⊢
((log‘2) · 3) = (3 · (log‘2)) |
| 103 | | 3z 12650 |
. . . . . . . . . . . . 13
⊢ 3 ∈
ℤ |
| 104 | | relogexp 26638 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℝ+ ∧ 3 ∈ ℤ) →
(log‘(2↑3)) = (3 · (log‘2))) |
| 105 | 98, 103, 104 | mp2an 692 |
. . . . . . . . . . . 12
⊢
(log‘(2↑3)) = (3 · (log‘2)) |
| 106 | 102, 105 | eqtr4i 2768 |
. . . . . . . . . . 11
⊢
((log‘2) · 3) = (log‘(2↑3)) |
| 107 | | cu2 14239 |
. . . . . . . . . . . 12
⊢
(2↑3) = 8 |
| 108 | 107 | fveq2i 6909 |
. . . . . . . . . . 11
⊢
(log‘(2↑3)) = (log‘8) |
| 109 | 106, 108 | eqtri 2765 |
. . . . . . . . . 10
⊢
((log‘2) · 3) = (log‘8) |
| 110 | 97, 109 | eqtrdi 2793 |
. . . . . . . . 9
⊢ (𝑘 ∈ (3...3) →
((log‘2) · ((2 · 𝑘) − 3)) =
(log‘8)) |
| 111 | 86, 90, 110 | 3brtr4d 5175 |
. . . . . . . 8
⊢ (𝑘 ∈ (3...3) →
(θ‘𝑘) <
((log‘2) · ((2 · 𝑘) − 3))) |
| 112 | 111 | rgen 3063 |
. . . . . . 7
⊢
∀𝑘 ∈
(3...3)(θ‘𝑘)
< ((log‘2) · ((2 · 𝑘) − 3)) |
| 113 | | df-2 12329 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 = (1 +
1) |
| 114 | | 2div2e1 12407 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (2 / 2) =
1 |
| 115 | | eluzle 12891 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈
(ℤ≥‘3) → 3 ≤ 𝑛) |
| 116 | 60, 115 | eqbrtrrid 5179 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 ∈
(ℤ≥‘3) → (2 + 1) ≤ 𝑛) |
| 117 | | 2z 12649 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 2 ∈
ℤ |
| 118 | | eluzelz 12888 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈
(ℤ≥‘3) → 𝑛 ∈ ℤ) |
| 119 | | zltp1le 12667 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((2
∈ ℤ ∧ 𝑛
∈ ℤ) → (2 < 𝑛 ↔ (2 + 1) ≤ 𝑛)) |
| 120 | 117, 118,
119 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 ∈
(ℤ≥‘3) → (2 < 𝑛 ↔ (2 + 1) ≤ 𝑛)) |
| 121 | 116, 120 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈
(ℤ≥‘3) → 2 < 𝑛) |
| 122 | | eluzelre 12889 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 ∈
(ℤ≥‘3) → 𝑛 ∈ ℝ) |
| 123 | | ltdiv1 12132 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((2
∈ ℝ ∧ 𝑛
∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (2 < 𝑛 ↔ (2 / 2) < (𝑛 / 2))) |
| 124 | 1, 23, 123 | mp3an13 1454 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 ∈ ℝ → (2 <
𝑛 ↔ (2 / 2) <
(𝑛 / 2))) |
| 125 | 122, 124 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈
(ℤ≥‘3) → (2 < 𝑛 ↔ (2 / 2) < (𝑛 / 2))) |
| 126 | 121, 125 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈
(ℤ≥‘3) → (2 / 2) < (𝑛 / 2)) |
| 127 | 114, 126 | eqbrtrrid 5179 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈
(ℤ≥‘3) → 1 < (𝑛 / 2)) |
| 128 | 122 | rehalfcld 12513 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈
(ℤ≥‘3) → (𝑛 / 2) ∈ ℝ) |
| 129 | | 1re 11261 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
ℝ |
| 130 | | ltadd1 11730 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((1
∈ ℝ ∧ (𝑛 /
2) ∈ ℝ ∧ 1 ∈ ℝ) → (1 < (𝑛 / 2) ↔ (1 + 1) < ((𝑛 / 2) + 1))) |
| 131 | 129, 129,
130 | mp3an13 1454 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 / 2) ∈ ℝ → (1
< (𝑛 / 2) ↔ (1 + 1)
< ((𝑛 / 2) +
1))) |
| 132 | 128, 131 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈
(ℤ≥‘3) → (1 < (𝑛 / 2) ↔ (1 + 1) < ((𝑛 / 2) + 1))) |
| 133 | 127, 132 | mpbid 232 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈
(ℤ≥‘3) → (1 + 1) < ((𝑛 / 2) + 1)) |
| 134 | 113, 133 | eqbrtrid 5178 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈
(ℤ≥‘3) → 2 < ((𝑛 / 2) + 1)) |
| 135 | 134 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → 2 < ((𝑛 / 2) + 1)) |
| 136 | | peano2z 12658 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 / 2) ∈ ℤ →
((𝑛 / 2) + 1) ∈
ℤ) |
| 137 | 136 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 / 2) + 1) ∈
ℤ) |
| 138 | | zltp1le 12667 |
. . . . . . . . . . . . . . . . 17
⊢ ((2
∈ ℤ ∧ ((𝑛 /
2) + 1) ∈ ℤ) → (2 < ((𝑛 / 2) + 1) ↔ (2 + 1) ≤ ((𝑛 / 2) + 1))) |
| 139 | 117, 137,
138 | sylancr 587 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 < ((𝑛 / 2) + 1) ↔ (2 + 1) ≤
((𝑛 / 2) +
1))) |
| 140 | 135, 139 | mpbid 232 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 + 1) ≤
((𝑛 / 2) +
1)) |
| 141 | 60, 140 | eqbrtrid 5178 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → 3 ≤ ((𝑛 / 2) + 1)) |
| 142 | | 1red 11262 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈
(ℤ≥‘3) → 1 ∈ ℝ) |
| 143 | | ltle 11349 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((1
∈ ℝ ∧ (𝑛 /
2) ∈ ℝ) → (1 < (𝑛 / 2) → 1 ≤ (𝑛 / 2))) |
| 144 | 129, 128,
143 | sylancr 587 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈
(ℤ≥‘3) → (1 < (𝑛 / 2) → 1 ≤ (𝑛 / 2))) |
| 145 | 127, 144 | mpd 15 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈
(ℤ≥‘3) → 1 ≤ (𝑛 / 2)) |
| 146 | 142, 128,
128, 145 | leadd2dd 11878 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈
(ℤ≥‘3) → ((𝑛 / 2) + 1) ≤ ((𝑛 / 2) + (𝑛 / 2))) |
| 147 | 122 | recnd 11289 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈
(ℤ≥‘3) → 𝑛 ∈ ℂ) |
| 148 | 147 | 2halvesd 12512 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈
(ℤ≥‘3) → ((𝑛 / 2) + (𝑛 / 2)) = 𝑛) |
| 149 | 146, 148 | breqtrd 5169 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈
(ℤ≥‘3) → ((𝑛 / 2) + 1) ≤ 𝑛) |
| 150 | 149 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 / 2) + 1) ≤ 𝑛) |
| 151 | | elfz 13553 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑛 / 2) + 1) ∈ ℤ ∧
3 ∈ ℤ ∧ 𝑛
∈ ℤ) → (((𝑛
/ 2) + 1) ∈ (3...𝑛)
↔ (3 ≤ ((𝑛 / 2) +
1) ∧ ((𝑛 / 2) + 1) ≤
𝑛))) |
| 152 | 103, 151 | mp3an2 1451 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑛 / 2) + 1) ∈ ℤ ∧
𝑛 ∈ ℤ) →
(((𝑛 / 2) + 1) ∈
(3...𝑛) ↔ (3 ≤
((𝑛 / 2) + 1) ∧ ((𝑛 / 2) + 1) ≤ 𝑛))) |
| 153 | 136, 118,
152 | syl2anr 597 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (((𝑛 / 2) + 1) ∈ (3...𝑛) ↔ (3 ≤ ((𝑛 / 2) + 1) ∧ ((𝑛 / 2) + 1) ≤ 𝑛))) |
| 154 | 141, 150,
153 | mpbir2and 713 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 / 2) + 1) ∈ (3...𝑛)) |
| 155 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = ((𝑛 / 2) + 1) → (θ‘𝑘) = (θ‘((𝑛 / 2) + 1))) |
| 156 | | oveq2 7439 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = ((𝑛 / 2) + 1) → (2 · 𝑘) = (2 · ((𝑛 / 2) + 1))) |
| 157 | 156 | oveq1d 7446 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = ((𝑛 / 2) + 1) → ((2 · 𝑘) − 3) = ((2 ·
((𝑛 / 2) + 1)) −
3)) |
| 158 | 157 | oveq2d 7447 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = ((𝑛 / 2) + 1) → ((log‘2) · ((2
· 𝑘) − 3)) =
((log‘2) · ((2 · ((𝑛 / 2) + 1)) − 3))) |
| 159 | 155, 158 | breq12d 5156 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = ((𝑛 / 2) + 1) → ((θ‘𝑘) < ((log‘2) ·
((2 · 𝑘) − 3))
↔ (θ‘((𝑛 /
2) + 1)) < ((log‘2) · ((2 · ((𝑛 / 2) + 1)) − 3)))) |
| 160 | 159 | rspcv 3618 |
. . . . . . . . . . . . 13
⊢ (((𝑛 / 2) + 1) ∈ (3...𝑛) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 ·
𝑘) − 3)) →
(θ‘((𝑛 / 2) +
1)) < ((log‘2) · ((2 · ((𝑛 / 2) + 1)) − 3)))) |
| 161 | 154, 160 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 ·
𝑘) − 3)) →
(θ‘((𝑛 / 2) +
1)) < ((log‘2) · ((2 · ((𝑛 / 2) + 1)) − 3)))) |
| 162 | 128 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈
(ℤ≥‘3) → (𝑛 / 2) ∈ ℂ) |
| 163 | 162 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (𝑛 / 2) ∈
ℂ) |
| 164 | | 2cn 12341 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 2 ∈
ℂ |
| 165 | | ax-1cn 11213 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
ℂ |
| 166 | | adddi 11244 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((2
∈ ℂ ∧ (𝑛 /
2) ∈ ℂ ∧ 1 ∈ ℂ) → (2 · ((𝑛 / 2) + 1)) = ((2 ·
(𝑛 / 2)) + (2 ·
1))) |
| 167 | 164, 165,
166 | mp3an13 1454 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 / 2) ∈ ℂ → (2
· ((𝑛 / 2) + 1)) =
((2 · (𝑛 / 2)) + (2
· 1))) |
| 168 | 163, 167 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 ·
((𝑛 / 2) + 1)) = ((2
· (𝑛 / 2)) + (2
· 1))) |
| 169 | 147 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → 𝑛 ∈
ℂ) |
| 170 | | 2ne0 12370 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 ≠
0 |
| 171 | | divcan2 11930 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑛 ∈ ℂ ∧ 2 ∈
ℂ ∧ 2 ≠ 0) → (2 · (𝑛 / 2)) = 𝑛) |
| 172 | 164, 170,
171 | mp3an23 1455 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ ℂ → (2
· (𝑛 / 2)) = 𝑛) |
| 173 | 169, 172 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 ·
(𝑛 / 2)) = 𝑛) |
| 174 | 164 | mulridi 11265 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (2
· 1) = 2 |
| 175 | 174 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 · 1) =
2) |
| 176 | 173, 175 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 ·
(𝑛 / 2)) + (2 · 1))
= (𝑛 + 2)) |
| 177 | 168, 176 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 ·
((𝑛 / 2) + 1)) = (𝑛 + 2)) |
| 178 | 177 | oveq1d 7446 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 ·
((𝑛 / 2) + 1)) − 3) =
((𝑛 + 2) −
3)) |
| 179 | | subsub3 11541 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ ℂ ∧ 3 ∈
ℂ ∧ 2 ∈ ℂ) → (𝑛 − (3 − 2)) = ((𝑛 + 2) −
3)) |
| 180 | 93, 164, 179 | mp3an23 1455 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℂ → (𝑛 − (3 − 2)) =
((𝑛 + 2) −
3)) |
| 181 | 169, 180 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (𝑛 − (3 − 2)) =
((𝑛 + 2) −
3)) |
| 182 | | 2p1e3 12408 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (2 + 1) =
3 |
| 183 | 93, 164, 165, 182 | subaddrii 11598 |
. . . . . . . . . . . . . . . . . . 19
⊢ (3
− 2) = 1 |
| 184 | 183 | oveq2i 7442 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 − (3 − 2)) = (𝑛 − 1) |
| 185 | 181, 184 | eqtr3di 2792 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 + 2) − 3) = (𝑛 − 1)) |
| 186 | 178, 185 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 ·
((𝑛 / 2) + 1)) − 3) =
(𝑛 −
1)) |
| 187 | 186 | oveq2d 7447 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘2)
· ((2 · ((𝑛 /
2) + 1)) − 3)) = ((log‘2) · (𝑛 − 1))) |
| 188 | 187 | breq2d 5155 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) →
((θ‘((𝑛 / 2) +
1)) < ((log‘2) · ((2 · ((𝑛 / 2) + 1)) − 3)) ↔
(θ‘((𝑛 / 2) +
1)) < ((log‘2) · (𝑛 − 1)))) |
| 189 | 137 | zred 12722 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 / 2) + 1) ∈
ℝ) |
| 190 | | chtcl 27152 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑛 / 2) + 1) ∈ ℝ →
(θ‘((𝑛 / 2) +
1)) ∈ ℝ) |
| 191 | 189, 190 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) →
(θ‘((𝑛 / 2) +
1)) ∈ ℝ) |
| 192 | 122 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → 𝑛 ∈
ℝ) |
| 193 | | peano2rem 11576 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℝ → (𝑛 − 1) ∈
ℝ) |
| 194 | 192, 193 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (𝑛 − 1) ∈
ℝ) |
| 195 | | remulcl 11240 |
. . . . . . . . . . . . . . . 16
⊢
(((log‘2) ∈ ℝ ∧ (𝑛 − 1) ∈ ℝ) →
((log‘2) · (𝑛
− 1)) ∈ ℝ) |
| 196 | 100, 194,
195 | sylancr 587 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘2)
· (𝑛 − 1))
∈ ℝ) |
| 197 | | remulcl 11240 |
. . . . . . . . . . . . . . . 16
⊢
(((log‘2) ∈ ℝ ∧ 𝑛 ∈ ℝ) → ((log‘2)
· 𝑛) ∈
ℝ) |
| 198 | 100, 192,
197 | sylancr 587 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘2)
· 𝑛) ∈
ℝ) |
| 199 | 191, 196,
198 | ltadd1d 11856 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) →
((θ‘((𝑛 / 2) +
1)) < ((log‘2) · (𝑛 − 1)) ↔ ((θ‘((𝑛 / 2) + 1)) + ((log‘2)
· 𝑛)) <
(((log‘2) · (𝑛
− 1)) + ((log‘2) · 𝑛)))) |
| 200 | 101 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (log‘2)
∈ ℂ) |
| 201 | 194 | recnd 11289 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (𝑛 − 1) ∈
ℂ) |
| 202 | 200, 201,
169 | adddid 11285 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘2)
· ((𝑛 − 1) +
𝑛)) = (((log‘2)
· (𝑛 − 1)) +
((log‘2) · 𝑛))) |
| 203 | | adddi 11244 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((2
∈ ℂ ∧ 𝑛
∈ ℂ ∧ 1 ∈ ℂ) → (2 · (𝑛 + 1)) = ((2 · 𝑛) + (2 · 1))) |
| 204 | 164, 165,
203 | mp3an13 1454 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ ℂ → (2
· (𝑛 + 1)) = ((2
· 𝑛) + (2 ·
1))) |
| 205 | 169, 204 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 ·
(𝑛 + 1)) = ((2 ·
𝑛) + (2 ·
1))) |
| 206 | 174 | oveq2i 7442 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((2
· 𝑛) + (2 ·
1)) = ((2 · 𝑛) +
2) |
| 207 | 205, 206 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 ·
(𝑛 + 1)) = ((2 ·
𝑛) + 2)) |
| 208 | 207 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 ·
(𝑛 + 1)) − 3) = (((2
· 𝑛) + 2) −
3)) |
| 209 | | zmulcl 12666 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((2
∈ ℤ ∧ 𝑛
∈ ℤ) → (2 · 𝑛) ∈ ℤ) |
| 210 | 117, 118,
209 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈
(ℤ≥‘3) → (2 · 𝑛) ∈ ℤ) |
| 211 | 210 | zcnd 12723 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈
(ℤ≥‘3) → (2 · 𝑛) ∈ ℂ) |
| 212 | 211 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 ·
𝑛) ∈
ℂ) |
| 213 | | subsub3 11541 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((2
· 𝑛) ∈ ℂ
∧ 3 ∈ ℂ ∧ 2 ∈ ℂ) → ((2 · 𝑛) − (3 − 2)) = (((2
· 𝑛) + 2) −
3)) |
| 214 | 93, 164, 213 | mp3an23 1455 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((2
· 𝑛) ∈ ℂ
→ ((2 · 𝑛)
− (3 − 2)) = (((2 · 𝑛) + 2) − 3)) |
| 215 | 212, 214 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 ·
𝑛) − (3 − 2)) =
(((2 · 𝑛) + 2)
− 3)) |
| 216 | 183 | oveq2i 7442 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((2
· 𝑛) − (3
− 2)) = ((2 · 𝑛) − 1) |
| 217 | 169 | 2timesd 12509 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 ·
𝑛) = (𝑛 + 𝑛)) |
| 218 | 217 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 ·
𝑛) − 1) = ((𝑛 + 𝑛) − 1)) |
| 219 | 165 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → 1 ∈
ℂ) |
| 220 | 169, 169,
219 | addsubd 11641 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 + 𝑛) − 1) = ((𝑛 − 1) + 𝑛)) |
| 221 | 218, 220 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 ·
𝑛) − 1) = ((𝑛 − 1) + 𝑛)) |
| 222 | 216, 221 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 ·
𝑛) − (3 − 2)) =
((𝑛 − 1) + 𝑛)) |
| 223 | 208, 215,
222 | 3eqtr2rd 2784 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 − 1) + 𝑛) = ((2 · (𝑛 + 1)) − 3)) |
| 224 | 223 | oveq2d 7447 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘2)
· ((𝑛 − 1) +
𝑛)) = ((log‘2)
· ((2 · (𝑛 +
1)) − 3))) |
| 225 | 202, 224 | eqtr3d 2779 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (((log‘2)
· (𝑛 − 1)) +
((log‘2) · 𝑛))
= ((log‘2) · ((2 · (𝑛 + 1)) − 3))) |
| 226 | 225 | breq2d 5155 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) →
(((θ‘((𝑛 / 2) +
1)) + ((log‘2) · 𝑛)) < (((log‘2) · (𝑛 − 1)) + ((log‘2)
· 𝑛)) ↔
((θ‘((𝑛 / 2) +
1)) + ((log‘2) · 𝑛)) < ((log‘2) · ((2 ·
(𝑛 + 1)) −
3)))) |
| 227 | 188, 199,
226 | 3bitrd 305 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) →
((θ‘((𝑛 / 2) +
1)) < ((log‘2) · ((2 · ((𝑛 / 2) + 1)) − 3)) ↔
((θ‘((𝑛 / 2) +
1)) + ((log‘2) · 𝑛)) < ((log‘2) · ((2 ·
(𝑛 + 1)) −
3)))) |
| 228 | | 3nn 12345 |
. . . . . . . . . . . . . . . . 17
⊢ 3 ∈
ℕ |
| 229 | | elfzuz 13560 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑛 / 2) + 1) ∈ (3...𝑛) → ((𝑛 / 2) + 1) ∈
(ℤ≥‘3)) |
| 230 | 154, 229 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 / 2) + 1) ∈
(ℤ≥‘3)) |
| 231 | | eluznn 12960 |
. . . . . . . . . . . . . . . . 17
⊢ ((3
∈ ℕ ∧ ((𝑛 /
2) + 1) ∈ (ℤ≥‘3)) → ((𝑛 / 2) + 1) ∈ ℕ) |
| 232 | 228, 230,
231 | sylancr 587 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 / 2) + 1) ∈
ℕ) |
| 233 | | chtublem 27255 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑛 / 2) + 1) ∈ ℕ →
(θ‘((2 · ((𝑛 / 2) + 1)) − 1)) ≤
((θ‘((𝑛 / 2) +
1)) + ((log‘4) · (((𝑛 / 2) + 1) − 1)))) |
| 234 | 232, 233 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) →
(θ‘((2 · ((𝑛 / 2) + 1)) − 1)) ≤
((θ‘((𝑛 / 2) +
1)) + ((log‘4) · (((𝑛 / 2) + 1) − 1)))) |
| 235 | 177 | oveq1d 7446 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 ·
((𝑛 / 2) + 1)) − 1) =
((𝑛 + 2) −
1)) |
| 236 | | addsubass 11518 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ ℂ ∧ 2 ∈
ℂ ∧ 1 ∈ ℂ) → ((𝑛 + 2) − 1) = (𝑛 + (2 − 1))) |
| 237 | 164, 165,
236 | mp3an23 1455 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℂ → ((𝑛 + 2) − 1) = (𝑛 + (2 −
1))) |
| 238 | 169, 237 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 + 2) − 1) = (𝑛 + (2 −
1))) |
| 239 | | 2m1e1 12392 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2
− 1) = 1 |
| 240 | 239 | oveq2i 7442 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 + (2 − 1)) = (𝑛 + 1) |
| 241 | 238, 240 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 + 2) − 1) = (𝑛 + 1)) |
| 242 | 235, 241 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 ·
((𝑛 / 2) + 1)) − 1) =
(𝑛 + 1)) |
| 243 | 242 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) →
(θ‘((2 · ((𝑛 / 2) + 1)) − 1)) =
(θ‘(𝑛 +
1))) |
| 244 | | pncan 11514 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 / 2) ∈ ℂ ∧ 1
∈ ℂ) → (((𝑛
/ 2) + 1) − 1) = (𝑛 /
2)) |
| 245 | 163, 165,
244 | sylancl 586 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (((𝑛 / 2) + 1) − 1) = (𝑛 / 2)) |
| 246 | 245 | oveq2d 7447 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘4)
· (((𝑛 / 2) + 1)
− 1)) = ((log‘4) · (𝑛 / 2))) |
| 247 | | relogexp 26638 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((2
∈ ℝ+ ∧ 2 ∈ ℤ) →
(log‘(2↑2)) = (2 · (log‘2))) |
| 248 | 98, 117, 247 | mp2an 692 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(log‘(2↑2)) = (2 · (log‘2)) |
| 249 | | sq2 14236 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(2↑2) = 4 |
| 250 | 249 | fveq2i 6909 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(log‘(2↑2)) = (log‘4) |
| 251 | 164, 101 | mulcomi 11269 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (2
· (log‘2)) = ((log‘2) · 2) |
| 252 | 248, 250,
251 | 3eqtr3i 2773 |
. . . . . . . . . . . . . . . . . . 19
⊢
(log‘4) = ((log‘2) · 2) |
| 253 | 252 | oveq1i 7441 |
. . . . . . . . . . . . . . . . . 18
⊢
((log‘4) · (𝑛 / 2)) = (((log‘2) · 2) ·
(𝑛 / 2)) |
| 254 | 164 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → 2 ∈
ℂ) |
| 255 | 200, 254,
163 | mulassd 11284 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (((log‘2)
· 2) · (𝑛 /
2)) = ((log‘2) · (2 · (𝑛 / 2)))) |
| 256 | 253, 255 | eqtrid 2789 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘4)
· (𝑛 / 2)) =
((log‘2) · (2 · (𝑛 / 2)))) |
| 257 | 173 | oveq2d 7447 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘2)
· (2 · (𝑛 /
2))) = ((log‘2) · 𝑛)) |
| 258 | 246, 256,
257 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘4)
· (((𝑛 / 2) + 1)
− 1)) = ((log‘2) · 𝑛)) |
| 259 | 258 | oveq2d 7447 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) →
((θ‘((𝑛 / 2) +
1)) + ((log‘4) · (((𝑛 / 2) + 1) − 1))) =
((θ‘((𝑛 / 2) +
1)) + ((log‘2) · 𝑛))) |
| 260 | 234, 243,
259 | 3brtr3d 5174 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) →
(θ‘(𝑛 + 1))
≤ ((θ‘((𝑛 /
2) + 1)) + ((log‘2) · 𝑛))) |
| 261 | | peano2uz 12943 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈
(ℤ≥‘3) → (𝑛 + 1) ∈
(ℤ≥‘3)) |
| 262 | | eluzelz 12888 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 + 1) ∈
(ℤ≥‘3) → (𝑛 + 1) ∈ ℤ) |
| 263 | 261, 262 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈
(ℤ≥‘3) → (𝑛 + 1) ∈ ℤ) |
| 264 | 263 | zred 12722 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈
(ℤ≥‘3) → (𝑛 + 1) ∈ ℝ) |
| 265 | 264 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (𝑛 + 1) ∈
ℝ) |
| 266 | | chtcl 27152 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 + 1) ∈ ℝ →
(θ‘(𝑛 + 1))
∈ ℝ) |
| 267 | 265, 266 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) →
(θ‘(𝑛 + 1))
∈ ℝ) |
| 268 | 191, 198 | readdcld 11290 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) →
((θ‘((𝑛 / 2) +
1)) + ((log‘2) · 𝑛)) ∈ ℝ) |
| 269 | | zmulcl 12666 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((2
∈ ℤ ∧ (𝑛 +
1) ∈ ℤ) → (2 · (𝑛 + 1)) ∈ ℤ) |
| 270 | 117, 263,
269 | sylancr 587 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈
(ℤ≥‘3) → (2 · (𝑛 + 1)) ∈ ℤ) |
| 271 | 270 | zred 12722 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈
(ℤ≥‘3) → (2 · (𝑛 + 1)) ∈ ℝ) |
| 272 | | resubcl 11573 |
. . . . . . . . . . . . . . . . . 18
⊢ (((2
· (𝑛 + 1)) ∈
ℝ ∧ 3 ∈ ℝ) → ((2 · (𝑛 + 1)) − 3) ∈
ℝ) |
| 273 | 271, 29, 272 | sylancl 586 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈
(ℤ≥‘3) → ((2 · (𝑛 + 1)) − 3) ∈
ℝ) |
| 274 | 273 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 ·
(𝑛 + 1)) − 3) ∈
ℝ) |
| 275 | | remulcl 11240 |
. . . . . . . . . . . . . . . 16
⊢
(((log‘2) ∈ ℝ ∧ ((2 · (𝑛 + 1)) − 3) ∈ ℝ) →
((log‘2) · ((2 · (𝑛 + 1)) − 3)) ∈
ℝ) |
| 276 | 100, 274,
275 | sylancr 587 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘2)
· ((2 · (𝑛 +
1)) − 3)) ∈ ℝ) |
| 277 | | lelttr 11351 |
. . . . . . . . . . . . . . 15
⊢
(((θ‘(𝑛
+ 1)) ∈ ℝ ∧ ((θ‘((𝑛 / 2) + 1)) + ((log‘2) · 𝑛)) ∈ ℝ ∧
((log‘2) · ((2 · (𝑛 + 1)) − 3)) ∈ ℝ) →
(((θ‘(𝑛 + 1))
≤ ((θ‘((𝑛 /
2) + 1)) + ((log‘2) · 𝑛)) ∧ ((θ‘((𝑛 / 2) + 1)) + ((log‘2) · 𝑛)) < ((log‘2) ·
((2 · (𝑛 + 1))
− 3))) → (θ‘(𝑛 + 1)) < ((log‘2) · ((2
· (𝑛 + 1)) −
3)))) |
| 278 | 267, 268,
276, 277 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) →
(((θ‘(𝑛 + 1))
≤ ((θ‘((𝑛 /
2) + 1)) + ((log‘2) · 𝑛)) ∧ ((θ‘((𝑛 / 2) + 1)) + ((log‘2) · 𝑛)) < ((log‘2) ·
((2 · (𝑛 + 1))
− 3))) → (θ‘(𝑛 + 1)) < ((log‘2) · ((2
· (𝑛 + 1)) −
3)))) |
| 279 | 260, 278 | mpand 695 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) →
(((θ‘((𝑛 / 2) +
1)) + ((log‘2) · 𝑛)) < ((log‘2) · ((2 ·
(𝑛 + 1)) − 3)) →
(θ‘(𝑛 + 1))
< ((log‘2) · ((2 · (𝑛 + 1)) − 3)))) |
| 280 | 227, 279 | sylbid 240 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) →
((θ‘((𝑛 / 2) +
1)) < ((log‘2) · ((2 · ((𝑛 / 2) + 1)) − 3)) →
(θ‘(𝑛 + 1))
< ((log‘2) · ((2 · (𝑛 + 1)) − 3)))) |
| 281 | 161, 280 | syld 47 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 ·
𝑘) − 3)) →
(θ‘(𝑛 + 1))
< ((log‘2) · ((2 · (𝑛 + 1)) − 3)))) |
| 282 | | eluzfz2 13572 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈
(ℤ≥‘3) → 𝑛 ∈ (3...𝑛)) |
| 283 | | fveq2 6906 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑛 → (θ‘𝑘) = (θ‘𝑛)) |
| 284 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑛 → (2 · 𝑘) = (2 · 𝑛)) |
| 285 | 284 | oveq1d 7446 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑛 → ((2 · 𝑘) − 3) = ((2 · 𝑛) − 3)) |
| 286 | 285 | oveq2d 7447 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑛 → ((log‘2) · ((2 ·
𝑘) − 3)) =
((log‘2) · ((2 · 𝑛) − 3))) |
| 287 | 283, 286 | breq12d 5156 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑛 → ((θ‘𝑘) < ((log‘2) · ((2 ·
𝑘) − 3)) ↔
(θ‘𝑛) <
((log‘2) · ((2 · 𝑛) − 3)))) |
| 288 | 287 | rspcv 3618 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ (3...𝑛) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 ·
𝑘) − 3)) →
(θ‘𝑛) <
((log‘2) · ((2 · 𝑛) − 3)))) |
| 289 | 282, 288 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈
(ℤ≥‘3) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 ·
𝑘) − 3)) →
(θ‘𝑛) <
((log‘2) · ((2 · 𝑛) − 3)))) |
| 290 | 289 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ ((𝑛 + 1) / 2) ∈ ℤ) →
(∀𝑘 ∈
(3...𝑛)(θ‘𝑘) < ((log‘2) ·
((2 · 𝑘) − 3))
→ (θ‘𝑛)
< ((log‘2) · ((2 · 𝑛) − 3)))) |
| 291 | 210 | zred 12722 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈
(ℤ≥‘3) → (2 · 𝑛) ∈ ℝ) |
| 292 | 29 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈
(ℤ≥‘3) → 3 ∈ ℝ) |
| 293 | 122 | ltp1d 12198 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈
(ℤ≥‘3) → 𝑛 < (𝑛 + 1)) |
| 294 | 23 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈
(ℤ≥‘3) → (2 ∈ ℝ ∧ 0 <
2)) |
| 295 | | ltmul2 12118 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈ ℝ ∧ (𝑛 + 1) ∈ ℝ ∧ (2
∈ ℝ ∧ 0 < 2)) → (𝑛 < (𝑛 + 1) ↔ (2 · 𝑛) < (2 · (𝑛 + 1)))) |
| 296 | 122, 264,
294, 295 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈
(ℤ≥‘3) → (𝑛 < (𝑛 + 1) ↔ (2 · 𝑛) < (2 · (𝑛 + 1)))) |
| 297 | 293, 296 | mpbid 232 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈
(ℤ≥‘3) → (2 · 𝑛) < (2 · (𝑛 + 1))) |
| 298 | 291, 271,
292, 297 | ltsub1dd 11875 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈
(ℤ≥‘3) → ((2 · 𝑛) − 3) < ((2 · (𝑛 + 1)) −
3)) |
| 299 | | resubcl 11573 |
. . . . . . . . . . . . . . . . . 18
⊢ (((2
· 𝑛) ∈ ℝ
∧ 3 ∈ ℝ) → ((2 · 𝑛) − 3) ∈ ℝ) |
| 300 | 291, 29, 299 | sylancl 586 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈
(ℤ≥‘3) → ((2 · 𝑛) − 3) ∈ ℝ) |
| 301 | 6 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈
(ℤ≥‘3) → ((log‘2) ∈ ℝ ∧ 0
< (log‘2))) |
| 302 | | ltmul2 12118 |
. . . . . . . . . . . . . . . . 17
⊢ ((((2
· 𝑛) − 3)
∈ ℝ ∧ ((2 · (𝑛 + 1)) − 3) ∈ ℝ ∧
((log‘2) ∈ ℝ ∧ 0 < (log‘2))) → (((2 ·
𝑛) − 3) < ((2
· (𝑛 + 1)) −
3) ↔ ((log‘2) · ((2 · 𝑛) − 3)) < ((log‘2) ·
((2 · (𝑛 + 1))
− 3)))) |
| 303 | 300, 273,
301, 302 | syl3anc 1373 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈
(ℤ≥‘3) → (((2 · 𝑛) − 3) < ((2 · (𝑛 + 1)) − 3) ↔
((log‘2) · ((2 · 𝑛) − 3)) < ((log‘2) ·
((2 · (𝑛 + 1))
− 3)))) |
| 304 | 298, 303 | mpbid 232 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈
(ℤ≥‘3) → ((log‘2) · ((2 ·
𝑛) − 3)) <
((log‘2) · ((2 · (𝑛 + 1)) − 3))) |
| 305 | | chtcl 27152 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℝ →
(θ‘𝑛) ∈
ℝ) |
| 306 | 122, 305 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈
(ℤ≥‘3) → (θ‘𝑛) ∈ ℝ) |
| 307 | | remulcl 11240 |
. . . . . . . . . . . . . . . . 17
⊢
(((log‘2) ∈ ℝ ∧ ((2 · 𝑛) − 3) ∈ ℝ) →
((log‘2) · ((2 · 𝑛) − 3)) ∈
ℝ) |
| 308 | 100, 300,
307 | sylancr 587 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈
(ℤ≥‘3) → ((log‘2) · ((2 ·
𝑛) − 3)) ∈
ℝ) |
| 309 | 100, 273,
275 | sylancr 587 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈
(ℤ≥‘3) → ((log‘2) · ((2 ·
(𝑛 + 1)) − 3)) ∈
ℝ) |
| 310 | | lttr 11337 |
. . . . . . . . . . . . . . . 16
⊢
(((θ‘𝑛)
∈ ℝ ∧ ((log‘2) · ((2 · 𝑛) − 3)) ∈ ℝ ∧
((log‘2) · ((2 · (𝑛 + 1)) − 3)) ∈ ℝ) →
(((θ‘𝑛) <
((log‘2) · ((2 · 𝑛) − 3)) ∧ ((log‘2) ·
((2 · 𝑛) − 3))
< ((log‘2) · ((2 · (𝑛 + 1)) − 3))) →
(θ‘𝑛) <
((log‘2) · ((2 · (𝑛 + 1)) − 3)))) |
| 311 | 306, 308,
309, 310 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈
(ℤ≥‘3) → (((θ‘𝑛) < ((log‘2) · ((2 ·
𝑛) − 3)) ∧
((log‘2) · ((2 · 𝑛) − 3)) < ((log‘2) ·
((2 · (𝑛 + 1))
− 3))) → (θ‘𝑛) < ((log‘2) · ((2 ·
(𝑛 + 1)) −
3)))) |
| 312 | 304, 311 | mpan2d 694 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈
(ℤ≥‘3) → ((θ‘𝑛) < ((log‘2) · ((2 ·
𝑛) − 3)) →
(θ‘𝑛) <
((log‘2) · ((2 · (𝑛 + 1)) − 3)))) |
| 313 | 312 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ ((𝑛 + 1) / 2) ∈ ℤ) →
((θ‘𝑛) <
((log‘2) · ((2 · 𝑛) − 3)) → (θ‘𝑛) < ((log‘2) ·
((2 · (𝑛 + 1))
− 3)))) |
| 314 | | evend2 16394 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 + 1) ∈ ℤ → (2
∥ (𝑛 + 1) ↔
((𝑛 + 1) / 2) ∈
ℤ)) |
| 315 | 263, 314 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈
(ℤ≥‘3) → (2 ∥ (𝑛 + 1) ↔ ((𝑛 + 1) / 2) ∈ ℤ)) |
| 316 | | 2lt3 12438 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 2 <
3 |
| 317 | 1, 29 | ltnlei 11382 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (2 < 3
↔ ¬ 3 ≤ 2) |
| 318 | 316, 317 | mpbi 230 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ¬ 3
≤ 2 |
| 319 | | breq2 5147 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (2 =
(𝑛 + 1) → (3 ≤ 2
↔ 3 ≤ (𝑛 +
1))) |
| 320 | 318, 319 | mtbii 326 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (2 =
(𝑛 + 1) → ¬ 3 ≤
(𝑛 + 1)) |
| 321 | | eluzle 12891 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑛 + 1) ∈
(ℤ≥‘3) → 3 ≤ (𝑛 + 1)) |
| 322 | 261, 321 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 ∈
(ℤ≥‘3) → 3 ≤ (𝑛 + 1)) |
| 323 | 320, 322 | nsyl3 138 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈
(ℤ≥‘3) → ¬ 2 = (𝑛 + 1)) |
| 324 | 323 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 + 1) ∈ ℙ) → ¬ 2 = (𝑛 + 1)) |
| 325 | | uzid 12893 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (2 ∈
ℤ → 2 ∈ (ℤ≥‘2)) |
| 326 | 117, 325 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 2 ∈
(ℤ≥‘2) |
| 327 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 + 1) ∈ ℙ) → (𝑛 + 1) ∈
ℙ) |
| 328 | | dvdsprm 16740 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((2
∈ (ℤ≥‘2) ∧ (𝑛 + 1) ∈ ℙ) → (2 ∥
(𝑛 + 1) ↔ 2 = (𝑛 + 1))) |
| 329 | 326, 327,
328 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 + 1) ∈ ℙ) → (2 ∥
(𝑛 + 1) ↔ 2 = (𝑛 + 1))) |
| 330 | 324, 329 | mtbird 325 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 + 1) ∈ ℙ) → ¬ 2 ∥
(𝑛 + 1)) |
| 331 | 330 | ex 412 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈
(ℤ≥‘3) → ((𝑛 + 1) ∈ ℙ → ¬ 2 ∥
(𝑛 + 1))) |
| 332 | 331 | con2d 134 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈
(ℤ≥‘3) → (2 ∥ (𝑛 + 1) → ¬ (𝑛 + 1) ∈ ℙ)) |
| 333 | 315, 332 | sylbird 260 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈
(ℤ≥‘3) → (((𝑛 + 1) / 2) ∈ ℤ → ¬ (𝑛 + 1) ∈
ℙ)) |
| 334 | 333 | imp 406 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ ((𝑛 + 1) / 2) ∈ ℤ) → ¬
(𝑛 + 1) ∈
ℙ) |
| 335 | | chtnprm 27197 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ ℤ ∧ ¬
(𝑛 + 1) ∈ ℙ)
→ (θ‘(𝑛 +
1)) = (θ‘𝑛)) |
| 336 | 118, 334,
335 | syl2an2r 685 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ ((𝑛 + 1) / 2) ∈ ℤ) →
(θ‘(𝑛 + 1)) =
(θ‘𝑛)) |
| 337 | 336 | breq1d 5153 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ ((𝑛 + 1) / 2) ∈ ℤ) →
((θ‘(𝑛 + 1))
< ((log‘2) · ((2 · (𝑛 + 1)) − 3)) ↔
(θ‘𝑛) <
((log‘2) · ((2 · (𝑛 + 1)) − 3)))) |
| 338 | 313, 337 | sylibrd 259 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ ((𝑛 + 1) / 2) ∈ ℤ) →
((θ‘𝑛) <
((log‘2) · ((2 · 𝑛) − 3)) → (θ‘(𝑛 + 1)) < ((log‘2)
· ((2 · (𝑛 +
1)) − 3)))) |
| 339 | 290, 338 | syld 47 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ ((𝑛 + 1) / 2) ∈ ℤ) →
(∀𝑘 ∈
(3...𝑛)(θ‘𝑘) < ((log‘2) ·
((2 · 𝑘) − 3))
→ (θ‘(𝑛 +
1)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3)))) |
| 340 | | zeo 12704 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℤ → ((𝑛 / 2) ∈ ℤ ∨
((𝑛 + 1) / 2) ∈
ℤ)) |
| 341 | 118, 340 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑛 ∈
(ℤ≥‘3) → ((𝑛 / 2) ∈ ℤ ∨ ((𝑛 + 1) / 2) ∈
ℤ)) |
| 342 | 281, 339,
341 | mpjaodan 961 |
. . . . . . . . . 10
⊢ (𝑛 ∈
(ℤ≥‘3) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 ·
𝑘) − 3)) →
(θ‘(𝑛 + 1))
< ((log‘2) · ((2 · (𝑛 + 1)) − 3)))) |
| 343 | | ovex 7464 |
. . . . . . . . . . 11
⊢ (𝑛 + 1) ∈ V |
| 344 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑘 = (𝑛 + 1) → (θ‘𝑘) = (θ‘(𝑛 + 1))) |
| 345 | | oveq2 7439 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (𝑛 + 1) → (2 · 𝑘) = (2 · (𝑛 + 1))) |
| 346 | 345 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (𝑛 + 1) → ((2 · 𝑘) − 3) = ((2 · (𝑛 + 1)) −
3)) |
| 347 | 346 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (𝑘 = (𝑛 + 1) → ((log‘2) · ((2
· 𝑘) − 3)) =
((log‘2) · ((2 · (𝑛 + 1)) − 3))) |
| 348 | 344, 347 | breq12d 5156 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝑛 + 1) → ((θ‘𝑘) < ((log‘2) ·
((2 · 𝑘) − 3))
↔ (θ‘(𝑛 +
1)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3)))) |
| 349 | 343, 348 | ralsn 4681 |
. . . . . . . . . 10
⊢
(∀𝑘 ∈
{(𝑛 + 1)}
(θ‘𝑘) <
((log‘2) · ((2 · 𝑘) − 3)) ↔ (θ‘(𝑛 + 1)) < ((log‘2)
· ((2 · (𝑛 +
1)) − 3))) |
| 350 | 342, 349 | imbitrrdi 252 |
. . . . . . . . 9
⊢ (𝑛 ∈
(ℤ≥‘3) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 ·
𝑘) − 3)) →
∀𝑘 ∈ {(𝑛 + 1)} (θ‘𝑘) < ((log‘2) ·
((2 · 𝑘) −
3)))) |
| 351 | 350 | ancld 550 |
. . . . . . . 8
⊢ (𝑛 ∈
(ℤ≥‘3) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 ·
𝑘) − 3)) →
(∀𝑘 ∈
(3...𝑛)(θ‘𝑘) < ((log‘2) ·
((2 · 𝑘) − 3))
∧ ∀𝑘 ∈
{(𝑛 + 1)}
(θ‘𝑘) <
((log‘2) · ((2 · 𝑘) − 3))))) |
| 352 | | ralun 4198 |
. . . . . . . . 9
⊢
((∀𝑘 ∈
(3...𝑛)(θ‘𝑘) < ((log‘2) ·
((2 · 𝑘) − 3))
∧ ∀𝑘 ∈
{(𝑛 + 1)}
(θ‘𝑘) <
((log‘2) · ((2 · 𝑘) − 3))) → ∀𝑘 ∈ ((3...𝑛) ∪ {(𝑛 + 1)})(θ‘𝑘) < ((log‘2) · ((2 ·
𝑘) −
3))) |
| 353 | | fzsuc 13611 |
. . . . . . . . . 10
⊢ (𝑛 ∈
(ℤ≥‘3) → (3...(𝑛 + 1)) = ((3...𝑛) ∪ {(𝑛 + 1)})) |
| 354 | 353 | raleqdv 3326 |
. . . . . . . . 9
⊢ (𝑛 ∈
(ℤ≥‘3) → (∀𝑘 ∈ (3...(𝑛 + 1))(θ‘𝑘) < ((log‘2) · ((2 ·
𝑘) − 3)) ↔
∀𝑘 ∈
((3...𝑛) ∪ {(𝑛 + 1)})(θ‘𝑘) < ((log‘2) ·
((2 · 𝑘) −
3)))) |
| 355 | 352, 354 | imbitrrid 246 |
. . . . . . . 8
⊢ (𝑛 ∈
(ℤ≥‘3) → ((∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 ·
𝑘) − 3)) ∧
∀𝑘 ∈ {(𝑛 + 1)} (θ‘𝑘) < ((log‘2) ·
((2 · 𝑘) −
3))) → ∀𝑘
∈ (3...(𝑛 +
1))(θ‘𝑘) <
((log‘2) · ((2 · 𝑘) − 3)))) |
| 356 | 351, 355 | syld 47 |
. . . . . . 7
⊢ (𝑛 ∈
(ℤ≥‘3) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 ·
𝑘) − 3)) →
∀𝑘 ∈
(3...(𝑛 +
1))(θ‘𝑘) <
((log‘2) · ((2 · 𝑘) − 3)))) |
| 357 | 69, 71, 73, 75, 112, 356 | uzind4i 12952 |
. . . . . 6
⊢
((⌊‘𝑁)
∈ (ℤ≥‘3) → ∀𝑘 ∈ (3...(⌊‘𝑁))(θ‘𝑘) < ((log‘2) · ((2 ·
𝑘) −
3))) |
| 358 | | eluzfz2 13572 |
. . . . . 6
⊢
((⌊‘𝑁)
∈ (ℤ≥‘3) → (⌊‘𝑁) ∈ (3...(⌊‘𝑁))) |
| 359 | 67, 357, 358 | rspcdva 3623 |
. . . . 5
⊢
((⌊‘𝑁)
∈ (ℤ≥‘3) →
(θ‘(⌊‘𝑁)) < ((log‘2) · ((2 ·
(⌊‘𝑁)) −
3))) |
| 360 | 62, 359 | syl 17 |
. . . 4
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) →
(θ‘(⌊‘𝑁)) < ((log‘2) · ((2 ·
(⌊‘𝑁)) −
3))) |
| 361 | 58, 360 | eqbrtrrd 5167 |
. . 3
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → (θ‘𝑁) < ((log‘2) · ((2 ·
(⌊‘𝑁)) −
3))) |
| 362 | 33 | adantr 480 |
. . . . 5
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → (2 · 𝑁) ∈ ℝ) |
| 363 | 29 | a1i 11 |
. . . . 5
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → 3 ∈
ℝ) |
| 364 | | flle 13839 |
. . . . . . 7
⊢ (𝑁 ∈ ℝ →
(⌊‘𝑁) ≤
𝑁) |
| 365 | 364 | ad2antrr 726 |
. . . . . 6
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → (⌊‘𝑁) ≤ 𝑁) |
| 366 | 21 | adantr 480 |
. . . . . . 7
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → 𝑁 ∈ ℝ) |
| 367 | 23 | a1i 11 |
. . . . . . 7
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → (2 ∈ ℝ ∧ 0 <
2)) |
| 368 | | lemul2 12120 |
. . . . . . 7
⊢
(((⌊‘𝑁)
∈ ℝ ∧ 𝑁
∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) →
((⌊‘𝑁) ≤
𝑁 ↔ (2 ·
(⌊‘𝑁)) ≤ (2
· 𝑁))) |
| 369 | 48, 366, 367, 368 | syl3anc 1373 |
. . . . . 6
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → ((⌊‘𝑁) ≤ 𝑁 ↔ (2 · (⌊‘𝑁)) ≤ (2 · 𝑁))) |
| 370 | 365, 369 | mpbid 232 |
. . . . 5
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → (2 · (⌊‘𝑁)) ≤ (2 · 𝑁)) |
| 371 | 50, 362, 363, 370 | lesub1dd 11879 |
. . . 4
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → ((2 ·
(⌊‘𝑁)) −
3) ≤ ((2 · 𝑁)
− 3)) |
| 372 | 6 | a1i 11 |
. . . . 5
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → ((log‘2) ∈ ℝ
∧ 0 < (log‘2))) |
| 373 | | lemul2 12120 |
. . . . 5
⊢ ((((2
· (⌊‘𝑁))
− 3) ∈ ℝ ∧ ((2 · 𝑁) − 3) ∈ ℝ ∧
((log‘2) ∈ ℝ ∧ 0 < (log‘2))) → (((2 ·
(⌊‘𝑁)) −
3) ≤ ((2 · 𝑁)
− 3) ↔ ((log‘2) · ((2 · (⌊‘𝑁)) − 3)) ≤
((log‘2) · ((2 · 𝑁) − 3)))) |
| 374 | 52, 55, 372, 373 | syl3anc 1373 |
. . . 4
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → (((2 ·
(⌊‘𝑁)) −
3) ≤ ((2 · 𝑁)
− 3) ↔ ((log‘2) · ((2 · (⌊‘𝑁)) − 3)) ≤
((log‘2) · ((2 · 𝑁) − 3)))) |
| 375 | 371, 374 | mpbid 232 |
. . 3
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → ((log‘2) · ((2
· (⌊‘𝑁))
− 3)) ≤ ((log‘2) · ((2 · 𝑁) − 3))) |
| 376 | 46, 54, 57, 361, 375 | ltletrd 11421 |
. 2
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → (θ‘𝑁) < ((log‘2) · ((2 ·
𝑁) −
3))) |
| 377 | 117 | a1i 11 |
. . . 4
⊢ ((𝑁 ∈ ℝ ∧ 2 <
𝑁) → 2 ∈
ℤ) |
| 378 | | flcl 13835 |
. . . . 5
⊢ (𝑁 ∈ ℝ →
(⌊‘𝑁) ∈
ℤ) |
| 379 | 378 | adantr 480 |
. . . 4
⊢ ((𝑁 ∈ ℝ ∧ 2 <
𝑁) →
(⌊‘𝑁) ∈
ℤ) |
| 380 | | ltle 11349 |
. . . . . . 7
⊢ ((2
∈ ℝ ∧ 𝑁
∈ ℝ) → (2 < 𝑁 → 2 ≤ 𝑁)) |
| 381 | 1, 380 | mpan 690 |
. . . . . 6
⊢ (𝑁 ∈ ℝ → (2 <
𝑁 → 2 ≤ 𝑁)) |
| 382 | | flge 13845 |
. . . . . . 7
⊢ ((𝑁 ∈ ℝ ∧ 2 ∈
ℤ) → (2 ≤ 𝑁
↔ 2 ≤ (⌊‘𝑁))) |
| 383 | 117, 382 | mpan2 691 |
. . . . . 6
⊢ (𝑁 ∈ ℝ → (2 ≤
𝑁 ↔ 2 ≤
(⌊‘𝑁))) |
| 384 | 381, 383 | sylibd 239 |
. . . . 5
⊢ (𝑁 ∈ ℝ → (2 <
𝑁 → 2 ≤
(⌊‘𝑁))) |
| 385 | 384 | imp 406 |
. . . 4
⊢ ((𝑁 ∈ ℝ ∧ 2 <
𝑁) → 2 ≤
(⌊‘𝑁)) |
| 386 | | eluz2 12884 |
. . . 4
⊢
((⌊‘𝑁)
∈ (ℤ≥‘2) ↔ (2 ∈ ℤ ∧
(⌊‘𝑁) ∈
ℤ ∧ 2 ≤ (⌊‘𝑁))) |
| 387 | 377, 379,
385, 386 | syl3anbrc 1344 |
. . 3
⊢ ((𝑁 ∈ ℝ ∧ 2 <
𝑁) →
(⌊‘𝑁) ∈
(ℤ≥‘2)) |
| 388 | | uzp1 12919 |
. . 3
⊢
((⌊‘𝑁)
∈ (ℤ≥‘2) → ((⌊‘𝑁) = 2 ∨ (⌊‘𝑁) ∈
(ℤ≥‘(2 + 1)))) |
| 389 | 387, 388 | syl 17 |
. 2
⊢ ((𝑁 ∈ ℝ ∧ 2 <
𝑁) →
((⌊‘𝑁) = 2 ∨
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1)))) |
| 390 | 44, 376, 389 | mpjaodan 961 |
1
⊢ ((𝑁 ∈ ℝ ∧ 2 <
𝑁) →
(θ‘𝑁) <
((log‘2) · ((2 · 𝑁) − 3))) |