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

Metamath Proof Explorer

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 ⊢ ∃ x ∈ ℝ ∀ k ∈ ℕ A ∈ ℝ ∧ A ≤ x → ∃ k ∈ ℕ A ≤ k

Proof

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