Metamath Proof Explorer

Theorem lo1bddrp

Description: Refine o1bdd2 to give a strictly positive upper bound. (Contributed by Mario Carneiro, 25-May-2016)

Ref Expression
Hypotheses lo1bdd2.1 ⊢ φ → A ⊆ ℝ
lo1bdd2.2 ⊢ φ → C ∈ ℝ
lo1bdd2.3 ⊢ φ ∧ x ∈ A → B ∈ ℝ
lo1bdd2.4 ⊢ φ → x ∈ A ⟼ B ∈ ≤𝑂⁡1
lo1bdd2.5 ⊢ φ ∧ y ∈ ℝ ∧ C ≤ y → M ∈ ℝ
lo1bdd2.6 ⊢ φ ∧ x ∈ A ∧ y ∈ ℝ ∧ C ≤ y ∧ x < y → B ≤ M
Assertion lo1bddrp ⊢ φ → ∃ m ∈ ℝ + ∀ x ∈ A B ≤ m

Proof

Step Hyp Ref Expression
1 lo1bdd2.1 ⊢ φ → A ⊆ ℝ
2 lo1bdd2.2 ⊢ φ → C ∈ ℝ
3 lo1bdd2.3 ⊢ φ ∧ x ∈ A → B ∈ ℝ
4 lo1bdd2.4 ⊢ φ → x ∈ A ⟼ B ∈ ≤𝑂⁡1
5 lo1bdd2.5 ⊢ φ ∧ y ∈ ℝ ∧ C ≤ y → M ∈ ℝ
6 lo1bdd2.6 ⊢ φ ∧ x ∈ A ∧ y ∈ ℝ ∧ C ≤ y ∧ x < y → B ≤ M
7 1 2 3 4 5 6 lo1bdd2 ⊢ φ → ∃ n ∈ ℝ ∀ x ∈ A B ≤ n
8 simpr ⊢ φ ∧ n ∈ ℝ → n ∈ ℝ
9 8 recnd ⊢ φ ∧ n ∈ ℝ → n ∈ ℂ
10 9 abscld ⊢ φ ∧ n ∈ ℝ → n ∈ ℝ
11 9 absge0d ⊢ φ ∧ n ∈ ℝ → 0 ≤ n
12 10 11 ge0p1rpd ⊢ φ ∧ n ∈ ℝ → n + 1 ∈ ℝ +
13 simplr ⊢ φ ∧ n ∈ ℝ ∧ x ∈ A → n ∈ ℝ
14 10 adantr ⊢ φ ∧ n ∈ ℝ ∧ x ∈ A → n ∈ ℝ
15 peano2re ⊢ n ∈ ℝ → n + 1 ∈ ℝ
16 14 15 syl ⊢ φ ∧ n ∈ ℝ ∧ x ∈ A → n + 1 ∈ ℝ
17 13 leabsd ⊢ φ ∧ n ∈ ℝ ∧ x ∈ A → n ≤ n
18 14 lep1d ⊢ φ ∧ n ∈ ℝ ∧ x ∈ A → n ≤ n + 1
19 13 14 16 17 18 letrd ⊢ φ ∧ n ∈ ℝ ∧ x ∈ A → n ≤ n + 1
20 3 adantlr ⊢ φ ∧ n ∈ ℝ ∧ x ∈ A → B ∈ ℝ
21 letr ⊢ B ∈ ℝ ∧ n ∈ ℝ ∧ n + 1 ∈ ℝ → B ≤ n ∧ n ≤ n + 1 → B ≤ n + 1
22 20 13 16 21 syl3anc ⊢ φ ∧ n ∈ ℝ ∧ x ∈ A → B ≤ n ∧ n ≤ n + 1 → B ≤ n + 1
23 19 22 mpan2d ⊢ φ ∧ n ∈ ℝ ∧ x ∈ A → B ≤ n → B ≤ n + 1
24 23 ralimdva ⊢ φ ∧ n ∈ ℝ → ∀ x ∈ A B ≤ n → ∀ x ∈ A B ≤ n + 1
25 brralrspcev ⊢ n + 1 ∈ ℝ + ∧ ∀ x ∈ A B ≤ n + 1 → ∃ m ∈ ℝ + ∀ x ∈ A B ≤ m
26 12 24 25 syl6an ⊢ φ ∧ n ∈ ℝ → ∀ x ∈ A B ≤ n → ∃ m ∈ ℝ + ∀ x ∈ A B ≤ m
27 26 rexlimdva ⊢ φ → ∃ n ∈ ℝ ∀ x ∈ A B ≤ n → ∃ m ∈ ℝ + ∀ x ∈ A B ≤ m
28 7 27 mpd ⊢ φ → ∃ m ∈ ℝ + ∀ x ∈ A B ≤ m