pntibndlem2a

	Ref	Expression
Hypotheses	pntibnd.r	⊢ 𝑅 = ( 𝑎 ∈ ℝ⁺ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
	pntibndlem1.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ⁺ )
	pntibndlem1.l	⊢ 𝐿 = ( ( 1 / 4 ) / ( 𝐴 + 3 ) )
	pntibndlem3.2	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ⁺ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝐴 )
	pntibndlem3.3	⊢ ( 𝜑 → 𝐵 ∈ ℝ⁺ )
	pntibndlem3.k	⊢ 𝐾 = ( exp ‘ ( 𝐵 / ( 𝐸 / 2 ) ) )
	pntibndlem3.c	⊢ 𝐶 = ( ( 2 · 𝐵 ) + ( log ‘ 2 ) )
	pntibndlem3.4	⊢ ( 𝜑 → 𝐸 ∈ ( 0 (,) 1 ) )
	pntibndlem3.6	⊢ ( 𝜑 → 𝑍 ∈ ℝ⁺ )
	pntibndlem2.10	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
Assertion	pntibndlem2a	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝑢 ∈ ℝ ∧ 𝑁 ≤ 𝑢 ∧ 𝑢 ≤ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pntibnd.r	⊢ 𝑅 = ( 𝑎 ∈ ℝ⁺ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
2		pntibndlem1.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ⁺ )
3		pntibndlem1.l	⊢ 𝐿 = ( ( 1 / 4 ) / ( 𝐴 + 3 ) )
4		pntibndlem3.2	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ⁺ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝐴 )
5		pntibndlem3.3	⊢ ( 𝜑 → 𝐵 ∈ ℝ⁺ )
6		pntibndlem3.k	⊢ 𝐾 = ( exp ‘ ( 𝐵 / ( 𝐸 / 2 ) ) )
7		pntibndlem3.c	⊢ 𝐶 = ( ( 2 · 𝐵 ) + ( log ‘ 2 ) )
8		pntibndlem3.4	⊢ ( 𝜑 → 𝐸 ∈ ( 0 (,) 1 ) )
9		pntibndlem3.6	⊢ ( 𝜑 → 𝑍 ∈ ℝ⁺ )
10		pntibndlem2.10	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
11	10	nnred	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
12		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
13		ioossre	⊢ ( 0 (,) 1 ) ⊆ ℝ
14	1 2 3	pntibndlem1	⊢ ( 𝜑 → 𝐿 ∈ ( 0 (,) 1 ) )
15	13 14	sselid	⊢ ( 𝜑 → 𝐿 ∈ ℝ )
16	13 8	sselid	⊢ ( 𝜑 → 𝐸 ∈ ℝ )
17	15 16	remulcld	⊢ ( 𝜑 → ( 𝐿 · 𝐸 ) ∈ ℝ )
18	12 17	readdcld	⊢ ( 𝜑 → ( 1 + ( 𝐿 · 𝐸 ) ) ∈ ℝ )
19	18 11	remulcld	⊢ ( 𝜑 → ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ∈ ℝ )
20		elicc2	⊢ ( ( 𝑁 ∈ ℝ ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ∈ ℝ ) → ( 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ↔ ( 𝑢 ∈ ℝ ∧ 𝑁 ≤ 𝑢 ∧ 𝑢 ≤ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) )
21	11 19 20	syl2anc	⊢ ( 𝜑 → ( 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ↔ ( 𝑢 ∈ ℝ ∧ 𝑁 ≤ 𝑢 ∧ 𝑢 ≤ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) )
22	21	biimpa	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝑢 ∈ ℝ ∧ 𝑁 ≤ 𝑢 ∧ 𝑢 ≤ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) )

Metamath Proof Explorer

Theorem pntibndlem2a

Proof