This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
lo1bdd2.2 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
lo1bdd2.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
lo1bdd2.4 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) )
lo1bdd2.5 ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦 ) ) → 𝑀 ∈ ℝ )
lo1bdd2.6 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ( ( 𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 𝐵 ≤ 𝑀 )
Assertion lo1bddrp ( 𝜑 → ∃ 𝑚 ∈ ℝ+ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑚 )

Proof

Step Hyp Ref Expression
1 lo1bdd2.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2 lo1bdd2.2 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
3 lo1bdd2.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
4 lo1bdd2.4 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) )
5 lo1bdd2.5 ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦 ) ) → 𝑀 ∈ ℝ )
6 lo1bdd2.6 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ( ( 𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 𝐵 ≤ 𝑀 )
7 1 2 3 4 5 6 lo1bdd2 ⊢ ( 𝜑 → ∃ 𝑛 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑛 )
8 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) → 𝑛 ∈ ℝ )
9 8 recnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) → 𝑛 ∈ ℂ )
10 9 abscld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) → ( abs ‘ 𝑛 ) ∈ ℝ )
11 9 absge0d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) → 0 ≤ ( abs ‘ 𝑛 ) )
12 10 11 ge0p1rpd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) → ( ( abs ‘ 𝑛 ) + 1 ) ∈ ℝ+ )
13 simplr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝑛 ∈ ℝ )
14 10 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ 𝑛 ) ∈ ℝ )
15 peano2re ⊢ ( ( abs ‘ 𝑛 ) ∈ ℝ → ( ( abs ‘ 𝑛 ) + 1 ) ∈ ℝ )
16 14 15 syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( abs ‘ 𝑛 ) + 1 ) ∈ ℝ )
17 13 leabsd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝑛 ≤ ( abs ‘ 𝑛 ) )
18 14 lep1d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ 𝑛 ) ≤ ( ( abs ‘ 𝑛 ) + 1 ) )
19 13 14 16 17 18 letrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝑛 ≤ ( ( abs ‘ 𝑛 ) + 1 ) )
20 3 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
21 letr ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ ( ( abs ‘ 𝑛 ) + 1 ) ∈ ℝ ) → ( ( 𝐵 ≤ 𝑛 ∧ 𝑛 ≤ ( ( abs ‘ 𝑛 ) + 1 ) ) → 𝐵 ≤ ( ( abs ‘ 𝑛 ) + 1 ) ) )
22 20 13 16 21 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐵 ≤ 𝑛 ∧ 𝑛 ≤ ( ( abs ‘ 𝑛 ) + 1 ) ) → 𝐵 ≤ ( ( abs ‘ 𝑛 ) + 1 ) ) )
23 19 22 mpan2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 ≤ 𝑛 → 𝐵 ≤ ( ( abs ‘ 𝑛 ) + 1 ) ) )
24 23 ralimdva ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) → ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑛 → ∀ 𝑥 ∈ 𝐴 𝐵 ≤ ( ( abs ‘ 𝑛 ) + 1 ) ) )
25 brralrspcev ⊢ ( ( ( ( abs ‘ 𝑛 ) + 1 ) ∈ ℝ+ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ ( ( abs ‘ 𝑛 ) + 1 ) ) → ∃ 𝑚 ∈ ℝ+ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑚 )
26 12 24 25 syl6an ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) → ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑛 → ∃ 𝑚 ∈ ℝ+ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑚 ) )
27 26 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑛 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑛 → ∃ 𝑚 ∈ ℝ+ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑚 ) )
28 7 27 mpd ⊢ ( 𝜑 → ∃ 𝑚 ∈ ℝ+ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑚 )