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

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 ( 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 )

Proof

Step Hyp Ref Expression
1 fzfi ⊢ ( 𝑀 ... 𝑁 ) ∈ Fin
2 ffvelcdm ⊢ ( ( 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
3 2 ralrimiva ⊢ ( 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ → ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
4 fimaxre3 ⊢ ( ( ( 𝑀 ... 𝑁 ) ∈ Fin ∧ ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 )
5 1 3 4 sylancr ⊢ ( 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 )
6 ffn ⊢ ( 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ → 𝐹 Fn ( 𝑀 ... 𝑁 ) )
7 breq1 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑘 ) → ( 𝑦 ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) )
8 7 ralrn ⊢ ( 𝐹 Fn ( 𝑀 ... 𝑁 ) → ( ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ↔ ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) )
9 6 8 syl ⊢ ( 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ → ( ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ↔ ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) )
10 9 rexbidv ⊢ ( 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ → ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) )
11 5 10 mpbird ⊢ ( 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 )