Metamath Proof Explorer

Theorem fseqsupcl

Description: The values of a finite real sequence have a supremum. (Contributed by NM, 20-Sep-2005) (Revised by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion fseqsupcl ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ ) → sup ( ran 𝐹 , ℝ , < ) ∈ ℝ )

Proof

Step Hyp Ref Expression
1 frn ⊢ ( 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ → ran 𝐹 ⊆ ℝ )
2 1 adantl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ ) → ran 𝐹 ⊆ ℝ )
3 fzfi ⊢ ( 𝑀 ... 𝑁 ) ∈ Fin
4 ffn ⊢ ( 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ → 𝐹 Fn ( 𝑀 ... 𝑁 ) )
5 4 adantl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ ) → 𝐹 Fn ( 𝑀 ... 𝑁 ) )
6 dffn4 ⊢ ( 𝐹 Fn ( 𝑀 ... 𝑁 ) ↔ 𝐹 : ( 𝑀 ... 𝑁 ) –onto→ ran 𝐹 )
7 5 6 sylib ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ ) → 𝐹 : ( 𝑀 ... 𝑁 ) –onto→ ran 𝐹 )
8 fofi ⊢ ( ( ( 𝑀 ... 𝑁 ) ∈ Fin ∧ 𝐹 : ( 𝑀 ... 𝑁 ) –onto→ ran 𝐹 ) → ran 𝐹 ∈ Fin )
9 3 7 8 sylancr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ ) → ran 𝐹 ∈ Fin )
10 fdm ⊢ ( 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ → dom 𝐹 = ( 𝑀 ... 𝑁 ) )
11 10 adantl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ ) → dom 𝐹 = ( 𝑀 ... 𝑁 ) )
12 simpl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
13 fzn0 ⊢ ( ( 𝑀 ... 𝑁 ) ≠ ∅ ↔ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
14 12 13 sylibr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ ) → ( 𝑀 ... 𝑁 ) ≠ ∅ )
15 11 14 eqnetrd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ ) → dom 𝐹 ≠ ∅ )
16 dm0rn0 ⊢ ( dom 𝐹 = ∅ ↔ ran 𝐹 = ∅ )
17 16 necon3bii ⊢ ( dom 𝐹 ≠ ∅ ↔ ran 𝐹 ≠ ∅ )
18 15 17 sylib ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ ) → ran 𝐹 ≠ ∅ )
19 ltso ⊢ < Or ℝ
20 fisupcl ⊢ ( ( < Or ℝ ∧ ( ran 𝐹 ∈ Fin ∧ ran 𝐹 ≠ ∅ ∧ ran 𝐹 ⊆ ℝ ) ) → sup ( ran 𝐹 , ℝ , < ) ∈ ran 𝐹 )
21 19 20 mpan ⊢ ( ( ran 𝐹 ∈ Fin ∧ ran 𝐹 ≠ ∅ ∧ ran 𝐹 ⊆ ℝ ) → sup ( ran 𝐹 , ℝ , < ) ∈ ran 𝐹 )
22 9 18 2 21 syl3anc ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ ) → sup ( ran 𝐹 , ℝ , < ) ∈ ran 𝐹 )
23 2 22 sseldd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ ) → sup ( ran 𝐹 , ℝ , < ) ∈ ℝ )