Metamath Proof Explorer

Theorem pntibndlem2a

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

Ref Expression
Hypotheses pntibnd.r ⊢ R = a ∈ ℝ + ⟼ ψ ⁡ a − a
pntibndlem1.1 ⊢ φ → A ∈ ℝ +
pntibndlem1.l ⊢ L = 1 4 A + 3
pntibndlem3.2 ⊢ φ → ∀ x ∈ ℝ + R ⁡ x x ≤ A
pntibndlem3.3 ⊢ φ → B ∈ ℝ +
pntibndlem3.k ⊢ K = e B E 2
pntibndlem3.c ⊢ C = 2 ⁢ B + log ⁡ 2
pntibndlem3.4 ⊢ φ → E ∈ 0 1
pntibndlem3.6 ⊢ φ → Z ∈ ℝ +
pntibndlem2.10 ⊢ φ → N ∈ ℕ
Assertion pntibndlem2a ⊢ φ ∧ u ∈ N 1 + L ⁢ E ⋅ N → u ∈ ℝ ∧ N ≤ u ∧ u ≤ 1 + L ⁢ E ⋅ N

Proof

Step Hyp Ref Expression
1 pntibnd.r ⊢ R = a ∈ ℝ + ⟼ ψ ⁡ a − a
2 pntibndlem1.1 ⊢ φ → A ∈ ℝ +
3 pntibndlem1.l ⊢ L = 1 4 A + 3
4 pntibndlem3.2 ⊢ φ → ∀ x ∈ ℝ + R ⁡ x x ≤ A
5 pntibndlem3.3 ⊢ φ → B ∈ ℝ +
6 pntibndlem3.k ⊢ K = e B E 2
7 pntibndlem3.c ⊢ C = 2 ⁢ B + log ⁡ 2
8 pntibndlem3.4 ⊢ φ → E ∈ 0 1
9 pntibndlem3.6 ⊢ φ → Z ∈ ℝ +
10 pntibndlem2.10 ⊢ φ → N ∈ ℕ
11 10 nnred ⊢ φ → N ∈ ℝ
12 1red ⊢ φ → 1 ∈ ℝ
13 ioossre ⊢ 0 1 ⊆ ℝ
14 1 2 3 pntibndlem1 ⊢ φ → L ∈ 0 1
15 13 14 sselid ⊢ φ → L ∈ ℝ
16 13 8 sselid ⊢ φ → E ∈ ℝ
17 15 16 remulcld ⊢ φ → L ⁢ E ∈ ℝ
18 12 17 readdcld ⊢ φ → 1 + L ⁢ E ∈ ℝ
19 18 11 remulcld ⊢ φ → 1 + L ⁢ E ⋅ N ∈ ℝ
20 elicc2 ⊢ N ∈ ℝ ∧ 1 + L ⁢ E ⋅ N ∈ ℝ → u ∈ N 1 + L ⁢ E ⋅ N ↔ u ∈ ℝ ∧ N ≤ u ∧ u ≤ 1 + L ⁢ E ⋅ N
21 11 19 20 syl2anc ⊢ φ → u ∈ N 1 + L ⁢ E ⋅ N ↔ u ∈ ℝ ∧ N ≤ u ∧ u ≤ 1 + L ⁢ E ⋅ N
22 21 biimpa ⊢ φ ∧ u ∈ N 1 + L ⁢ E ⋅ N → u ∈ ℝ ∧ N ≤ u ∧ u ≤ 1 + L ⁢ E ⋅ N