Theorem bndndx

Description: A bounded real sequence A ( k ) is less than or equal to at least one of its indices. (Contributed by NM, 18-Jan-2008)

	Ref	Expression
Assertion	bndndx	⊢ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℕ ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ) → ∃ 𝑘 ∈ ℕ 𝐴 ≤ 𝑘 )

Proof

Step	Hyp	Ref	Expression
1		arch	⊢ ( 𝑥 ∈ ℝ → ∃ 𝑘 ∈ ℕ 𝑥 < 𝑘 )
2		nnre	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ )
3		lelttr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( ( 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝑘 ) → 𝐴 < 𝑘 ) )
4		ltle	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( 𝐴 < 𝑘 → 𝐴 ≤ 𝑘 ) )
5	4	3adant2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( 𝐴 < 𝑘 → 𝐴 ≤ 𝑘 ) )
6	3 5	syld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( ( 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝑘 ) → 𝐴 ≤ 𝑘 ) )
7	6	exp5o	⊢ ( 𝐴 ∈ ℝ → ( 𝑥 ∈ ℝ → ( 𝑘 ∈ ℝ → ( 𝐴 ≤ 𝑥 → ( 𝑥 < 𝑘 → 𝐴 ≤ 𝑘 ) ) ) ) )
8	7	com3l	⊢ ( 𝑥 ∈ ℝ → ( 𝑘 ∈ ℝ → ( 𝐴 ∈ ℝ → ( 𝐴 ≤ 𝑥 → ( 𝑥 < 𝑘 → 𝐴 ≤ 𝑘 ) ) ) ) )
9	8	imp4b	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ) → ( 𝑥 < 𝑘 → 𝐴 ≤ 𝑘 ) ) )
10	9	com23	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( 𝑥 < 𝑘 → ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ) → 𝐴 ≤ 𝑘 ) ) )
11	2 10	sylan2	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( 𝑥 < 𝑘 → ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ) → 𝐴 ≤ 𝑘 ) ) )
12	11	reximdva	⊢ ( 𝑥 ∈ ℝ → ( ∃ 𝑘 ∈ ℕ 𝑥 < 𝑘 → ∃ 𝑘 ∈ ℕ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ) → 𝐴 ≤ 𝑘 ) ) )
13	1 12	mpd	⊢ ( 𝑥 ∈ ℝ → ∃ 𝑘 ∈ ℕ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ) → 𝐴 ≤ 𝑘 ) )
14		r19.35	⊢ ( ∃ 𝑘 ∈ ℕ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ) → 𝐴 ≤ 𝑘 ) ↔ ( ∀ 𝑘 ∈ ℕ ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ) → ∃ 𝑘 ∈ ℕ 𝐴 ≤ 𝑘 ) )
15	13 14	sylib	⊢ ( 𝑥 ∈ ℝ → ( ∀ 𝑘 ∈ ℕ ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ) → ∃ 𝑘 ∈ ℕ 𝐴 ≤ 𝑘 ) )
16	15	rexlimiv	⊢ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℕ ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ) → ∃ 𝑘 ∈ ℕ 𝐴 ≤ 𝑘 )