| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 2div2e1 12407 | . . 3
⊢ (2 / 2) =
1 | 
| 2 |  | 2re 12340 | . . . . 5
⊢ 2 ∈
ℝ | 
| 3 | 2 | a1i 11 | . . . 4
⊢ (𝜑 → 2 ∈
ℝ) | 
| 4 |  | ioossre 13448 | . . . . . 6
⊢ (0(,)1)
⊆ ℝ | 
| 5 |  | pntpbnd1.e | . . . . . 6
⊢ (𝜑 → 𝐸 ∈ (0(,)1)) | 
| 6 | 4, 5 | sselid 3981 | . . . . 5
⊢ (𝜑 → 𝐸 ∈ ℝ) | 
| 7 |  | eliooord 13446 | . . . . . . 7
⊢ (𝐸 ∈ (0(,)1) → (0 <
𝐸 ∧ 𝐸 < 1)) | 
| 8 | 5, 7 | syl 17 | . . . . . 6
⊢ (𝜑 → (0 < 𝐸 ∧ 𝐸 < 1)) | 
| 9 | 8 | simpld 494 | . . . . 5
⊢ (𝜑 → 0 < 𝐸) | 
| 10 | 6, 9 | elrpd 13074 | . . . 4
⊢ (𝜑 → 𝐸 ∈
ℝ+) | 
| 11 |  | 2rp 13039 | . . . . 5
⊢ 2 ∈
ℝ+ | 
| 12 | 11 | a1i 11 | . . . 4
⊢ (𝜑 → 2 ∈
ℝ+) | 
| 13 |  | pntpbnd1.c | . . . . . . . . 9
⊢ 𝐶 = (𝐴 + 2) | 
| 14 | 13 | oveq1i 7441 | . . . . . . . 8
⊢ (𝐶 − 𝐴) = ((𝐴 + 2) − 𝐴) | 
| 15 |  | pntpbnd1.1 | . . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈
ℝ+) | 
| 16 | 15 | rpcnd 13079 | . . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℂ) | 
| 17 |  | 2cn 12341 | . . . . . . . . 9
⊢ 2 ∈
ℂ | 
| 18 |  | pncan2 11515 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 2 ∈
ℂ) → ((𝐴 + 2)
− 𝐴) =
2) | 
| 19 | 16, 17, 18 | sylancl 586 | . . . . . . . 8
⊢ (𝜑 → ((𝐴 + 2) − 𝐴) = 2) | 
| 20 | 14, 19 | eqtrid 2789 | . . . . . . 7
⊢ (𝜑 → (𝐶 − 𝐴) = 2) | 
| 21 | 20 | oveq1d 7446 | . . . . . 6
⊢ (𝜑 → ((𝐶 − 𝐴) / 𝐸) = (2 / 𝐸)) | 
| 22 |  | rpaddcl 13057 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 2 ∈ ℝ+) → (𝐴 + 2) ∈
ℝ+) | 
| 23 | 15, 11, 22 | sylancl 586 | . . . . . . . . 9
⊢ (𝜑 → (𝐴 + 2) ∈
ℝ+) | 
| 24 | 13, 23 | eqeltrid 2845 | . . . . . . . 8
⊢ (𝜑 → 𝐶 ∈
ℝ+) | 
| 25 | 24 | rpcnd 13079 | . . . . . . 7
⊢ (𝜑 → 𝐶 ∈ ℂ) | 
| 26 | 6 | recnd 11289 | . . . . . . 7
⊢ (𝜑 → 𝐸 ∈ ℂ) | 
| 27 | 10 | rpne0d 13082 | . . . . . . 7
⊢ (𝜑 → 𝐸 ≠ 0) | 
| 28 | 25, 16, 26, 27 | divsubdird 12082 | . . . . . 6
⊢ (𝜑 → ((𝐶 − 𝐴) / 𝐸) = ((𝐶 / 𝐸) − (𝐴 / 𝐸))) | 
| 29 | 21, 28 | eqtr3d 2779 | . . . . 5
⊢ (𝜑 → (2 / 𝐸) = ((𝐶 / 𝐸) − (𝐴 / 𝐸))) | 
| 30 | 24, 10 | rpdivcld 13094 | . . . . . . 7
⊢ (𝜑 → (𝐶 / 𝐸) ∈
ℝ+) | 
| 31 | 30 | rpred 13077 | . . . . . 6
⊢ (𝜑 → (𝐶 / 𝐸) ∈ ℝ) | 
| 32 | 15 | rpred 13077 | . . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 33 | 32, 10 | rerpdivcld 13108 | . . . . . 6
⊢ (𝜑 → (𝐴 / 𝐸) ∈ ℝ) | 
| 34 |  | resubcl 11573 | . . . . . . . 8
⊢ (((𝐶 / 𝐸) ∈ ℝ ∧ 2 ∈ ℝ)
→ ((𝐶 / 𝐸) − 2) ∈
ℝ) | 
| 35 | 31, 2, 34 | sylancl 586 | . . . . . . 7
⊢ (𝜑 → ((𝐶 / 𝐸) − 2) ∈
ℝ) | 
| 36 |  | pntpbnd1.k | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) | 
| 37 | 31 | reefcld 16124 | . . . . . . . . . . . . 13
⊢ (𝜑 → (exp‘(𝐶 / 𝐸)) ∈ ℝ) | 
| 38 |  | elicopnf 13485 | . . . . . . . . . . . . 13
⊢
((exp‘(𝐶 /
𝐸)) ∈ ℝ →
(𝐾 ∈
((exp‘(𝐶 / 𝐸))[,)+∞) ↔ (𝐾 ∈ ℝ ∧
(exp‘(𝐶 / 𝐸)) ≤ 𝐾))) | 
| 39 | 37, 38 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐾 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ↔ (𝐾 ∈ ℝ ∧ (exp‘(𝐶 / 𝐸)) ≤ 𝐾))) | 
| 40 | 36, 39 | mpbid 232 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐾 ∈ ℝ ∧ (exp‘(𝐶 / 𝐸)) ≤ 𝐾)) | 
| 41 | 40 | simpld 494 | . . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈ ℝ) | 
| 42 |  | 0red 11264 | . . . . . . . . . . 11
⊢ (𝜑 → 0 ∈
ℝ) | 
| 43 |  | 1re 11261 | . . . . . . . . . . . 12
⊢ 1 ∈
ℝ | 
| 44 | 43 | a1i 11 | . . . . . . . . . . 11
⊢ (𝜑 → 1 ∈
ℝ) | 
| 45 |  | 0lt1 11785 | . . . . . . . . . . . 12
⊢ 0 <
1 | 
| 46 | 45 | a1i 11 | . . . . . . . . . . 11
⊢ (𝜑 → 0 < 1) | 
| 47 |  | efgt1 16152 | . . . . . . . . . . . . 13
⊢ ((𝐶 / 𝐸) ∈ ℝ+ → 1 <
(exp‘(𝐶 / 𝐸))) | 
| 48 | 30, 47 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → 1 < (exp‘(𝐶 / 𝐸))) | 
| 49 | 40 | simprd 495 | . . . . . . . . . . . 12
⊢ (𝜑 → (exp‘(𝐶 / 𝐸)) ≤ 𝐾) | 
| 50 | 44, 37, 41, 48, 49 | ltletrd 11421 | . . . . . . . . . . 11
⊢ (𝜑 → 1 < 𝐾) | 
| 51 | 42, 44, 41, 46, 50 | lttrd 11422 | . . . . . . . . . 10
⊢ (𝜑 → 0 < 𝐾) | 
| 52 | 41, 51 | elrpd 13074 | . . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈
ℝ+) | 
| 53 | 52 | relogcld 26665 | . . . . . . . 8
⊢ (𝜑 → (log‘𝐾) ∈
ℝ) | 
| 54 |  | resubcl 11573 | . . . . . . . 8
⊢
(((log‘𝐾)
∈ ℝ ∧ 2 ∈ ℝ) → ((log‘𝐾) − 2) ∈
ℝ) | 
| 55 | 53, 2, 54 | sylancl 586 | . . . . . . 7
⊢ (𝜑 → ((log‘𝐾) − 2) ∈
ℝ) | 
| 56 | 52 | reeflogd 26666 | . . . . . . . . . 10
⊢ (𝜑 →
(exp‘(log‘𝐾)) =
𝐾) | 
| 57 | 49, 56 | breqtrrd 5171 | . . . . . . . . 9
⊢ (𝜑 → (exp‘(𝐶 / 𝐸)) ≤ (exp‘(log‘𝐾))) | 
| 58 |  | efle 16154 | . . . . . . . . . 10
⊢ (((𝐶 / 𝐸) ∈ ℝ ∧ (log‘𝐾) ∈ ℝ) → ((𝐶 / 𝐸) ≤ (log‘𝐾) ↔ (exp‘(𝐶 / 𝐸)) ≤ (exp‘(log‘𝐾)))) | 
| 59 | 31, 53, 58 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → ((𝐶 / 𝐸) ≤ (log‘𝐾) ↔ (exp‘(𝐶 / 𝐸)) ≤ (exp‘(log‘𝐾)))) | 
| 60 | 57, 59 | mpbird 257 | . . . . . . . 8
⊢ (𝜑 → (𝐶 / 𝐸) ≤ (log‘𝐾)) | 
| 61 | 31, 53, 3, 60 | lesub1dd 11879 | . . . . . . 7
⊢ (𝜑 → ((𝐶 / 𝐸) − 2) ≤ ((log‘𝐾) − 2)) | 
| 62 |  | fzfid 14014 | . . . . . . . . 9
⊢ (𝜑 → (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌))) ∈ Fin) | 
| 63 |  | ioossre 13448 | . . . . . . . . . . . . . . 15
⊢ (𝑋(,)+∞) ⊆
ℝ | 
| 64 |  | pntpbnd1.y | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑌 ∈ (𝑋(,)+∞)) | 
| 65 | 63, 64 | sselid 3981 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑌 ∈ ℝ) | 
| 66 |  | pntpbnd1.x | . . . . . . . . . . . . . . . . 17
⊢ 𝑋 = (exp‘(2 / 𝐸)) | 
| 67 |  | rerpdivcl 13065 | . . . . . . . . . . . . . . . . . . 19
⊢ ((2
∈ ℝ ∧ 𝐸
∈ ℝ+) → (2 / 𝐸) ∈ ℝ) | 
| 68 | 2, 10, 67 | sylancr 587 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (2 / 𝐸) ∈ ℝ) | 
| 69 | 68 | reefcld 16124 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (exp‘(2 / 𝐸)) ∈
ℝ) | 
| 70 | 66, 69 | eqeltrid 2845 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑋 ∈ ℝ) | 
| 71 |  | efgt0 16139 | . . . . . . . . . . . . . . . . . 18
⊢ ((2 /
𝐸) ∈ ℝ → 0
< (exp‘(2 / 𝐸))) | 
| 72 | 68, 71 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 0 < (exp‘(2 /
𝐸))) | 
| 73 | 72, 66 | breqtrrdi 5185 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 0 < 𝑋) | 
| 74 | 70 | rexrd 11311 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑋 ∈
ℝ*) | 
| 75 |  | elioopnf 13483 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑋 ∈ ℝ*
→ (𝑌 ∈ (𝑋(,)+∞) ↔ (𝑌 ∈ ℝ ∧ 𝑋 < 𝑌))) | 
| 76 | 74, 75 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑌 ∈ (𝑋(,)+∞) ↔ (𝑌 ∈ ℝ ∧ 𝑋 < 𝑌))) | 
| 77 | 64, 76 | mpbid 232 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑌 ∈ ℝ ∧ 𝑋 < 𝑌)) | 
| 78 | 77 | simprd 495 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑋 < 𝑌) | 
| 79 | 42, 70, 65, 73, 78 | lttrd 11422 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 < 𝑌) | 
| 80 | 42, 65, 79 | ltled 11409 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 0 ≤ 𝑌) | 
| 81 |  | flge0nn0 13860 | . . . . . . . . . . . . . 14
⊢ ((𝑌 ∈ ℝ ∧ 0 ≤
𝑌) →
(⌊‘𝑌) ∈
ℕ0) | 
| 82 | 65, 80, 81 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (𝜑 → (⌊‘𝑌) ∈
ℕ0) | 
| 83 |  | nn0p1nn 12565 | . . . . . . . . . . . . 13
⊢
((⌊‘𝑌)
∈ ℕ0 → ((⌊‘𝑌) + 1) ∈ ℕ) | 
| 84 | 82, 83 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → ((⌊‘𝑌) + 1) ∈
ℕ) | 
| 85 |  | elfzuz 13560 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌))) → 𝑛 ∈
(ℤ≥‘((⌊‘𝑌) + 1))) | 
| 86 |  | eluznn 12960 | . . . . . . . . . . . 12
⊢
((((⌊‘𝑌)
+ 1) ∈ ℕ ∧ 𝑛
∈ (ℤ≥‘((⌊‘𝑌) + 1))) → 𝑛 ∈ ℕ) | 
| 87 | 84, 85, 86 | syl2an 596 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑛 ∈ ℕ) | 
| 88 | 87 | peano2nnd 12283 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑛 + 1) ∈ ℕ) | 
| 89 | 88 | nnrecred 12317 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (1 / (𝑛 + 1)) ∈ ℝ) | 
| 90 | 62, 89 | fsumrecl 15770 | . . . . . . . 8
⊢ (𝜑 → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1)) ∈ ℝ) | 
| 91 | 53 | recnd 11289 | . . . . . . . . . 10
⊢ (𝜑 → (log‘𝐾) ∈
ℂ) | 
| 92 |  | 2cnd 12344 | . . . . . . . . . 10
⊢ (𝜑 → 2 ∈
ℂ) | 
| 93 | 65, 79 | elrpd 13074 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑌 ∈
ℝ+) | 
| 94 | 93 | relogcld 26665 | . . . . . . . . . . 11
⊢ (𝜑 → (log‘𝑌) ∈
ℝ) | 
| 95 | 94 | recnd 11289 | . . . . . . . . . 10
⊢ (𝜑 → (log‘𝑌) ∈
ℂ) | 
| 96 | 91, 92, 95 | pnpcan2d 11658 | . . . . . . . . 9
⊢ (𝜑 → (((log‘𝐾) + (log‘𝑌)) − (2 + (log‘𝑌))) = ((log‘𝐾) − 2)) | 
| 97 | 52, 93 | relogmuld 26667 | . . . . . . . . . . 11
⊢ (𝜑 → (log‘(𝐾 · 𝑌)) = ((log‘𝐾) + (log‘𝑌))) | 
| 98 | 53, 94 | readdcld 11290 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((log‘𝐾) + (log‘𝑌)) ∈ ℝ) | 
| 99 | 97, 98 | eqeltrd 2841 | . . . . . . . . . . . 12
⊢ (𝜑 → (log‘(𝐾 · 𝑌)) ∈ ℝ) | 
| 100 |  | fzfid 14014 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (0...(⌊‘𝑌)) ∈ Fin) | 
| 101 |  | elfznn0 13660 | . . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈
(0...(⌊‘𝑌))
→ 𝑛 ∈
ℕ0) | 
| 102 | 101 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (0...(⌊‘𝑌))) → 𝑛 ∈ ℕ0) | 
| 103 |  | nn0p1nn 12565 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ0
→ (𝑛 + 1) ∈
ℕ) | 
| 104 | 102, 103 | syl 17 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (0...(⌊‘𝑌))) → (𝑛 + 1) ∈ ℕ) | 
| 105 | 104 | nnrecred 12317 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (0...(⌊‘𝑌))) → (1 / (𝑛 + 1)) ∈ ℝ) | 
| 106 | 100, 105 | fsumrecl 15770 | . . . . . . . . . . . . 13
⊢ (𝜑 → Σ𝑛 ∈ (0...(⌊‘𝑌))(1 / (𝑛 + 1)) ∈ ℝ) | 
| 107 | 106, 90 | readdcld 11290 | . . . . . . . . . . . 12
⊢ (𝜑 → (Σ𝑛 ∈ (0...(⌊‘𝑌))(1 / (𝑛 + 1)) + Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1))) ∈ ℝ) | 
| 108 |  | readdcl 11238 | . . . . . . . . . . . . . 14
⊢ ((2
∈ ℝ ∧ (log‘𝑌) ∈ ℝ) → (2 +
(log‘𝑌)) ∈
ℝ) | 
| 109 | 2, 94, 108 | sylancr 587 | . . . . . . . . . . . . 13
⊢ (𝜑 → (2 + (log‘𝑌)) ∈
ℝ) | 
| 110 | 109, 90 | readdcld 11290 | . . . . . . . . . . . 12
⊢ (𝜑 → ((2 + (log‘𝑌)) + Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1))) ∈ ℝ) | 
| 111 | 41, 65 | remulcld 11291 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐾 · 𝑌) ∈ ℝ) | 
| 112 | 65 | recnd 11289 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑌 ∈ ℂ) | 
| 113 | 112 | mullidd 11279 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (1 · 𝑌) = 𝑌) | 
| 114 | 44, 41, 50 | ltled 11409 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 1 ≤ 𝐾) | 
| 115 |  | lemul1 12119 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((1
∈ ℝ ∧ 𝐾
∈ ℝ ∧ (𝑌
∈ ℝ ∧ 0 < 𝑌)) → (1 ≤ 𝐾 ↔ (1 · 𝑌) ≤ (𝐾 · 𝑌))) | 
| 116 | 44, 41, 65, 79, 115 | syl112anc 1376 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (1 ≤ 𝐾 ↔ (1 · 𝑌) ≤ (𝐾 · 𝑌))) | 
| 117 | 114, 116 | mpbid 232 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (1 · 𝑌) ≤ (𝐾 · 𝑌)) | 
| 118 | 113, 117 | eqbrtrrd 5167 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑌 ≤ (𝐾 · 𝑌)) | 
| 119 | 42, 65, 111, 80, 118 | letrd 11418 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 0 ≤ (𝐾 · 𝑌)) | 
| 120 |  | flge0nn0 13860 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐾 · 𝑌) ∈ ℝ ∧ 0 ≤ (𝐾 · 𝑌)) → (⌊‘(𝐾 · 𝑌)) ∈
ℕ0) | 
| 121 | 111, 119,
120 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (⌊‘(𝐾 · 𝑌)) ∈
ℕ0) | 
| 122 |  | nn0p1nn 12565 | . . . . . . . . . . . . . . . . 17
⊢
((⌊‘(𝐾
· 𝑌)) ∈
ℕ0 → ((⌊‘(𝐾 · 𝑌)) + 1) ∈ ℕ) | 
| 123 | 121, 122 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((⌊‘(𝐾 · 𝑌)) + 1) ∈ ℕ) | 
| 124 | 123 | nnrpd 13075 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((⌊‘(𝐾 · 𝑌)) + 1) ∈
ℝ+) | 
| 125 | 124 | relogcld 26665 | . . . . . . . . . . . . . 14
⊢ (𝜑 →
(log‘((⌊‘(𝐾 · 𝑌)) + 1)) ∈ ℝ) | 
| 126 |  | 1zzd 12648 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 1 ∈
ℤ) | 
| 127 | 111 | flcld 13838 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (⌊‘(𝐾 · 𝑌)) ∈ ℤ) | 
| 128 | 127 | peano2zd 12725 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((⌊‘(𝐾 · 𝑌)) + 1) ∈ ℤ) | 
| 129 |  | elfznn 13593 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈
(1...((⌊‘(𝐾
· 𝑌)) + 1)) →
𝑘 ∈
ℕ) | 
| 130 | 129 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))) → 𝑘 ∈ ℕ) | 
| 131 |  | nnrecre 12308 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ ℕ → (1 /
𝑘) ∈
ℝ) | 
| 132 | 131 | recnd 11289 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℕ → (1 /
𝑘) ∈
ℂ) | 
| 133 | 130, 132 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))) → (1 / 𝑘) ∈ ℂ) | 
| 134 |  | oveq2 7439 | . . . . . . . . . . . . . . . . 17
⊢ (𝑘 = (𝑛 + 1) → (1 / 𝑘) = (1 / (𝑛 + 1))) | 
| 135 | 126, 126,
128, 133, 134 | fsumshftm 15817 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘) = Σ𝑛 ∈ ((1 −
1)...(((⌊‘(𝐾
· 𝑌)) + 1) −
1))(1 / (𝑛 +
1))) | 
| 136 |  | 1m1e0 12338 | . . . . . . . . . . . . . . . . . . 19
⊢ (1
− 1) = 0 | 
| 137 | 136 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (1 − 1) =
0) | 
| 138 | 127 | zcnd 12723 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (⌊‘(𝐾 · 𝑌)) ∈ ℂ) | 
| 139 |  | ax-1cn 11213 | . . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℂ | 
| 140 |  | pncan 11514 | . . . . . . . . . . . . . . . . . . 19
⊢
(((⌊‘(𝐾
· 𝑌)) ∈ ℂ
∧ 1 ∈ ℂ) → (((⌊‘(𝐾 · 𝑌)) + 1) − 1) = (⌊‘(𝐾 · 𝑌))) | 
| 141 | 138, 139,
140 | sylancl 586 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((⌊‘(𝐾 · 𝑌)) + 1) − 1) = (⌊‘(𝐾 · 𝑌))) | 
| 142 | 137, 141 | oveq12d 7449 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((1 −
1)...(((⌊‘(𝐾
· 𝑌)) + 1) −
1)) = (0...(⌊‘(𝐾 · 𝑌)))) | 
| 143 | 142 | sumeq1d 15736 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → Σ𝑛 ∈ ((1 −
1)...(((⌊‘(𝐾
· 𝑌)) + 1) −
1))(1 / (𝑛 + 1)) =
Σ𝑛 ∈
(0...(⌊‘(𝐾
· 𝑌)))(1 / (𝑛 + 1))) | 
| 144 |  | reflcl 13836 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑌 ∈ ℝ →
(⌊‘𝑌) ∈
ℝ) | 
| 145 | 65, 144 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (⌊‘𝑌) ∈
ℝ) | 
| 146 | 145 | ltp1d 12198 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (⌊‘𝑌) < ((⌊‘𝑌) + 1)) | 
| 147 |  | fzdisj 13591 | . . . . . . . . . . . . . . . . . 18
⊢
((⌊‘𝑌)
< ((⌊‘𝑌) +
1) → ((0...(⌊‘𝑌)) ∩ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) = ∅) | 
| 148 | 146, 147 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((0...(⌊‘𝑌)) ∩ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) = ∅) | 
| 149 |  | flwordi 13852 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑌 ∈ ℝ ∧ (𝐾 · 𝑌) ∈ ℝ ∧ 𝑌 ≤ (𝐾 · 𝑌)) → (⌊‘𝑌) ≤ (⌊‘(𝐾 · 𝑌))) | 
| 150 | 65, 111, 118, 149 | syl3anc 1373 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (⌊‘𝑌) ≤ (⌊‘(𝐾 · 𝑌))) | 
| 151 |  | elfz2nn0 13658 | . . . . . . . . . . . . . . . . . . 19
⊢
((⌊‘𝑌)
∈ (0...(⌊‘(𝐾 · 𝑌))) ↔ ((⌊‘𝑌) ∈ ℕ0 ∧
(⌊‘(𝐾 ·
𝑌)) ∈
ℕ0 ∧ (⌊‘𝑌) ≤ (⌊‘(𝐾 · 𝑌)))) | 
| 152 | 82, 121, 150, 151 | syl3anbrc 1344 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (⌊‘𝑌) ∈
(0...(⌊‘(𝐾
· 𝑌)))) | 
| 153 |  | fzsplit 13590 | . . . . . . . . . . . . . . . . . 18
⊢
((⌊‘𝑌)
∈ (0...(⌊‘(𝐾 · 𝑌))) → (0...(⌊‘(𝐾 · 𝑌))) = ((0...(⌊‘𝑌)) ∪ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌))))) | 
| 154 | 152, 153 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (0...(⌊‘(𝐾 · 𝑌))) = ((0...(⌊‘𝑌)) ∪ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌))))) | 
| 155 |  | fzfid 14014 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (0...(⌊‘(𝐾 · 𝑌))) ∈ Fin) | 
| 156 |  | elfznn0 13660 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈
(0...(⌊‘(𝐾
· 𝑌))) → 𝑛 ∈
ℕ0) | 
| 157 | 156 | adantl 481 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ (0...(⌊‘(𝐾 · 𝑌)))) → 𝑛 ∈ ℕ0) | 
| 158 | 157, 103 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ (0...(⌊‘(𝐾 · 𝑌)))) → (𝑛 + 1) ∈ ℕ) | 
| 159 | 158 | nnrecred 12317 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ (0...(⌊‘(𝐾 · 𝑌)))) → (1 / (𝑛 + 1)) ∈ ℝ) | 
| 160 | 159 | recnd 11289 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (0...(⌊‘(𝐾 · 𝑌)))) → (1 / (𝑛 + 1)) ∈ ℂ) | 
| 161 | 148, 154,
155, 160 | fsumsplit 15777 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → Σ𝑛 ∈ (0...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1)) = (Σ𝑛 ∈ (0...(⌊‘𝑌))(1 / (𝑛 + 1)) + Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1)))) | 
| 162 | 135, 143,
161 | 3eqtrd 2781 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘) = (Σ𝑛 ∈ (0...(⌊‘𝑌))(1 / (𝑛 + 1)) + Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1)))) | 
| 163 | 162, 107 | eqeltrd 2841 | . . . . . . . . . . . . . 14
⊢ (𝜑 → Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘) ∈ ℝ) | 
| 164 |  | fllep1 13841 | . . . . . . . . . . . . . . . 16
⊢ ((𝐾 · 𝑌) ∈ ℝ → (𝐾 · 𝑌) ≤ ((⌊‘(𝐾 · 𝑌)) + 1)) | 
| 165 | 111, 164 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐾 · 𝑌) ≤ ((⌊‘(𝐾 · 𝑌)) + 1)) | 
| 166 | 52, 93 | rpmulcld 13093 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐾 · 𝑌) ∈
ℝ+) | 
| 167 | 166, 124 | logled 26669 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐾 · 𝑌) ≤ ((⌊‘(𝐾 · 𝑌)) + 1) ↔ (log‘(𝐾 · 𝑌)) ≤ (log‘((⌊‘(𝐾 · 𝑌)) + 1)))) | 
| 168 | 165, 167 | mpbid 232 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (log‘(𝐾 · 𝑌)) ≤ (log‘((⌊‘(𝐾 · 𝑌)) + 1))) | 
| 169 |  | emre 27049 | . . . . . . . . . . . . . . . . 17
⊢ γ
∈ ℝ | 
| 170 | 169 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → γ ∈
ℝ) | 
| 171 | 163, 125 | resubcld 11691 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘) − (log‘((⌊‘(𝐾 · 𝑌)) + 1))) ∈ ℝ) | 
| 172 |  | 0re 11263 | . . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
ℝ | 
| 173 |  | emgt0 27050 | . . . . . . . . . . . . . . . . . 18
⊢ 0 <
γ | 
| 174 | 172, 169,
173 | ltleii 11384 | . . . . . . . . . . . . . . . . 17
⊢ 0 ≤
γ | 
| 175 | 174 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 0 ≤
γ) | 
| 176 |  | harmonicbnd 27047 | . . . . . . . . . . . . . . . . . 18
⊢
(((⌊‘(𝐾
· 𝑌)) + 1) ∈
ℕ → (Σ𝑘
∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘) − (log‘((⌊‘(𝐾 · 𝑌)) + 1))) ∈
(γ[,]1)) | 
| 177 | 123, 176 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘) − (log‘((⌊‘(𝐾 · 𝑌)) + 1))) ∈
(γ[,]1)) | 
| 178 | 169, 43 | elicc2i 13453 | . . . . . . . . . . . . . . . . . 18
⊢
((Σ𝑘 ∈
(1...((⌊‘(𝐾
· 𝑌)) + 1))(1 /
𝑘) −
(log‘((⌊‘(𝐾 · 𝑌)) + 1))) ∈ (γ[,]1) ↔
((Σ𝑘 ∈
(1...((⌊‘(𝐾
· 𝑌)) + 1))(1 /
𝑘) −
(log‘((⌊‘(𝐾 · 𝑌)) + 1))) ∈ ℝ ∧ γ ≤
(Σ𝑘 ∈
(1...((⌊‘(𝐾
· 𝑌)) + 1))(1 /
𝑘) −
(log‘((⌊‘(𝐾 · 𝑌)) + 1))) ∧ (Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘) − (log‘((⌊‘(𝐾 · 𝑌)) + 1))) ≤ 1)) | 
| 179 | 178 | simp2bi 1147 | . . . . . . . . . . . . . . . . 17
⊢
((Σ𝑘 ∈
(1...((⌊‘(𝐾
· 𝑌)) + 1))(1 /
𝑘) −
(log‘((⌊‘(𝐾 · 𝑌)) + 1))) ∈ (γ[,]1) →
γ ≤ (Σ𝑘
∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘) − (log‘((⌊‘(𝐾 · 𝑌)) + 1)))) | 
| 180 | 177, 179 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → γ ≤ (Σ𝑘 ∈
(1...((⌊‘(𝐾
· 𝑌)) + 1))(1 /
𝑘) −
(log‘((⌊‘(𝐾 · 𝑌)) + 1)))) | 
| 181 | 42, 170, 171, 175, 180 | letrd 11418 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 ≤ (Σ𝑘 ∈
(1...((⌊‘(𝐾
· 𝑌)) + 1))(1 /
𝑘) −
(log‘((⌊‘(𝐾 · 𝑌)) + 1)))) | 
| 182 | 163, 125 | subge0d 11853 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (0 ≤ (Σ𝑘 ∈
(1...((⌊‘(𝐾
· 𝑌)) + 1))(1 /
𝑘) −
(log‘((⌊‘(𝐾 · 𝑌)) + 1))) ↔
(log‘((⌊‘(𝐾 · 𝑌)) + 1)) ≤ Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘))) | 
| 183 | 181, 182 | mpbid 232 | . . . . . . . . . . . . . 14
⊢ (𝜑 →
(log‘((⌊‘(𝐾 · 𝑌)) + 1)) ≤ Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘)) | 
| 184 | 99, 125, 163, 168, 183 | letrd 11418 | . . . . . . . . . . . . 13
⊢ (𝜑 → (log‘(𝐾 · 𝑌)) ≤ Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘)) | 
| 185 | 184, 162 | breqtrd 5169 | . . . . . . . . . . . 12
⊢ (𝜑 → (log‘(𝐾 · 𝑌)) ≤ (Σ𝑛 ∈ (0...(⌊‘𝑌))(1 / (𝑛 + 1)) + Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1)))) | 
| 186 | 65 | flcld 13838 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (⌊‘𝑌) ∈
ℤ) | 
| 187 | 186 | peano2zd 12725 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((⌊‘𝑌) + 1) ∈
ℤ) | 
| 188 |  | elfznn 13593 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈
(1...((⌊‘𝑌) +
1)) → 𝑘 ∈
ℕ) | 
| 189 | 188 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (1...((⌊‘𝑌) + 1))) → 𝑘 ∈
ℕ) | 
| 190 | 189, 132 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (1...((⌊‘𝑌) + 1))) → (1 / 𝑘) ∈
ℂ) | 
| 191 | 126, 126,
187, 190, 134 | fsumshftm 15817 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) = Σ𝑛 ∈ ((1 −
1)...(((⌊‘𝑌) +
1) − 1))(1 / (𝑛 +
1))) | 
| 192 | 145 | recnd 11289 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (⌊‘𝑌) ∈
ℂ) | 
| 193 |  | pncan 11514 | . . . . . . . . . . . . . . . . . 18
⊢
(((⌊‘𝑌)
∈ ℂ ∧ 1 ∈ ℂ) → (((⌊‘𝑌) + 1) − 1) =
(⌊‘𝑌)) | 
| 194 | 192, 139,
193 | sylancl 586 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((⌊‘𝑌) + 1) − 1) =
(⌊‘𝑌)) | 
| 195 | 137, 194 | oveq12d 7449 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((1 −
1)...(((⌊‘𝑌) +
1) − 1)) = (0...(⌊‘𝑌))) | 
| 196 | 195 | sumeq1d 15736 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → Σ𝑛 ∈ ((1 −
1)...(((⌊‘𝑌) +
1) − 1))(1 / (𝑛 + 1))
= Σ𝑛 ∈
(0...(⌊‘𝑌))(1 /
(𝑛 + 1))) | 
| 197 | 191, 196 | eqtrd 2777 | . . . . . . . . . . . . . 14
⊢ (𝜑 → Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) = Σ𝑛 ∈ (0...(⌊‘𝑌))(1 / (𝑛 + 1))) | 
| 198 | 197, 106 | eqeltrd 2841 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) ∈ ℝ) | 
| 199 | 84 | nnrpd 13075 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((⌊‘𝑌) + 1) ∈
ℝ+) | 
| 200 | 199 | relogcld 26665 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 →
(log‘((⌊‘𝑌) + 1)) ∈ ℝ) | 
| 201 |  | readdcl 11238 | . . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℝ ∧ (log‘((⌊‘𝑌) + 1)) ∈ ℝ) → (1 +
(log‘((⌊‘𝑌) + 1))) ∈ ℝ) | 
| 202 | 43, 200, 201 | sylancr 587 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (1 +
(log‘((⌊‘𝑌) + 1))) ∈ ℝ) | 
| 203 |  | harmonicbnd 27047 | . . . . . . . . . . . . . . . . . 18
⊢
(((⌊‘𝑌)
+ 1) ∈ ℕ → (Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) − (log‘((⌊‘𝑌) + 1))) ∈
(γ[,]1)) | 
| 204 | 84, 203 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) − (log‘((⌊‘𝑌) + 1))) ∈
(γ[,]1)) | 
| 205 | 169, 43 | elicc2i 13453 | . . . . . . . . . . . . . . . . . 18
⊢
((Σ𝑘 ∈
(1...((⌊‘𝑌) +
1))(1 / 𝑘) −
(log‘((⌊‘𝑌) + 1))) ∈ (γ[,]1) ↔
((Σ𝑘 ∈
(1...((⌊‘𝑌) +
1))(1 / 𝑘) −
(log‘((⌊‘𝑌) + 1))) ∈ ℝ ∧ γ ≤
(Σ𝑘 ∈
(1...((⌊‘𝑌) +
1))(1 / 𝑘) −
(log‘((⌊‘𝑌) + 1))) ∧ (Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) − (log‘((⌊‘𝑌) + 1))) ≤
1)) | 
| 206 | 205 | simp3bi 1148 | . . . . . . . . . . . . . . . . 17
⊢
((Σ𝑘 ∈
(1...((⌊‘𝑌) +
1))(1 / 𝑘) −
(log‘((⌊‘𝑌) + 1))) ∈ (γ[,]1) →
(Σ𝑘 ∈
(1...((⌊‘𝑌) +
1))(1 / 𝑘) −
(log‘((⌊‘𝑌) + 1))) ≤ 1) | 
| 207 | 204, 206 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) − (log‘((⌊‘𝑌) + 1))) ≤
1) | 
| 208 | 198, 200,
44 | lesubaddd 11860 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((Σ𝑘 ∈
(1...((⌊‘𝑌) +
1))(1 / 𝑘) −
(log‘((⌊‘𝑌) + 1))) ≤ 1 ↔ Σ𝑘 ∈
(1...((⌊‘𝑌) +
1))(1 / 𝑘) ≤ (1 +
(log‘((⌊‘𝑌) + 1))))) | 
| 209 | 207, 208 | mpbid 232 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) ≤ (1 + (log‘((⌊‘𝑌) + 1)))) | 
| 210 |  | readdcl 11238 | . . . . . . . . . . . . . . . . . 18
⊢ ((1
∈ ℝ ∧ (log‘𝑌) ∈ ℝ) → (1 +
(log‘𝑌)) ∈
ℝ) | 
| 211 | 43, 94, 210 | sylancr 587 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (1 + (log‘𝑌)) ∈
ℝ) | 
| 212 |  | peano2re 11434 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((⌊‘𝑌)
∈ ℝ → ((⌊‘𝑌) + 1) ∈ ℝ) | 
| 213 | 145, 212 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((⌊‘𝑌) + 1) ∈
ℝ) | 
| 214 | 3, 65 | remulcld 11291 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (2 · 𝑌) ∈
ℝ) | 
| 215 |  | epr 16244 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ e ∈
ℝ+ | 
| 216 |  | rpmulcl 13058 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((e
∈ ℝ+ ∧ 𝑌 ∈ ℝ+) → (e
· 𝑌) ∈
ℝ+) | 
| 217 | 215, 93, 216 | sylancr 587 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (e · 𝑌) ∈
ℝ+) | 
| 218 | 217 | rpred 13077 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (e · 𝑌) ∈
ℝ) | 
| 219 |  | flle 13839 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑌 ∈ ℝ →
(⌊‘𝑌) ≤
𝑌) | 
| 220 | 65, 219 | syl 17 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (⌊‘𝑌) ≤ 𝑌) | 
| 221 | 12, 10 | rpdivcld 13094 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (2 / 𝐸) ∈
ℝ+) | 
| 222 |  | efgt1 16152 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((2 /
𝐸) ∈
ℝ+ → 1 < (exp‘(2 / 𝐸))) | 
| 223 | 221, 222 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 1 < (exp‘(2 /
𝐸))) | 
| 224 | 223, 66 | breqtrrdi 5185 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 1 < 𝑋) | 
| 225 | 44, 70, 65, 224, 78 | lttrd 11422 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 1 < 𝑌) | 
| 226 | 44, 65, 225 | ltled 11409 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 1 ≤ 𝑌) | 
| 227 | 145, 44, 65, 65, 220, 226 | le2addd 11882 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((⌊‘𝑌) + 1) ≤ (𝑌 + 𝑌)) | 
| 228 | 112 | 2timesd 12509 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (2 · 𝑌) = (𝑌 + 𝑌)) | 
| 229 | 227, 228 | breqtrrd 5171 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((⌊‘𝑌) + 1) ≤ (2 · 𝑌)) | 
| 230 |  | ere 16125 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ e ∈
ℝ | 
| 231 |  | egt2lt3 16242 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (2 < e
∧ e < 3) | 
| 232 | 231 | simpli 483 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ 2 <
e | 
| 233 | 2, 230, 232 | ltleii 11384 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 ≤
e | 
| 234 | 233 | a1i 11 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 2 ≤ e) | 
| 235 | 230 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → e ∈
ℝ) | 
| 236 |  | lemul1 12119 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((2
∈ ℝ ∧ e ∈ ℝ ∧ (𝑌 ∈ ℝ ∧ 0 < 𝑌)) → (2 ≤ e ↔ (2
· 𝑌) ≤ (e
· 𝑌))) | 
| 237 | 3, 235, 65, 79, 236 | syl112anc 1376 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (2 ≤ e ↔ (2
· 𝑌) ≤ (e
· 𝑌))) | 
| 238 | 234, 237 | mpbid 232 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (2 · 𝑌) ≤ (e · 𝑌)) | 
| 239 | 213, 214,
218, 229, 238 | letrd 11418 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((⌊‘𝑌) + 1) ≤ (e · 𝑌)) | 
| 240 | 199, 217 | logled 26669 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (((⌊‘𝑌) + 1) ≤ (e · 𝑌) ↔
(log‘((⌊‘𝑌) + 1)) ≤ (log‘(e · 𝑌)))) | 
| 241 | 239, 240 | mpbid 232 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 →
(log‘((⌊‘𝑌) + 1)) ≤ (log‘(e · 𝑌))) | 
| 242 |  | relogmul 26634 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((e
∈ ℝ+ ∧ 𝑌 ∈ ℝ+) →
(log‘(e · 𝑌))
= ((log‘e) + (log‘𝑌))) | 
| 243 | 215, 93, 242 | sylancr 587 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (log‘(e ·
𝑌)) = ((log‘e) +
(log‘𝑌))) | 
| 244 |  | loge 26628 | . . . . . . . . . . . . . . . . . . . 20
⊢
(log‘e) = 1 | 
| 245 | 244 | oveq1i 7441 | . . . . . . . . . . . . . . . . . . 19
⊢
((log‘e) + (log‘𝑌)) = (1 + (log‘𝑌)) | 
| 246 | 243, 245 | eqtrdi 2793 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (log‘(e ·
𝑌)) = (1 + (log‘𝑌))) | 
| 247 | 241, 246 | breqtrd 5169 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 →
(log‘((⌊‘𝑌) + 1)) ≤ (1 + (log‘𝑌))) | 
| 248 | 200, 211,
44, 247 | leadd2dd 11878 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1 +
(log‘((⌊‘𝑌) + 1))) ≤ (1 + (1 + (log‘𝑌)))) | 
| 249 |  | df-2 12329 | . . . . . . . . . . . . . . . . . 18
⊢ 2 = (1 +
1) | 
| 250 | 249 | oveq1i 7441 | . . . . . . . . . . . . . . . . 17
⊢ (2 +
(log‘𝑌)) = ((1 + 1) +
(log‘𝑌)) | 
| 251 | 139 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 1 ∈
ℂ) | 
| 252 | 251, 251,
95 | addassd 11283 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((1 + 1) +
(log‘𝑌)) = (1 + (1 +
(log‘𝑌)))) | 
| 253 | 250, 252 | eqtrid 2789 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2 + (log‘𝑌)) = (1 + (1 + (log‘𝑌)))) | 
| 254 | 248, 253 | breqtrrd 5171 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (1 +
(log‘((⌊‘𝑌) + 1))) ≤ (2 + (log‘𝑌))) | 
| 255 | 198, 202,
109, 209, 254 | letrd 11418 | . . . . . . . . . . . . . 14
⊢ (𝜑 → Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) ≤ (2 + (log‘𝑌))) | 
| 256 | 197, 255 | eqbrtrrd 5167 | . . . . . . . . . . . . 13
⊢ (𝜑 → Σ𝑛 ∈ (0...(⌊‘𝑌))(1 / (𝑛 + 1)) ≤ (2 + (log‘𝑌))) | 
| 257 | 106, 109,
90, 256 | leadd1dd 11877 | . . . . . . . . . . . 12
⊢ (𝜑 → (Σ𝑛 ∈ (0...(⌊‘𝑌))(1 / (𝑛 + 1)) + Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1))) ≤ ((2 + (log‘𝑌)) + Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1)))) | 
| 258 | 99, 107, 110, 185, 257 | letrd 11418 | . . . . . . . . . . 11
⊢ (𝜑 → (log‘(𝐾 · 𝑌)) ≤ ((2 + (log‘𝑌)) + Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1)))) | 
| 259 | 97, 258 | eqbrtrrd 5167 | . . . . . . . . . 10
⊢ (𝜑 → ((log‘𝐾) + (log‘𝑌)) ≤ ((2 + (log‘𝑌)) + Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1)))) | 
| 260 | 98, 109, 90 | lesubadd2d 11862 | . . . . . . . . . 10
⊢ (𝜑 → ((((log‘𝐾) + (log‘𝑌)) − (2 + (log‘𝑌))) ≤ Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1)) ↔ ((log‘𝐾) + (log‘𝑌)) ≤ ((2 + (log‘𝑌)) + Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1))))) | 
| 261 | 259, 260 | mpbird 257 | . . . . . . . . 9
⊢ (𝜑 → (((log‘𝐾) + (log‘𝑌)) − (2 + (log‘𝑌))) ≤ Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1))) | 
| 262 | 96, 261 | eqbrtrrd 5167 | . . . . . . . 8
⊢ (𝜑 → ((log‘𝐾) − 2) ≤ Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1))) | 
| 263 | 89 | recnd 11289 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (1 / (𝑛 + 1)) ∈ ℂ) | 
| 264 | 62, 26, 263 | fsummulc2 15820 | . . . . . . . . . 10
⊢ (𝜑 → (𝐸 · Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1))) = Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝐸 · (1 / (𝑛 + 1)))) | 
| 265 | 6 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝐸 ∈ ℝ) | 
| 266 | 265 | recnd 11289 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝐸 ∈ ℂ) | 
| 267 | 88 | nncnd 12282 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑛 + 1) ∈ ℂ) | 
| 268 | 88 | nnne0d 12316 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑛 + 1) ≠ 0) | 
| 269 | 266, 267,
268 | divrecd 12046 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝐸 / (𝑛 + 1)) = (𝐸 · (1 / (𝑛 + 1)))) | 
| 270 | 265, 88 | nndivred 12320 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝐸 / (𝑛 + 1)) ∈ ℝ) | 
| 271 | 269, 270 | eqeltrrd 2842 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝐸 · (1 / (𝑛 + 1))) ∈ ℝ) | 
| 272 | 62, 271 | fsumrecl 15770 | . . . . . . . . . . 11
⊢ (𝜑 → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝐸 · (1 / (𝑛 + 1))) ∈ ℝ) | 
| 273 | 87 | nnrpd 13075 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑛 ∈ ℝ+) | 
| 274 |  | pntpbnd.r | . . . . . . . . . . . . . . . . . 18
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦
((ψ‘𝑎) −
𝑎)) | 
| 275 | 274 | pntrf 27607 | . . . . . . . . . . . . . . . . 17
⊢ 𝑅:ℝ+⟶ℝ | 
| 276 | 275 | ffvelcdmi 7103 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℝ+
→ (𝑅‘𝑛) ∈
ℝ) | 
| 277 | 273, 276 | syl 17 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑅‘𝑛) ∈ ℝ) | 
| 278 | 87, 88 | nnmulcld 12319 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑛 · (𝑛 + 1)) ∈ ℕ) | 
| 279 | 277, 278 | nndivred 12320 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) | 
| 280 | 279 | recnd 11289 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ) | 
| 281 | 280 | abscld 15475 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ ℝ) | 
| 282 | 62, 281 | fsumrecl 15770 | . . . . . . . . . . 11
⊢ (𝜑 → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ ℝ) | 
| 283 | 277, 87 | nndivred 12320 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((𝑅‘𝑛) / 𝑛) ∈ ℝ) | 
| 284 | 283 | recnd 11289 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((𝑅‘𝑛) / 𝑛) ∈ ℂ) | 
| 285 | 284 | abscld 15475 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (abs‘((𝑅‘𝑛) / 𝑛)) ∈ ℝ) | 
| 286 | 88 | nnrpd 13075 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑛 + 1) ∈
ℝ+) | 
| 287 |  | pntpbnd1.3 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ¬ ∃𝑦 ∈ ℕ ((𝑌 < 𝑦 ∧ 𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝐸)) | 
| 288 | 287 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ¬ ∃𝑦 ∈ ℕ ((𝑌 < 𝑦 ∧ 𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝐸)) | 
| 289 |  | elfzle1 13567 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌))) → ((⌊‘𝑌) + 1) ≤ 𝑛) | 
| 290 | 289 | adantl 481 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((⌊‘𝑌) + 1) ≤ 𝑛) | 
| 291 | 65 | adantr 480 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑌 ∈ ℝ) | 
| 292 | 291 | flcld 13838 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (⌊‘𝑌) ∈ ℤ) | 
| 293 | 87 | nnzd 12640 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑛 ∈ ℤ) | 
| 294 |  | zltp1le 12667 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((⌊‘𝑌)
∈ ℤ ∧ 𝑛
∈ ℤ) → ((⌊‘𝑌) < 𝑛 ↔ ((⌊‘𝑌) + 1) ≤ 𝑛)) | 
| 295 | 292, 293,
294 | syl2anc 584 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((⌊‘𝑌) < 𝑛 ↔ ((⌊‘𝑌) + 1) ≤ 𝑛)) | 
| 296 | 290, 295 | mpbird 257 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (⌊‘𝑌) < 𝑛) | 
| 297 |  | fllt 13846 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑌 ∈ ℝ ∧ 𝑛 ∈ ℤ) → (𝑌 < 𝑛 ↔ (⌊‘𝑌) < 𝑛)) | 
| 298 | 291, 293,
297 | syl2anc 584 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑌 < 𝑛 ↔ (⌊‘𝑌) < 𝑛)) | 
| 299 | 296, 298 | mpbird 257 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑌 < 𝑛) | 
| 300 |  | elfzle2 13568 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌))) → 𝑛 ≤ (⌊‘(𝐾 · 𝑌))) | 
| 301 | 300 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑛 ≤ (⌊‘(𝐾 · 𝑌))) | 
| 302 | 111 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝐾 · 𝑌) ∈ ℝ) | 
| 303 |  | flge 13845 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝐾 · 𝑌) ∈ ℝ ∧ 𝑛 ∈ ℤ) → (𝑛 ≤ (𝐾 · 𝑌) ↔ 𝑛 ≤ (⌊‘(𝐾 · 𝑌)))) | 
| 304 | 302, 293,
303 | syl2anc 584 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑛 ≤ (𝐾 · 𝑌) ↔ 𝑛 ≤ (⌊‘(𝐾 · 𝑌)))) | 
| 305 | 301, 304 | mpbird 257 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑛 ≤ (𝐾 · 𝑌)) | 
| 306 |  | breq2 5147 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = 𝑛 → (𝑌 < 𝑦 ↔ 𝑌 < 𝑛)) | 
| 307 |  | breq1 5146 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = 𝑛 → (𝑦 ≤ (𝐾 · 𝑌) ↔ 𝑛 ≤ (𝐾 · 𝑌))) | 
| 308 | 306, 307 | anbi12d 632 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑛 → ((𝑌 < 𝑦 ∧ 𝑦 ≤ (𝐾 · 𝑌)) ↔ (𝑌 < 𝑛 ∧ 𝑛 ≤ (𝐾 · 𝑌)))) | 
| 309 |  | fveq2 6906 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 = 𝑛 → (𝑅‘𝑦) = (𝑅‘𝑛)) | 
| 310 |  | id 22 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 = 𝑛 → 𝑦 = 𝑛) | 
| 311 | 309, 310 | oveq12d 7449 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = 𝑛 → ((𝑅‘𝑦) / 𝑦) = ((𝑅‘𝑛) / 𝑛)) | 
| 312 | 311 | fveq2d 6910 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = 𝑛 → (abs‘((𝑅‘𝑦) / 𝑦)) = (abs‘((𝑅‘𝑛) / 𝑛))) | 
| 313 | 312 | breq1d 5153 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑛 → ((abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝐸 ↔ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ 𝐸)) | 
| 314 | 308, 313 | anbi12d 632 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑛 → (((𝑌 < 𝑦 ∧ 𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝐸) ↔ ((𝑌 < 𝑛 ∧ 𝑛 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ 𝐸))) | 
| 315 | 314 | rspcev 3622 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈ ℕ ∧ ((𝑌 < 𝑛 ∧ 𝑛 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ 𝐸)) → ∃𝑦 ∈ ℕ ((𝑌 < 𝑦 ∧ 𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝐸)) | 
| 316 | 315 | expr 456 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ ℕ ∧ (𝑌 < 𝑛 ∧ 𝑛 ≤ (𝐾 · 𝑌))) → ((abs‘((𝑅‘𝑛) / 𝑛)) ≤ 𝐸 → ∃𝑦 ∈ ℕ ((𝑌 < 𝑦 ∧ 𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝐸))) | 
| 317 | 87, 299, 305, 316 | syl12anc 837 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((abs‘((𝑅‘𝑛) / 𝑛)) ≤ 𝐸 → ∃𝑦 ∈ ℕ ((𝑌 < 𝑦 ∧ 𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝐸))) | 
| 318 | 288, 317 | mtod 198 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ¬ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ 𝐸) | 
| 319 | 285, 265 | letrid 11413 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((abs‘((𝑅‘𝑛) / 𝑛)) ≤ 𝐸 ∨ 𝐸 ≤ (abs‘((𝑅‘𝑛) / 𝑛)))) | 
| 320 | 319 | ord 865 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (¬ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ 𝐸 → 𝐸 ≤ (abs‘((𝑅‘𝑛) / 𝑛)))) | 
| 321 | 318, 320 | mpd 15 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝐸 ≤ (abs‘((𝑅‘𝑛) / 𝑛))) | 
| 322 | 265, 285,
286, 321 | lediv1dd 13135 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝐸 / (𝑛 + 1)) ≤ ((abs‘((𝑅‘𝑛) / 𝑛)) / (𝑛 + 1))) | 
| 323 | 284, 267,
268 | absdivd 15494 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (abs‘(((𝑅‘𝑛) / 𝑛) / (𝑛 + 1))) = ((abs‘((𝑅‘𝑛) / 𝑛)) / (abs‘(𝑛 + 1)))) | 
| 324 | 277 | recnd 11289 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑅‘𝑛) ∈ ℂ) | 
| 325 | 87 | nncnd 12282 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑛 ∈ ℂ) | 
| 326 | 87 | nnne0d 12316 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑛 ≠ 0) | 
| 327 | 324, 325,
267, 326, 268 | divdiv1d 12074 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (((𝑅‘𝑛) / 𝑛) / (𝑛 + 1)) = ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) | 
| 328 | 327 | fveq2d 6910 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (abs‘(((𝑅‘𝑛) / 𝑛) / (𝑛 + 1))) = (abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) | 
| 329 | 286 | rprege0d 13084 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((𝑛 + 1) ∈ ℝ ∧ 0 ≤ (𝑛 + 1))) | 
| 330 |  | absid 15335 | . . . . . . . . . . . . . . . 16
⊢ (((𝑛 + 1) ∈ ℝ ∧ 0
≤ (𝑛 + 1)) →
(abs‘(𝑛 + 1)) =
(𝑛 + 1)) | 
| 331 | 329, 330 | syl 17 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (abs‘(𝑛 + 1)) = (𝑛 + 1)) | 
| 332 | 331 | oveq2d 7447 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((abs‘((𝑅‘𝑛) / 𝑛)) / (abs‘(𝑛 + 1))) = ((abs‘((𝑅‘𝑛) / 𝑛)) / (𝑛 + 1))) | 
| 333 | 323, 328,
332 | 3eqtr3rd 2786 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((abs‘((𝑅‘𝑛) / 𝑛)) / (𝑛 + 1)) = (abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) | 
| 334 | 322, 269,
333 | 3brtr3d 5174 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝐸 · (1 / (𝑛 + 1))) ≤ (abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) | 
| 335 | 62, 271, 281, 334 | fsumle 15835 | . . . . . . . . . . 11
⊢ (𝜑 → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝐸 · (1 / (𝑛 + 1))) ≤ Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) | 
| 336 |  | pntpbnd1.2 | . . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑖 ∈ ℕ ∀𝑗 ∈ ℤ (abs‘Σ𝑦 ∈ (𝑖...𝑗)((𝑅‘𝑦) / (𝑦 · (𝑦 + 1)))) ≤ 𝐴) | 
| 337 | 274, 5, 66, 64, 15, 336, 13, 36, 287 | pntpbnd1 27630 | . . . . . . . . . . 11
⊢ (𝜑 → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝐴) | 
| 338 | 272, 282,
32, 335, 337 | letrd 11418 | . . . . . . . . . 10
⊢ (𝜑 → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝐸 · (1 / (𝑛 + 1))) ≤ 𝐴) | 
| 339 | 264, 338 | eqbrtrd 5165 | . . . . . . . . 9
⊢ (𝜑 → (𝐸 · Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1))) ≤ 𝐴) | 
| 340 | 90, 32, 10 | lemuldiv2d 13127 | . . . . . . . . 9
⊢ (𝜑 → ((𝐸 · Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1))) ≤ 𝐴 ↔ Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1)) ≤ (𝐴 / 𝐸))) | 
| 341 | 339, 340 | mpbid 232 | . . . . . . . 8
⊢ (𝜑 → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1)) ≤ (𝐴 / 𝐸)) | 
| 342 | 55, 90, 33, 262, 341 | letrd 11418 | . . . . . . 7
⊢ (𝜑 → ((log‘𝐾) − 2) ≤ (𝐴 / 𝐸)) | 
| 343 | 35, 55, 33, 61, 342 | letrd 11418 | . . . . . 6
⊢ (𝜑 → ((𝐶 / 𝐸) − 2) ≤ (𝐴 / 𝐸)) | 
| 344 | 31, 3, 33, 343 | subled 11866 | . . . . 5
⊢ (𝜑 → ((𝐶 / 𝐸) − (𝐴 / 𝐸)) ≤ 2) | 
| 345 | 29, 344 | eqbrtrd 5165 | . . . 4
⊢ (𝜑 → (2 / 𝐸) ≤ 2) | 
| 346 | 3, 10, 12, 345 | lediv23d 13145 | . . 3
⊢ (𝜑 → (2 / 2) ≤ 𝐸) | 
| 347 | 1, 346 | eqbrtrrid 5179 | . 2
⊢ (𝜑 → 1 ≤ 𝐸) | 
| 348 | 8 | simprd 495 | . . 3
⊢ (𝜑 → 𝐸 < 1) | 
| 349 |  | ltnle 11340 | . . . 4
⊢ ((𝐸 ∈ ℝ ∧ 1 ∈
ℝ) → (𝐸 < 1
↔ ¬ 1 ≤ 𝐸)) | 
| 350 | 6, 43, 349 | sylancl 586 | . . 3
⊢ (𝜑 → (𝐸 < 1 ↔ ¬ 1 ≤ 𝐸)) | 
| 351 | 348, 350 | mpbid 232 | . 2
⊢ (𝜑 → ¬ 1 ≤ 𝐸) | 
| 352 | 347, 351 | pm2.65i 194 | 1
⊢  ¬
𝜑 |