Metamath Proof Explorer

Theorem pntpbnd2

Description: Lemma for pntpbnd . (Contributed by Mario Carneiro, 11-Apr-2016)

Ref Expression
Hypotheses pntpbnd.r ⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
pntpbnd1.e ⊢ ( 𝜑 → 𝐸 ∈ ( 0 (,) 1 ) )
pntpbnd1.x ⊢ 𝑋 = ( exp ‘ ( 2 / 𝐸 ) )
pntpbnd1.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑋 (,) +∞ ) )
pntpbnd1.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
pntpbnd1.2 ⊢ ( 𝜑 → ∀ 𝑖 ∈ ℕ ∀ 𝑗 ∈ ℤ ( abs ‘ Σ 𝑦 ∈ ( 𝑖 ... 𝑗 ) ( ( 𝑅 ‘ 𝑦 ) / ( 𝑦 · ( 𝑦 + 1 ) ) ) ) ≤ 𝐴 )
pntpbnd1.c ⊢ 𝐶 = ( 𝐴 + 2 )
pntpbnd1.k ⊢ ( 𝜑 → 𝐾 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) )
pntpbnd1.3 ⊢ ( 𝜑 → ¬ ∃ 𝑦 ∈ ℕ ( ( 𝑌 < 𝑦 ∧ 𝑦 ≤ ( 𝐾 · 𝑌 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑦 ) / 𝑦 ) ) ≤ 𝐸 ) )
Assertion pntpbnd2 ¬ 𝜑

Proof

