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