Step | Hyp | Ref
| Expression |
1 | | 2div2e1 11996 |
. . 3
⊢ (2 / 2) =
1 |
2 | | 2re 11929 |
. . . . 5
⊢ 2 ∈
ℝ |
3 | 2 | a1i 11 |
. . . 4
⊢ (𝜑 → 2 ∈
ℝ) |
4 | | ioossre 13021 |
. . . . . 6
⊢ (0(,)1)
⊆ ℝ |
5 | | pntpbnd1.e |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈ (0(,)1)) |
6 | 4, 5 | sselid 3913 |
. . . . 5
⊢ (𝜑 → 𝐸 ∈ ℝ) |
7 | | eliooord 13019 |
. . . . . . 7
⊢ (𝐸 ∈ (0(,)1) → (0 <
𝐸 ∧ 𝐸 < 1)) |
8 | 5, 7 | syl 17 |
. . . . . 6
⊢ (𝜑 → (0 < 𝐸 ∧ 𝐸 < 1)) |
9 | 8 | simpld 498 |
. . . . 5
⊢ (𝜑 → 0 < 𝐸) |
10 | 6, 9 | elrpd 12650 |
. . . 4
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
11 | | 2rp 12616 |
. . . . 5
⊢ 2 ∈
ℝ+ |
12 | 11 | a1i 11 |
. . . 4
⊢ (𝜑 → 2 ∈
ℝ+) |
13 | | pntpbnd1.c |
. . . . . . . . 9
⊢ 𝐶 = (𝐴 + 2) |
14 | 13 | oveq1i 7242 |
. . . . . . . 8
⊢ (𝐶 − 𝐴) = ((𝐴 + 2) − 𝐴) |
15 | | pntpbnd1.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈
ℝ+) |
16 | 15 | rpcnd 12655 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℂ) |
17 | | 2cn 11930 |
. . . . . . . . 9
⊢ 2 ∈
ℂ |
18 | | pncan2 11110 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 2 ∈
ℂ) → ((𝐴 + 2)
− 𝐴) =
2) |
19 | 16, 17, 18 | sylancl 589 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 + 2) − 𝐴) = 2) |
20 | 14, 19 | syl5eq 2791 |
. . . . . . 7
⊢ (𝜑 → (𝐶 − 𝐴) = 2) |
21 | 20 | oveq1d 7247 |
. . . . . 6
⊢ (𝜑 → ((𝐶 − 𝐴) / 𝐸) = (2 / 𝐸)) |
22 | | rpaddcl 12633 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 2 ∈ ℝ+) → (𝐴 + 2) ∈
ℝ+) |
23 | 15, 11, 22 | sylancl 589 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 + 2) ∈
ℝ+) |
24 | 13, 23 | eqeltrid 2843 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈
ℝ+) |
25 | 24 | rpcnd 12655 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ ℂ) |
26 | 6 | recnd 10886 |
. . . . . . 7
⊢ (𝜑 → 𝐸 ∈ ℂ) |
27 | 10 | rpne0d 12658 |
. . . . . . 7
⊢ (𝜑 → 𝐸 ≠ 0) |
28 | 25, 16, 26, 27 | divsubdird 11672 |
. . . . . 6
⊢ (𝜑 → ((𝐶 − 𝐴) / 𝐸) = ((𝐶 / 𝐸) − (𝐴 / 𝐸))) |
29 | 21, 28 | eqtr3d 2780 |
. . . . 5
⊢ (𝜑 → (2 / 𝐸) = ((𝐶 / 𝐸) − (𝐴 / 𝐸))) |
30 | 24, 10 | rpdivcld 12670 |
. . . . . . 7
⊢ (𝜑 → (𝐶 / 𝐸) ∈
ℝ+) |
31 | 30 | rpred 12653 |
. . . . . 6
⊢ (𝜑 → (𝐶 / 𝐸) ∈ ℝ) |
32 | 15 | rpred 12653 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℝ) |
33 | 32, 10 | rerpdivcld 12684 |
. . . . . 6
⊢ (𝜑 → (𝐴 / 𝐸) ∈ ℝ) |
34 | | resubcl 11167 |
. . . . . . . 8
⊢ (((𝐶 / 𝐸) ∈ ℝ ∧ 2 ∈ ℝ)
→ ((𝐶 / 𝐸) − 2) ∈
ℝ) |
35 | 31, 2, 34 | sylancl 589 |
. . . . . . 7
⊢ (𝜑 → ((𝐶 / 𝐸) − 2) ∈
ℝ) |
36 | | pntpbnd1.k |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) |
37 | 31 | reefcld 15677 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (exp‘(𝐶 / 𝐸)) ∈ ℝ) |
38 | | elicopnf 13058 |
. . . . . . . . . . . . 13
⊢
((exp‘(𝐶 /
𝐸)) ∈ ℝ →
(𝐾 ∈
((exp‘(𝐶 / 𝐸))[,)+∞) ↔ (𝐾 ∈ ℝ ∧
(exp‘(𝐶 / 𝐸)) ≤ 𝐾))) |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐾 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ↔ (𝐾 ∈ ℝ ∧ (exp‘(𝐶 / 𝐸)) ≤ 𝐾))) |
40 | 36, 39 | mpbid 235 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐾 ∈ ℝ ∧ (exp‘(𝐶 / 𝐸)) ≤ 𝐾)) |
41 | 40 | simpld 498 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈ ℝ) |
42 | | 0red 10861 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ∈
ℝ) |
43 | | 1re 10858 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ |
44 | 43 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 ∈
ℝ) |
45 | | 0lt1 11379 |
. . . . . . . . . . . 12
⊢ 0 <
1 |
46 | 45 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 < 1) |
47 | | efgt1 15705 |
. . . . . . . . . . . . 13
⊢ ((𝐶 / 𝐸) ∈ ℝ+ → 1 <
(exp‘(𝐶 / 𝐸))) |
48 | 30, 47 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 < (exp‘(𝐶 / 𝐸))) |
49 | 40 | simprd 499 |
. . . . . . . . . . . 12
⊢ (𝜑 → (exp‘(𝐶 / 𝐸)) ≤ 𝐾) |
50 | 44, 37, 41, 48, 49 | ltletrd 11017 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 < 𝐾) |
51 | 42, 44, 41, 46, 50 | lttrd 11018 |
. . . . . . . . . 10
⊢ (𝜑 → 0 < 𝐾) |
52 | 41, 51 | elrpd 12650 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈
ℝ+) |
53 | 52 | relogcld 25538 |
. . . . . . . 8
⊢ (𝜑 → (log‘𝐾) ∈
ℝ) |
54 | | resubcl 11167 |
. . . . . . . 8
⊢
(((log‘𝐾)
∈ ℝ ∧ 2 ∈ ℝ) → ((log‘𝐾) − 2) ∈
ℝ) |
55 | 53, 2, 54 | sylancl 589 |
. . . . . . 7
⊢ (𝜑 → ((log‘𝐾) − 2) ∈
ℝ) |
56 | 52 | reeflogd 25539 |
. . . . . . . . . 10
⊢ (𝜑 →
(exp‘(log‘𝐾)) =
𝐾) |
57 | 49, 56 | breqtrrd 5096 |
. . . . . . . . 9
⊢ (𝜑 → (exp‘(𝐶 / 𝐸)) ≤ (exp‘(log‘𝐾))) |
58 | | efle 15707 |
. . . . . . . . . 10
⊢ (((𝐶 / 𝐸) ∈ ℝ ∧ (log‘𝐾) ∈ ℝ) → ((𝐶 / 𝐸) ≤ (log‘𝐾) ↔ (exp‘(𝐶 / 𝐸)) ≤ (exp‘(log‘𝐾)))) |
59 | 31, 53, 58 | syl2anc 587 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐶 / 𝐸) ≤ (log‘𝐾) ↔ (exp‘(𝐶 / 𝐸)) ≤ (exp‘(log‘𝐾)))) |
60 | 57, 59 | mpbird 260 |
. . . . . . . 8
⊢ (𝜑 → (𝐶 / 𝐸) ≤ (log‘𝐾)) |
61 | 31, 53, 3, 60 | lesub1dd 11473 |
. . . . . . 7
⊢ (𝜑 → ((𝐶 / 𝐸) − 2) ≤ ((log‘𝐾) − 2)) |
62 | | fzfid 13573 |
. . . . . . . . 9
⊢ (𝜑 → (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌))) ∈ Fin) |
63 | | ioossre 13021 |
. . . . . . . . . . . . . . 15
⊢ (𝑋(,)+∞) ⊆
ℝ |
64 | | pntpbnd1.y |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑌 ∈ (𝑋(,)+∞)) |
65 | 63, 64 | sselid 3913 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑌 ∈ ℝ) |
66 | | pntpbnd1.x |
. . . . . . . . . . . . . . . . 17
⊢ 𝑋 = (exp‘(2 / 𝐸)) |
67 | | rerpdivcl 12641 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((2
∈ ℝ ∧ 𝐸
∈ ℝ+) → (2 / 𝐸) ∈ ℝ) |
68 | 2, 10, 67 | sylancr 590 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (2 / 𝐸) ∈ ℝ) |
69 | 68 | reefcld 15677 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (exp‘(2 / 𝐸)) ∈
ℝ) |
70 | 66, 69 | eqeltrid 2843 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑋 ∈ ℝ) |
71 | | efgt0 15692 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2 /
𝐸) ∈ ℝ → 0
< (exp‘(2 / 𝐸))) |
72 | 68, 71 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 0 < (exp‘(2 /
𝐸))) |
73 | 72, 66 | breqtrrdi 5110 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 0 < 𝑋) |
74 | 70 | rexrd 10908 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑋 ∈
ℝ*) |
75 | | elioopnf 13056 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑋 ∈ ℝ*
→ (𝑌 ∈ (𝑋(,)+∞) ↔ (𝑌 ∈ ℝ ∧ 𝑋 < 𝑌))) |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑌 ∈ (𝑋(,)+∞) ↔ (𝑌 ∈ ℝ ∧ 𝑋 < 𝑌))) |
77 | 64, 76 | mpbid 235 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑌 ∈ ℝ ∧ 𝑋 < 𝑌)) |
78 | 77 | simprd 499 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑋 < 𝑌) |
79 | 42, 70, 65, 73, 78 | lttrd 11018 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 < 𝑌) |
80 | 42, 65, 79 | ltled 11005 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 ≤ 𝑌) |
81 | | flge0nn0 13420 |
. . . . . . . . . . . . . 14
⊢ ((𝑌 ∈ ℝ ∧ 0 ≤
𝑌) →
(⌊‘𝑌) ∈
ℕ0) |
82 | 65, 80, 81 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (⌊‘𝑌) ∈
ℕ0) |
83 | | nn0p1nn 12154 |
. . . . . . . . . . . . 13
⊢
((⌊‘𝑌)
∈ ℕ0 → ((⌊‘𝑌) + 1) ∈ ℕ) |
84 | 82, 83 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((⌊‘𝑌) + 1) ∈
ℕ) |
85 | | elfzuz 13133 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌))) → 𝑛 ∈
(ℤ≥‘((⌊‘𝑌) + 1))) |
86 | | eluznn 12539 |
. . . . . . . . . . . 12
⊢
((((⌊‘𝑌)
+ 1) ∈ ℕ ∧ 𝑛
∈ (ℤ≥‘((⌊‘𝑌) + 1))) → 𝑛 ∈ ℕ) |
87 | 84, 85, 86 | syl2an 599 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑛 ∈ ℕ) |
88 | 87 | peano2nnd 11872 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑛 + 1) ∈ ℕ) |
89 | 88 | nnrecred 11906 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (1 / (𝑛 + 1)) ∈ ℝ) |
90 | 62, 89 | fsumrecl 15326 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1)) ∈ ℝ) |
91 | 53 | recnd 10886 |
. . . . . . . . . 10
⊢ (𝜑 → (log‘𝐾) ∈
ℂ) |
92 | | 2cnd 11933 |
. . . . . . . . . 10
⊢ (𝜑 → 2 ∈
ℂ) |
93 | 65, 79 | elrpd 12650 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑌 ∈
ℝ+) |
94 | 93 | relogcld 25538 |
. . . . . . . . . . 11
⊢ (𝜑 → (log‘𝑌) ∈
ℝ) |
95 | 94 | recnd 10886 |
. . . . . . . . . 10
⊢ (𝜑 → (log‘𝑌) ∈
ℂ) |
96 | 91, 92, 95 | pnpcan2d 11252 |
. . . . . . . . 9
⊢ (𝜑 → (((log‘𝐾) + (log‘𝑌)) − (2 + (log‘𝑌))) = ((log‘𝐾) − 2)) |
97 | 52, 93 | relogmuld 25540 |
. . . . . . . . . . 11
⊢ (𝜑 → (log‘(𝐾 · 𝑌)) = ((log‘𝐾) + (log‘𝑌))) |
98 | 53, 94 | readdcld 10887 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((log‘𝐾) + (log‘𝑌)) ∈ ℝ) |
99 | 97, 98 | eqeltrd 2839 |
. . . . . . . . . . . 12
⊢ (𝜑 → (log‘(𝐾 · 𝑌)) ∈ ℝ) |
100 | | fzfid 13573 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (0...(⌊‘𝑌)) ∈ Fin) |
101 | | elfznn0 13230 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈
(0...(⌊‘𝑌))
→ 𝑛 ∈
ℕ0) |
102 | 101 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (0...(⌊‘𝑌))) → 𝑛 ∈ ℕ0) |
103 | | nn0p1nn 12154 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ0
→ (𝑛 + 1) ∈
ℕ) |
104 | 102, 103 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (0...(⌊‘𝑌))) → (𝑛 + 1) ∈ ℕ) |
105 | 104 | nnrecred 11906 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (0...(⌊‘𝑌))) → (1 / (𝑛 + 1)) ∈ ℝ) |
106 | 100, 105 | fsumrecl 15326 |
. . . . . . . . . . . . 13
⊢ (𝜑 → Σ𝑛 ∈ (0...(⌊‘𝑌))(1 / (𝑛 + 1)) ∈ ℝ) |
107 | 106, 90 | readdcld 10887 |
. . . . . . . . . . . 12
⊢ (𝜑 → (Σ𝑛 ∈ (0...(⌊‘𝑌))(1 / (𝑛 + 1)) + Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1))) ∈ ℝ) |
108 | | readdcl 10837 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℝ ∧ (log‘𝑌) ∈ ℝ) → (2 +
(log‘𝑌)) ∈
ℝ) |
109 | 2, 94, 108 | sylancr 590 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2 + (log‘𝑌)) ∈
ℝ) |
110 | 109, 90 | readdcld 10887 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2 + (log‘𝑌)) + Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1))) ∈ ℝ) |
111 | 41, 65 | remulcld 10888 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐾 · 𝑌) ∈ ℝ) |
112 | 65 | recnd 10886 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑌 ∈ ℂ) |
113 | 112 | mulid2d 10876 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (1 · 𝑌) = 𝑌) |
114 | 44, 41, 50 | ltled 11005 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 1 ≤ 𝐾) |
115 | | lemul1 11709 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((1
∈ ℝ ∧ 𝐾
∈ ℝ ∧ (𝑌
∈ ℝ ∧ 0 < 𝑌)) → (1 ≤ 𝐾 ↔ (1 · 𝑌) ≤ (𝐾 · 𝑌))) |
116 | 44, 41, 65, 79, 115 | syl112anc 1376 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (1 ≤ 𝐾 ↔ (1 · 𝑌) ≤ (𝐾 · 𝑌))) |
117 | 114, 116 | mpbid 235 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (1 · 𝑌) ≤ (𝐾 · 𝑌)) |
118 | 113, 117 | eqbrtrrd 5092 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑌 ≤ (𝐾 · 𝑌)) |
119 | 42, 65, 111, 80, 118 | letrd 11014 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 0 ≤ (𝐾 · 𝑌)) |
120 | | flge0nn0 13420 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐾 · 𝑌) ∈ ℝ ∧ 0 ≤ (𝐾 · 𝑌)) → (⌊‘(𝐾 · 𝑌)) ∈
ℕ0) |
121 | 111, 119,
120 | syl2anc 587 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (⌊‘(𝐾 · 𝑌)) ∈
ℕ0) |
122 | | nn0p1nn 12154 |
. . . . . . . . . . . . . . . . 17
⊢
((⌊‘(𝐾
· 𝑌)) ∈
ℕ0 → ((⌊‘(𝐾 · 𝑌)) + 1) ∈ ℕ) |
123 | 121, 122 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((⌊‘(𝐾 · 𝑌)) + 1) ∈ ℕ) |
124 | 123 | nnrpd 12651 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((⌊‘(𝐾 · 𝑌)) + 1) ∈
ℝ+) |
125 | 124 | relogcld 25538 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(log‘((⌊‘(𝐾 · 𝑌)) + 1)) ∈ ℝ) |
126 | | 1zzd 12233 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 1 ∈
ℤ) |
127 | 111 | flcld 13398 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (⌊‘(𝐾 · 𝑌)) ∈ ℤ) |
128 | 127 | peano2zd 12310 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((⌊‘(𝐾 · 𝑌)) + 1) ∈ ℤ) |
129 | | elfznn 13166 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈
(1...((⌊‘(𝐾
· 𝑌)) + 1)) →
𝑘 ∈
ℕ) |
130 | 129 | adantl 485 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))) → 𝑘 ∈ ℕ) |
131 | | nnrecre 11897 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ ℕ → (1 /
𝑘) ∈
ℝ) |
132 | 131 | recnd 10886 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℕ → (1 /
𝑘) ∈
ℂ) |
133 | 130, 132 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))) → (1 / 𝑘) ∈ ℂ) |
134 | | oveq2 7240 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = (𝑛 + 1) → (1 / 𝑘) = (1 / (𝑛 + 1))) |
135 | 126, 126,
128, 133, 134 | fsumshftm 15373 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘) = Σ𝑛 ∈ ((1 −
1)...(((⌊‘(𝐾
· 𝑌)) + 1) −
1))(1 / (𝑛 +
1))) |
136 | | 1m1e0 11927 |
. . . . . . . . . . . . . . . . . . 19
⊢ (1
− 1) = 0 |
137 | 136 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (1 − 1) =
0) |
138 | 127 | zcnd 12308 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (⌊‘(𝐾 · 𝑌)) ∈ ℂ) |
139 | | ax-1cn 10812 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℂ |
140 | | pncan 11109 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((⌊‘(𝐾
· 𝑌)) ∈ ℂ
∧ 1 ∈ ℂ) → (((⌊‘(𝐾 · 𝑌)) + 1) − 1) = (⌊‘(𝐾 · 𝑌))) |
141 | 138, 139,
140 | sylancl 589 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((⌊‘(𝐾 · 𝑌)) + 1) − 1) = (⌊‘(𝐾 · 𝑌))) |
142 | 137, 141 | oveq12d 7250 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((1 −
1)...(((⌊‘(𝐾
· 𝑌)) + 1) −
1)) = (0...(⌊‘(𝐾 · 𝑌)))) |
143 | 142 | sumeq1d 15293 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → Σ𝑛 ∈ ((1 −
1)...(((⌊‘(𝐾
· 𝑌)) + 1) −
1))(1 / (𝑛 + 1)) =
Σ𝑛 ∈
(0...(⌊‘(𝐾
· 𝑌)))(1 / (𝑛 + 1))) |
144 | | reflcl 13396 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑌 ∈ ℝ →
(⌊‘𝑌) ∈
ℝ) |
145 | 65, 144 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (⌊‘𝑌) ∈
ℝ) |
146 | 145 | ltp1d 11787 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (⌊‘𝑌) < ((⌊‘𝑌) + 1)) |
147 | | fzdisj 13164 |
. . . . . . . . . . . . . . . . . 18
⊢
((⌊‘𝑌)
< ((⌊‘𝑌) +
1) → ((0...(⌊‘𝑌)) ∩ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) = ∅) |
148 | 146, 147 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((0...(⌊‘𝑌)) ∩ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) = ∅) |
149 | | flwordi 13412 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑌 ∈ ℝ ∧ (𝐾 · 𝑌) ∈ ℝ ∧ 𝑌 ≤ (𝐾 · 𝑌)) → (⌊‘𝑌) ≤ (⌊‘(𝐾 · 𝑌))) |
150 | 65, 111, 118, 149 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (⌊‘𝑌) ≤ (⌊‘(𝐾 · 𝑌))) |
151 | | elfz2nn0 13228 |
. . . . . . . . . . . . . . . . . . 19
⊢
((⌊‘𝑌)
∈ (0...(⌊‘(𝐾 · 𝑌))) ↔ ((⌊‘𝑌) ∈ ℕ0 ∧
(⌊‘(𝐾 ·
𝑌)) ∈
ℕ0 ∧ (⌊‘𝑌) ≤ (⌊‘(𝐾 · 𝑌)))) |
152 | 82, 121, 150, 151 | syl3anbrc 1345 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (⌊‘𝑌) ∈
(0...(⌊‘(𝐾
· 𝑌)))) |
153 | | fzsplit 13163 |
. . . . . . . . . . . . . . . . . 18
⊢
((⌊‘𝑌)
∈ (0...(⌊‘(𝐾 · 𝑌))) → (0...(⌊‘(𝐾 · 𝑌))) = ((0...(⌊‘𝑌)) ∪ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌))))) |
154 | 152, 153 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (0...(⌊‘(𝐾 · 𝑌))) = ((0...(⌊‘𝑌)) ∪ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌))))) |
155 | | fzfid 13573 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (0...(⌊‘(𝐾 · 𝑌))) ∈ Fin) |
156 | | elfznn0 13230 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈
(0...(⌊‘(𝐾
· 𝑌))) → 𝑛 ∈
ℕ0) |
157 | 156 | adantl 485 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ (0...(⌊‘(𝐾 · 𝑌)))) → 𝑛 ∈ ℕ0) |
158 | 157, 103 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ (0...(⌊‘(𝐾 · 𝑌)))) → (𝑛 + 1) ∈ ℕ) |
159 | 158 | nnrecred 11906 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ (0...(⌊‘(𝐾 · 𝑌)))) → (1 / (𝑛 + 1)) ∈ ℝ) |
160 | 159 | recnd 10886 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (0...(⌊‘(𝐾 · 𝑌)))) → (1 / (𝑛 + 1)) ∈ ℂ) |
161 | 148, 154,
155, 160 | fsumsplit 15333 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → Σ𝑛 ∈ (0...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1)) = (Σ𝑛 ∈ (0...(⌊‘𝑌))(1 / (𝑛 + 1)) + Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1)))) |
162 | 135, 143,
161 | 3eqtrd 2782 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘) = (Σ𝑛 ∈ (0...(⌊‘𝑌))(1 / (𝑛 + 1)) + Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1)))) |
163 | 162, 107 | eqeltrd 2839 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘) ∈ ℝ) |
164 | | fllep1 13401 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐾 · 𝑌) ∈ ℝ → (𝐾 · 𝑌) ≤ ((⌊‘(𝐾 · 𝑌)) + 1)) |
165 | 111, 164 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐾 · 𝑌) ≤ ((⌊‘(𝐾 · 𝑌)) + 1)) |
166 | 52, 93 | rpmulcld 12669 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐾 · 𝑌) ∈
ℝ+) |
167 | 166, 124 | logled 25542 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐾 · 𝑌) ≤ ((⌊‘(𝐾 · 𝑌)) + 1) ↔ (log‘(𝐾 · 𝑌)) ≤ (log‘((⌊‘(𝐾 · 𝑌)) + 1)))) |
168 | 165, 167 | mpbid 235 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (log‘(𝐾 · 𝑌)) ≤ (log‘((⌊‘(𝐾 · 𝑌)) + 1))) |
169 | | emre 25915 |
. . . . . . . . . . . . . . . . 17
⊢ γ
∈ ℝ |
170 | 169 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → γ ∈
ℝ) |
171 | 163, 125 | resubcld 11285 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘) − (log‘((⌊‘(𝐾 · 𝑌)) + 1))) ∈ ℝ) |
172 | | 0re 10860 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
ℝ |
173 | | emgt0 25916 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 <
γ |
174 | 172, 169,
173 | ltleii 10980 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ≤
γ |
175 | 174 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 0 ≤
γ) |
176 | | harmonicbnd 25913 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⌊‘(𝐾
· 𝑌)) + 1) ∈
ℕ → (Σ𝑘
∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘) − (log‘((⌊‘(𝐾 · 𝑌)) + 1))) ∈
(γ[,]1)) |
177 | 123, 176 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘) − (log‘((⌊‘(𝐾 · 𝑌)) + 1))) ∈
(γ[,]1)) |
178 | 169, 43 | elicc2i 13026 |
. . . . . . . . . . . . . . . . . 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 1148 |
. . . . . . . . . . . . . . . . 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 11014 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 ≤ (Σ𝑘 ∈
(1...((⌊‘(𝐾
· 𝑌)) + 1))(1 /
𝑘) −
(log‘((⌊‘(𝐾 · 𝑌)) + 1)))) |
182 | 163, 125 | subge0d 11447 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (0 ≤ (Σ𝑘 ∈
(1...((⌊‘(𝐾
· 𝑌)) + 1))(1 /
𝑘) −
(log‘((⌊‘(𝐾 · 𝑌)) + 1))) ↔
(log‘((⌊‘(𝐾 · 𝑌)) + 1)) ≤ Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘))) |
183 | 181, 182 | mpbid 235 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(log‘((⌊‘(𝐾 · 𝑌)) + 1)) ≤ Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘)) |
184 | 99, 125, 163, 168, 183 | letrd 11014 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (log‘(𝐾 · 𝑌)) ≤ Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘)) |
185 | 184, 162 | breqtrd 5094 |
. . . . . . . . . . . 12
⊢ (𝜑 → (log‘(𝐾 · 𝑌)) ≤ (Σ𝑛 ∈ (0...(⌊‘𝑌))(1 / (𝑛 + 1)) + Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1)))) |
186 | 65 | flcld 13398 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (⌊‘𝑌) ∈
ℤ) |
187 | 186 | peano2zd 12310 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((⌊‘𝑌) + 1) ∈
ℤ) |
188 | | elfznn 13166 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈
(1...((⌊‘𝑌) +
1)) → 𝑘 ∈
ℕ) |
189 | 188 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (1...((⌊‘𝑌) + 1))) → 𝑘 ∈
ℕ) |
190 | 189, 132 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (1...((⌊‘𝑌) + 1))) → (1 / 𝑘) ∈
ℂ) |
191 | 126, 126,
187, 190, 134 | fsumshftm 15373 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) = Σ𝑛 ∈ ((1 −
1)...(((⌊‘𝑌) +
1) − 1))(1 / (𝑛 +
1))) |
192 | 145 | recnd 10886 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (⌊‘𝑌) ∈
ℂ) |
193 | | pncan 11109 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⌊‘𝑌)
∈ ℂ ∧ 1 ∈ ℂ) → (((⌊‘𝑌) + 1) − 1) =
(⌊‘𝑌)) |
194 | 192, 139,
193 | sylancl 589 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((⌊‘𝑌) + 1) − 1) =
(⌊‘𝑌)) |
195 | 137, 194 | oveq12d 7250 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((1 −
1)...(((⌊‘𝑌) +
1) − 1)) = (0...(⌊‘𝑌))) |
196 | 195 | sumeq1d 15293 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → Σ𝑛 ∈ ((1 −
1)...(((⌊‘𝑌) +
1) − 1))(1 / (𝑛 + 1))
= Σ𝑛 ∈
(0...(⌊‘𝑌))(1 /
(𝑛 + 1))) |
197 | 191, 196 | eqtrd 2778 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) = Σ𝑛 ∈ (0...(⌊‘𝑌))(1 / (𝑛 + 1))) |
198 | 197, 106 | eqeltrd 2839 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) ∈ ℝ) |
199 | 84 | nnrpd 12651 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((⌊‘𝑌) + 1) ∈
ℝ+) |
200 | 199 | relogcld 25538 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 →
(log‘((⌊‘𝑌) + 1)) ∈ ℝ) |
201 | | readdcl 10837 |
. . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℝ ∧ (log‘((⌊‘𝑌) + 1)) ∈ ℝ) → (1 +
(log‘((⌊‘𝑌) + 1))) ∈ ℝ) |
202 | 43, 200, 201 | sylancr 590 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1 +
(log‘((⌊‘𝑌) + 1))) ∈ ℝ) |
203 | | harmonicbnd 25913 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⌊‘𝑌)
+ 1) ∈ ℕ → (Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) − (log‘((⌊‘𝑌) + 1))) ∈
(γ[,]1)) |
204 | 84, 203 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) − (log‘((⌊‘𝑌) + 1))) ∈
(γ[,]1)) |
205 | 169, 43 | elicc2i 13026 |
. . . . . . . . . . . . . . . . . 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 1149 |
. . . . . . . . . . . . . . . . 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 11454 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((Σ𝑘 ∈
(1...((⌊‘𝑌) +
1))(1 / 𝑘) −
(log‘((⌊‘𝑌) + 1))) ≤ 1 ↔ Σ𝑘 ∈
(1...((⌊‘𝑌) +
1))(1 / 𝑘) ≤ (1 +
(log‘((⌊‘𝑌) + 1))))) |
209 | 207, 208 | mpbid 235 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) ≤ (1 + (log‘((⌊‘𝑌) + 1)))) |
210 | | readdcl 10837 |
. . . . . . . . . . . . . . . . . 18
⊢ ((1
∈ ℝ ∧ (log‘𝑌) ∈ ℝ) → (1 +
(log‘𝑌)) ∈
ℝ) |
211 | 43, 94, 210 | sylancr 590 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (1 + (log‘𝑌)) ∈
ℝ) |
212 | | peano2re 11030 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((⌊‘𝑌)
∈ ℝ → ((⌊‘𝑌) + 1) ∈ ℝ) |
213 | 145, 212 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((⌊‘𝑌) + 1) ∈
ℝ) |
214 | 3, 65 | remulcld 10888 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (2 · 𝑌) ∈
ℝ) |
215 | | epr 15797 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ e ∈
ℝ+ |
216 | | rpmulcl 12634 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((e
∈ ℝ+ ∧ 𝑌 ∈ ℝ+) → (e
· 𝑌) ∈
ℝ+) |
217 | 215, 93, 216 | sylancr 590 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (e · 𝑌) ∈
ℝ+) |
218 | 217 | rpred 12653 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (e · 𝑌) ∈
ℝ) |
219 | | flle 13399 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑌 ∈ ℝ →
(⌊‘𝑌) ≤
𝑌) |
220 | 65, 219 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (⌊‘𝑌) ≤ 𝑌) |
221 | 12, 10 | rpdivcld 12670 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (2 / 𝐸) ∈
ℝ+) |
222 | | efgt1 15705 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((2 /
𝐸) ∈
ℝ+ → 1 < (exp‘(2 / 𝐸))) |
223 | 221, 222 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 1 < (exp‘(2 /
𝐸))) |
224 | 223, 66 | breqtrrdi 5110 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 1 < 𝑋) |
225 | 44, 70, 65, 224, 78 | lttrd 11018 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 1 < 𝑌) |
226 | 44, 65, 225 | ltled 11005 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 1 ≤ 𝑌) |
227 | 145, 44, 65, 65, 220, 226 | le2addd 11476 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((⌊‘𝑌) + 1) ≤ (𝑌 + 𝑌)) |
228 | 112 | 2timesd 12098 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (2 · 𝑌) = (𝑌 + 𝑌)) |
229 | 227, 228 | breqtrrd 5096 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((⌊‘𝑌) + 1) ≤ (2 · 𝑌)) |
230 | | ere 15678 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ e ∈
ℝ |
231 | | egt2lt3 15795 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (2 < e
∧ e < 3) |
232 | 231 | simpli 487 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 2 <
e |
233 | 2, 230, 232 | ltleii 10980 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 ≤
e |
234 | 233 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 2 ≤ e) |
235 | 230 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → e ∈
ℝ) |
236 | | lemul1 11709 |
. . . . . . . . . . . . . . . . . . . . . 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 235 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (2 · 𝑌) ≤ (e · 𝑌)) |
239 | 213, 214,
218, 229, 238 | letrd 11014 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((⌊‘𝑌) + 1) ≤ (e · 𝑌)) |
240 | 199, 217 | logled 25542 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (((⌊‘𝑌) + 1) ≤ (e · 𝑌) ↔
(log‘((⌊‘𝑌) + 1)) ≤ (log‘(e · 𝑌)))) |
241 | 239, 240 | mpbid 235 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 →
(log‘((⌊‘𝑌) + 1)) ≤ (log‘(e · 𝑌))) |
242 | | relogmul 25507 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((e
∈ ℝ+ ∧ 𝑌 ∈ ℝ+) →
(log‘(e · 𝑌))
= ((log‘e) + (log‘𝑌))) |
243 | 215, 93, 242 | sylancr 590 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (log‘(e ·
𝑌)) = ((log‘e) +
(log‘𝑌))) |
244 | | loge 25502 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(log‘e) = 1 |
245 | 244 | oveq1i 7242 |
. . . . . . . . . . . . . . . . . . 19
⊢
((log‘e) + (log‘𝑌)) = (1 + (log‘𝑌)) |
246 | 243, 245 | eqtrdi 2795 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (log‘(e ·
𝑌)) = (1 + (log‘𝑌))) |
247 | 241, 246 | breqtrd 5094 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 →
(log‘((⌊‘𝑌) + 1)) ≤ (1 + (log‘𝑌))) |
248 | 200, 211,
44, 247 | leadd2dd 11472 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1 +
(log‘((⌊‘𝑌) + 1))) ≤ (1 + (1 + (log‘𝑌)))) |
249 | | df-2 11918 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 = (1 +
1) |
250 | 249 | oveq1i 7242 |
. . . . . . . . . . . . . . . . 17
⊢ (2 +
(log‘𝑌)) = ((1 + 1) +
(log‘𝑌)) |
251 | 139 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 1 ∈
ℂ) |
252 | 251, 251,
95 | addassd 10880 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((1 + 1) +
(log‘𝑌)) = (1 + (1 +
(log‘𝑌)))) |
253 | 250, 252 | syl5eq 2791 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2 + (log‘𝑌)) = (1 + (1 + (log‘𝑌)))) |
254 | 248, 253 | breqtrrd 5096 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1 +
(log‘((⌊‘𝑌) + 1))) ≤ (2 + (log‘𝑌))) |
255 | 198, 202,
109, 209, 254 | letrd 11014 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) ≤ (2 + (log‘𝑌))) |
256 | 197, 255 | eqbrtrrd 5092 |
. . . . . . . . . . . . 13
⊢ (𝜑 → Σ𝑛 ∈ (0...(⌊‘𝑌))(1 / (𝑛 + 1)) ≤ (2 + (log‘𝑌))) |
257 | 106, 109,
90, 256 | leadd1dd 11471 |
. . . . . . . . . . . 12
⊢ (𝜑 → (Σ𝑛 ∈ (0...(⌊‘𝑌))(1 / (𝑛 + 1)) + Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1))) ≤ ((2 + (log‘𝑌)) + Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1)))) |
258 | 99, 107, 110, 185, 257 | letrd 11014 |
. . . . . . . . . . 11
⊢ (𝜑 → (log‘(𝐾 · 𝑌)) ≤ ((2 + (log‘𝑌)) + Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1)))) |
259 | 97, 258 | eqbrtrrd 5092 |
. . . . . . . . . 10
⊢ (𝜑 → ((log‘𝐾) + (log‘𝑌)) ≤ ((2 + (log‘𝑌)) + Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1)))) |
260 | 98, 109, 90 | lesubadd2d 11456 |
. . . . . . . . . 10
⊢ (𝜑 → ((((log‘𝐾) + (log‘𝑌)) − (2 + (log‘𝑌))) ≤ Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1)) ↔ ((log‘𝐾) + (log‘𝑌)) ≤ ((2 + (log‘𝑌)) + Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1))))) |
261 | 259, 260 | mpbird 260 |
. . . . . . . . 9
⊢ (𝜑 → (((log‘𝐾) + (log‘𝑌)) − (2 + (log‘𝑌))) ≤ Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1))) |
262 | 96, 261 | eqbrtrrd 5092 |
. . . . . . . 8
⊢ (𝜑 → ((log‘𝐾) − 2) ≤ Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1))) |
263 | 89 | recnd 10886 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (1 / (𝑛 + 1)) ∈ ℂ) |
264 | 62, 26, 263 | fsummulc2 15376 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐸 · Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1))) = Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝐸 · (1 / (𝑛 + 1)))) |
265 | 6 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝐸 ∈ ℝ) |
266 | 265 | recnd 10886 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝐸 ∈ ℂ) |
267 | 88 | nncnd 11871 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑛 + 1) ∈ ℂ) |
268 | 88 | nnne0d 11905 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑛 + 1) ≠ 0) |
269 | 266, 267,
268 | divrecd 11636 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝐸 / (𝑛 + 1)) = (𝐸 · (1 / (𝑛 + 1)))) |
270 | 265, 88 | nndivred 11909 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝐸 / (𝑛 + 1)) ∈ ℝ) |
271 | 269, 270 | eqeltrrd 2840 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝐸 · (1 / (𝑛 + 1))) ∈ ℝ) |
272 | 62, 271 | fsumrecl 15326 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝐸 · (1 / (𝑛 + 1))) ∈ ℝ) |
273 | 87 | nnrpd 12651 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑛 ∈ ℝ+) |
274 | | pntpbnd.r |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦
((ψ‘𝑎) −
𝑎)) |
275 | 274 | pntrf 26471 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑅:ℝ+⟶ℝ |
276 | 275 | ffvelrni 6922 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℝ+
→ (𝑅‘𝑛) ∈
ℝ) |
277 | 273, 276 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑅‘𝑛) ∈ ℝ) |
278 | 87, 88 | nnmulcld 11908 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑛 · (𝑛 + 1)) ∈ ℕ) |
279 | 277, 278 | nndivred 11909 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) |
280 | 279 | recnd 10886 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ) |
281 | 280 | abscld 15028 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ ℝ) |
282 | 62, 281 | fsumrecl 15326 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ ℝ) |
283 | 277, 87 | nndivred 11909 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((𝑅‘𝑛) / 𝑛) ∈ ℝ) |
284 | 283 | recnd 10886 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((𝑅‘𝑛) / 𝑛) ∈ ℂ) |
285 | 284 | abscld 15028 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (abs‘((𝑅‘𝑛) / 𝑛)) ∈ ℝ) |
286 | 88 | nnrpd 12651 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑛 + 1) ∈
ℝ+) |
287 | | pntpbnd1.3 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ¬ ∃𝑦 ∈ ℕ ((𝑌 < 𝑦 ∧ 𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝐸)) |
288 | 287 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ¬ ∃𝑦 ∈ ℕ ((𝑌 < 𝑦 ∧ 𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝐸)) |
289 | | elfzle1 13140 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌))) → ((⌊‘𝑌) + 1) ≤ 𝑛) |
290 | 289 | adantl 485 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((⌊‘𝑌) + 1) ≤ 𝑛) |
291 | 65 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑌 ∈ ℝ) |
292 | 291 | flcld 13398 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (⌊‘𝑌) ∈ ℤ) |
293 | 87 | nnzd 12306 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑛 ∈ ℤ) |
294 | | zltp1le 12252 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((⌊‘𝑌)
∈ ℤ ∧ 𝑛
∈ ℤ) → ((⌊‘𝑌) < 𝑛 ↔ ((⌊‘𝑌) + 1) ≤ 𝑛)) |
295 | 292, 293,
294 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((⌊‘𝑌) < 𝑛 ↔ ((⌊‘𝑌) + 1) ≤ 𝑛)) |
296 | 290, 295 | mpbird 260 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (⌊‘𝑌) < 𝑛) |
297 | | fllt 13406 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑌 ∈ ℝ ∧ 𝑛 ∈ ℤ) → (𝑌 < 𝑛 ↔ (⌊‘𝑌) < 𝑛)) |
298 | 291, 293,
297 | syl2anc 587 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑌 < 𝑛 ↔ (⌊‘𝑌) < 𝑛)) |
299 | 296, 298 | mpbird 260 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑌 < 𝑛) |
300 | | elfzle2 13141 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌))) → 𝑛 ≤ (⌊‘(𝐾 · 𝑌))) |
301 | 300 | adantl 485 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑛 ≤ (⌊‘(𝐾 · 𝑌))) |
302 | 111 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝐾 · 𝑌) ∈ ℝ) |
303 | | flge 13405 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐾 · 𝑌) ∈ ℝ ∧ 𝑛 ∈ ℤ) → (𝑛 ≤ (𝐾 · 𝑌) ↔ 𝑛 ≤ (⌊‘(𝐾 · 𝑌)))) |
304 | 302, 293,
303 | syl2anc 587 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑛 ≤ (𝐾 · 𝑌) ↔ 𝑛 ≤ (⌊‘(𝐾 · 𝑌)))) |
305 | 301, 304 | mpbird 260 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑛 ≤ (𝐾 · 𝑌)) |
306 | | breq2 5072 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = 𝑛 → (𝑌 < 𝑦 ↔ 𝑌 < 𝑛)) |
307 | | breq1 5071 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = 𝑛 → (𝑦 ≤ (𝐾 · 𝑌) ↔ 𝑛 ≤ (𝐾 · 𝑌))) |
308 | 306, 307 | anbi12d 634 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑛 → ((𝑌 < 𝑦 ∧ 𝑦 ≤ (𝐾 · 𝑌)) ↔ (𝑌 < 𝑛 ∧ 𝑛 ≤ (𝐾 · 𝑌)))) |
309 | | fveq2 6736 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 = 𝑛 → (𝑅‘𝑦) = (𝑅‘𝑛)) |
310 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 = 𝑛 → 𝑦 = 𝑛) |
311 | 309, 310 | oveq12d 7250 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = 𝑛 → ((𝑅‘𝑦) / 𝑦) = ((𝑅‘𝑛) / 𝑛)) |
312 | 311 | fveq2d 6740 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = 𝑛 → (abs‘((𝑅‘𝑦) / 𝑦)) = (abs‘((𝑅‘𝑛) / 𝑛))) |
313 | 312 | breq1d 5078 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑛 → ((abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝐸 ↔ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ 𝐸)) |
314 | 308, 313 | anbi12d 634 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑛 → (((𝑌 < 𝑦 ∧ 𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝐸) ↔ ((𝑌 < 𝑛 ∧ 𝑛 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ 𝐸))) |
315 | 314 | rspcev 3550 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈ ℕ ∧ ((𝑌 < 𝑛 ∧ 𝑛 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ 𝐸)) → ∃𝑦 ∈ ℕ ((𝑌 < 𝑦 ∧ 𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝐸)) |
316 | 315 | expr 460 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ ℕ ∧ (𝑌 < 𝑛 ∧ 𝑛 ≤ (𝐾 · 𝑌))) → ((abs‘((𝑅‘𝑛) / 𝑛)) ≤ 𝐸 → ∃𝑦 ∈ ℕ ((𝑌 < 𝑦 ∧ 𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝐸))) |
317 | 87, 299, 305, 316 | syl12anc 837 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((abs‘((𝑅‘𝑛) / 𝑛)) ≤ 𝐸 → ∃𝑦 ∈ ℕ ((𝑌 < 𝑦 ∧ 𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝐸))) |
318 | 288, 317 | mtod 201 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ¬ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ 𝐸) |
319 | 285, 265 | letrid 11009 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((abs‘((𝑅‘𝑛) / 𝑛)) ≤ 𝐸 ∨ 𝐸 ≤ (abs‘((𝑅‘𝑛) / 𝑛)))) |
320 | 319 | ord 864 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (¬ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ 𝐸 → 𝐸 ≤ (abs‘((𝑅‘𝑛) / 𝑛)))) |
321 | 318, 320 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝐸 ≤ (abs‘((𝑅‘𝑛) / 𝑛))) |
322 | 265, 285,
286, 321 | lediv1dd 12711 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝐸 / (𝑛 + 1)) ≤ ((abs‘((𝑅‘𝑛) / 𝑛)) / (𝑛 + 1))) |
323 | 284, 267,
268 | absdivd 15047 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (abs‘(((𝑅‘𝑛) / 𝑛) / (𝑛 + 1))) = ((abs‘((𝑅‘𝑛) / 𝑛)) / (abs‘(𝑛 + 1)))) |
324 | 277 | recnd 10886 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑅‘𝑛) ∈ ℂ) |
325 | 87 | nncnd 11871 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑛 ∈ ℂ) |
326 | 87 | nnne0d 11905 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑛 ≠ 0) |
327 | 324, 325,
267, 326, 268 | divdiv1d 11664 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (((𝑅‘𝑛) / 𝑛) / (𝑛 + 1)) = ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
328 | 327 | fveq2d 6740 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (abs‘(((𝑅‘𝑛) / 𝑛) / (𝑛 + 1))) = (abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
329 | 286 | rprege0d 12660 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((𝑛 + 1) ∈ ℝ ∧ 0 ≤ (𝑛 + 1))) |
330 | | absid 14888 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑛 + 1) ∈ ℝ ∧ 0
≤ (𝑛 + 1)) →
(abs‘(𝑛 + 1)) =
(𝑛 + 1)) |
331 | 329, 330 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (abs‘(𝑛 + 1)) = (𝑛 + 1)) |
332 | 331 | oveq2d 7248 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((abs‘((𝑅‘𝑛) / 𝑛)) / (abs‘(𝑛 + 1))) = ((abs‘((𝑅‘𝑛) / 𝑛)) / (𝑛 + 1))) |
333 | 323, 328,
332 | 3eqtr3rd 2787 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((abs‘((𝑅‘𝑛) / 𝑛)) / (𝑛 + 1)) = (abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
334 | 322, 269,
333 | 3brtr3d 5099 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝐸 · (1 / (𝑛 + 1))) ≤ (abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
335 | 62, 271, 281, 334 | fsumle 15391 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝐸 · (1 / (𝑛 + 1))) ≤ Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
336 | | pntpbnd1.2 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑖 ∈ ℕ ∀𝑗 ∈ ℤ (abs‘Σ𝑦 ∈ (𝑖...𝑗)((𝑅‘𝑦) / (𝑦 · (𝑦 + 1)))) ≤ 𝐴) |
337 | 274, 5, 66, 64, 15, 336, 13, 36, 287 | pntpbnd1 26494 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝐴) |
338 | 272, 282,
32, 335, 337 | letrd 11014 |
. . . . . . . . . 10
⊢ (𝜑 → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝐸 · (1 / (𝑛 + 1))) ≤ 𝐴) |
339 | 264, 338 | eqbrtrd 5090 |
. . . . . . . . 9
⊢ (𝜑 → (𝐸 · Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1))) ≤ 𝐴) |
340 | 90, 32, 10 | lemuldiv2d 12703 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐸 · Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1))) ≤ 𝐴 ↔ Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1)) ≤ (𝐴 / 𝐸))) |
341 | 339, 340 | mpbid 235 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1)) ≤ (𝐴 / 𝐸)) |
342 | 55, 90, 33, 262, 341 | letrd 11014 |
. . . . . . 7
⊢ (𝜑 → ((log‘𝐾) − 2) ≤ (𝐴 / 𝐸)) |
343 | 35, 55, 33, 61, 342 | letrd 11014 |
. . . . . 6
⊢ (𝜑 → ((𝐶 / 𝐸) − 2) ≤ (𝐴 / 𝐸)) |
344 | 31, 3, 33, 343 | subled 11460 |
. . . . 5
⊢ (𝜑 → ((𝐶 / 𝐸) − (𝐴 / 𝐸)) ≤ 2) |
345 | 29, 344 | eqbrtrd 5090 |
. . . 4
⊢ (𝜑 → (2 / 𝐸) ≤ 2) |
346 | 3, 10, 12, 345 | lediv23d 12721 |
. . 3
⊢ (𝜑 → (2 / 2) ≤ 𝐸) |
347 | 1, 346 | eqbrtrrid 5104 |
. 2
⊢ (𝜑 → 1 ≤ 𝐸) |
348 | 8 | simprd 499 |
. . 3
⊢ (𝜑 → 𝐸 < 1) |
349 | | ltnle 10937 |
. . . 4
⊢ ((𝐸 ∈ ℝ ∧ 1 ∈
ℝ) → (𝐸 < 1
↔ ¬ 1 ≤ 𝐸)) |
350 | 6, 43, 349 | sylancl 589 |
. . 3
⊢ (𝜑 → (𝐸 < 1 ↔ ¬ 1 ≤ 𝐸)) |
351 | 348, 350 | mpbid 235 |
. 2
⊢ (𝜑 → ¬ 1 ≤ 𝐸) |
352 | 347, 351 | pm2.65i 197 |
1
⊢ ¬
𝜑 |