Proof of Theorem chebbnd1lem2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 2rp 13040 | . . . . 5
⊢ 2 ∈
ℝ+ | 
| 2 |  | 4nn 12350 | . . . . . . 7
⊢ 4 ∈
ℕ | 
| 3 |  | 4z 12653 | . . . . . . . . 9
⊢ 4 ∈
ℤ | 
| 4 | 3 | a1i 11 | . . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → 4 ∈
ℤ) | 
| 5 |  | chebbnd1lem2.1 | . . . . . . . . 9
⊢ 𝑀 = (⌊‘(𝑁 / 2)) | 
| 6 |  | rehalfcl 12495 | . . . . . . . . . . 11
⊢ (𝑁 ∈ ℝ → (𝑁 / 2) ∈
ℝ) | 
| 7 | 6 | adantr 480 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → (𝑁 / 2) ∈
ℝ) | 
| 8 | 7 | flcld 13839 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) →
(⌊‘(𝑁 / 2))
∈ ℤ) | 
| 9 | 5, 8 | eqeltrid 2844 | . . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → 𝑀 ∈ ℤ) | 
| 10 |  | 4t2e8 12435 | . . . . . . . . . . . 12
⊢ (4
· 2) = 8 | 
| 11 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → 8 ≤ 𝑁) | 
| 12 | 10, 11 | eqbrtrid 5177 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → (4 · 2)
≤ 𝑁) | 
| 13 |  | 4re 12351 | . . . . . . . . . . . . 13
⊢ 4 ∈
ℝ | 
| 14 | 13 | a1i 11 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → 4 ∈
ℝ) | 
| 15 |  | simpl 482 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → 𝑁 ∈ ℝ) | 
| 16 |  | 2re 12341 | . . . . . . . . . . . . 13
⊢ 2 ∈
ℝ | 
| 17 | 16 | a1i 11 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → 2 ∈
ℝ) | 
| 18 |  | 2pos 12370 | . . . . . . . . . . . . 13
⊢ 0 <
2 | 
| 19 | 18 | a1i 11 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → 0 <
2) | 
| 20 |  | lemuldiv 12149 | . . . . . . . . . . . 12
⊢ ((4
∈ ℝ ∧ 𝑁
∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((4 · 2)
≤ 𝑁 ↔ 4 ≤ (𝑁 / 2))) | 
| 21 | 14, 15, 17, 19, 20 | syl112anc 1375 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → ((4 · 2)
≤ 𝑁 ↔ 4 ≤ (𝑁 / 2))) | 
| 22 | 12, 21 | mpbid 232 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → 4 ≤ (𝑁 / 2)) | 
| 23 |  | flge 13846 | . . . . . . . . . . 11
⊢ (((𝑁 / 2) ∈ ℝ ∧ 4
∈ ℤ) → (4 ≤ (𝑁 / 2) ↔ 4 ≤ (⌊‘(𝑁 / 2)))) | 
| 24 | 7, 3, 23 | sylancl 586 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → (4 ≤ (𝑁 / 2) ↔ 4 ≤
(⌊‘(𝑁 /
2)))) | 
| 25 | 22, 24 | mpbid 232 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → 4 ≤
(⌊‘(𝑁 /
2))) | 
| 26 | 25, 5 | breqtrrdi 5184 | . . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → 4 ≤ 𝑀) | 
| 27 |  | eluz2 12885 | . . . . . . . 8
⊢ (𝑀 ∈
(ℤ≥‘4) ↔ (4 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 4 ≤
𝑀)) | 
| 28 | 4, 9, 26, 27 | syl3anbrc 1343 | . . . . . . 7
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → 𝑀 ∈
(ℤ≥‘4)) | 
| 29 |  | eluznn 12961 | . . . . . . 7
⊢ ((4
∈ ℕ ∧ 𝑀
∈ (ℤ≥‘4)) → 𝑀 ∈ ℕ) | 
| 30 | 2, 28, 29 | sylancr 587 | . . . . . 6
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → 𝑀 ∈ ℕ) | 
| 31 | 30 | nnrpd 13076 | . . . . 5
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → 𝑀 ∈
ℝ+) | 
| 32 |  | rpmulcl 13059 | . . . . 5
⊢ ((2
∈ ℝ+ ∧ 𝑀 ∈ ℝ+) → (2
· 𝑀) ∈
ℝ+) | 
| 33 | 1, 31, 32 | sylancr 587 | . . . 4
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → (2 · 𝑀) ∈
ℝ+) | 
| 34 | 33 | relogcld 26666 | . . 3
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → (log‘(2
· 𝑀)) ∈
ℝ) | 
| 35 | 34, 33 | rerpdivcld 13109 | . 2
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → ((log‘(2
· 𝑀)) / (2 ·
𝑀)) ∈
ℝ) | 
| 36 |  | 0red 11265 | . . . . . . 7
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → 0 ∈
ℝ) | 
| 37 |  | 8re 12363 | . . . . . . . 8
⊢ 8 ∈
ℝ | 
| 38 | 37 | a1i 11 | . . . . . . 7
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → 8 ∈
ℝ) | 
| 39 |  | 8pos 12379 | . . . . . . . 8
⊢ 0 <
8 | 
| 40 | 39 | a1i 11 | . . . . . . 7
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → 0 <
8) | 
| 41 | 36, 38, 15, 40, 11 | ltletrd 11422 | . . . . . 6
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → 0 < 𝑁) | 
| 42 | 15, 41 | elrpd 13075 | . . . . 5
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → 𝑁 ∈
ℝ+) | 
| 43 | 42 | rphalfcld 13090 | . . . 4
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → (𝑁 / 2) ∈
ℝ+) | 
| 44 | 43 | relogcld 26666 | . . 3
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → (log‘(𝑁 / 2)) ∈
ℝ) | 
| 45 | 44, 43 | rerpdivcld 13109 | . 2
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) →
((log‘(𝑁 / 2)) /
(𝑁 / 2)) ∈
ℝ) | 
| 46 | 42 | relogcld 26666 | . . . 4
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → (log‘𝑁) ∈
ℝ) | 
| 47 | 46, 42 | rerpdivcld 13109 | . . 3
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → ((log‘𝑁) / 𝑁) ∈ ℝ) | 
| 48 |  | remulcl 11241 | . . 3
⊢ ((2
∈ ℝ ∧ ((log‘𝑁) / 𝑁) ∈ ℝ) → (2 ·
((log‘𝑁) / 𝑁)) ∈
ℝ) | 
| 49 | 16, 47, 48 | sylancr 587 | . 2
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → (2 ·
((log‘𝑁) / 𝑁)) ∈
ℝ) | 
| 50 | 9 | zred 12724 | . . . . 5
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → 𝑀 ∈ ℝ) | 
| 51 |  | peano2re 11435 | . . . . 5
⊢ (𝑀 ∈ ℝ → (𝑀 + 1) ∈
ℝ) | 
| 52 | 50, 51 | syl 17 | . . . 4
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → (𝑀 + 1) ∈
ℝ) | 
| 53 |  | remulcl 11241 | . . . . 5
⊢ ((2
∈ ℝ ∧ 𝑀
∈ ℝ) → (2 · 𝑀) ∈ ℝ) | 
| 54 | 16, 50, 53 | sylancr 587 | . . . 4
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → (2 · 𝑀) ∈
ℝ) | 
| 55 |  | flltp1 13841 | . . . . . 6
⊢ ((𝑁 / 2) ∈ ℝ →
(𝑁 / 2) <
((⌊‘(𝑁 / 2)) +
1)) | 
| 56 | 7, 55 | syl 17 | . . . . 5
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → (𝑁 / 2) <
((⌊‘(𝑁 / 2)) +
1)) | 
| 57 | 5 | oveq1i 7442 | . . . . 5
⊢ (𝑀 + 1) = ((⌊‘(𝑁 / 2)) + 1) | 
| 58 | 56, 57 | breqtrrdi 5184 | . . . 4
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → (𝑁 / 2) < (𝑀 + 1)) | 
| 59 |  | 1red 11263 | . . . . . 6
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → 1 ∈
ℝ) | 
| 60 | 30 | nnge1d 12315 | . . . . . 6
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → 1 ≤ 𝑀) | 
| 61 | 59, 50, 50, 60 | leadd2dd 11879 | . . . . 5
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → (𝑀 + 1) ≤ (𝑀 + 𝑀)) | 
| 62 | 50 | recnd 11290 | . . . . . 6
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → 𝑀 ∈ ℂ) | 
| 63 | 62 | 2timesd 12511 | . . . . 5
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → (2 · 𝑀) = (𝑀 + 𝑀)) | 
| 64 | 61, 63 | breqtrrd 5170 | . . . 4
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → (𝑀 + 1) ≤ (2 · 𝑀)) | 
| 65 | 7, 52, 54, 58, 64 | ltletrd 11422 | . . 3
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → (𝑁 / 2) < (2 · 𝑀)) | 
| 66 |  | ere 16126 | . . . . . 6
⊢ e ∈
ℝ | 
| 67 | 66 | a1i 11 | . . . . 5
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → e ∈
ℝ) | 
| 68 |  | egt2lt3 16243 | . . . . . . . . 9
⊢ (2 < e
∧ e < 3) | 
| 69 | 68 | simpri 485 | . . . . . . . 8
⊢ e <
3 | 
| 70 |  | 3lt4 12441 | . . . . . . . 8
⊢ 3 <
4 | 
| 71 |  | 3re 12347 | . . . . . . . . 9
⊢ 3 ∈
ℝ | 
| 72 | 66, 71, 13 | lttri 11388 | . . . . . . . 8
⊢ ((e <
3 ∧ 3 < 4) → e < 4) | 
| 73 | 69, 70, 72 | mp2an 692 | . . . . . . 7
⊢ e <
4 | 
| 74 | 73 | a1i 11 | . . . . . 6
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → e <
4) | 
| 75 | 67, 14, 7, 74, 22 | ltletrd 11422 | . . . . 5
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → e < (𝑁 / 2)) | 
| 76 | 67, 7, 75 | ltled 11410 | . . . 4
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → e ≤ (𝑁 / 2)) | 
| 77 | 67, 7, 54, 75, 65 | lttrd 11423 | . . . . 5
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → e < (2
· 𝑀)) | 
| 78 | 67, 54, 77 | ltled 11410 | . . . 4
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → e ≤ (2
· 𝑀)) | 
| 79 |  | logdivlt 26664 | . . . 4
⊢ ((((𝑁 / 2) ∈ ℝ ∧ e
≤ (𝑁 / 2)) ∧ ((2
· 𝑀) ∈ ℝ
∧ e ≤ (2 · 𝑀))) → ((𝑁 / 2) < (2 · 𝑀) ↔ ((log‘(2 · 𝑀)) / (2 · 𝑀)) < ((log‘(𝑁 / 2)) / (𝑁 / 2)))) | 
| 80 | 7, 76, 54, 78, 79 | syl22anc 838 | . . 3
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → ((𝑁 / 2) < (2 · 𝑀) ↔ ((log‘(2 ·
𝑀)) / (2 · 𝑀)) < ((log‘(𝑁 / 2)) / (𝑁 / 2)))) | 
| 81 | 65, 80 | mpbid 232 | . 2
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → ((log‘(2
· 𝑀)) / (2 ·
𝑀)) < ((log‘(𝑁 / 2)) / (𝑁 / 2))) | 
| 82 |  | rphalflt 13065 | . . . . . 6
⊢ (𝑁 ∈ ℝ+
→ (𝑁 / 2) < 𝑁) | 
| 83 | 42, 82 | syl 17 | . . . . 5
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → (𝑁 / 2) < 𝑁) | 
| 84 |  | logltb 26643 | . . . . . 6
⊢ (((𝑁 / 2) ∈ ℝ+
∧ 𝑁 ∈
ℝ+) → ((𝑁 / 2) < 𝑁 ↔ (log‘(𝑁 / 2)) < (log‘𝑁))) | 
| 85 | 43, 42, 84 | syl2anc 584 | . . . . 5
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → ((𝑁 / 2) < 𝑁 ↔ (log‘(𝑁 / 2)) < (log‘𝑁))) | 
| 86 | 83, 85 | mpbid 232 | . . . 4
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → (log‘(𝑁 / 2)) < (log‘𝑁)) | 
| 87 | 44, 46, 43, 86 | ltdiv1dd 13135 | . . 3
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) →
((log‘(𝑁 / 2)) /
(𝑁 / 2)) <
((log‘𝑁) / (𝑁 / 2))) | 
| 88 | 46 | recnd 11290 | . . . . 5
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → (log‘𝑁) ∈
ℂ) | 
| 89 | 15 | recnd 11290 | . . . . 5
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → 𝑁 ∈ ℂ) | 
| 90 | 17 | recnd 11290 | . . . . 5
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → 2 ∈
ℂ) | 
| 91 | 42 | rpne0d 13083 | . . . . 5
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → 𝑁 ≠ 0) | 
| 92 |  | 2ne0 12371 | . . . . . 6
⊢ 2 ≠
0 | 
| 93 | 92 | a1i 11 | . . . . 5
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → 2 ≠
0) | 
| 94 | 88, 89, 90, 91, 93 | divdiv2d 12076 | . . . 4
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → ((log‘𝑁) / (𝑁 / 2)) = (((log‘𝑁) · 2) / 𝑁)) | 
| 95 | 88, 90 | mulcomd 11283 | . . . . 5
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → ((log‘𝑁) · 2) = (2 ·
(log‘𝑁))) | 
| 96 | 95 | oveq1d 7447 | . . . 4
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) →
(((log‘𝑁) · 2)
/ 𝑁) = ((2 ·
(log‘𝑁)) / 𝑁)) | 
| 97 | 90, 88, 89, 91 | divassd 12079 | . . . 4
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → ((2 ·
(log‘𝑁)) / 𝑁) = (2 ·
((log‘𝑁) / 𝑁))) | 
| 98 | 94, 96, 97 | 3eqtrd 2780 | . . 3
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → ((log‘𝑁) / (𝑁 / 2)) = (2 · ((log‘𝑁) / 𝑁))) | 
| 99 | 87, 98 | breqtrd 5168 | . 2
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) →
((log‘(𝑁 / 2)) /
(𝑁 / 2)) < (2 ·
((log‘𝑁) / 𝑁))) | 
| 100 | 35, 45, 49, 81, 99 | lttrd 11423 | 1
⊢ ((𝑁 ∈ ℝ ∧ 8 ≤
𝑁) → ((log‘(2
· 𝑀)) / (2 ·
𝑀)) < (2 ·
((log‘𝑁) / 𝑁))) |