Step Hyp Ref Expression
1 pntpbnd.r ⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
2 pntpbnd1.e ⊢ ( 𝜑 → 𝐸 ∈ ( 0 (,) 1 ) )
3 pntpbnd1.x ⊢ 𝑋 = ( exp ‘ ( 2 / 𝐸 ) )
4 pntpbnd1.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑋 (,) +∞ ) )
5 pntpbnd1.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
6 pntpbnd1.2 ⊢ ( 𝜑 → ∀ 𝑖 ∈ ℕ ∀ 𝑗 ∈ ℤ ( abs ‘ Σ 𝑦 ∈ ( 𝑖 ... 𝑗 ) ( ( 𝑅 ‘ 𝑦 ) / ( 𝑦 · ( 𝑦 + 1 ) ) ) ) ≤ 𝐴 )
7 pntpbnd1.c ⊢ 𝐶 = ( 𝐴 + 2 )
8 pntpbnd1.k ⊢ ( 𝜑 → 𝐾 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) )
9 pntpbnd1.3 ⊢ ( 𝜑 → ¬ ∃ 𝑦 ∈ ℕ ( ( 𝑌 < 𝑦 ∧ 𝑦 ≤ ( 𝐾 · 𝑌 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑦 ) / 𝑦 ) ) ≤ 𝐸 ) )
10 2div2e1 ⊢ ( 2 / 2 ) = 1
11 2re ⊢ 2 ∈ ℝ
12 11 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
13 ioossre ⊢ ( 0 (,) 1 ) ⊆ ℝ
14 13 2 sselid ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
15 eliooord ⊢ ( 𝐸 ∈ ( 0 (,) 1 ) → ( 0 < 𝐸 ∧ 𝐸 < 1 ) )
16 2 15 syl ⊢ ( 𝜑 → ( 0 < 𝐸 ∧ 𝐸 < 1 ) )
17 16 simpld ⊢ ( 𝜑 → 0 < 𝐸 )
18 14 17 elrpd ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
19 2rp ⊢ 2 ∈ ℝ+
20 19 a1i ⊢ ( 𝜑 → 2 ∈ ℝ+ )
21 7 oveq1i ⊢ ( 𝐶 − 𝐴 ) = ( ( 𝐴 + 2 ) − 𝐴 )
22 5 rpcnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
23 2cn ⊢ 2 ∈ ℂ
24 pncan2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 2 ∈ ℂ ) → ( ( 𝐴 + 2 ) − 𝐴 ) = 2 )
25 22 23 24 sylancl ⊢ ( 𝜑 → ( ( 𝐴 + 2 ) − 𝐴 ) = 2 )
26 21 25 syl5eq ⊢ ( 𝜑 → ( 𝐶 − 𝐴 ) = 2 )
27 26 oveq1d ⊢ ( 𝜑 → ( ( 𝐶 − 𝐴 ) / 𝐸 ) = ( 2 / 𝐸 ) )
28 rpaddcl ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 2 ∈ ℝ+ ) → ( 𝐴 + 2 ) ∈ ℝ+ )
29 5 19 28 sylancl ⊢ ( 𝜑 → ( 𝐴 + 2 ) ∈ ℝ+ )
30 7 29 eqeltrid ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
31 30 rpcnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
32 14 recnd ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
33 18 rpne0d ⊢ ( 𝜑 → 𝐸 ≠ 0 )
34 31 22 32 33 divsubdird ⊢ ( 𝜑 → ( ( 𝐶 − 𝐴 ) / 𝐸 ) = ( ( 𝐶 / 𝐸 ) − ( 𝐴 / 𝐸 ) ) )
35 27 34 eqtr3d ⊢ ( 𝜑 → ( 2 / 𝐸 ) = ( ( 𝐶 / 𝐸 ) − ( 𝐴 / 𝐸 ) ) )
36 30 18 rpdivcld ⊢ ( 𝜑 → ( 𝐶 / 𝐸 ) ∈ ℝ+ )
37 36 rpred ⊢ ( 𝜑 → ( 𝐶 / 𝐸 ) ∈ ℝ )
38 5 rpred ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
39 38 18 rerpdivcld ⊢ ( 𝜑 → ( 𝐴 / 𝐸 ) ∈ ℝ )
40 resubcl ⊢ ( ( ( 𝐶 / 𝐸 ) ∈ ℝ ∧ 2 ∈ ℝ ) → ( ( 𝐶 / 𝐸 ) − 2 ) ∈ ℝ )
41 37 11 40 sylancl ⊢ ( 𝜑 → ( ( 𝐶 / 𝐸 ) − 2 ) ∈ ℝ )
42 37 reefcld ⊢ ( 𝜑 → ( exp ‘ ( 𝐶 / 𝐸 ) ) ∈ ℝ )
43 elicopnf ⊢ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) ∈ ℝ → ( 𝐾 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ↔ ( 𝐾 ∈ ℝ ∧ ( exp ‘ ( 𝐶 / 𝐸 ) ) ≤ 𝐾 ) ) )
44 42 43 syl ⊢ ( 𝜑 → ( 𝐾 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ↔ ( 𝐾 ∈ ℝ ∧ ( exp ‘ ( 𝐶 / 𝐸 ) ) ≤ 𝐾 ) ) )
45 8 44 mpbid ⊢ ( 𝜑 → ( 𝐾 ∈ ℝ ∧ ( exp ‘ ( 𝐶 / 𝐸 ) ) ≤ 𝐾 ) )
46 45 simpld ⊢ ( 𝜑 → 𝐾 ∈ ℝ )
47 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
48 1re ⊢ 1 ∈ ℝ
49 48 a1i ⊢ ( 𝜑 → 1 ∈ ℝ )
50 0lt1 ⊢ 0 < 1
51 50 a1i ⊢ ( 𝜑 → 0 < 1 )
52 efgt1 ⊢ ( ( 𝐶 / 𝐸 ) ∈ ℝ+ → 1 < ( exp ‘ ( 𝐶 / 𝐸 ) ) )
53 36 52 syl ⊢ ( 𝜑 → 1 < ( exp ‘ ( 𝐶 / 𝐸 ) ) )
54 45 simprd ⊢ ( 𝜑 → ( exp ‘ ( 𝐶 / 𝐸 ) ) ≤ 𝐾 )
55 49 42 46 53 54 ltletrd ⊢ ( 𝜑 → 1 < 𝐾 )
56 47 49 46 51 55 lttrd ⊢ ( 𝜑 → 0 < 𝐾 )
57 46 56 elrpd ⊢ ( 𝜑 → 𝐾 ∈ ℝ+ )
58 57 relogcld ⊢ ( 𝜑 → ( log ‘ 𝐾 ) ∈ ℝ )
59 resubcl ⊢ ( ( ( log ‘ 𝐾 ) ∈ ℝ ∧ 2 ∈ ℝ ) → ( ( log ‘ 𝐾 ) − 2 ) ∈ ℝ )
60 58 11 59 sylancl ⊢ ( 𝜑 → ( ( log ‘ 𝐾 ) − 2 ) ∈ ℝ )
61 57 reeflogd ⊢ ( 𝜑 → ( exp ‘ ( log ‘ 𝐾 ) ) = 𝐾 )
62 54 61 breqtrrd ⊢ ( 𝜑 → ( exp ‘ ( 𝐶 / 𝐸 ) ) ≤ ( exp ‘ ( log ‘ 𝐾 ) ) )
63 efle ⊢ ( ( ( 𝐶 / 𝐸 ) ∈ ℝ ∧ ( log ‘ 𝐾 ) ∈ ℝ ) → ( ( 𝐶 / 𝐸 ) ≤ ( log ‘ 𝐾 ) ↔ ( exp ‘ ( 𝐶 / 𝐸 ) ) ≤ ( exp ‘ ( log ‘ 𝐾 ) ) ) )
64 37 58 63 syl2anc ⊢ ( 𝜑 → ( ( 𝐶 / 𝐸 ) ≤ ( log ‘ 𝐾 ) ↔ ( exp ‘ ( 𝐶 / 𝐸 ) ) ≤ ( exp ‘ ( log ‘ 𝐾 ) ) ) )
65 62 64 mpbird ⊢ ( 𝜑 → ( 𝐶 / 𝐸 ) ≤ ( log ‘ 𝐾 ) )
66 37 58 12 65 lesub1dd ⊢ ( 𝜑 → ( ( 𝐶 / 𝐸 ) − 2 ) ≤ ( ( log ‘ 𝐾 ) − 2 ) )
67 fzfid ⊢ ( 𝜑 → ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ∈ Fin )
68 ioossre ⊢ ( 𝑋 (,) +∞ ) ⊆ ℝ
69 68 4 sselid ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
70 rerpdivcl ⊢ ( ( 2 ∈ ℝ ∧ 𝐸 ∈ ℝ+ ) → ( 2 / 𝐸 ) ∈ ℝ )
71 11 18 70 sylancr ⊢ ( 𝜑 → ( 2 / 𝐸 ) ∈ ℝ )
72 71 reefcld ⊢ ( 𝜑 → ( exp ‘ ( 2 / 𝐸 ) ) ∈ ℝ )
73 3 72 eqeltrid ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
74 efgt0 ⊢ ( ( 2 / 𝐸 ) ∈ ℝ → 0 < ( exp ‘ ( 2 / 𝐸 ) ) )
75 71 74 syl ⊢ ( 𝜑 → 0 < ( exp ‘ ( 2 / 𝐸 ) ) )
76 75 3 breqtrrdi ⊢ ( 𝜑 → 0 < 𝑋 )
77 73 rexrd ⊢ ( 𝜑 → 𝑋 ∈ ℝ* )
78 elioopnf ⊢ ( 𝑋 ∈ ℝ* → ( 𝑌 ∈ ( 𝑋 (,) +∞ ) ↔ ( 𝑌 ∈ ℝ ∧ 𝑋 < 𝑌 ) ) )
79 77 78 syl ⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝑋 (,) +∞ ) ↔ ( 𝑌 ∈ ℝ ∧ 𝑋 < 𝑌 ) ) )
80 4 79 mpbid ⊢ ( 𝜑 → ( 𝑌 ∈ ℝ ∧ 𝑋 < 𝑌 ) )
81 80 simprd ⊢ ( 𝜑 → 𝑋 < 𝑌 )
82 47 73 69 76 81 lttrd ⊢ ( 𝜑 → 0 < 𝑌 )
83 47 69 82 ltled ⊢ ( 𝜑 → 0 ≤ 𝑌 )
84 flge0nn0 ⊢ ( ( 𝑌 ∈ ℝ ∧ 0 ≤ 𝑌 ) → ( ⌊ ‘ 𝑌 ) ∈ ℕ0 )
85 69 83 84 syl2anc ⊢ ( 𝜑 → ( ⌊ ‘ 𝑌 ) ∈ ℕ0 )
86 nn0p1nn ⊢ ( ( ⌊ ‘ 𝑌 ) ∈ ℕ0 → ( ( ⌊ ‘ 𝑌 ) + 1 ) ∈ ℕ )
87 85 86 syl ⊢ ( 𝜑 → ( ( ⌊ ‘ 𝑌 ) + 1 ) ∈ ℕ )
88 elfzuz ⊢ ( 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) → 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) )
89 eluznn ⊢ ( ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ∈ ℕ ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ) → 𝑛 ∈ ℕ )
90 87 88 89 syl2an ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → 𝑛 ∈ ℕ )
91 90 peano2nnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 𝑛 + 1 ) ∈ ℕ )
92 91 nnrecred ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 1 / ( 𝑛 + 1 ) ) ∈ ℝ )
93 67 92 fsumrecl ⊢ ( 𝜑 → Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 1 / ( 𝑛 + 1 ) ) ∈ ℝ )
94 58 recnd ⊢ ( 𝜑 → ( log ‘ 𝐾 ) ∈ ℂ )
95 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
96 69 82 elrpd ⊢ ( 𝜑 → 𝑌 ∈ ℝ+ )
97 96 relogcld ⊢ ( 𝜑 → ( log ‘ 𝑌 ) ∈ ℝ )
98 97 recnd ⊢ ( 𝜑 → ( log ‘ 𝑌 ) ∈ ℂ )
99 94 95 98 pnpcan2d ⊢ ( 𝜑 → ( ( ( log ‘ 𝐾 ) + ( log ‘ 𝑌 ) ) − ( 2 + ( log ‘ 𝑌 ) ) ) = ( ( log ‘ 𝐾 ) − 2 ) )
100 57 96 relogmuld ⊢ ( 𝜑 → ( log ‘ ( 𝐾 · 𝑌 ) ) = ( ( log ‘ 𝐾 ) + ( log ‘ 𝑌 ) ) )
101 58 97 readdcld ⊢ ( 𝜑 → ( ( log ‘ 𝐾 ) + ( log ‘ 𝑌 ) ) ∈ ℝ )
102 100 101 eqeltrd ⊢ ( 𝜑 → ( log ‘ ( 𝐾 · 𝑌 ) ) ∈ ℝ )
103 fzfid ⊢ ( 𝜑 → ( 0 ... ( ⌊ ‘ 𝑌 ) ) ∈ Fin )
104 elfznn0 ⊢ ( 𝑛 ∈ ( 0 ... ( ⌊ ‘ 𝑌 ) ) → 𝑛 ∈ ℕ0 )
105 104 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... ( ⌊ ‘ 𝑌 ) ) ) → 𝑛 ∈ ℕ0 )
106 nn0p1nn ⊢ ( 𝑛 ∈ ℕ0 → ( 𝑛 + 1 ) ∈ ℕ )
107 105 106 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... ( ⌊ ‘ 𝑌 ) ) ) → ( 𝑛 + 1 ) ∈ ℕ )
108 107 nnrecred ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... ( ⌊ ‘ 𝑌 ) ) ) → ( 1 / ( 𝑛 + 1 ) ) ∈ ℝ )
109 103 108 fsumrecl ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 0 ... ( ⌊ ‘ 𝑌 ) ) ( 1 / ( 𝑛 + 1 ) ) ∈ ℝ )
110 109 93 readdcld ⊢ ( 𝜑 → ( Σ 𝑛 ∈ ( 0 ... ( ⌊ ‘ 𝑌 ) ) ( 1 / ( 𝑛 + 1 ) ) + Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 1 / ( 𝑛 + 1 ) ) ) ∈ ℝ )
111 readdcl ⊢ ( ( 2 ∈ ℝ ∧ ( log ‘ 𝑌 ) ∈ ℝ ) → ( 2 + ( log ‘ 𝑌 ) ) ∈ ℝ )
112 11 97 111 sylancr ⊢ ( 𝜑 → ( 2 + ( log ‘ 𝑌 ) ) ∈ ℝ )
113 112 93 readdcld ⊢ ( 𝜑 → ( ( 2 + ( log ‘ 𝑌 ) ) + Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 1 / ( 𝑛 + 1 ) ) ) ∈ ℝ )
114 46 69 remulcld ⊢ ( 𝜑 → ( 𝐾 · 𝑌 ) ∈ ℝ )
115 69 recnd ⊢ ( 𝜑 → 𝑌 ∈ ℂ )
116 115 mulid2d ⊢ ( 𝜑 → ( 1 · 𝑌 ) = 𝑌 )
117 49 46 55 ltled ⊢ ( 𝜑 → 1 ≤ 𝐾 )
118 lemul1 ⊢ ( ( 1 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ ( 𝑌 ∈ ℝ ∧ 0 < 𝑌 ) ) → ( 1 ≤ 𝐾 ↔ ( 1 · 𝑌 ) ≤ ( 𝐾 · 𝑌 ) ) )
119 49 46 69 82 118 syl112anc ⊢ ( 𝜑 → ( 1 ≤ 𝐾 ↔ ( 1 · 𝑌 ) ≤ ( 𝐾 · 𝑌 ) ) )
120 117 119 mpbid ⊢ ( 𝜑 → ( 1 · 𝑌 ) ≤ ( 𝐾 · 𝑌 ) )
121 116 120 eqbrtrrd ⊢ ( 𝜑 → 𝑌 ≤ ( 𝐾 · 𝑌 ) )
122 47 69 114 83 121 letrd ⊢ ( 𝜑 → 0 ≤ ( 𝐾 · 𝑌 ) )
123 flge0nn0 ⊢ ( ( ( 𝐾 · 𝑌 ) ∈ ℝ ∧ 0 ≤ ( 𝐾 · 𝑌 ) ) → ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ∈ ℕ0 )
124 114 122 123 syl2anc ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ∈ ℕ0 )
125 nn0p1nn ⊢ ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ∈ ℕ0 → ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ∈ ℕ )
126 124 125 syl ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ∈ ℕ )
127 126 nnrpd ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ∈ ℝ+ )
128 127 relogcld ⊢ ( 𝜑 → ( log ‘ ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ) ∈ ℝ )
129 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
130 114 flcld ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ∈ ℤ )
131 130 peano2zd ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ∈ ℤ )
132 elfznn ⊢ ( 𝑘 ∈ ( 1 ... ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ) → 𝑘 ∈ ℕ )
133 132 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ) ) → 𝑘 ∈ ℕ )
134 nnrecre ⊢ ( 𝑘 ∈ ℕ → ( 1 / 𝑘 ) ∈ ℝ )
135 134 recnd ⊢ ( 𝑘 ∈ ℕ → ( 1 / 𝑘 ) ∈ ℂ )
136 133 135 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ) ) → ( 1 / 𝑘 ) ∈ ℂ )
137 oveq2 ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( 1 / 𝑘 ) = ( 1 / ( 𝑛 + 1 ) ) )
138 129 129 131 136 137 fsumshftm ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 1 ... ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ) ( 1 / 𝑘 ) = Σ 𝑛 ∈ ( ( 1 − 1 ) ... ( ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) − 1 ) ) ( 1 / ( 𝑛 + 1 ) ) )
139 1m1e0 ⊢ ( 1 − 1 ) = 0
140 139 a1i ⊢ ( 𝜑 → ( 1 − 1 ) = 0 )
141 130 zcnd ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ∈ ℂ )
142 ax-1cn ⊢ 1 ∈ ℂ
143 pncan ⊢ ( ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) − 1 ) = ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) )
144 141 142 143 sylancl ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) − 1 ) = ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) )
145 140 144 oveq12d ⊢ ( 𝜑 → ( ( 1 − 1 ) ... ( ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) − 1 ) ) = ( 0 ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) )
146 145 sumeq1d ⊢ ( 𝜑 → Σ 𝑛 ∈ ( ( 1 − 1 ) ... ( ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) − 1 ) ) ( 1 / ( 𝑛 + 1 ) ) = Σ 𝑛 ∈ ( 0 ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 1 / ( 𝑛 + 1 ) ) )
147 reflcl ⊢ ( 𝑌 ∈ ℝ → ( ⌊ ‘ 𝑌 ) ∈ ℝ )
148 69 147 syl ⊢ ( 𝜑 → ( ⌊ ‘ 𝑌 ) ∈ ℝ )
149 148 ltp1d ⊢ ( 𝜑 → ( ⌊ ‘ 𝑌 ) < ( ( ⌊ ‘ 𝑌 ) + 1 ) )
150 fzdisj ⊢ ( ( ⌊ ‘ 𝑌 ) < ( ( ⌊ ‘ 𝑌 ) + 1 ) → ( ( 0 ... ( ⌊ ‘ 𝑌 ) ) ∩ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) = ∅ )
151 149 150 syl ⊢ ( 𝜑 → ( ( 0 ... ( ⌊ ‘ 𝑌 ) ) ∩ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) = ∅ )
152 flwordi ⊢ ( ( 𝑌 ∈ ℝ ∧ ( 𝐾 · 𝑌 ) ∈ ℝ ∧ 𝑌 ≤ ( 𝐾 · 𝑌 ) ) → ( ⌊ ‘ 𝑌 ) ≤ ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) )
153 69 114 121 152 syl3anc ⊢ ( 𝜑 → ( ⌊ ‘ 𝑌 ) ≤ ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) )
154 elfz2nn0 ⊢ ( ( ⌊ ‘ 𝑌 ) ∈ ( 0 ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ↔ ( ( ⌊ ‘ 𝑌 ) ∈ ℕ0 ∧ ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ∈ ℕ0 ∧ ( ⌊ ‘ 𝑌 ) ≤ ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) )
155 85 124 153 154 syl3anbrc ⊢ ( 𝜑 → ( ⌊ ‘ 𝑌 ) ∈ ( 0 ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) )
156 fzsplit ⊢ ( ( ⌊ ‘ 𝑌 ) ∈ ( 0 ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) → ( 0 ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) = ( ( 0 ... ( ⌊ ‘ 𝑌 ) ) ∪ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) )
157 155 156 syl ⊢ ( 𝜑 → ( 0 ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) = ( ( 0 ... ( ⌊ ‘ 𝑌 ) ) ∪ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) )
158 fzfid ⊢ ( 𝜑 → ( 0 ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ∈ Fin )
159 elfznn0 ⊢ ( 𝑛 ∈ ( 0 ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) → 𝑛 ∈ ℕ0 )
160 159 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → 𝑛 ∈ ℕ0 )
161 160 106 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 𝑛 + 1 ) ∈ ℕ )
162 161 nnrecred ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 1 / ( 𝑛 + 1 ) ) ∈ ℝ )
163 162 recnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 1 / ( 𝑛 + 1 ) ) ∈ ℂ )
164 151 157 158 163 fsumsplit ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 0 ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 1 / ( 𝑛 + 1 ) ) = ( Σ 𝑛 ∈ ( 0 ... ( ⌊ ‘ 𝑌 ) ) ( 1 / ( 𝑛 + 1 ) ) + Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 1 / ( 𝑛 + 1 ) ) ) )
165 138 146 164 3eqtrd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 1 ... ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ) ( 1 / 𝑘 ) = ( Σ 𝑛 ∈ ( 0 ... ( ⌊ ‘ 𝑌 ) ) ( 1 / ( 𝑛 + 1 ) ) + Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 1 / ( 𝑛 + 1 ) ) ) )
166 165 110 eqeltrd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 1 ... ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ) ( 1 / 𝑘 ) ∈ ℝ )
167 fllep1 ⊢ ( ( 𝐾 · 𝑌 ) ∈ ℝ → ( 𝐾 · 𝑌 ) ≤ ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) )
168 114 167 syl ⊢ ( 𝜑 → ( 𝐾 · 𝑌 ) ≤ ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) )
169 57 96 rpmulcld ⊢ ( 𝜑 → ( 𝐾 · 𝑌 ) ∈ ℝ+ )
170 169 127 logled ⊢ ( 𝜑 → ( ( 𝐾 · 𝑌 ) ≤ ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ↔ ( log ‘ ( 𝐾 · 𝑌 ) ) ≤ ( log ‘ ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ) ) )
171 168 170 mpbid ⊢ ( 𝜑 → ( log ‘ ( 𝐾 · 𝑌 ) ) ≤ ( log ‘ ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ) )
172 emre ⊢ γ ∈ ℝ
173 172 a1i ⊢ ( 𝜑 → γ ∈ ℝ )
174 166 128 resubcld ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 1 ... ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ) ( 1 / 𝑘 ) − ( log ‘ ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ) ) ∈ ℝ )
175 0re ⊢ 0 ∈ ℝ
176 emgt0 ⊢ 0 < γ
177 175 172 176 ltleii ⊢ 0 ≤ γ
178 177 a1i ⊢ ( 𝜑 → 0 ≤ γ )
179 harmonicbnd ⊢ ( ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ∈ ℕ → ( Σ 𝑘 ∈ ( 1 ... ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ) ( 1 / 𝑘 ) − ( log ‘ ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ) ) ∈ ( γ [,] 1 ) )
180 126 179 syl ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 1 ... ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ) ( 1 / 𝑘 ) − ( log ‘ ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ) ) ∈ ( γ [,] 1 ) )
181 172 48 elicc2i ⊢ ( ( Σ 𝑘 ∈ ( 1 ... ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ) ( 1 / 𝑘 ) − ( log ‘ ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ) ) ∈ ( γ [,] 1 ) ↔ ( ( Σ 𝑘 ∈ ( 1 ... ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ) ( 1 / 𝑘 ) − ( log ‘ ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ) ) ∈ ℝ ∧ γ ≤ ( Σ 𝑘 ∈ ( 1 ... ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ) ( 1 / 𝑘 ) − ( log ‘ ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ) ) ∧ ( Σ 𝑘 ∈ ( 1 ... ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ) ( 1 / 𝑘 ) − ( log ‘ ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ) ) ≤ 1 ) )
182 181 simp2bi ⊢ ( ( Σ 𝑘 ∈ ( 1 ... ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ) ( 1 / 𝑘 ) − ( log ‘ ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ) ) ∈ ( γ [,] 1 ) → γ ≤ ( Σ 𝑘 ∈ ( 1 ... ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ) ( 1 / 𝑘 ) − ( log ‘ ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ) ) )
183 180 182 syl ⊢ ( 𝜑 → γ ≤ ( Σ 𝑘 ∈ ( 1 ... ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ) ( 1 / 𝑘 ) − ( log ‘ ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ) ) )
184 47 173 174 178 183 letrd ⊢ ( 𝜑 → 0 ≤ ( Σ 𝑘 ∈ ( 1 ... ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ) ( 1 / 𝑘 ) − ( log ‘ ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ) ) )
185 166 128 subge0d ⊢ ( 𝜑 → ( 0 ≤ ( Σ 𝑘 ∈ ( 1 ... ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ) ( 1 / 𝑘 ) − ( log ‘ ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ) ) ↔ ( log ‘ ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ) ≤ Σ 𝑘 ∈ ( 1 ... ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ) ( 1 / 𝑘 ) ) )
186 184 185 mpbid ⊢ ( 𝜑 → ( log ‘ ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ) ≤ Σ 𝑘 ∈ ( 1 ... ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ) ( 1 / 𝑘 ) )
187 102 128 166 171 186 letrd ⊢ ( 𝜑 → ( log ‘ ( 𝐾 · 𝑌 ) ) ≤ Σ 𝑘 ∈ ( 1 ... ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) + 1 ) ) ( 1 / 𝑘 ) )
188 187 165 breqtrd ⊢ ( 𝜑 → ( log ‘ ( 𝐾 · 𝑌 ) ) ≤ ( Σ 𝑛 ∈ ( 0 ... ( ⌊ ‘ 𝑌 ) ) ( 1 / ( 𝑛 + 1 ) ) + Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 1 / ( 𝑛 + 1 ) ) ) )
189 69 flcld ⊢ ( 𝜑 → ( ⌊ ‘ 𝑌 ) ∈ ℤ )
190 189 peano2zd ⊢ ( 𝜑 → ( ( ⌊ ‘ 𝑌 ) + 1 ) ∈ ℤ )
191 elfznn ⊢ ( 𝑘 ∈ ( 1 ... ( ( ⌊ ‘ 𝑌 ) + 1 ) ) → 𝑘 ∈ ℕ )
192 191 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ) → 𝑘 ∈ ℕ )
193 192 135 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ) → ( 1 / 𝑘 ) ∈ ℂ )
194 129 129 190 193 137 fsumshftm ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 1 ... ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ( 1 / 𝑘 ) = Σ 𝑛 ∈ ( ( 1 − 1 ) ... ( ( ( ⌊ ‘ 𝑌 ) + 1 ) − 1 ) ) ( 1 / ( 𝑛 + 1 ) ) )
195 148 recnd ⊢ ( 𝜑 → ( ⌊ ‘ 𝑌 ) ∈ ℂ )
196 pncan ⊢ ( ( ( ⌊ ‘ 𝑌 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( ⌊ ‘ 𝑌 ) + 1 ) − 1 ) = ( ⌊ ‘ 𝑌 ) )
197 195 142 196 sylancl ⊢ ( 𝜑 → ( ( ( ⌊ ‘ 𝑌 ) + 1 ) − 1 ) = ( ⌊ ‘ 𝑌 ) )
198 140 197 oveq12d ⊢ ( 𝜑 → ( ( 1 − 1 ) ... ( ( ( ⌊ ‘ 𝑌 ) + 1 ) − 1 ) ) = ( 0 ... ( ⌊ ‘ 𝑌 ) ) )
199 198 sumeq1d ⊢ ( 𝜑 → Σ 𝑛 ∈ ( ( 1 − 1 ) ... ( ( ( ⌊ ‘ 𝑌 ) + 1 ) − 1 ) ) ( 1 / ( 𝑛 + 1 ) ) = Σ 𝑛 ∈ ( 0 ... ( ⌊ ‘ 𝑌 ) ) ( 1 / ( 𝑛 + 1 ) ) )
200 194 199 eqtrd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 1 ... ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ( 1 / 𝑘 ) = Σ 𝑛 ∈ ( 0 ... ( ⌊ ‘ 𝑌 ) ) ( 1 / ( 𝑛 + 1 ) ) )
201 200 109 eqeltrd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 1 ... ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ( 1 / 𝑘 ) ∈ ℝ )
202 87 nnrpd ⊢ ( 𝜑 → ( ( ⌊ ‘ 𝑌 ) + 1 ) ∈ ℝ+ )
203 202 relogcld ⊢ ( 𝜑 → ( log ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ∈ ℝ )
204 readdcl ⊢ ( ( 1 ∈ ℝ ∧ ( log ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ∈ ℝ ) → ( 1 + ( log ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ) ∈ ℝ )
205 48 203 204 sylancr ⊢ ( 𝜑 → ( 1 + ( log ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ) ∈ ℝ )
206 harmonicbnd ⊢ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ∈ ℕ → ( Σ 𝑘 ∈ ( 1 ... ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ( 1 / 𝑘 ) − ( log ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ) ∈ ( γ [,] 1 ) )
207 87 206 syl ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 1 ... ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ( 1 / 𝑘 ) − ( log ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ) ∈ ( γ [,] 1 ) )
208 172 48 elicc2i ⊢ ( ( Σ 𝑘 ∈ ( 1 ... ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ( 1 / 𝑘 ) − ( log ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ) ∈ ( γ [,] 1 ) ↔ ( ( Σ 𝑘 ∈ ( 1 ... ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ( 1 / 𝑘 ) − ( log ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ) ∈ ℝ ∧ γ ≤ ( Σ 𝑘 ∈ ( 1 ... ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ( 1 / 𝑘 ) − ( log ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ) ∧ ( Σ 𝑘 ∈ ( 1 ... ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ( 1 / 𝑘 ) − ( log ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ) ≤ 1 ) )
209 208 simp3bi ⊢ ( ( Σ 𝑘 ∈ ( 1 ... ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ( 1 / 𝑘 ) − ( log ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ) ∈ ( γ [,] 1 ) → ( Σ 𝑘 ∈ ( 1 ... ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ( 1 / 𝑘 ) − ( log ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ) ≤ 1 )
210 207 209 syl ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 1 ... ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ( 1 / 𝑘 ) − ( log ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ) ≤ 1 )
211 201 203 49 lesubaddd ⊢ ( 𝜑 → ( ( Σ 𝑘 ∈ ( 1 ... ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ( 1 / 𝑘 ) − ( log ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ) ≤ 1 ↔ Σ 𝑘 ∈ ( 1 ... ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ( 1 / 𝑘 ) ≤ ( 1 + ( log ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ) ) )
212 210 211 mpbid ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 1 ... ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ( 1 / 𝑘 ) ≤ ( 1 + ( log ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ) )
213 readdcl ⊢ ( ( 1 ∈ ℝ ∧ ( log ‘ 𝑌 ) ∈ ℝ ) → ( 1 + ( log ‘ 𝑌 ) ) ∈ ℝ )
214 48 97 213 sylancr ⊢ ( 𝜑 → ( 1 + ( log ‘ 𝑌 ) ) ∈ ℝ )
215 peano2re ⊢ ( ( ⌊ ‘ 𝑌 ) ∈ ℝ → ( ( ⌊ ‘ 𝑌 ) + 1 ) ∈ ℝ )
216 148 215 syl ⊢ ( 𝜑 → ( ( ⌊ ‘ 𝑌 ) + 1 ) ∈ ℝ )
217 12 69 remulcld ⊢ ( 𝜑 → ( 2 · 𝑌 ) ∈ ℝ )
218 epr ⊢ e ∈ ℝ+
219 rpmulcl ⊢ ( ( e ∈ ℝ+ ∧ 𝑌 ∈ ℝ+ ) → ( e · 𝑌 ) ∈ ℝ+ )
220 218 96 219 sylancr ⊢ ( 𝜑 → ( e · 𝑌 ) ∈ ℝ+ )
221 220 rpred ⊢ ( 𝜑 → ( e · 𝑌 ) ∈ ℝ )
222 flle ⊢ ( 𝑌 ∈ ℝ → ( ⌊ ‘ 𝑌 ) ≤ 𝑌 )
223 69 222 syl ⊢ ( 𝜑 → ( ⌊ ‘ 𝑌 ) ≤ 𝑌 )
224 20 18 rpdivcld ⊢ ( 𝜑 → ( 2 / 𝐸 ) ∈ ℝ+ )
225 efgt1 ⊢ ( ( 2 / 𝐸 ) ∈ ℝ+ → 1 < ( exp ‘ ( 2 / 𝐸 ) ) )
226 224 225 syl ⊢ ( 𝜑 → 1 < ( exp ‘ ( 2 / 𝐸 ) ) )
227 226 3 breqtrrdi ⊢ ( 𝜑 → 1 < 𝑋 )
228 49 73 69 227 81 lttrd ⊢ ( 𝜑 → 1 < 𝑌 )
229 49 69 228 ltled ⊢ ( 𝜑 → 1 ≤ 𝑌 )
230 148 49 69 69 223 229 le2addd ⊢ ( 𝜑 → ( ( ⌊ ‘ 𝑌 ) + 1 ) ≤ ( 𝑌 + 𝑌 ) )
231 115 2timesd ⊢ ( 𝜑 → ( 2 · 𝑌 ) = ( 𝑌 + 𝑌 ) )
232 230 231 breqtrrd ⊢ ( 𝜑 → ( ( ⌊ ‘ 𝑌 ) + 1 ) ≤ ( 2 · 𝑌 ) )
233 ere ⊢ e ∈ ℝ
234 egt2lt3 ⊢ ( 2 < e ∧ e < 3 )
235 234 simpli ⊢ 2 < e
236 11 233 235 ltleii ⊢ 2 ≤ e
237 236 a1i ⊢ ( 𝜑 → 2 ≤ e )
238 233 a1i ⊢ ( 𝜑 → e ∈ ℝ )
239 lemul1 ⊢ ( ( 2 ∈ ℝ ∧ e ∈ ℝ ∧ ( 𝑌 ∈ ℝ ∧ 0 < 𝑌 ) ) → ( 2 ≤ e ↔ ( 2 · 𝑌 ) ≤ ( e · 𝑌 ) ) )
240 12 238 69 82 239 syl112anc ⊢ ( 𝜑 → ( 2 ≤ e ↔ ( 2 · 𝑌 ) ≤ ( e · 𝑌 ) ) )
241 237 240 mpbid ⊢ ( 𝜑 → ( 2 · 𝑌 ) ≤ ( e · 𝑌 ) )
242 216 217 221 232 241 letrd ⊢ ( 𝜑 → ( ( ⌊ ‘ 𝑌 ) + 1 ) ≤ ( e · 𝑌 ) )
243 202 220 logled ⊢ ( 𝜑 → ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ≤ ( e · 𝑌 ) ↔ ( log ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ≤ ( log ‘ ( e · 𝑌 ) ) ) )
244 242 243 mpbid ⊢ ( 𝜑 → ( log ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ≤ ( log ‘ ( e · 𝑌 ) ) )
245 relogmul ⊢ ( ( e ∈ ℝ+ ∧ 𝑌 ∈ ℝ+ ) → ( log ‘ ( e · 𝑌 ) ) = ( ( log ‘ e ) + ( log ‘ 𝑌 ) ) )
246 218 96 245 sylancr ⊢ ( 𝜑 → ( log ‘ ( e · 𝑌 ) ) = ( ( log ‘ e ) + ( log ‘ 𝑌 ) ) )
247 loge ⊢ ( log ‘ e ) = 1
248 247 oveq1i ⊢ ( ( log ‘ e ) + ( log ‘ 𝑌 ) ) = ( 1 + ( log ‘ 𝑌 ) )
249 246 248 eqtrdi ⊢ ( 𝜑 → ( log ‘ ( e · 𝑌 ) ) = ( 1 + ( log ‘ 𝑌 ) ) )
250 244 249 breqtrd ⊢ ( 𝜑 → ( log ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ≤ ( 1 + ( log ‘ 𝑌 ) ) )
251 203 214 49 250 leadd2dd ⊢ ( 𝜑 → ( 1 + ( log ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ) ≤ ( 1 + ( 1 + ( log ‘ 𝑌 ) ) ) )
252 df-2 ⊢ 2 = ( 1 + 1 )
253 252 oveq1i ⊢ ( 2 + ( log ‘ 𝑌 ) ) = ( ( 1 + 1 ) + ( log ‘ 𝑌 ) )
254 142 a1i ⊢ ( 𝜑 → 1 ∈ ℂ )
255 254 254 98 addassd ⊢ ( 𝜑 → ( ( 1 + 1 ) + ( log ‘ 𝑌 ) ) = ( 1 + ( 1 + ( log ‘ 𝑌 ) ) ) )
256 253 255 syl5eq ⊢ ( 𝜑 → ( 2 + ( log ‘ 𝑌 ) ) = ( 1 + ( 1 + ( log ‘ 𝑌 ) ) ) )
257 251 256 breqtrrd ⊢ ( 𝜑 → ( 1 + ( log ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ) ≤ ( 2 + ( log ‘ 𝑌 ) ) )
258 201 205 112 212 257 letrd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 1 ... ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ( 1 / 𝑘 ) ≤ ( 2 + ( log ‘ 𝑌 ) ) )
259 200 258 eqbrtrrd ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 0 ... ( ⌊ ‘ 𝑌 ) ) ( 1 / ( 𝑛 + 1 ) ) ≤ ( 2 + ( log ‘ 𝑌 ) ) )
260 109 112 93 259 leadd1dd ⊢ ( 𝜑 → ( Σ 𝑛 ∈ ( 0 ... ( ⌊ ‘ 𝑌 ) ) ( 1 / ( 𝑛 + 1 ) ) + Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 1 / ( 𝑛 + 1 ) ) ) ≤ ( ( 2 + ( log ‘ 𝑌 ) ) + Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 1 / ( 𝑛 + 1 ) ) ) )
261 102 110 113 188 260 letrd ⊢ ( 𝜑 → ( log ‘ ( 𝐾 · 𝑌 ) ) ≤ ( ( 2 + ( log ‘ 𝑌 ) ) + Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 1 / ( 𝑛 + 1 ) ) ) )
262 100 261 eqbrtrrd ⊢ ( 𝜑 → ( ( log ‘ 𝐾 ) + ( log ‘ 𝑌 ) ) ≤ ( ( 2 + ( log ‘ 𝑌 ) ) + Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 1 / ( 𝑛 + 1 ) ) ) )
263 101 112 93 lesubadd2d ⊢ ( 𝜑 → ( ( ( ( log ‘ 𝐾 ) + ( log ‘ 𝑌 ) ) − ( 2 + ( log ‘ 𝑌 ) ) ) ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 1 / ( 𝑛 + 1 ) ) ↔ ( ( log ‘ 𝐾 ) + ( log ‘ 𝑌 ) ) ≤ ( ( 2 + ( log ‘ 𝑌 ) ) + Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 1 / ( 𝑛 + 1 ) ) ) ) )
264 262 263 mpbird ⊢ ( 𝜑 → ( ( ( log ‘ 𝐾 ) + ( log ‘ 𝑌 ) ) − ( 2 + ( log ‘ 𝑌 ) ) ) ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 1 / ( 𝑛 + 1 ) ) )
265 99 264 eqbrtrrd ⊢ ( 𝜑 → ( ( log ‘ 𝐾 ) − 2 ) ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 1 / ( 𝑛 + 1 ) ) )
266 92 recnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 1 / ( 𝑛 + 1 ) ) ∈ ℂ )
267 67 32 266 fsummulc2 ⊢ ( 𝜑 → ( 𝐸 · Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 1 / ( 𝑛 + 1 ) ) ) = Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 𝐸 · ( 1 / ( 𝑛 + 1 ) ) ) )
268 14 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → 𝐸 ∈ ℝ )
269 268 recnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → 𝐸 ∈ ℂ )
270 91 nncnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 𝑛 + 1 ) ∈ ℂ )
271 91 nnne0d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 𝑛 + 1 ) ≠ 0 )
272 269 270 271 divrecd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 𝐸 / ( 𝑛 + 1 ) ) = ( 𝐸 · ( 1 / ( 𝑛 + 1 ) ) ) )
273 268 91 nndivred ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 𝐸 / ( 𝑛 + 1 ) ) ∈ ℝ )
274 272 273 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 𝐸 · ( 1 / ( 𝑛 + 1 ) ) ) ∈ ℝ )
275 67 274 fsumrecl ⊢ ( 𝜑 → Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 𝐸 · ( 1 / ( 𝑛 + 1 ) ) ) ∈ ℝ )
276 90 nnrpd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → 𝑛 ∈ ℝ+ )
277 1 pntrf ⊢ 𝑅 : ℝ+ ⟶ ℝ
278 277 ffvelrni ⊢ ( 𝑛 ∈ ℝ+ → ( 𝑅 ‘ 𝑛 ) ∈ ℝ )
279 276 278 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 𝑅 ‘ 𝑛 ) ∈ ℝ )
280 90 91 nnmulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 𝑛 · ( 𝑛 + 1 ) ) ∈ ℕ )
281 279 280 nndivred ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ∈ ℝ )
282 281 recnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ∈ ℂ )
283 282 abscld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ∈ ℝ )
284 67 283 fsumrecl ⊢ ( 𝜑 → Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ∈ ℝ )
285 279 90 nndivred ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
286 285 recnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
287 286 abscld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ∈ ℝ )
288 91 nnrpd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 𝑛 + 1 ) ∈ ℝ+ )
289 9 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ¬ ∃ 𝑦 ∈ ℕ ( ( 𝑌 < 𝑦 ∧ 𝑦 ≤ ( 𝐾 · 𝑌 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑦 ) / 𝑦 ) ) ≤ 𝐸 ) )
290 elfzle1 ⊢ ( 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) → ( ( ⌊ ‘ 𝑌 ) + 1 ) ≤ 𝑛 )
291 290 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ( ⌊ ‘ 𝑌 ) + 1 ) ≤ 𝑛 )
292 69 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → 𝑌 ∈ ℝ )
293 292 flcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ⌊ ‘ 𝑌 ) ∈ ℤ )
294 90 nnzd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → 𝑛 ∈ ℤ )
295 zltp1le ⊢ ( ( ( ⌊ ‘ 𝑌 ) ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( ⌊ ‘ 𝑌 ) < 𝑛 ↔ ( ( ⌊ ‘ 𝑌 ) + 1 ) ≤ 𝑛 ) )
296 293 294 295 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ( ⌊ ‘ 𝑌 ) < 𝑛 ↔ ( ( ⌊ ‘ 𝑌 ) + 1 ) ≤ 𝑛 ) )
297 291 296 mpbird ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ⌊ ‘ 𝑌 ) < 𝑛 )
298 fllt ⊢ ( ( 𝑌 ∈ ℝ ∧ 𝑛 ∈ ℤ ) → ( 𝑌 < 𝑛 ↔ ( ⌊ ‘ 𝑌 ) < 𝑛 ) )
299 292 294 298 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 𝑌 < 𝑛 ↔ ( ⌊ ‘ 𝑌 ) < 𝑛 ) )
300 297 299 mpbird ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → 𝑌 < 𝑛 )
301 elfzle2 ⊢ ( 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) → 𝑛 ≤ ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) )
302 301 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → 𝑛 ≤ ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) )
303 114 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 𝐾 · 𝑌 ) ∈ ℝ )
304 flge ⊢ ( ( ( 𝐾 · 𝑌 ) ∈ ℝ ∧ 𝑛 ∈ ℤ ) → ( 𝑛 ≤ ( 𝐾 · 𝑌 ) ↔ 𝑛 ≤ ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) )
305 303 294 304 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 𝑛 ≤ ( 𝐾 · 𝑌 ) ↔ 𝑛 ≤ ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) )
306 302 305 mpbird ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → 𝑛 ≤ ( 𝐾 · 𝑌 ) )
307 breq2 ⊢ ( 𝑦 = 𝑛 → ( 𝑌 < 𝑦 ↔ 𝑌 < 𝑛 ) )
308 breq1 ⊢ ( 𝑦 = 𝑛 → ( 𝑦 ≤ ( 𝐾 · 𝑌 ) ↔ 𝑛 ≤ ( 𝐾 · 𝑌 ) ) )
309 307 308 anbi12d ⊢ ( 𝑦 = 𝑛 → ( ( 𝑌 < 𝑦 ∧ 𝑦 ≤ ( 𝐾 · 𝑌 ) ) ↔ ( 𝑌 < 𝑛 ∧ 𝑛 ≤ ( 𝐾 · 𝑌 ) ) ) )
310 fveq2 ⊢ ( 𝑦 = 𝑛 → ( 𝑅 ‘ 𝑦 ) = ( 𝑅 ‘ 𝑛 ) )
311 id ⊢ ( 𝑦 = 𝑛 → 𝑦 = 𝑛 )
312 310 311 oveq12d ⊢ ( 𝑦 = 𝑛 → ( ( 𝑅 ‘ 𝑦 ) / 𝑦 ) = ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) )
313 312 fveq2d ⊢ ( 𝑦 = 𝑛 → ( abs ‘ ( ( 𝑅 ‘ 𝑦 ) / 𝑦 ) ) = ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) )
314 313 breq1d ⊢ ( 𝑦 = 𝑛 → ( ( abs ‘ ( ( 𝑅 ‘ 𝑦 ) / 𝑦 ) ) ≤ 𝐸 ↔ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝐸 ) )
315 309 314 anbi12d ⊢ ( 𝑦 = 𝑛 → ( ( ( 𝑌 < 𝑦 ∧ 𝑦 ≤ ( 𝐾 · 𝑌 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑦 ) / 𝑦 ) ) ≤ 𝐸 ) ↔ ( ( 𝑌 < 𝑛 ∧ 𝑛 ≤ ( 𝐾 · 𝑌 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝐸 ) ) )
316 315 rspcev ⊢ ( ( 𝑛 ∈ ℕ ∧ ( ( 𝑌 < 𝑛 ∧ 𝑛 ≤ ( 𝐾 · 𝑌 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝐸 ) ) → ∃ 𝑦 ∈ ℕ ( ( 𝑌 < 𝑦 ∧ 𝑦 ≤ ( 𝐾 · 𝑌 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑦 ) / 𝑦 ) ) ≤ 𝐸 ) )
317 316 expr ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝑌 < 𝑛 ∧ 𝑛 ≤ ( 𝐾 · 𝑌 ) ) ) → ( ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝐸 → ∃ 𝑦 ∈ ℕ ( ( 𝑌 < 𝑦 ∧ 𝑦 ≤ ( 𝐾 · 𝑌 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑦 ) / 𝑦 ) ) ≤ 𝐸 ) ) )
318 90 300 306 317 syl12anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝐸 → ∃ 𝑦 ∈ ℕ ( ( 𝑌 < 𝑦 ∧ 𝑦 ≤ ( 𝐾 · 𝑌 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑦 ) / 𝑦 ) ) ≤ 𝐸 ) ) )
319 289 318 mtod ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ¬ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝐸 )
320 287 268 letrid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝐸 ∨ 𝐸 ≤ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ) )
321 320 ord ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ¬ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝐸 → 𝐸 ≤ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ) )
322 319 321 mpd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → 𝐸 ≤ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) )
323 268 287 288 322 lediv1dd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 𝐸 / ( 𝑛 + 1 ) ) ≤ ( ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) / ( 𝑛 + 1 ) ) )
324 286 270 271 absdivd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( abs ‘ ( ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) / ( 𝑛 + 1 ) ) ) = ( ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) / ( abs ‘ ( 𝑛 + 1 ) ) ) )
325 279 recnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 𝑅 ‘ 𝑛 ) ∈ ℂ )
326 90 nncnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → 𝑛 ∈ ℂ )
327 90 nnne0d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → 𝑛 ≠ 0 )
328 325 326 270 327 271 divdiv1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) / ( 𝑛 + 1 ) ) = ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) )
329 328 fveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( abs ‘ ( ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) / ( 𝑛 + 1 ) ) ) = ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) )
330 288 rprege0d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ( 𝑛 + 1 ) ∈ ℝ ∧ 0 ≤ ( 𝑛 + 1 ) ) )
331 absid ⊢ ( ( ( 𝑛 + 1 ) ∈ ℝ ∧ 0 ≤ ( 𝑛 + 1 ) ) → ( abs ‘ ( 𝑛 + 1 ) ) = ( 𝑛 + 1 ) )
332 330 331 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( abs ‘ ( 𝑛 + 1 ) ) = ( 𝑛 + 1 ) )
333 332 oveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) / ( abs ‘ ( 𝑛 + 1 ) ) ) = ( ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) / ( 𝑛 + 1 ) ) )
334 324 329 333 3eqtr3rd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) / ( 𝑛 + 1 ) ) = ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) )
335 323 272 334 3brtr3d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 𝐸 · ( 1 / ( 𝑛 + 1 ) ) ) ≤ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) )
336 67 274 283 335 fsumle ⊢ ( 𝜑 → Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 𝐸 · ( 1 / ( 𝑛 + 1 ) ) ) ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) )
337 1 2 3 4 5 6 7 8 9 pntpbnd1 ⊢ ( 𝜑 → Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝐴 )
338 275 284 38 336 337 letrd ⊢ ( 𝜑 → Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 𝐸 · ( 1 / ( 𝑛 + 1 ) ) ) ≤ 𝐴 )
339 267 338 eqbrtrd ⊢ ( 𝜑 → ( 𝐸 · Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 1 / ( 𝑛 + 1 ) ) ) ≤ 𝐴 )
340 93 38 18 lemuldiv2d ⊢ ( 𝜑 → ( ( 𝐸 · Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 1 / ( 𝑛 + 1 ) ) ) ≤ 𝐴 ↔ Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 1 / ( 𝑛 + 1 ) ) ≤ ( 𝐴 / 𝐸 ) ) )
341 339 340 mpbid ⊢ ( 𝜑 → Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 1 / ( 𝑛 + 1 ) ) ≤ ( 𝐴 / 𝐸 ) )
342 60 93 39 265 341 letrd ⊢ ( 𝜑 → ( ( log ‘ 𝐾 ) − 2 ) ≤ ( 𝐴 / 𝐸 ) )
343 41 60 39 66 342 letrd ⊢ ( 𝜑 → ( ( 𝐶 / 𝐸 ) − 2 ) ≤ ( 𝐴 / 𝐸 ) )
344 37 12 39 343 subled ⊢ ( 𝜑 → ( ( 𝐶 / 𝐸 ) − ( 𝐴 / 𝐸 ) ) ≤ 2 )
345 35 344 eqbrtrd ⊢ ( 𝜑 → ( 2 / 𝐸 ) ≤ 2 )
346 12 18 20 345 lediv23d ⊢ ( 𝜑 → ( 2 / 2 ) ≤ 𝐸 )
347 10 346 eqbrtrrid ⊢ ( 𝜑 → 1 ≤ 𝐸 )
348 16 simprd ⊢ ( 𝜑 → 𝐸 < 1 )
349 ltnle ⊢ ( ( 𝐸 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 𝐸 < 1 ↔ ¬ 1 ≤ 𝐸 ) )
350 14 48 349 sylancl ⊢ ( 𝜑 → ( 𝐸 < 1 ↔ ¬ 1 ≤ 𝐸 ) )
351 348 350 mpbid ⊢ ( 𝜑 → ¬ 1 ≤ 𝐸 )
352 347 351 pm2.65i ⊢ ¬ 𝜑