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 ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑒 )

Metamath Proof Explorer

Theorem pntpbnd

Proof