Metamath Proof Explorer

Theorem pntibndlem2a

Description: Lemma for pntibndlem2 . (Contributed by Mario Carneiro, 7-Jun-2016)

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 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) )