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

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 ( ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) < 𝑥 )

Proof

Step Hyp Ref Expression
1 fzfi ⊢ ( 𝑀 ... 𝑁 ) ∈ Fin
2 fimaxre3 ⊢ ( ( ( 𝑀 ... 𝑁 ) ∈ Fin ∧ ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) → ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑦 )
3 1 2 mpan ⊢ ( ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ → ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑦 )
4 r19.26 ⊢ ( ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑘 ) ≤ 𝑦 ) ↔ ( ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑦 ) )
5 peano2re ⊢ ( 𝑦 ∈ ℝ → ( 𝑦 + 1 ) ∈ ℝ )
6 ltp1 ⊢ ( 𝑦 ∈ ℝ → 𝑦 < ( 𝑦 + 1 ) )
7 6 adantr ⊢ ( ( 𝑦 ∈ ℝ ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) → 𝑦 < ( 𝑦 + 1 ) )
8 simpr ⊢ ( ( 𝑦 ∈ ℝ ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
9 simpl ⊢ ( ( 𝑦 ∈ ℝ ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) → 𝑦 ∈ ℝ )
10 5 adantr ⊢ ( ( 𝑦 ∈ ℝ ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) → ( 𝑦 + 1 ) ∈ ℝ )
11 lelttr ⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ ( 𝑦 + 1 ) ∈ ℝ ) → ( ( ( 𝐹 ‘ 𝑘 ) ≤ 𝑦 ∧ 𝑦 < ( 𝑦 + 1 ) ) → ( 𝐹 ‘ 𝑘 ) < ( 𝑦 + 1 ) ) )
12 8 9 10 11 syl3anc ⊢ ( ( 𝑦 ∈ ℝ ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) → ( ( ( 𝐹 ‘ 𝑘 ) ≤ 𝑦 ∧ 𝑦 < ( 𝑦 + 1 ) ) → ( 𝐹 ‘ 𝑘 ) < ( 𝑦 + 1 ) ) )
13 7 12 mpan2d ⊢ ( ( 𝑦 ∈ ℝ ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) → ( ( 𝐹 ‘ 𝑘 ) ≤ 𝑦 → ( 𝐹 ‘ 𝑘 ) < ( 𝑦 + 1 ) ) )
14 13 expimpd ⊢ ( 𝑦 ∈ ℝ → ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑘 ) ≤ 𝑦 ) → ( 𝐹 ‘ 𝑘 ) < ( 𝑦 + 1 ) ) )
15 14 ralimdv ⊢ ( 𝑦 ∈ ℝ → ( ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑘 ) ≤ 𝑦 ) → ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) < ( 𝑦 + 1 ) ) )
16 brralrspcev ⊢ ( ( ( 𝑦 + 1 ) ∈ ℝ ∧ ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) < ( 𝑦 + 1 ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) < 𝑥 )
17 5 15 16 syl6an ⊢ ( 𝑦 ∈ ℝ → ( ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑘 ) ≤ 𝑦 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) < 𝑥 ) )
18 4 17 biimtrrid ⊢ ( 𝑦 ∈ ℝ → ( ( ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑦 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) < 𝑥 ) )
19 18 expd ⊢ ( 𝑦 ∈ ℝ → ( ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ → ( ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑦 → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) < 𝑥 ) ) )
20 19 impcom ⊢ ( ( ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑦 → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) < 𝑥 ) )
21 20 rexlimdva ⊢ ( ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ → ( ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑦 → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) < 𝑥 ) )
22 3 21 mpd ⊢ ( ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) < 𝑥 )