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…NF⁡k∈ℝ→∃x∈ℝ∀k∈M…NF⁡k<x

Proof

Step Hyp Ref Expression
1 fzfi ⊢M…N∈Fin
2 fimaxre3 ⊢M…N∈Fin∧∀k∈M…NF⁡k∈ℝ→∃y∈ℝ∀k∈M…NF⁡k≤y
3 1 2 mpan ⊢∀k∈M…NF⁡k∈ℝ→∃y∈ℝ∀k∈M…NF⁡k≤y
4 r19.26 ⊢∀k∈M…NF⁡k∈ℝ∧F⁡k≤y↔∀k∈M…NF⁡k∈ℝ∧∀k∈M…NF⁡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…NF⁡k∈ℝ∧F⁡k≤y→∀k∈M…NF⁡k<y+1
16 brralrspcev ⊢y+1∈ℝ∧∀k∈M…NF⁡k<y+1→∃x∈ℝ∀k∈M…NF⁡k<x
17 5 15 16 syl6an ⊢y∈ℝ→∀k∈M…NF⁡k∈ℝ∧F⁡k≤y→∃x∈ℝ∀k∈M…NF⁡k<x
18 4 17 biimtrrid ⊢y∈ℝ→∀k∈M…NF⁡k∈ℝ∧∀k∈M…NF⁡k≤y→∃x∈ℝ∀k∈M…NF⁡k<x
19 18 expd ⊢y∈ℝ→∀k∈M…NF⁡k∈ℝ→∀k∈M…NF⁡k≤y→∃x∈ℝ∀k∈M…NF⁡k<x
20 19 impcom ⊢∀k∈M…NF⁡k∈ℝ∧y∈ℝ→∀k∈M…NF⁡k≤y→∃x∈ℝ∀k∈M…NF⁡k<x
21 20 rexlimdva ⊢∀k∈M…NF⁡k∈ℝ→∃y∈ℝ∀k∈M…NF⁡k≤y→∃x∈ℝ∀k∈M…NF⁡k<x
22 3 21 mpd ⊢∀k∈M…NF⁡k∈ℝ→∃x∈ℝ∀k∈M…NF⁡k<x