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	⊢ ( 𝜑 → ∃ 𝑚 ∈ ℝ+ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑚 )