Metamath Proof Explorer

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