Metamath Proof Explorer

Theorem fsequb

Description: The values of a finite real sequence have an upper bound. (Contributed by NM, 19-Sep-2005) (Proof shortened by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion fsequb ⊢ ∀ k ∈ M … N F ⁡ k ∈ ℝ → ∃ x ∈ ℝ ∀ k ∈ M … N F ⁡ k < x

Proof

Step Hyp Ref Expression
1 fzfi ⊢ M … N ∈ Fin
2 fimaxre3 ⊢ M … N ∈ Fin ∧ ∀ k ∈ M … N F ⁡ k ∈ ℝ → ∃ y ∈ ℝ ∀ k ∈ M … N F ⁡ k ≤ y
3 1 2 mpan ⊢ ∀ k ∈ M … N F ⁡ k ∈ ℝ → ∃ y ∈ ℝ ∀ k ∈ M … N F ⁡ k ≤ y
4 r19.26 ⊢ ∀ k ∈ M … N F ⁡ k ∈ ℝ ∧ F ⁡ k ≤ y ↔ ∀ k ∈ M … N F ⁡ k ∈ ℝ ∧ ∀ k ∈ M … N F ⁡ k ≤ y
5 peano2re ⊢ y ∈ ℝ → y + 1 ∈ ℝ
6 ltp1 ⊢ y ∈ ℝ → y < y + 1
7 6 adantr ⊢ y ∈ ℝ ∧ F ⁡ k ∈ ℝ → y < y + 1
8 simpr ⊢ y ∈ ℝ ∧ F ⁡ k ∈ ℝ → F ⁡ k ∈ ℝ
9 simpl ⊢ y ∈ ℝ ∧ F ⁡ k ∈ ℝ → y ∈ ℝ
10 5 adantr ⊢ y ∈ ℝ ∧ F ⁡ k ∈ ℝ → y + 1 ∈ ℝ
11 lelttr ⊢ F ⁡ k ∈ ℝ ∧ y ∈ ℝ ∧ y + 1 ∈ ℝ → F ⁡ k ≤ y ∧ y < y + 1 → F ⁡ k < y + 1
12 8 9 10 11 syl3anc ⊢ y ∈ ℝ ∧ F ⁡ k ∈ ℝ → F ⁡ k ≤ y ∧ y < y + 1 → F ⁡ k < y + 1
13 7 12 mpan2d ⊢ y ∈ ℝ ∧ F ⁡ k ∈ ℝ → F ⁡ k ≤ y → F ⁡ k < y + 1
14 13 expimpd ⊢ y ∈ ℝ → F ⁡ k ∈ ℝ ∧ F ⁡ k ≤ y → F ⁡ k < y + 1
15 14 ralimdv ⊢ y ∈ ℝ → ∀ k ∈ M … N F ⁡ k ∈ ℝ ∧ F ⁡ k ≤ y → ∀ k ∈ M … N F ⁡ k < y + 1
16 brralrspcev ⊢ y + 1 ∈ ℝ ∧ ∀ k ∈ M … N F ⁡ k < y + 1 → ∃ x ∈ ℝ ∀ k ∈ M … N F ⁡ k < x
17 5 15 16 syl6an ⊢ y ∈ ℝ → ∀ k ∈ M … N F ⁡ k ∈ ℝ ∧ F ⁡ k ≤ y → ∃ x ∈ ℝ ∀ k ∈ M … N F ⁡ k < x
18 4 17 biimtrrid ⊢ y ∈ ℝ → ∀ k ∈ M … N F ⁡ k ∈ ℝ ∧ ∀ k ∈ M … N F ⁡ k ≤ y → ∃ x ∈ ℝ ∀ k ∈ M … N F ⁡ k < x
19 18 expd ⊢ y ∈ ℝ → ∀ k ∈ M … N F ⁡ k ∈ ℝ → ∀ k ∈ M … N F ⁡ k ≤ y → ∃ x ∈ ℝ ∀ k ∈ M … N F ⁡ k < x
20 19 impcom ⊢ ∀ k ∈ M … N F ⁡ k ∈ ℝ ∧ y ∈ ℝ → ∀ k ∈ M … N F ⁡ k ≤ y → ∃ x ∈ ℝ ∀ k ∈ M … N F ⁡ k < x
21 20 rexlimdva ⊢ ∀ k ∈ M … N F ⁡ k ∈ ℝ → ∃ y ∈ ℝ ∀ k ∈ M … N F ⁡ k ≤ y → ∃ x ∈ ℝ ∀ k ∈ M … N F ⁡ k < x
22 3 21 mpd ⊢ ∀ k ∈ M … N F ⁡ k ∈ ℝ → ∃ x ∈ ℝ ∀ k ∈ M … N F ⁡ k < x