Metamath Proof Explorer

Theorem pntpbnd

Description: Lemma for pnt . Establish smallness of R at a point. Lemma 10.6.1 in Shapiro, p. 436. (Contributed by Mario Carneiro, 10-Apr-2016)

Ref Expression
Hypothesis pntibnd.r ⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
Assertion pntpbnd ∃ 𝑐 ∈ ℝ+ ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝑐 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( 𝑘 · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑒 )

Proof

Step Hyp Ref Expression
1 pntibnd.r ⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
2 1 pntrsumbnd2 ⊢ ∃ 𝑑 ∈ ℝ+ ∀ 𝑖 ∈ ℕ ∀ 𝑗 ∈ ℤ ( abs ‘ Σ 𝑛 ∈ ( 𝑖 ... 𝑗 ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝑑
3 simpl ⊢ ( ( 𝑑 ∈ ℝ+ ∧ ∀ 𝑖 ∈ ℕ ∀ 𝑗 ∈ ℤ ( abs ‘ Σ 𝑛 ∈ ( 𝑖 ... 𝑗 ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝑑 ) → 𝑑 ∈ ℝ+ )
4 2rp ⊢ 2 ∈ ℝ+
5 rpaddcl ⊢ ( ( 𝑑 ∈ ℝ+ ∧ 2 ∈ ℝ+ ) → ( 𝑑 + 2 ) ∈ ℝ+ )
6 3 4 5 sylancl ⊢ ( ( 𝑑 ∈ ℝ+ ∧ ∀ 𝑖 ∈ ℕ ∀ 𝑗 ∈ ℤ ( abs ‘ Σ 𝑛 ∈ ( 𝑖 ... 𝑗 ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝑑 ) → ( 𝑑 + 2 ) ∈ ℝ+ )
7 2re ⊢ 2 ∈ ℝ
8 elioore ⊢ ( 𝑒 ∈ ( 0 (,) 1 ) → 𝑒 ∈ ℝ )
9 8 adantl ⊢ ( ( ( 𝑑 ∈ ℝ+ ∧ ∀ 𝑖 ∈ ℕ ∀ 𝑗 ∈ ℤ ( abs ‘ Σ 𝑛 ∈ ( 𝑖 ... 𝑗 ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝑑 ) ∧ 𝑒 ∈ ( 0 (,) 1 ) ) → 𝑒 ∈ ℝ )
10 eliooord ⊢ ( 𝑒 ∈ ( 0 (,) 1 ) → ( 0 < 𝑒 ∧ 𝑒 < 1 ) )
11 10 adantl ⊢ ( ( ( 𝑑 ∈ ℝ+ ∧ ∀ 𝑖 ∈ ℕ ∀ 𝑗 ∈ ℤ ( abs ‘ Σ 𝑛 ∈ ( 𝑖 ... 𝑗 ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝑑 ) ∧ 𝑒 ∈ ( 0 (,) 1 ) ) → ( 0 < 𝑒 ∧ 𝑒 < 1 ) )
12 11 simpld ⊢ ( ( ( 𝑑 ∈ ℝ+ ∧ ∀ 𝑖 ∈ ℕ ∀ 𝑗 ∈ ℤ ( abs ‘ Σ 𝑛 ∈ ( 𝑖 ... 𝑗 ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝑑 ) ∧ 𝑒 ∈ ( 0 (,) 1 ) ) → 0 < 𝑒 )
13 9 12 elrpd ⊢ ( ( ( 𝑑 ∈ ℝ+ ∧ ∀ 𝑖 ∈ ℕ ∀ 𝑗 ∈ ℤ ( abs ‘ Σ 𝑛 ∈ ( 𝑖 ... 𝑗 ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝑑 ) ∧ 𝑒 ∈ ( 0 (,) 1 ) ) → 𝑒 ∈ ℝ+ )
14 rerpdivcl ⊢ ( ( 2 ∈ ℝ ∧ 𝑒 ∈ ℝ+ ) → ( 2 / 𝑒 ) ∈ ℝ )
15 7 13 14 sylancr ⊢ ( ( ( 𝑑 ∈ ℝ+ ∧ ∀ 𝑖 ∈ ℕ ∀ 𝑗 ∈ ℤ ( abs ‘ Σ 𝑛 ∈ ( 𝑖 ... 𝑗 ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝑑 ) ∧ 𝑒 ∈ ( 0 (,) 1 ) ) → ( 2 / 𝑒 ) ∈ ℝ )
16 15 rpefcld ⊢ ( ( ( 𝑑 ∈ ℝ+ ∧ ∀ 𝑖 ∈ ℕ ∀ 𝑗 ∈ ℤ ( abs ‘ Σ 𝑛 ∈ ( 𝑖 ... 𝑗 ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝑑 ) ∧ 𝑒 ∈ ( 0 (,) 1 ) ) → ( exp ‘ ( 2 / 𝑒 ) ) ∈ ℝ+ )
17 simpllr ⊢ ( ( ( ( ( 𝑑 ∈ ℝ+ ∧ ∀ 𝑖 ∈ ℕ ∀ 𝑗 ∈ ℤ ( abs ‘ Σ 𝑛 ∈ ( 𝑖 ... 𝑗 ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝑑 ) ∧ 𝑒 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑘 ∈ ( ( exp ‘ ( ( 𝑑 + 2 ) / 𝑒 ) ) [,) +∞ ) ∧ 𝑦 ∈ ( ( exp ‘ ( 2 / 𝑒 ) ) (,) +∞ ) ) ) ∧ ¬ ∃ 𝑛 ∈ ℕ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( 𝑘 · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑒 ) ) → 𝑒 ∈ ( 0 (,) 1 ) )
18 eqid ⊢ ( exp ‘ ( 2 / 𝑒 ) ) = ( exp ‘ ( 2 / 𝑒 ) )
19 simplrr ⊢ ( ( ( ( ( 𝑑 ∈ ℝ+ ∧ ∀ 𝑖 ∈ ℕ ∀ 𝑗 ∈ ℤ ( abs ‘ Σ 𝑛 ∈ ( 𝑖 ... 𝑗 ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝑑 ) ∧ 𝑒 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑘 ∈ ( ( exp ‘ ( ( 𝑑 + 2 ) / 𝑒 ) ) [,) +∞ ) ∧ 𝑦 ∈ ( ( exp ‘ ( 2 / 𝑒 ) ) (,) +∞ ) ) ) ∧ ¬ ∃ 𝑛 ∈ ℕ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( 𝑘 · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑒 ) ) → 𝑦 ∈ ( ( exp ‘ ( 2 / 𝑒 ) ) (,) +∞ ) )
20 simp-4l ⊢ ( ( ( ( ( 𝑑 ∈ ℝ+ ∧ ∀ 𝑖 ∈ ℕ ∀ 𝑗 ∈ ℤ ( abs ‘ Σ 𝑛 ∈ ( 𝑖 ... 𝑗 ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝑑 ) ∧ 𝑒 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑘 ∈ ( ( exp ‘ ( ( 𝑑 + 2 ) / 𝑒 ) ) [,) +∞ ) ∧ 𝑦 ∈ ( ( exp ‘ ( 2 / 𝑒 ) ) (,) +∞ ) ) ) ∧ ¬ ∃ 𝑛 ∈ ℕ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( 𝑘 · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑒 ) ) → 𝑑 ∈ ℝ+ )
21 simp-4r ⊢ ( ( ( ( ( 𝑑 ∈ ℝ+ ∧ ∀ 𝑖 ∈ ℕ ∀ 𝑗 ∈ ℤ ( abs ‘ Σ 𝑛 ∈ ( 𝑖 ... 𝑗 ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝑑 ) ∧ 𝑒 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑘 ∈ ( ( exp ‘ ( ( 𝑑 + 2 ) / 𝑒 ) ) [,) +∞ ) ∧ 𝑦 ∈ ( ( exp ‘ ( 2 / 𝑒 ) ) (,) +∞ ) ) ) ∧ ¬ ∃ 𝑛 ∈ ℕ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( 𝑘 · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑒 ) ) → ∀ 𝑖 ∈ ℕ ∀ 𝑗 ∈ ℤ ( abs ‘ Σ 𝑛 ∈ ( 𝑖 ... 𝑗 ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝑑 )
22 eqid ⊢ ( 𝑑 + 2 ) = ( 𝑑 + 2 )
23 simplrl ⊢ ( ( ( ( ( 𝑑 ∈ ℝ+ ∧ ∀ 𝑖 ∈ ℕ ∀ 𝑗 ∈ ℤ ( abs ‘ Σ 𝑛 ∈ ( 𝑖 ... 𝑗 ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝑑 ) ∧ 𝑒 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑘 ∈ ( ( exp ‘ ( ( 𝑑 + 2 ) / 𝑒 ) ) [,) +∞ ) ∧ 𝑦 ∈ ( ( exp ‘ ( 2 / 𝑒 ) ) (,) +∞ ) ) ) ∧ ¬ ∃ 𝑛 ∈ ℕ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( 𝑘 · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑒 ) ) → 𝑘 ∈ ( ( exp ‘ ( ( 𝑑 + 2 ) / 𝑒 ) ) [,) +∞ ) )
24 simpr ⊢ ( ( ( ( ( 𝑑 ∈ ℝ+ ∧ ∀ 𝑖 ∈ ℕ ∀ 𝑗 ∈ ℤ ( abs ‘ Σ 𝑛 ∈ ( 𝑖 ... 𝑗 ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝑑 ) ∧ 𝑒 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑘 ∈ ( ( exp ‘ ( ( 𝑑 + 2 ) / 𝑒 ) ) [,) +∞ ) ∧ 𝑦 ∈ ( ( exp ‘ ( 2 / 𝑒 ) ) (,) +∞ ) ) ) ∧ ¬ ∃ 𝑛 ∈ ℕ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( 𝑘 · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑒 ) ) → ¬ ∃ 𝑛 ∈ ℕ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( 𝑘 · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑒 ) )
25 1 17 18 19 20 21 22 23 24 pntpbnd2 ⊢ ¬ ( ( ( ( 𝑑 ∈ ℝ+ ∧ ∀ 𝑖 ∈ ℕ ∀ 𝑗 ∈ ℤ ( abs ‘ Σ 𝑛 ∈ ( 𝑖 ... 𝑗 ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝑑 ) ∧ 𝑒 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑘 ∈ ( ( exp ‘ ( ( 𝑑 + 2 ) / 𝑒 ) ) [,) +∞ ) ∧ 𝑦 ∈ ( ( exp ‘ ( 2 / 𝑒 ) ) (,) +∞ ) ) ) ∧ ¬ ∃ 𝑛 ∈ ℕ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( 𝑘 · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑒 ) )
26 iman ⊢ ( ( ( ( ( 𝑑 ∈ ℝ+ ∧ ∀ 𝑖 ∈ ℕ ∀ 𝑗 ∈ ℤ ( abs ‘ Σ 𝑛 ∈ ( 𝑖 ... 𝑗 ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝑑 ) ∧ 𝑒 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑘 ∈ ( ( exp ‘ ( ( 𝑑 + 2 ) / 𝑒 ) ) [,) +∞ ) ∧ 𝑦 ∈ ( ( exp ‘ ( 2 / 𝑒 ) ) (,) +∞ ) ) ) → ∃ 𝑛 ∈ ℕ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( 𝑘 · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑒 ) ) ↔ ¬ ( ( ( ( 𝑑 ∈ ℝ+ ∧ ∀ 𝑖 ∈ ℕ ∀ 𝑗 ∈ ℤ ( abs ‘ Σ 𝑛 ∈ ( 𝑖 ... 𝑗 ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝑑 ) ∧ 𝑒 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑘 ∈ ( ( exp ‘ ( ( 𝑑 + 2 ) / 𝑒 ) ) [,) +∞ ) ∧ 𝑦 ∈ ( ( exp ‘ ( 2 / 𝑒 ) ) (,) +∞ ) ) ) ∧ ¬ ∃ 𝑛 ∈ ℕ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( 𝑘 · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑒 ) ) )
27 25 26 mpbir ⊢ ( ( ( ( 𝑑 ∈ ℝ+ ∧ ∀ 𝑖 ∈ ℕ ∀ 𝑗 ∈ ℤ ( abs ‘ Σ 𝑛 ∈ ( 𝑖 ... 𝑗 ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝑑 ) ∧ 𝑒 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑘 ∈ ( ( exp ‘ ( ( 𝑑 + 2 ) / 𝑒 ) ) [,) +∞ ) ∧ 𝑦 ∈ ( ( exp ‘ ( 2 / 𝑒 ) ) (,) +∞ ) ) ) → ∃ 𝑛 ∈ ℕ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( 𝑘 · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑒 ) )
28 27 ralrimivva ⊢ ( ( ( 𝑑 ∈ ℝ+ ∧ ∀ 𝑖 ∈ ℕ ∀ 𝑗 ∈ ℤ ( abs ‘ Σ 𝑛 ∈ ( 𝑖 ... 𝑗 ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝑑 ) ∧ 𝑒 ∈ ( 0 (,) 1 ) ) → ∀ 𝑘 ∈ ( ( exp ‘ ( ( 𝑑 + 2 ) / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( ( exp ‘ ( 2 / 𝑒 ) ) (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( 𝑘 · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑒 ) )
29 oveq1 ⊢ ( 𝑥 = ( exp ‘ ( 2 / 𝑒 ) ) → ( 𝑥 (,) +∞ ) = ( ( exp ‘ ( 2 / 𝑒 ) ) (,) +∞ ) )
30 29 raleqdv ⊢ ( 𝑥 = ( exp ‘ ( 2 / 𝑒 ) ) → ( ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( 𝑘 · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑒 ) ↔ ∀ 𝑦 ∈ ( ( exp ‘ ( 2 / 𝑒 ) ) (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( 𝑘 · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑒 ) ) )
31 30 ralbidv ⊢ ( 𝑥 = ( exp ‘ ( 2 / 𝑒 ) ) → ( ∀ 𝑘 ∈ ( ( exp ‘ ( ( 𝑑 + 2 ) / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( 𝑘 · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑒 ) ↔ ∀ 𝑘 ∈ ( ( exp ‘ ( ( 𝑑 + 2 ) / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( ( exp ‘ ( 2 / 𝑒 ) ) (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( 𝑘 · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑒 ) ) )
32 31 rspcev ⊢ ( ( ( exp ‘ ( 2 / 𝑒 ) ) ∈ ℝ+ ∧ ∀ 𝑘 ∈ ( ( exp ‘ ( ( 𝑑 + 2 ) / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( ( exp ‘ ( 2 / 𝑒 ) ) (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( 𝑘 · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑒 ) ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( ( 𝑑 + 2 ) / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( 𝑘 · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑒 ) )
33 16 28 32 syl2anc ⊢ ( ( ( 𝑑 ∈ ℝ+ ∧ ∀ 𝑖 ∈ ℕ ∀ 𝑗 ∈ ℤ ( abs ‘ Σ 𝑛 ∈ ( 𝑖 ... 𝑗 ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝑑 ) ∧ 𝑒 ∈ ( 0 (,) 1 ) ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( ( 𝑑 + 2 ) / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( 𝑘 · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑒 ) )
34 33 ralrimiva ⊢ ( ( 𝑑 ∈ ℝ+ ∧ ∀ 𝑖 ∈ ℕ ∀ 𝑗 ∈ ℤ ( abs ‘ Σ 𝑛 ∈ ( 𝑖 ... 𝑗 ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝑑 ) → ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( ( 𝑑 + 2 ) / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( 𝑘 · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑒 ) )
35 fvoveq1 ⊢ ( 𝑐 = ( 𝑑 + 2 ) → ( exp ‘ ( 𝑐 / 𝑒 ) ) = ( exp ‘ ( ( 𝑑 + 2 ) / 𝑒 ) ) )
36 35 oveq1d ⊢ ( 𝑐 = ( 𝑑 + 2 ) → ( ( exp ‘ ( 𝑐 / 𝑒 ) ) [,) +∞ ) = ( ( exp ‘ ( ( 𝑑 + 2 ) / 𝑒 ) ) [,) +∞ ) )
37 36 raleqdv ⊢ ( 𝑐 = ( 𝑑 + 2 ) → ( ∀ 𝑘 ∈ ( ( exp ‘ ( 𝑐 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( 𝑘 · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑒 ) ↔ ∀ 𝑘 ∈ ( ( exp ‘ ( ( 𝑑 + 2 ) / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( 𝑘 · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑒 ) ) )
38 37 rexbidv ⊢ ( 𝑐 = ( 𝑑 + 2 ) → ( ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝑐 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( 𝑘 · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑒 ) ↔ ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( ( 𝑑 + 2 ) / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( 𝑘 · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑒 ) ) )
39 38 ralbidv ⊢ ( 𝑐 = ( 𝑑 + 2 ) → ( ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝑐 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( 𝑘 · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑒 ) ↔ ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( ( 𝑑 + 2 ) / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( 𝑘 · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑒 ) ) )
40 39 rspcev ⊢ ( ( ( 𝑑 + 2 ) ∈ ℝ+ ∧ ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( ( 𝑑 + 2 ) / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( 𝑘 · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑒 ) ) → ∃ 𝑐 ∈ ℝ+ ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝑐 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( 𝑘 · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑒 ) )
41 6 34 40 syl2anc ⊢ ( ( 𝑑 ∈ ℝ+ ∧ ∀ 𝑖 ∈ ℕ ∀ 𝑗 ∈ ℤ ( abs ‘ Σ 𝑛 ∈ ( 𝑖 ... 𝑗 ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝑑 ) → ∃ 𝑐 ∈ ℝ+ ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝑐 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( 𝑘 · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑒 ) )
42 41 rexlimiva ⊢ ( ∃ 𝑑 ∈ ℝ+ ∀ 𝑖 ∈ ℕ ∀ 𝑗 ∈ ℤ ( abs ‘ Σ 𝑛 ∈ ( 𝑖 ... 𝑗 ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝑑 → ∃ 𝑐 ∈ ℝ+ ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝑐 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( 𝑘 · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑒 ) )
43 2 42 ax-mp ⊢ ∃ 𝑐 ∈ ℝ+ ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝑐 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( 𝑘 · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑒 )