Metamath Proof Explorer

Theorem fsequb2

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

Ref Expression
Assertion fsequb2 ⊢ F : M … N ⟶ ℝ → ∃ x ∈ ℝ ∀ y ∈ ran ⁡ F y ≤ x

Proof

Step Hyp Ref Expression
1 fzfi ⊢ M … N ∈ Fin
2 ffvelrn ⊢ F : M … N ⟶ ℝ ∧ k ∈ M … N → F ⁡ k ∈ ℝ
3 2 ralrimiva ⊢ F : M … N ⟶ ℝ → ∀ k ∈ M … N F ⁡ k ∈ ℝ
4 fimaxre3 ⊢ M … N ∈ Fin ∧ ∀ k ∈ M … N F ⁡ k ∈ ℝ → ∃ x ∈ ℝ ∀ k ∈ M … N F ⁡ k ≤ x
5 1 3 4 sylancr ⊢ F : M … N ⟶ ℝ → ∃ x ∈ ℝ ∀ k ∈ M … N F ⁡ k ≤ x
6 ffn ⊢ F : M … N ⟶ ℝ → F Fn M … N
7 breq1 ⊢ y = F ⁡ k → y ≤ x ↔ F ⁡ k ≤ x
8 7 ralrn ⊢ F Fn M … N → ∀ y ∈ ran ⁡ F y ≤ x ↔ ∀ k ∈ M … N F ⁡ k ≤ x
9 6 8 syl ⊢ F : M … N ⟶ ℝ → ∀ y ∈ ran ⁡ F y ≤ x ↔ ∀ k ∈ M … N F ⁡ k ≤ x
10 9 rexbidv ⊢ F : M … N ⟶ ℝ → ∃ x ∈ ℝ ∀ y ∈ ran ⁡ F y ≤ x ↔ ∃ x ∈ ℝ ∀ k ∈ M … N F ⁡ k ≤ x
11 5 10 mpbird ⊢ F : M … N ⟶ ℝ → ∃ x ∈ ℝ ∀ y ∈ ran ⁡ F y ≤ x