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∈AB≤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∈AB≤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∈AB≤n→∀x∈AB≤n+1
25 brralrspcev ⊢n+1∈ℝ+∧∀x∈AB≤n+1→∃m∈ℝ+∀x∈AB≤m
26 12 24 25 syl6an ⊢φ∧n∈ℝ→∀x∈AB≤n→∃m∈ℝ+∀x∈AB≤m
27 26 rexlimdva ⊢φ→∃n∈ℝ∀x∈AB≤n→∃m∈ℝ+∀x∈AB≤m
28 7 27 mpd ⊢φ→∃m∈ℝ+∀x∈AB≤m