Theorem pnt3

Description: The Prime Number Theorem, version 3: the second Chebyshev function tends asymptotically to x . (Contributed by Mario Carneiro, 1-Jun-2016)

	Ref	Expression
Assertion	pnt3	⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) ⇝𝑟 1

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
2	1	pntrmax	⊢ ∃ 𝑏 ∈ ℝ+ ∀ 𝑟 ∈ ℝ+ ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑟 ) / 𝑟 ) ) ≤ 𝑏
3	1	pntibnd	⊢ ∃ 𝑐 ∈ ℝ+ ∃ 𝑙 ∈ ( 0 (,) 1 ) ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑟 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝑐 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑟 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 )
4		simpll	⊢ ( ( ( 𝑏 ∈ ℝ+ ∧ ∀ 𝑟 ∈ ℝ+ ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑟 ) / 𝑟 ) ) ≤ 𝑏 ) ∧ ( ( 𝑐 ∈ ℝ+ ∧ 𝑙 ∈ ( 0 (,) 1 ) ) ∧ ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑟 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝑐 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑟 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ) ) → 𝑏 ∈ ℝ+ )
5		simplr	⊢ ( ( ( 𝑏 ∈ ℝ+ ∧ ∀ 𝑟 ∈ ℝ+ ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑟 ) / 𝑟 ) ) ≤ 𝑏 ) ∧ ( ( 𝑐 ∈ ℝ+ ∧ 𝑙 ∈ ( 0 (,) 1 ) ) ∧ ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑟 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝑐 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑟 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ) ) → ∀ 𝑟 ∈ ℝ+ ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑟 ) / 𝑟 ) ) ≤ 𝑏 )
6		fveq2	⊢ ( 𝑟 = 𝑥 → ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑟 ) = ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑥 ) )
7		id	⊢ ( 𝑟 = 𝑥 → 𝑟 = 𝑥 )
8	6 7	oveq12d	⊢ ( 𝑟 = 𝑥 → ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑟 ) / 𝑟 ) = ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑥 ) / 𝑥 ) )
9	8	fveq2d	⊢ ( 𝑟 = 𝑥 → ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑟 ) / 𝑟 ) ) = ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑥 ) / 𝑥 ) ) )
10	9	breq1d	⊢ ( 𝑟 = 𝑥 → ( ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑟 ) / 𝑟 ) ) ≤ 𝑏 ↔ ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝑏 ) )
11	10	cbvralvw	⊢ ( ∀ 𝑟 ∈ ℝ+ ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑟 ) / 𝑟 ) ) ≤ 𝑏 ↔ ∀ 𝑥 ∈ ℝ+ ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝑏 )
12	5 11	sylib	⊢ ( ( ( 𝑏 ∈ ℝ+ ∧ ∀ 𝑟 ∈ ℝ+ ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑟 ) / 𝑟 ) ) ≤ 𝑏 ) ∧ ( ( 𝑐 ∈ ℝ+ ∧ 𝑙 ∈ ( 0 (,) 1 ) ) ∧ ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑟 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝑐 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑟 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ) ) → ∀ 𝑥 ∈ ℝ+ ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝑏 )
13		simprll	⊢ ( ( ( 𝑏 ∈ ℝ+ ∧ ∀ 𝑟 ∈ ℝ+ ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑟 ) / 𝑟 ) ) ≤ 𝑏 ) ∧ ( ( 𝑐 ∈ ℝ+ ∧ 𝑙 ∈ ( 0 (,) 1 ) ) ∧ ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑟 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝑐 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑟 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ) ) → 𝑐 ∈ ℝ+ )
14		simprlr	⊢ ( ( ( 𝑏 ∈ ℝ+ ∧ ∀ 𝑟 ∈ ℝ+ ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑟 ) / 𝑟 ) ) ≤ 𝑏 ) ∧ ( ( 𝑐 ∈ ℝ+ ∧ 𝑙 ∈ ( 0 (,) 1 ) ) ∧ ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑟 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝑐 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑟 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ) ) → 𝑙 ∈ ( 0 (,) 1 ) )
15		eqid	⊢ ( 𝑏 + 1 ) = ( 𝑏 + 1 )
16		eqid	⊢ ( ( 1 − ( 1 / ( 𝑏 + 1 ) ) ) · ( ( 𝑙 / ( ; 3 2 · 𝑐 ) ) / ( ( 𝑏 + 1 ) ↑ 2 ) ) ) = ( ( 1 − ( 1 / ( 𝑏 + 1 ) ) ) · ( ( 𝑙 / ( ; 3 2 · 𝑐 ) ) / ( ( 𝑏 + 1 ) ↑ 2 ) ) )
17		simprr	⊢ ( ( ( 𝑏 ∈ ℝ+ ∧ ∀ 𝑟 ∈ ℝ+ ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑟 ) / 𝑟 ) ) ≤ 𝑏 ) ∧ ( ( 𝑐 ∈ ℝ+ ∧ 𝑙 ∈ ( 0 (,) 1 ) ) ∧ ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑟 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝑐 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑟 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ) ) → ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑟 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝑐 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑟 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) )
18		breq2	⊢ ( 𝑧 = 𝑔 → ( 𝑦 < 𝑧 ↔ 𝑦 < 𝑔 ) )
19		oveq2	⊢ ( 𝑧 = 𝑔 → ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) = ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑔 ) )
20	19	breq1d	⊢ ( 𝑧 = 𝑔 → ( ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ↔ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑔 ) < ( 𝑘 · 𝑦 ) ) )
21	18 20	anbi12d	⊢ ( 𝑧 = 𝑔 → ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ↔ ( 𝑦 < 𝑔 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑔 ) < ( 𝑘 · 𝑦 ) ) ) )
22		id	⊢ ( 𝑧 = 𝑔 → 𝑧 = 𝑔 )
23	22 19	oveq12d	⊢ ( 𝑧 = 𝑔 → ( 𝑧 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) ) = ( 𝑔 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑔 ) ) )
24	23	raleqdv	⊢ ( 𝑧 = 𝑔 → ( ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ↔ ∀ 𝑢 ∈ ( 𝑔 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑔 ) ) ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) )
25	21 24	anbi12d	⊢ ( 𝑧 = 𝑔 → ( ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ↔ ( ( 𝑦 < 𝑔 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑔 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑔 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑔 ) ) ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ) )
26	25	cbvrexvw	⊢ ( ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ↔ ∃ 𝑔 ∈ ℝ+ ( ( 𝑦 < 𝑔 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑔 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑔 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑔 ) ) ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) )
27		breq1	⊢ ( 𝑦 = 𝑓 → ( 𝑦 < 𝑔 ↔ 𝑓 < 𝑔 ) )
28		oveq2	⊢ ( 𝑦 = 𝑓 → ( 𝑘 · 𝑦 ) = ( 𝑘 · 𝑓 ) )
29	28	breq2d	⊢ ( 𝑦 = 𝑓 → ( ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑔 ) < ( 𝑘 · 𝑦 ) ↔ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑔 ) < ( 𝑘 · 𝑓 ) ) )
30	27 29	anbi12d	⊢ ( 𝑦 = 𝑓 → ( ( 𝑦 < 𝑔 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑔 ) < ( 𝑘 · 𝑦 ) ) ↔ ( 𝑓 < 𝑔 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑔 ) < ( 𝑘 · 𝑓 ) ) ) )
31	30	anbi1d	⊢ ( 𝑦 = 𝑓 → ( ( ( 𝑦 < 𝑔 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑔 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑔 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑔 ) ) ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ↔ ( ( 𝑓 < 𝑔 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑔 ) < ( 𝑘 · 𝑓 ) ) ∧ ∀ 𝑢 ∈ ( 𝑔 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑔 ) ) ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ) )
32	31	rexbidv	⊢ ( 𝑦 = 𝑓 → ( ∃ 𝑔 ∈ ℝ+ ( ( 𝑦 < 𝑔 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑔 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑔 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑔 ) ) ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ↔ ∃ 𝑔 ∈ ℝ+ ( ( 𝑓 < 𝑔 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑔 ) < ( 𝑘 · 𝑓 ) ) ∧ ∀ 𝑢 ∈ ( 𝑔 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑔 ) ) ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ) )
33	26 32	bitrid	⊢ ( 𝑦 = 𝑓 → ( ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ↔ ∃ 𝑔 ∈ ℝ+ ( ( 𝑓 < 𝑔 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑔 ) < ( 𝑘 · 𝑓 ) ) ∧ ∀ 𝑢 ∈ ( 𝑔 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑔 ) ) ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ) )
34	33	cbvralvw	⊢ ( ∀ 𝑦 ∈ ( 𝑟 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ↔ ∀ 𝑓 ∈ ( 𝑟 (,) +∞ ) ∃ 𝑔 ∈ ℝ+ ( ( 𝑓 < 𝑔 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑔 ) < ( 𝑘 · 𝑓 ) ) ∧ ∀ 𝑢 ∈ ( 𝑔 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑔 ) ) ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) )
35		oveq1	⊢ ( 𝑟 = 𝑥 → ( 𝑟 (,) +∞ ) = ( 𝑥 (,) +∞ ) )
36	35	raleqdv	⊢ ( 𝑟 = 𝑥 → ( ∀ 𝑓 ∈ ( 𝑟 (,) +∞ ) ∃ 𝑔 ∈ ℝ+ ( ( 𝑓 < 𝑔 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑔 ) < ( 𝑘 · 𝑓 ) ) ∧ ∀ 𝑢 ∈ ( 𝑔 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑔 ) ) ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ↔ ∀ 𝑓 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑔 ∈ ℝ+ ( ( 𝑓 < 𝑔 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑔 ) < ( 𝑘 · 𝑓 ) ) ∧ ∀ 𝑢 ∈ ( 𝑔 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑔 ) ) ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ) )
37	34 36	bitrid	⊢ ( 𝑟 = 𝑥 → ( ∀ 𝑦 ∈ ( 𝑟 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ↔ ∀ 𝑓 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑔 ∈ ℝ+ ( ( 𝑓 < 𝑔 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑔 ) < ( 𝑘 · 𝑓 ) ) ∧ ∀ 𝑢 ∈ ( 𝑔 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑔 ) ) ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ) )
38	37	ralbidv	⊢ ( 𝑟 = 𝑥 → ( ∀ 𝑘 ∈ ( ( exp ‘ ( 𝑐 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑟 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ↔ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝑐 / 𝑒 ) ) [,) +∞ ) ∀ 𝑓 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑔 ∈ ℝ+ ( ( 𝑓 < 𝑔 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑔 ) < ( 𝑘 · 𝑓 ) ) ∧ ∀ 𝑢 ∈ ( 𝑔 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑔 ) ) ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ) )
39	38	cbvrexvw	⊢ ( ∃ 𝑟 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝑐 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑟 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ↔ ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝑐 / 𝑒 ) ) [,) +∞ ) ∀ 𝑓 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑔 ∈ ℝ+ ( ( 𝑓 < 𝑔 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑔 ) < ( 𝑘 · 𝑓 ) ) ∧ ∀ 𝑢 ∈ ( 𝑔 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑔 ) ) ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) )
40	39	ralbii	⊢ ( ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑟 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝑐 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑟 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ↔ ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝑐 / 𝑒 ) ) [,) +∞ ) ∀ 𝑓 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑔 ∈ ℝ+ ( ( 𝑓 < 𝑔 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑔 ) < ( 𝑘 · 𝑓 ) ) ∧ ∀ 𝑢 ∈ ( 𝑔 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑔 ) ) ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) )
41	17 40	sylib	⊢ ( ( ( 𝑏 ∈ ℝ+ ∧ ∀ 𝑟 ∈ ℝ+ ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑟 ) / 𝑟 ) ) ≤ 𝑏 ) ∧ ( ( 𝑐 ∈ ℝ+ ∧ 𝑙 ∈ ( 0 (,) 1 ) ) ∧ ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑟 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝑐 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑟 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ) ) → ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝑐 / 𝑒 ) ) [,) +∞ ) ∀ 𝑓 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑔 ∈ ℝ+ ( ( 𝑓 < 𝑔 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑔 ) < ( 𝑘 · 𝑓 ) ) ∧ ∀ 𝑢 ∈ ( 𝑔 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑔 ) ) ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) )
42	1 4 12 13 14 15 16 41	pntleml	⊢ ( ( ( 𝑏 ∈ ℝ+ ∧ ∀ 𝑟 ∈ ℝ+ ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑟 ) / 𝑟 ) ) ≤ 𝑏 ) ∧ ( ( 𝑐 ∈ ℝ+ ∧ 𝑙 ∈ ( 0 (,) 1 ) ) ∧ ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑟 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝑐 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑟 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ) ) → ( 𝑥 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) ⇝𝑟 1 )
43	42	expr	⊢ ( ( ( 𝑏 ∈ ℝ+ ∧ ∀ 𝑟 ∈ ℝ+ ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑟 ) / 𝑟 ) ) ≤ 𝑏 ) ∧ ( 𝑐 ∈ ℝ+ ∧ 𝑙 ∈ ( 0 (,) 1 ) ) ) → ( ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑟 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝑐 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑟 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) → ( 𝑥 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) ⇝𝑟 1 ) )
44	43	rexlimdvva	⊢ ( ( 𝑏 ∈ ℝ+ ∧ ∀ 𝑟 ∈ ℝ+ ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑟 ) / 𝑟 ) ) ≤ 𝑏 ) → ( ∃ 𝑐 ∈ ℝ+ ∃ 𝑙 ∈ ( 0 (,) 1 ) ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑟 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝑐 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑟 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) → ( 𝑥 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) ⇝𝑟 1 ) )
45	3 44	mpi	⊢ ( ( 𝑏 ∈ ℝ+ ∧ ∀ 𝑟 ∈ ℝ+ ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑟 ) / 𝑟 ) ) ≤ 𝑏 ) → ( 𝑥 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) ⇝𝑟 1 )
46	45	rexlimiva	⊢ ( ∃ 𝑏 ∈ ℝ+ ∀ 𝑟 ∈ ℝ+ ( abs ‘ ( ( ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) ‘ 𝑟 ) / 𝑟 ) ) ≤ 𝑏 → ( 𝑥 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) ⇝𝑟 1 )
47	2 46	ax-mp	⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) ⇝𝑟 1