Metamath Proof Explorer

Theorem pntpbnd1

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 pntpbnd1 ( 𝜑 → Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝐴 )

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 fzfid ⊢ ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ) → ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ∈ Fin )
11 ioossre ⊢ ( 𝑋 (,) +∞ ) ⊆ ℝ
12 11 4 sseldi ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
13 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
14 2re ⊢ 2 ∈ ℝ
15 ioossre ⊢ ( 0 (,) 1 ) ⊆ ℝ
16 15 2 sseldi ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
17 eliooord ⊢ ( 𝐸 ∈ ( 0 (,) 1 ) → ( 0 < 𝐸 ∧ 𝐸 < 1 ) )
18 2 17 syl ⊢ ( 𝜑 → ( 0 < 𝐸 ∧ 𝐸 < 1 ) )
19 18 simpld ⊢ ( 𝜑 → 0 < 𝐸 )
20 16 19 elrpd ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
21 rerpdivcl ⊢ ( ( 2 ∈ ℝ ∧ 𝐸 ∈ ℝ+ ) → ( 2 / 𝐸 ) ∈ ℝ )
22 14 20 21 sylancr ⊢ ( 𝜑 → ( 2 / 𝐸 ) ∈ ℝ )
23 22 reefcld ⊢ ( 𝜑 → ( exp ‘ ( 2 / 𝐸 ) ) ∈ ℝ )
24 3 23 eqeltrid ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
25 efgt0 ⊢ ( ( 2 / 𝐸 ) ∈ ℝ → 0 < ( exp ‘ ( 2 / 𝐸 ) ) )
26 22 25 syl ⊢ ( 𝜑 → 0 < ( exp ‘ ( 2 / 𝐸 ) ) )
27 26 3 breqtrrdi ⊢ ( 𝜑 → 0 < 𝑋 )
28 eliooord ⊢ ( 𝑌 ∈ ( 𝑋 (,) +∞ ) → ( 𝑋 < 𝑌 ∧ 𝑌 < +∞ ) )
29 4 28 syl ⊢ ( 𝜑 → ( 𝑋 < 𝑌 ∧ 𝑌 < +∞ ) )
30 29 simpld ⊢ ( 𝜑 → 𝑋 < 𝑌 )
31 13 24 12 27 30 lttrd ⊢ ( 𝜑 → 0 < 𝑌 )
32 13 12 31 ltled ⊢ ( 𝜑 → 0 ≤ 𝑌 )
33 flge0nn0 ⊢ ( ( 𝑌 ∈ ℝ ∧ 0 ≤ 𝑌 ) → ( ⌊ ‘ 𝑌 ) ∈ ℕ0 )
34 12 32 33 syl2anc ⊢ ( 𝜑 → ( ⌊ ‘ 𝑌 ) ∈ ℕ0 )
35 nn0p1nn ⊢ ( ( ⌊ ‘ 𝑌 ) ∈ ℕ0 → ( ( ⌊ ‘ 𝑌 ) + 1 ) ∈ ℕ )
36 34 35 syl ⊢ ( 𝜑 → ( ( ⌊ ‘ 𝑌 ) + 1 ) ∈ ℕ )
37 elfzuz ⊢ ( 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) → 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) )
38 eluznn ⊢ ( ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ∈ ℕ ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ) → 𝑛 ∈ ℕ )
39 36 37 38 syl2an ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → 𝑛 ∈ ℕ )
40 39 nnrpd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → 𝑛 ∈ ℝ+ )
41 1 pntrf ⊢ 𝑅 : ℝ+ ⟶ ℝ
42 41 ffvelrni ⊢ ( 𝑛 ∈ ℝ+ → ( 𝑅 ‘ 𝑛 ) ∈ ℝ )
43 40 42 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 𝑅 ‘ 𝑛 ) ∈ ℝ )
44 39 peano2nnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 𝑛 + 1 ) ∈ ℕ )
45 39 44 nnmulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 𝑛 · ( 𝑛 + 1 ) ) ∈ ℕ )
46 43 45 nndivred ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ∈ ℝ )
47 46 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ∈ ℝ )
48 10 47 fsumrecl ⊢ ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ) → Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ∈ ℝ )
49 43 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 𝑅 ‘ 𝑛 ) ∈ ℝ )
50 fveq2 ⊢ ( 𝑖 = 𝑛 → ( 𝑅 ‘ 𝑖 ) = ( 𝑅 ‘ 𝑛 ) )
51 50 breq2d ⊢ ( 𝑖 = 𝑛 → ( 0 ≤ ( 𝑅 ‘ 𝑖 ) ↔ 0 ≤ ( 𝑅 ‘ 𝑛 ) ) )
52 51 rspccva ⊢ ( ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → 0 ≤ ( 𝑅 ‘ 𝑛 ) )
53 52 adantll ⊢ ( ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → 0 ≤ ( 𝑅 ‘ 𝑛 ) )
54 45 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 𝑛 · ( 𝑛 + 1 ) ) ∈ ℕ )
55 54 nnred ⊢ ( ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 𝑛 · ( 𝑛 + 1 ) ) ∈ ℝ )
56 54 nngt0d ⊢ ( ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → 0 < ( 𝑛 · ( 𝑛 + 1 ) ) )
57 divge0 ⊢ ( ( ( ( 𝑅 ‘ 𝑛 ) ∈ ℝ ∧ 0 ≤ ( 𝑅 ‘ 𝑛 ) ) ∧ ( ( 𝑛 · ( 𝑛 + 1 ) ) ∈ ℝ ∧ 0 < ( 𝑛 · ( 𝑛 + 1 ) ) ) ) → 0 ≤ ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) )
58 49 53 55 56 57 syl22anc ⊢ ( ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → 0 ≤ ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) )
59 10 47 58 fsumge0 ⊢ ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ) → 0 ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) )
60 48 59 absidd ⊢ ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ) → ( abs ‘ Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) = Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) )
61 47 58 absidd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) = ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) )
62 61 sumeq2dv ⊢ ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ) → Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) = Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) )
63 60 62 eqtr4d ⊢ ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ) → ( abs ‘ Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) = Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) )
64 fzfid ⊢ ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) → ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ∈ Fin )
65 46 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ∈ ℝ )
66 65 recnd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ∈ ℂ )
67 64 66 fsumneg ⊢ ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) → Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) - ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) = - Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) )
68 43 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 𝑅 ‘ 𝑛 ) ∈ ℝ )
69 68 renegcld ⊢ ( ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → - ( 𝑅 ‘ 𝑛 ) ∈ ℝ )
70 50 breq1d ⊢ ( 𝑖 = 𝑛 → ( ( 𝑅 ‘ 𝑖 ) ≤ 0 ↔ ( 𝑅 ‘ 𝑛 ) ≤ 0 ) )
71 70 rspccva ⊢ ( ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 𝑅 ‘ 𝑛 ) ≤ 0 )
72 71 adantll ⊢ ( ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 𝑅 ‘ 𝑛 ) ≤ 0 )
73 68 le0neg1d ⊢ ( ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ( 𝑅 ‘ 𝑛 ) ≤ 0 ↔ 0 ≤ - ( 𝑅 ‘ 𝑛 ) ) )
74 72 73 mpbid ⊢ ( ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → 0 ≤ - ( 𝑅 ‘ 𝑛 ) )
75 45 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 𝑛 · ( 𝑛 + 1 ) ) ∈ ℕ )
76 75 nnred ⊢ ( ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 𝑛 · ( 𝑛 + 1 ) ) ∈ ℝ )
77 75 nngt0d ⊢ ( ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → 0 < ( 𝑛 · ( 𝑛 + 1 ) ) )
78 divge0 ⊢ ( ( ( - ( 𝑅 ‘ 𝑛 ) ∈ ℝ ∧ 0 ≤ - ( 𝑅 ‘ 𝑛 ) ) ∧ ( ( 𝑛 · ( 𝑛 + 1 ) ) ∈ ℝ ∧ 0 < ( 𝑛 · ( 𝑛 + 1 ) ) ) ) → 0 ≤ ( - ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) )
79 69 74 76 77 78 syl22anc ⊢ ( ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → 0 ≤ ( - ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) )
80 43 recnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 𝑅 ‘ 𝑛 ) ∈ ℂ )
81 45 nncnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 𝑛 · ( 𝑛 + 1 ) ) ∈ ℂ )
82 45 nnne0d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 𝑛 · ( 𝑛 + 1 ) ) ≠ 0 )
83 80 81 82 divnegd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → - ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) = ( - ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) )
84 83 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → - ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) = ( - ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) )
85 79 84 breqtrrd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → 0 ≤ - ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) )
86 65 le0neg1d ⊢ ( ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ≤ 0 ↔ 0 ≤ - ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) )
87 85 86 mpbird ⊢ ( ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ≤ 0 )
88 65 87 absnidd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) = - ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) )
89 88 sumeq2dv ⊢ ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) → Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) = Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) - ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) )
90 64 65 fsumrecl ⊢ ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) → Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ∈ ℝ )
91 65 renegcld ⊢ ( ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → - ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ∈ ℝ )
92 64 91 85 fsumge0 ⊢ ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) → 0 ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) - ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) )
93 92 67 breqtrd ⊢ ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) → 0 ≤ - Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) )
94 90 le0neg1d ⊢ ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) → ( Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ≤ 0 ↔ 0 ≤ - Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) )
95 93 94 mpbird ⊢ ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) → Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ≤ 0 )
96 90 95 absnidd ⊢ ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) → ( abs ‘ Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) = - Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) )
97 67 89 96 3eqtr4rd ⊢ ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) → ( abs ‘ Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) = Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) )
98 2rp ⊢ 2 ∈ ℝ+
99 rpaddcl ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 2 ∈ ℝ+ ) → ( 𝐴 + 2 ) ∈ ℝ+ )
100 5 98 99 sylancl ⊢ ( 𝜑 → ( 𝐴 + 2 ) ∈ ℝ+ )
101 7 100 eqeltrid ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
102 101 20 rpdivcld ⊢ ( 𝜑 → ( 𝐶 / 𝐸 ) ∈ ℝ+ )
103 102 rpred ⊢ ( 𝜑 → ( 𝐶 / 𝐸 ) ∈ ℝ )
104 103 reefcld ⊢ ( 𝜑 → ( exp ‘ ( 𝐶 / 𝐸 ) ) ∈ ℝ )
105 pnfxr ⊢ +∞ ∈ ℝ*
106 icossre ⊢ ( ( ( exp ‘ ( 𝐶 / 𝐸 ) ) ∈ ℝ ∧ +∞ ∈ ℝ* ) → ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ⊆ ℝ )
107 104 105 106 sylancl ⊢ ( 𝜑 → ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ⊆ ℝ )
108 107 8 sseldd ⊢ ( 𝜑 → 𝐾 ∈ ℝ )
109 108 12 remulcld ⊢ ( 𝜑 → ( 𝐾 · 𝑌 ) ∈ ℝ )
110 12 recnd ⊢ ( 𝜑 → 𝑌 ∈ ℂ )
111 110 mulid2d ⊢ ( 𝜑 → ( 1 · 𝑌 ) = 𝑌 )
112 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
113 efgt1 ⊢ ( ( 𝐶 / 𝐸 ) ∈ ℝ+ → 1 < ( exp ‘ ( 𝐶 / 𝐸 ) ) )
114 102 113 syl ⊢ ( 𝜑 → 1 < ( exp ‘ ( 𝐶 / 𝐸 ) ) )
115 elicopnf ⊢ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) ∈ ℝ → ( 𝐾 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ↔ ( 𝐾 ∈ ℝ ∧ ( exp ‘ ( 𝐶 / 𝐸 ) ) ≤ 𝐾 ) ) )
116 104 115 syl ⊢ ( 𝜑 → ( 𝐾 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ↔ ( 𝐾 ∈ ℝ ∧ ( exp ‘ ( 𝐶 / 𝐸 ) ) ≤ 𝐾 ) ) )
117 116 simplbda ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ) → ( exp ‘ ( 𝐶 / 𝐸 ) ) ≤ 𝐾 )
118 8 117 mpdan ⊢ ( 𝜑 → ( exp ‘ ( 𝐶 / 𝐸 ) ) ≤ 𝐾 )
119 112 104 108 114 118 ltletrd ⊢ ( 𝜑 → 1 < 𝐾 )
120 ltmul1 ⊢ ( ( 1 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ ( 𝑌 ∈ ℝ ∧ 0 < 𝑌 ) ) → ( 1 < 𝐾 ↔ ( 1 · 𝑌 ) < ( 𝐾 · 𝑌 ) ) )
121 112 108 12 31 120 syl112anc ⊢ ( 𝜑 → ( 1 < 𝐾 ↔ ( 1 · 𝑌 ) < ( 𝐾 · 𝑌 ) ) )
122 119 121 mpbid ⊢ ( 𝜑 → ( 1 · 𝑌 ) < ( 𝐾 · 𝑌 ) )
123 111 122 eqbrtrrd ⊢ ( 𝜑 → 𝑌 < ( 𝐾 · 𝑌 ) )
124 12 109 123 ltled ⊢ ( 𝜑 → 𝑌 ≤ ( 𝐾 · 𝑌 ) )
125 flword2 ⊢ ( ( 𝑌 ∈ ℝ ∧ ( 𝐾 · 𝑌 ) ∈ ℝ ∧ 𝑌 ≤ ( 𝐾 · 𝑌 ) ) → ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑌 ) ) )
126 12 109 124 125 syl3anc ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑌 ) ) )
127 109 flcld ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ∈ ℤ )
128 uzid ⊢ ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ∈ ℤ → ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) )
129 127 128 syl ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) )
130 elfzuzb ⊢ ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ∈ ( ( ⌊ ‘ 𝑌 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ↔ ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑌 ) ) ∧ ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) )
131 126 129 130 sylanbrc ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ∈ ( ( ⌊ ‘ 𝑌 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) )
132 oveq2 ⊢ ( 𝑥 = ( ⌊ ‘ 𝑌 ) → ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑥 ) = ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ 𝑌 ) ) )
133 132 raleqdv ⊢ ( 𝑥 = ( ⌊ ‘ 𝑌 ) → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑥 ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ↔ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ 𝑌 ) ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ) )
134 132 raleqdv ⊢ ( 𝑥 = ( ⌊ ‘ 𝑌 ) → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑥 ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ↔ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ 𝑌 ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) )
135 133 134 orbi12d ⊢ ( 𝑥 = ( ⌊ ‘ 𝑌 ) → ( ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑥 ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ∨ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑥 ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ↔ ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ 𝑌 ) ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ∨ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ 𝑌 ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ) )
136 135 imbi2d ⊢ ( 𝑥 = ( ⌊ ‘ 𝑌 ) → ( ( 𝜑 → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑥 ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ∨ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑥 ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ) ↔ ( 𝜑 → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ 𝑌 ) ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ∨ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ 𝑌 ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ) ) )
137 oveq2 ⊢ ( 𝑥 = 𝑚 → ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑥 ) = ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) )
138 137 raleqdv ⊢ ( 𝑥 = 𝑚 → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑥 ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ↔ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ) )
139 137 raleqdv ⊢ ( 𝑥 = 𝑚 → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑥 ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ↔ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) )
140 138 139 orbi12d ⊢ ( 𝑥 = 𝑚 → ( ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑥 ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ∨ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑥 ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ↔ ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ∨ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ) )
141 140 imbi2d ⊢ ( 𝑥 = 𝑚 → ( ( 𝜑 → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑥 ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ∨ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑥 ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ) ↔ ( 𝜑 → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ∨ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ) ) )
142 oveq2 ⊢ ( 𝑥 = ( 𝑚 + 1 ) → ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑥 ) = ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( 𝑚 + 1 ) ) )
143 142 raleqdv ⊢ ( 𝑥 = ( 𝑚 + 1 ) → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑥 ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ↔ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( 𝑚 + 1 ) ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ) )
144 142 raleqdv ⊢ ( 𝑥 = ( 𝑚 + 1 ) → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑥 ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ↔ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( 𝑚 + 1 ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) )
145 143 144 orbi12d ⊢ ( 𝑥 = ( 𝑚 + 1 ) → ( ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑥 ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ∨ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑥 ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ↔ ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( 𝑚 + 1 ) ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ∨ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( 𝑚 + 1 ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ) )
146 145 imbi2d ⊢ ( 𝑥 = ( 𝑚 + 1 ) → ( ( 𝜑 → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑥 ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ∨ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑥 ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ) ↔ ( 𝜑 → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( 𝑚 + 1 ) ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ∨ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( 𝑚 + 1 ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ) ) )
147 oveq2 ⊢ ( 𝑥 = ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) → ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑥 ) = ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) )
148 147 raleqdv ⊢ ( 𝑥 = ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑥 ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ↔ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ) )
149 147 raleqdv ⊢ ( 𝑥 = ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑥 ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ↔ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) )
150 148 149 orbi12d ⊢ ( 𝑥 = ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) → ( ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑥 ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ∨ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑥 ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ↔ ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ∨ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ) )
151 150 imbi2d ⊢ ( 𝑥 = ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) → ( ( 𝜑 → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑥 ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ∨ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑥 ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ) ↔ ( 𝜑 → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ∨ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ) ) )
152 elfzle3 ⊢ ( 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ 𝑌 ) ) → ( ( ⌊ ‘ 𝑌 ) + 1 ) ≤ ( ⌊ ‘ 𝑌 ) )
153 elfzel2 ⊢ ( 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ 𝑌 ) ) → ( ⌊ ‘ 𝑌 ) ∈ ℤ )
154 153 zred ⊢ ( 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ 𝑌 ) ) → ( ⌊ ‘ 𝑌 ) ∈ ℝ )
155 154 ltp1d ⊢ ( 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ 𝑌 ) ) → ( ⌊ ‘ 𝑌 ) < ( ( ⌊ ‘ 𝑌 ) + 1 ) )
156 peano2re ⊢ ( ( ⌊ ‘ 𝑌 ) ∈ ℝ → ( ( ⌊ ‘ 𝑌 ) + 1 ) ∈ ℝ )
157 154 156 syl ⊢ ( 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ 𝑌 ) ) → ( ( ⌊ ‘ 𝑌 ) + 1 ) ∈ ℝ )
158 154 157 ltnled ⊢ ( 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ 𝑌 ) ) → ( ( ⌊ ‘ 𝑌 ) < ( ( ⌊ ‘ 𝑌 ) + 1 ) ↔ ¬ ( ( ⌊ ‘ 𝑌 ) + 1 ) ≤ ( ⌊ ‘ 𝑌 ) ) )
159 155 158 mpbid ⊢ ( 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ 𝑌 ) ) → ¬ ( ( ⌊ ‘ 𝑌 ) + 1 ) ≤ ( ⌊ ‘ 𝑌 ) )
160 152 159 pm2.21dd ⊢ ( 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ 𝑌 ) ) → ( 𝑅 ‘ 𝑖 ) ≤ 0 )
161 160 rgen ⊢ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ 𝑌 ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0
162 161 olci ⊢ ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ 𝑌 ) ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ∨ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ 𝑌 ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 )
163 162 2a1i ⊢ ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑌 ) ) → ( 𝜑 → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ 𝑌 ) ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ∨ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ 𝑌 ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ) )
164 elfzofz ⊢ ( 𝑚 ∈ ( ( ⌊ ‘ 𝑌 ) ..^ ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) → 𝑚 ∈ ( ( ⌊ ‘ 𝑌 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) )
165 elfzp12 ⊢ ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑌 ) ) → ( 𝑚 ∈ ( ( ⌊ ‘ 𝑌 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ↔ ( 𝑚 = ( ⌊ ‘ 𝑌 ) ∨ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ) )
166 126 165 syl ⊢ ( 𝜑 → ( 𝑚 ∈ ( ( ⌊ ‘ 𝑌 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ↔ ( 𝑚 = ( ⌊ ‘ 𝑌 ) ∨ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ) )
167 164 166 syl5ib ⊢ ( 𝜑 → ( 𝑚 ∈ ( ( ⌊ ‘ 𝑌 ) ..^ ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) → ( 𝑚 = ( ⌊ ‘ 𝑌 ) ∨ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ) )
168 167 imp ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ⌊ ‘ 𝑌 ) ..^ ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 𝑚 = ( ⌊ ‘ 𝑌 ) ∨ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) )
169 36 nnrpd ⊢ ( 𝜑 → ( ( ⌊ ‘ 𝑌 ) + 1 ) ∈ ℝ+ )
170 41 ffvelrni ⊢ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ∈ ℝ+ → ( 𝑅 ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ∈ ℝ )
171 169 170 syl ⊢ ( 𝜑 → ( 𝑅 ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ∈ ℝ )
172 13 171 letrid ⊢ ( 𝜑 → ( 0 ≤ ( 𝑅 ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ∨ ( 𝑅 ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ≤ 0 ) )
173 172 adantr ⊢ ( ( 𝜑 ∧ 𝑚 = ( ⌊ ‘ 𝑌 ) ) → ( 0 ≤ ( 𝑅 ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ∨ ( 𝑅 ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ≤ 0 ) )
174 oveq1 ⊢ ( 𝑚 = ( ⌊ ‘ 𝑌 ) → ( 𝑚 + 1 ) = ( ( ⌊ ‘ 𝑌 ) + 1 ) )
175 174 oveq2d ⊢ ( 𝑚 = ( ⌊ ‘ 𝑌 ) → ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( 𝑚 + 1 ) ) = ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) + 1 ) ) )
176 12 flcld ⊢ ( 𝜑 → ( ⌊ ‘ 𝑌 ) ∈ ℤ )
177 176 peano2zd ⊢ ( 𝜑 → ( ( ⌊ ‘ 𝑌 ) + 1 ) ∈ ℤ )
178 fzsn ⊢ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ∈ ℤ → ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) + 1 ) ) = { ( ( ⌊ ‘ 𝑌 ) + 1 ) } )
179 177 178 syl ⊢ ( 𝜑 → ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) + 1 ) ) = { ( ( ⌊ ‘ 𝑌 ) + 1 ) } )
180 175 179 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑚 = ( ⌊ ‘ 𝑌 ) ) → ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( 𝑚 + 1 ) ) = { ( ( ⌊ ‘ 𝑌 ) + 1 ) } )
181 180 raleqdv ⊢ ( ( 𝜑 ∧ 𝑚 = ( ⌊ ‘ 𝑌 ) ) → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( 𝑚 + 1 ) ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ↔ ∀ 𝑖 ∈ { ( ( ⌊ ‘ 𝑌 ) + 1 ) } 0 ≤ ( 𝑅 ‘ 𝑖 ) ) )
182 ovex ⊢ ( ( ⌊ ‘ 𝑌 ) + 1 ) ∈ V
183 fveq2 ⊢ ( 𝑖 = ( ( ⌊ ‘ 𝑌 ) + 1 ) → ( 𝑅 ‘ 𝑖 ) = ( 𝑅 ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) )
184 183 breq2d ⊢ ( 𝑖 = ( ( ⌊ ‘ 𝑌 ) + 1 ) → ( 0 ≤ ( 𝑅 ‘ 𝑖 ) ↔ 0 ≤ ( 𝑅 ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ) )
185 182 184 ralsn ⊢ ( ∀ 𝑖 ∈ { ( ( ⌊ ‘ 𝑌 ) + 1 ) } 0 ≤ ( 𝑅 ‘ 𝑖 ) ↔ 0 ≤ ( 𝑅 ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) )
186 181 185 bitrdi ⊢ ( ( 𝜑 ∧ 𝑚 = ( ⌊ ‘ 𝑌 ) ) → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( 𝑚 + 1 ) ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ↔ 0 ≤ ( 𝑅 ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ) )
187 180 raleqdv ⊢ ( ( 𝜑 ∧ 𝑚 = ( ⌊ ‘ 𝑌 ) ) → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( 𝑚 + 1 ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ↔ ∀ 𝑖 ∈ { ( ( ⌊ ‘ 𝑌 ) + 1 ) } ( 𝑅 ‘ 𝑖 ) ≤ 0 ) )
188 183 breq1d ⊢ ( 𝑖 = ( ( ⌊ ‘ 𝑌 ) + 1 ) → ( ( 𝑅 ‘ 𝑖 ) ≤ 0 ↔ ( 𝑅 ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ≤ 0 ) )
189 182 188 ralsn ⊢ ( ∀ 𝑖 ∈ { ( ( ⌊ ‘ 𝑌 ) + 1 ) } ( 𝑅 ‘ 𝑖 ) ≤ 0 ↔ ( 𝑅 ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ≤ 0 )
190 187 189 bitrdi ⊢ ( ( 𝜑 ∧ 𝑚 = ( ⌊ ‘ 𝑌 ) ) → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( 𝑚 + 1 ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ↔ ( 𝑅 ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ≤ 0 ) )
191 186 190 orbi12d ⊢ ( ( 𝜑 ∧ 𝑚 = ( ⌊ ‘ 𝑌 ) ) → ( ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( 𝑚 + 1 ) ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ∨ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( 𝑚 + 1 ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ↔ ( 0 ≤ ( 𝑅 ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ∨ ( 𝑅 ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ≤ 0 ) ) )
192 173 191 mpbird ⊢ ( ( 𝜑 ∧ 𝑚 = ( ⌊ ‘ 𝑌 ) ) → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( 𝑚 + 1 ) ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ∨ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( 𝑚 + 1 ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) )
193 192 a1d ⊢ ( ( 𝜑 ∧ 𝑚 = ( ⌊ ‘ 𝑌 ) ) → ( ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ∨ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( 𝑚 + 1 ) ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ∨ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( 𝑚 + 1 ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ) )
194 elfzuz ⊢ ( 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) → 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) )
195 194 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) )
196 eluzfz2 ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) → 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) )
197 195 196 syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) )
198 fveq2 ⊢ ( 𝑖 = 𝑚 → ( 𝑅 ‘ 𝑖 ) = ( 𝑅 ‘ 𝑚 ) )
199 198 breq2d ⊢ ( 𝑖 = 𝑚 → ( 0 ≤ ( 𝑅 ‘ 𝑖 ) ↔ 0 ≤ ( 𝑅 ‘ 𝑚 ) ) )
200 199 rspcv ⊢ ( 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) 0 ≤ ( 𝑅 ‘ 𝑖 ) → 0 ≤ ( 𝑅 ‘ 𝑚 ) ) )
201 197 200 syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) 0 ≤ ( 𝑅 ‘ 𝑖 ) → 0 ≤ ( 𝑅 ‘ 𝑚 ) ) )
202 9 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ¬ ∃ 𝑦 ∈ ℕ ( ( 𝑌 < 𝑦 ∧ 𝑦 ≤ ( 𝐾 · 𝑌 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑦 ) / 𝑦 ) ) ≤ 𝐸 ) )
203 eluznn ⊢ ( ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) ) → 𝑚 ∈ ℕ )
204 36 194 203 syl2an ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → 𝑚 ∈ ℕ )
205 204 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ ( abs ‘ ( 𝑅 ‘ 𝑚 ) ) ≤ ( abs ‘ ( ( 𝑅 ‘ ( 𝑚 + 1 ) ) − ( 𝑅 ‘ 𝑚 ) ) ) ) → 𝑚 ∈ ℕ )
206 elfzle1 ⊢ ( 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) → ( ( ⌊ ‘ 𝑌 ) + 1 ) ≤ 𝑚 )
207 206 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ( ⌊ ‘ 𝑌 ) + 1 ) ≤ 𝑚 )
208 elfzelz ⊢ ( 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) → 𝑚 ∈ ℤ )
209 zltp1le ⊢ ( ( ( ⌊ ‘ 𝑌 ) ∈ ℤ ∧ 𝑚 ∈ ℤ ) → ( ( ⌊ ‘ 𝑌 ) < 𝑚 ↔ ( ( ⌊ ‘ 𝑌 ) + 1 ) ≤ 𝑚 ) )
210 176 208 209 syl2an ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ( ⌊ ‘ 𝑌 ) < 𝑚 ↔ ( ( ⌊ ‘ 𝑌 ) + 1 ) ≤ 𝑚 ) )
211 207 210 mpbird ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ⌊ ‘ 𝑌 ) < 𝑚 )
212 fllt ⊢ ( ( 𝑌 ∈ ℝ ∧ 𝑚 ∈ ℤ ) → ( 𝑌 < 𝑚 ↔ ( ⌊ ‘ 𝑌 ) < 𝑚 ) )
213 12 208 212 syl2an ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 𝑌 < 𝑚 ↔ ( ⌊ ‘ 𝑌 ) < 𝑚 ) )
214 211 213 mpbird ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → 𝑌 < 𝑚 )
215 elfzle2 ⊢ ( 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) → 𝑚 ≤ ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) )
216 215 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → 𝑚 ≤ ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) )
217 flge ⊢ ( ( ( 𝐾 · 𝑌 ) ∈ ℝ ∧ 𝑚 ∈ ℤ ) → ( 𝑚 ≤ ( 𝐾 · 𝑌 ) ↔ 𝑚 ≤ ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) )
218 109 208 217 syl2an ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 𝑚 ≤ ( 𝐾 · 𝑌 ) ↔ 𝑚 ≤ ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) )
219 216 218 mpbird ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → 𝑚 ≤ ( 𝐾 · 𝑌 ) )
220 214 219 jca ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 𝑌 < 𝑚 ∧ 𝑚 ≤ ( 𝐾 · 𝑌 ) ) )
221 220 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ ( abs ‘ ( 𝑅 ‘ 𝑚 ) ) ≤ ( abs ‘ ( ( 𝑅 ‘ ( 𝑚 + 1 ) ) − ( 𝑅 ‘ 𝑚 ) ) ) ) → ( 𝑌 < 𝑚 ∧ 𝑚 ≤ ( 𝐾 · 𝑌 ) ) )
222 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ ( abs ‘ ( 𝑅 ‘ 𝑚 ) ) ≤ ( abs ‘ ( ( 𝑅 ‘ ( 𝑚 + 1 ) ) − ( 𝑅 ‘ 𝑚 ) ) ) ) → 𝐸 ∈ ( 0 (,) 1 ) )
223 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ ( abs ‘ ( 𝑅 ‘ 𝑚 ) ) ≤ ( abs ‘ ( ( 𝑅 ‘ ( 𝑚 + 1 ) ) − ( 𝑅 ‘ 𝑚 ) ) ) ) → 𝑌 ∈ ( 𝑋 (,) +∞ ) )
224 simpr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ ( abs ‘ ( 𝑅 ‘ 𝑚 ) ) ≤ ( abs ‘ ( ( 𝑅 ‘ ( 𝑚 + 1 ) ) − ( 𝑅 ‘ 𝑚 ) ) ) ) → ( abs ‘ ( 𝑅 ‘ 𝑚 ) ) ≤ ( abs ‘ ( ( 𝑅 ‘ ( 𝑚 + 1 ) ) − ( 𝑅 ‘ 𝑚 ) ) ) )
225 1 222 3 223 205 221 224 pntpbnd1a ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ ( abs ‘ ( 𝑅 ‘ 𝑚 ) ) ≤ ( abs ‘ ( ( 𝑅 ‘ ( 𝑚 + 1 ) ) − ( 𝑅 ‘ 𝑚 ) ) ) ) → ( abs ‘ ( ( 𝑅 ‘ 𝑚 ) / 𝑚 ) ) ≤ 𝐸 )
226 breq2 ⊢ ( 𝑦 = 𝑚 → ( 𝑌 < 𝑦 ↔ 𝑌 < 𝑚 ) )
227 breq1 ⊢ ( 𝑦 = 𝑚 → ( 𝑦 ≤ ( 𝐾 · 𝑌 ) ↔ 𝑚 ≤ ( 𝐾 · 𝑌 ) ) )
228 226 227 anbi12d ⊢ ( 𝑦 = 𝑚 → ( ( 𝑌 < 𝑦 ∧ 𝑦 ≤ ( 𝐾 · 𝑌 ) ) ↔ ( 𝑌 < 𝑚 ∧ 𝑚 ≤ ( 𝐾 · 𝑌 ) ) ) )
229 fveq2 ⊢ ( 𝑦 = 𝑚 → ( 𝑅 ‘ 𝑦 ) = ( 𝑅 ‘ 𝑚 ) )
230 id ⊢ ( 𝑦 = 𝑚 → 𝑦 = 𝑚 )
231 229 230 oveq12d ⊢ ( 𝑦 = 𝑚 → ( ( 𝑅 ‘ 𝑦 ) / 𝑦 ) = ( ( 𝑅 ‘ 𝑚 ) / 𝑚 ) )
232 231 fveq2d ⊢ ( 𝑦 = 𝑚 → ( abs ‘ ( ( 𝑅 ‘ 𝑦 ) / 𝑦 ) ) = ( abs ‘ ( ( 𝑅 ‘ 𝑚 ) / 𝑚 ) ) )
233 232 breq1d ⊢ ( 𝑦 = 𝑚 → ( ( abs ‘ ( ( 𝑅 ‘ 𝑦 ) / 𝑦 ) ) ≤ 𝐸 ↔ ( abs ‘ ( ( 𝑅 ‘ 𝑚 ) / 𝑚 ) ) ≤ 𝐸 ) )
234 228 233 anbi12d ⊢ ( 𝑦 = 𝑚 → ( ( ( 𝑌 < 𝑦 ∧ 𝑦 ≤ ( 𝐾 · 𝑌 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑦 ) / 𝑦 ) ) ≤ 𝐸 ) ↔ ( ( 𝑌 < 𝑚 ∧ 𝑚 ≤ ( 𝐾 · 𝑌 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑚 ) / 𝑚 ) ) ≤ 𝐸 ) ) )
235 234 rspcev ⊢ ( ( 𝑚 ∈ ℕ ∧ ( ( 𝑌 < 𝑚 ∧ 𝑚 ≤ ( 𝐾 · 𝑌 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑚 ) / 𝑚 ) ) ≤ 𝐸 ) ) → ∃ 𝑦 ∈ ℕ ( ( 𝑌 < 𝑦 ∧ 𝑦 ≤ ( 𝐾 · 𝑌 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑦 ) / 𝑦 ) ) ≤ 𝐸 ) )
236 205 221 225 235 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ ( abs ‘ ( 𝑅 ‘ 𝑚 ) ) ≤ ( abs ‘ ( ( 𝑅 ‘ ( 𝑚 + 1 ) ) − ( 𝑅 ‘ 𝑚 ) ) ) ) → ∃ 𝑦 ∈ ℕ ( ( 𝑌 < 𝑦 ∧ 𝑦 ≤ ( 𝐾 · 𝑌 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑦 ) / 𝑦 ) ) ≤ 𝐸 ) )
237 202 236 mtand ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ¬ ( abs ‘ ( 𝑅 ‘ 𝑚 ) ) ≤ ( abs ‘ ( ( 𝑅 ‘ ( 𝑚 + 1 ) ) − ( 𝑅 ‘ 𝑚 ) ) ) )
238 237 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ 0 ≤ ( 𝑅 ‘ 𝑚 ) ) → ¬ ( abs ‘ ( 𝑅 ‘ 𝑚 ) ) ≤ ( abs ‘ ( ( 𝑅 ‘ ( 𝑚 + 1 ) ) − ( 𝑅 ‘ 𝑚 ) ) ) )
239 204 nnrpd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → 𝑚 ∈ ℝ+ )
240 41 ffvelrni ⊢ ( 𝑚 ∈ ℝ+ → ( 𝑅 ‘ 𝑚 ) ∈ ℝ )
241 239 240 syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 𝑅 ‘ 𝑚 ) ∈ ℝ )
242 241 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ ( 0 ≤ ( 𝑅 ‘ 𝑚 ) ∧ ¬ 0 ≤ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ) ) → ( 𝑅 ‘ 𝑚 ) ∈ ℝ )
243 242 recnd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ ( 0 ≤ ( 𝑅 ‘ 𝑚 ) ∧ ¬ 0 ≤ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ) ) → ( 𝑅 ‘ 𝑚 ) ∈ ℂ )
244 243 subid1d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ ( 0 ≤ ( 𝑅 ‘ 𝑚 ) ∧ ¬ 0 ≤ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ) ) → ( ( 𝑅 ‘ 𝑚 ) − 0 ) = ( 𝑅 ‘ 𝑚 ) )
245 204 peano2nnd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 𝑚 + 1 ) ∈ ℕ )
246 245 nnrpd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 𝑚 + 1 ) ∈ ℝ+ )
247 41 ffvelrni ⊢ ( ( 𝑚 + 1 ) ∈ ℝ+ → ( 𝑅 ‘ ( 𝑚 + 1 ) ) ∈ ℝ )
248 246 247 syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 𝑅 ‘ ( 𝑚 + 1 ) ) ∈ ℝ )
249 248 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ ( 0 ≤ ( 𝑅 ‘ 𝑚 ) ∧ ¬ 0 ≤ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ) ) → ( 𝑅 ‘ ( 𝑚 + 1 ) ) ∈ ℝ )
250 0red ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ ( 0 ≤ ( 𝑅 ‘ 𝑚 ) ∧ ¬ 0 ≤ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ) ) → 0 ∈ ℝ )
251 0re ⊢ 0 ∈ ℝ
252 letric ⊢ ( ( 0 ∈ ℝ ∧ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ∈ ℝ ) → ( 0 ≤ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ∨ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ≤ 0 ) )
253 251 248 252 sylancr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 0 ≤ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ∨ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ≤ 0 ) )
254 253 ord ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ¬ 0 ≤ ( 𝑅 ‘ ( 𝑚 + 1 ) ) → ( 𝑅 ‘ ( 𝑚 + 1 ) ) ≤ 0 ) )
255 254 imp ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ ¬ 0 ≤ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ) → ( 𝑅 ‘ ( 𝑚 + 1 ) ) ≤ 0 )
256 255 adantrl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ ( 0 ≤ ( 𝑅 ‘ 𝑚 ) ∧ ¬ 0 ≤ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ) ) → ( 𝑅 ‘ ( 𝑚 + 1 ) ) ≤ 0 )
257 249 250 242 256 lesub2dd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ ( 0 ≤ ( 𝑅 ‘ 𝑚 ) ∧ ¬ 0 ≤ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ) ) → ( ( 𝑅 ‘ 𝑚 ) − 0 ) ≤ ( ( 𝑅 ‘ 𝑚 ) − ( 𝑅 ‘ ( 𝑚 + 1 ) ) ) )
258 244 257 eqbrtrrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ ( 0 ≤ ( 𝑅 ‘ 𝑚 ) ∧ ¬ 0 ≤ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ) ) → ( 𝑅 ‘ 𝑚 ) ≤ ( ( 𝑅 ‘ 𝑚 ) − ( 𝑅 ‘ ( 𝑚 + 1 ) ) ) )
259 simprl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ ( 0 ≤ ( 𝑅 ‘ 𝑚 ) ∧ ¬ 0 ≤ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ) ) → 0 ≤ ( 𝑅 ‘ 𝑚 ) )
260 242 259 absidd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ ( 0 ≤ ( 𝑅 ‘ 𝑚 ) ∧ ¬ 0 ≤ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ) ) → ( abs ‘ ( 𝑅 ‘ 𝑚 ) ) = ( 𝑅 ‘ 𝑚 ) )
261 249 250 242 256 259 letrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ ( 0 ≤ ( 𝑅 ‘ 𝑚 ) ∧ ¬ 0 ≤ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ) ) → ( 𝑅 ‘ ( 𝑚 + 1 ) ) ≤ ( 𝑅 ‘ 𝑚 ) )
262 249 242 261 abssuble0d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ ( 0 ≤ ( 𝑅 ‘ 𝑚 ) ∧ ¬ 0 ≤ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ) ) → ( abs ‘ ( ( 𝑅 ‘ ( 𝑚 + 1 ) ) − ( 𝑅 ‘ 𝑚 ) ) ) = ( ( 𝑅 ‘ 𝑚 ) − ( 𝑅 ‘ ( 𝑚 + 1 ) ) ) )
263 258 260 262 3brtr4d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ ( 0 ≤ ( 𝑅 ‘ 𝑚 ) ∧ ¬ 0 ≤ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ) ) → ( abs ‘ ( 𝑅 ‘ 𝑚 ) ) ≤ ( abs ‘ ( ( 𝑅 ‘ ( 𝑚 + 1 ) ) − ( 𝑅 ‘ 𝑚 ) ) ) )
264 263 expr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ 0 ≤ ( 𝑅 ‘ 𝑚 ) ) → ( ¬ 0 ≤ ( 𝑅 ‘ ( 𝑚 + 1 ) ) → ( abs ‘ ( 𝑅 ‘ 𝑚 ) ) ≤ ( abs ‘ ( ( 𝑅 ‘ ( 𝑚 + 1 ) ) − ( 𝑅 ‘ 𝑚 ) ) ) ) )
265 238 264 mt3d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ 0 ≤ ( 𝑅 ‘ 𝑚 ) ) → 0 ≤ ( 𝑅 ‘ ( 𝑚 + 1 ) ) )
266 265 ex ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( 0 ≤ ( 𝑅 ‘ 𝑚 ) → 0 ≤ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ) )
267 201 266 syld ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) 0 ≤ ( 𝑅 ‘ 𝑖 ) → 0 ≤ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ) )
268 ovex ⊢ ( 𝑚 + 1 ) ∈ V
269 fveq2 ⊢ ( 𝑖 = ( 𝑚 + 1 ) → ( 𝑅 ‘ 𝑖 ) = ( 𝑅 ‘ ( 𝑚 + 1 ) ) )
270 269 breq2d ⊢ ( 𝑖 = ( 𝑚 + 1 ) → ( 0 ≤ ( 𝑅 ‘ 𝑖 ) ↔ 0 ≤ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ) )
271 268 270 ralsn ⊢ ( ∀ 𝑖 ∈ { ( 𝑚 + 1 ) } 0 ≤ ( 𝑅 ‘ 𝑖 ) ↔ 0 ≤ ( 𝑅 ‘ ( 𝑚 + 1 ) ) )
272 267 271 syl6ibr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) 0 ≤ ( 𝑅 ‘ 𝑖 ) → ∀ 𝑖 ∈ { ( 𝑚 + 1 ) } 0 ≤ ( 𝑅 ‘ 𝑖 ) ) )
273 272 ancld ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) 0 ≤ ( 𝑅 ‘ 𝑖 ) → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ∧ ∀ 𝑖 ∈ { ( 𝑚 + 1 ) } 0 ≤ ( 𝑅 ‘ 𝑖 ) ) ) )
274 fzsuc ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑌 ) + 1 ) ) → ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( 𝑚 + 1 ) ) = ( ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) ∪ { ( 𝑚 + 1 ) } ) )
275 195 274 syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( 𝑚 + 1 ) ) = ( ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) ∪ { ( 𝑚 + 1 ) } ) )
276 275 raleqdv ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( 𝑚 + 1 ) ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ↔ ∀ 𝑖 ∈ ( ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) ∪ { ( 𝑚 + 1 ) } ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ) )
277 ralunb ⊢ ( ∀ 𝑖 ∈ ( ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) ∪ { ( 𝑚 + 1 ) } ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ↔ ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ∧ ∀ 𝑖 ∈ { ( 𝑚 + 1 ) } 0 ≤ ( 𝑅 ‘ 𝑖 ) ) )
278 276 277 bitrdi ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( 𝑚 + 1 ) ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ↔ ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ∧ ∀ 𝑖 ∈ { ( 𝑚 + 1 ) } 0 ≤ ( 𝑅 ‘ 𝑖 ) ) ) )
279 273 278 sylibrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) 0 ≤ ( 𝑅 ‘ 𝑖 ) → ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( 𝑚 + 1 ) ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ) )
280 198 breq1d ⊢ ( 𝑖 = 𝑚 → ( ( 𝑅 ‘ 𝑖 ) ≤ 0 ↔ ( 𝑅 ‘ 𝑚 ) ≤ 0 ) )
281 280 rspcv ⊢ ( 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) ( 𝑅 ‘ 𝑖 ) ≤ 0 → ( 𝑅 ‘ 𝑚 ) ≤ 0 ) )
282 197 281 syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) ( 𝑅 ‘ 𝑖 ) ≤ 0 → ( 𝑅 ‘ 𝑚 ) ≤ 0 ) )
283 237 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ ( 𝑅 ‘ 𝑚 ) ≤ 0 ) → ¬ ( abs ‘ ( 𝑅 ‘ 𝑚 ) ) ≤ ( abs ‘ ( ( 𝑅 ‘ ( 𝑚 + 1 ) ) − ( 𝑅 ‘ 𝑚 ) ) ) )
284 254 con1d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ¬ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ≤ 0 → 0 ≤ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ) )
285 284 imp ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ ¬ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ≤ 0 ) → 0 ≤ ( 𝑅 ‘ ( 𝑚 + 1 ) ) )
286 285 adantrl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ ( ( 𝑅 ‘ 𝑚 ) ≤ 0 ∧ ¬ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ≤ 0 ) ) → 0 ≤ ( 𝑅 ‘ ( 𝑚 + 1 ) ) )
287 241 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ ( ( 𝑅 ‘ 𝑚 ) ≤ 0 ∧ ¬ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ≤ 0 ) ) → ( 𝑅 ‘ 𝑚 ) ∈ ℝ )
288 287 renegcld ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ ( ( 𝑅 ‘ 𝑚 ) ≤ 0 ∧ ¬ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ≤ 0 ) ) → - ( 𝑅 ‘ 𝑚 ) ∈ ℝ )
289 248 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ ( ( 𝑅 ‘ 𝑚 ) ≤ 0 ∧ ¬ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ≤ 0 ) ) → ( 𝑅 ‘ ( 𝑚 + 1 ) ) ∈ ℝ )
290 288 289 addge02d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ ( ( 𝑅 ‘ 𝑚 ) ≤ 0 ∧ ¬ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ≤ 0 ) ) → ( 0 ≤ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ↔ - ( 𝑅 ‘ 𝑚 ) ≤ ( ( 𝑅 ‘ ( 𝑚 + 1 ) ) + - ( 𝑅 ‘ 𝑚 ) ) ) )
291 286 290 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ ( ( 𝑅 ‘ 𝑚 ) ≤ 0 ∧ ¬ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ≤ 0 ) ) → - ( 𝑅 ‘ 𝑚 ) ≤ ( ( 𝑅 ‘ ( 𝑚 + 1 ) ) + - ( 𝑅 ‘ 𝑚 ) ) )
292 289 recnd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ ( ( 𝑅 ‘ 𝑚 ) ≤ 0 ∧ ¬ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ≤ 0 ) ) → ( 𝑅 ‘ ( 𝑚 + 1 ) ) ∈ ℂ )
293 287 recnd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ ( ( 𝑅 ‘ 𝑚 ) ≤ 0 ∧ ¬ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ≤ 0 ) ) → ( 𝑅 ‘ 𝑚 ) ∈ ℂ )
294 292 293 negsubd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ ( ( 𝑅 ‘ 𝑚 ) ≤ 0 ∧ ¬ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ≤ 0 ) ) → ( ( 𝑅 ‘ ( 𝑚 + 1 ) ) + - ( 𝑅 ‘ 𝑚 ) ) = ( ( 𝑅 ‘ ( 𝑚 + 1 ) ) − ( 𝑅 ‘ 𝑚 ) ) )
295 291 294 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ ( ( 𝑅 ‘ 𝑚 ) ≤ 0 ∧ ¬ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ≤ 0 ) ) → - ( 𝑅 ‘ 𝑚 ) ≤ ( ( 𝑅 ‘ ( 𝑚 + 1 ) ) − ( 𝑅 ‘ 𝑚 ) ) )
296 simprl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ ( ( 𝑅 ‘ 𝑚 ) ≤ 0 ∧ ¬ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ≤ 0 ) ) → ( 𝑅 ‘ 𝑚 ) ≤ 0 )
297 287 296 absnidd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ ( ( 𝑅 ‘ 𝑚 ) ≤ 0 ∧ ¬ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ≤ 0 ) ) → ( abs ‘ ( 𝑅 ‘ 𝑚 ) ) = - ( 𝑅 ‘ 𝑚 ) )
298 0red ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ ( ( 𝑅 ‘ 𝑚 ) ≤ 0 ∧ ¬ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ≤ 0 ) ) → 0 ∈ ℝ )
299 287 298 289 296 286 letrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ ( ( 𝑅 ‘ 𝑚 ) ≤ 0 ∧ ¬ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ≤ 0 ) ) → ( 𝑅 ‘ 𝑚 ) ≤ ( 𝑅 ‘ ( 𝑚 + 1 ) ) )
300 287 289 299 abssubge0d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ ( ( 𝑅 ‘ 𝑚 ) ≤ 0 ∧ ¬ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ≤ 0 ) ) → ( abs ‘ ( ( 𝑅 ‘ ( 𝑚 + 1 ) ) − ( 𝑅 ‘ 𝑚 ) ) ) = ( ( 𝑅 ‘ ( 𝑚 + 1 ) ) − ( 𝑅 ‘ 𝑚 ) ) )
301 295 297 300 3brtr4d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ ( ( 𝑅 ‘ 𝑚 ) ≤ 0 ∧ ¬ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ≤ 0 ) ) → ( abs ‘ ( 𝑅 ‘ 𝑚 ) ) ≤ ( abs ‘ ( ( 𝑅 ‘ ( 𝑚 + 1 ) ) − ( 𝑅 ‘ 𝑚 ) ) ) )
302 301 expr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ ( 𝑅 ‘ 𝑚 ) ≤ 0 ) → ( ¬ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ≤ 0 → ( abs ‘ ( 𝑅 ‘ 𝑚 ) ) ≤ ( abs ‘ ( ( 𝑅 ‘ ( 𝑚 + 1 ) ) − ( 𝑅 ‘ 𝑚 ) ) ) ) )
303 283 302 mt3d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ∧ ( 𝑅 ‘ 𝑚 ) ≤ 0 ) → ( 𝑅 ‘ ( 𝑚 + 1 ) ) ≤ 0 )
304 303 ex ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ( 𝑅 ‘ 𝑚 ) ≤ 0 → ( 𝑅 ‘ ( 𝑚 + 1 ) ) ≤ 0 ) )
305 282 304 syld ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) ( 𝑅 ‘ 𝑖 ) ≤ 0 → ( 𝑅 ‘ ( 𝑚 + 1 ) ) ≤ 0 ) )
306 269 breq1d ⊢ ( 𝑖 = ( 𝑚 + 1 ) → ( ( 𝑅 ‘ 𝑖 ) ≤ 0 ↔ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ≤ 0 ) )
307 268 306 ralsn ⊢ ( ∀ 𝑖 ∈ { ( 𝑚 + 1 ) } ( 𝑅 ‘ 𝑖 ) ≤ 0 ↔ ( 𝑅 ‘ ( 𝑚 + 1 ) ) ≤ 0 )
308 305 307 syl6ibr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) ( 𝑅 ‘ 𝑖 ) ≤ 0 → ∀ 𝑖 ∈ { ( 𝑚 + 1 ) } ( 𝑅 ‘ 𝑖 ) ≤ 0 ) )
309 308 ancld ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) ( 𝑅 ‘ 𝑖 ) ≤ 0 → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ∧ ∀ 𝑖 ∈ { ( 𝑚 + 1 ) } ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ) )
310 275 raleqdv ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( 𝑚 + 1 ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ↔ ∀ 𝑖 ∈ ( ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) ∪ { ( 𝑚 + 1 ) } ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) )
311 ralunb ⊢ ( ∀ 𝑖 ∈ ( ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) ∪ { ( 𝑚 + 1 ) } ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ↔ ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ∧ ∀ 𝑖 ∈ { ( 𝑚 + 1 ) } ( 𝑅 ‘ 𝑖 ) ≤ 0 ) )
312 310 311 bitrdi ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( 𝑚 + 1 ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ↔ ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ∧ ∀ 𝑖 ∈ { ( 𝑚 + 1 ) } ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ) )
313 309 312 sylibrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) ( 𝑅 ‘ 𝑖 ) ≤ 0 → ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( 𝑚 + 1 ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) )
314 279 313 orim12d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ∨ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( 𝑚 + 1 ) ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ∨ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( 𝑚 + 1 ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ) )
315 193 314 jaodan ⊢ ( ( 𝜑 ∧ ( 𝑚 = ( ⌊ ‘ 𝑌 ) ∨ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) ) → ( ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ∨ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( 𝑚 + 1 ) ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ∨ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( 𝑚 + 1 ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ) )
316 168 315 syldan ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ⌊ ‘ 𝑌 ) ..^ ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ) → ( ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ∨ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( 𝑚 + 1 ) ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ∨ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( 𝑚 + 1 ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ) )
317 316 expcom ⊢ ( 𝑚 ∈ ( ( ⌊ ‘ 𝑌 ) ..^ ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) → ( 𝜑 → ( ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ∨ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( 𝑚 + 1 ) ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ∨ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( 𝑚 + 1 ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ) ) )
318 317 a2d ⊢ ( 𝑚 ∈ ( ( ⌊ ‘ 𝑌 ) ..^ ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) → ( ( 𝜑 → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ∨ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑚 ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ) → ( 𝜑 → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( 𝑚 + 1 ) ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ∨ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( 𝑚 + 1 ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ) ) )
319 136 141 146 151 163 318 fzind2 ⊢ ( ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ∈ ( ( ⌊ ‘ 𝑌 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) → ( 𝜑 → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ∨ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) ) )
320 131 319 mpcom ⊢ ( 𝜑 → ( ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) 0 ≤ ( 𝑅 ‘ 𝑖 ) ∨ ∀ 𝑖 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( 𝑅 ‘ 𝑖 ) ≤ 0 ) )
321 63 97 320 mpjaodan ⊢ ( 𝜑 → ( abs ‘ Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) = Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) )
322 fveq2 ⊢ ( 𝑦 = 𝑛 → ( 𝑅 ‘ 𝑦 ) = ( 𝑅 ‘ 𝑛 ) )
323 id ⊢ ( 𝑦 = 𝑛 → 𝑦 = 𝑛 )
324 oveq1 ⊢ ( 𝑦 = 𝑛 → ( 𝑦 + 1 ) = ( 𝑛 + 1 ) )
325 323 324 oveq12d ⊢ ( 𝑦 = 𝑛 → ( 𝑦 · ( 𝑦 + 1 ) ) = ( 𝑛 · ( 𝑛 + 1 ) ) )
326 322 325 oveq12d ⊢ ( 𝑦 = 𝑛 → ( ( 𝑅 ‘ 𝑦 ) / ( 𝑦 · ( 𝑦 + 1 ) ) ) = ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) )
327 326 cbvsumv ⊢ Σ 𝑦 ∈ ( 𝑖 ... 𝑗 ) ( ( 𝑅 ‘ 𝑦 ) / ( 𝑦 · ( 𝑦 + 1 ) ) ) = Σ 𝑛 ∈ ( 𝑖 ... 𝑗 ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) )
328 oveq1 ⊢ ( 𝑖 = ( ( ⌊ ‘ 𝑌 ) + 1 ) → ( 𝑖 ... 𝑗 ) = ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑗 ) )
329 328 sumeq1d ⊢ ( 𝑖 = ( ( ⌊ ‘ 𝑌 ) + 1 ) → Σ 𝑛 ∈ ( 𝑖 ... 𝑗 ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) = Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑗 ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) )
330 327 329 syl5eq ⊢ ( 𝑖 = ( ( ⌊ ‘ 𝑌 ) + 1 ) → Σ 𝑦 ∈ ( 𝑖 ... 𝑗 ) ( ( 𝑅 ‘ 𝑦 ) / ( 𝑦 · ( 𝑦 + 1 ) ) ) = Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑗 ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) )
331 330 fveq2d ⊢ ( 𝑖 = ( ( ⌊ ‘ 𝑌 ) + 1 ) → ( abs ‘ Σ 𝑦 ∈ ( 𝑖 ... 𝑗 ) ( ( 𝑅 ‘ 𝑦 ) / ( 𝑦 · ( 𝑦 + 1 ) ) ) ) = ( abs ‘ Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑗 ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) )
332 331 breq1d ⊢ ( 𝑖 = ( ( ⌊ ‘ 𝑌 ) + 1 ) → ( ( abs ‘ Σ 𝑦 ∈ ( 𝑖 ... 𝑗 ) ( ( 𝑅 ‘ 𝑦 ) / ( 𝑦 · ( 𝑦 + 1 ) ) ) ) ≤ 𝐴 ↔ ( abs ‘ Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑗 ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝐴 ) )
333 oveq2 ⊢ ( 𝑗 = ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) → ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑗 ) = ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) )
334 333 sumeq1d ⊢ ( 𝑗 = ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) → Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑗 ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) = Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) )
335 334 fveq2d ⊢ ( 𝑗 = ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) → ( abs ‘ Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑗 ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) = ( abs ‘ Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) )
336 335 breq1d ⊢ ( 𝑗 = ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) → ( ( abs ‘ Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... 𝑗 ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝐴 ↔ ( abs ‘ Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝐴 ) )
337 332 336 rspc2va ⊢ ( ( ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ∈ ℕ ∧ ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ∈ ℤ ) ∧ ∀ 𝑖 ∈ ℕ ∀ 𝑗 ∈ ℤ ( abs ‘ Σ 𝑦 ∈ ( 𝑖 ... 𝑗 ) ( ( 𝑅 ‘ 𝑦 ) / ( 𝑦 · ( 𝑦 + 1 ) ) ) ) ≤ 𝐴 ) → ( abs ‘ Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝐴 )
338 36 127 6 337 syl21anc ⊢ ( 𝜑 → ( abs ‘ Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝐴 )
339 321 338 eqbrtrrd ⊢ ( 𝜑 → Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑌 ) + 1 ) ... ( ⌊ ‘ ( 𝐾 · 𝑌 ) ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝐴 )