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

Metamath Proof Explorer

Theorem fseqsupubi

Description: The values of a finite real sequence are bounded by their supremum. (Contributed by NM, 20-Sep-2005)

Ref Expression
Assertion fseqsupubi ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ ) → ( 𝐹 ‘ 𝐾 ) ≤ sup ( ran 𝐹 , ℝ , < ) )

Proof

Step Hyp Ref Expression
1 frn ⊢ ( 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ → ran 𝐹 ⊆ ℝ )
2 1 adantl ⊢ ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ ) → ran 𝐹 ⊆ ℝ )
3 fdm ⊢ ( 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ → dom 𝐹 = ( 𝑀 ... 𝑁 ) )
4 ne0i ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝑀 ... 𝑁 ) ≠ ∅ )
5 dm0rn0 ⊢ ( dom 𝐹 = ∅ ↔ ran 𝐹 = ∅ )
6 eqeq1 ⊢ ( dom 𝐹 = ( 𝑀 ... 𝑁 ) → ( dom 𝐹 = ∅ ↔ ( 𝑀 ... 𝑁 ) = ∅ ) )
7 6 biimpd ⊢ ( dom 𝐹 = ( 𝑀 ... 𝑁 ) → ( dom 𝐹 = ∅ → ( 𝑀 ... 𝑁 ) = ∅ ) )
8 5 7 biimtrrid ⊢ ( dom 𝐹 = ( 𝑀 ... 𝑁 ) → ( ran 𝐹 = ∅ → ( 𝑀 ... 𝑁 ) = ∅ ) )
9 8 necon3d ⊢ ( dom 𝐹 = ( 𝑀 ... 𝑁 ) → ( ( 𝑀 ... 𝑁 ) ≠ ∅ → ran 𝐹 ≠ ∅ ) )
10 4 9 mpan9 ⊢ ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ dom 𝐹 = ( 𝑀 ... 𝑁 ) ) → ran 𝐹 ≠ ∅ )
11 3 10 sylan2 ⊢ ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ ) → ran 𝐹 ≠ ∅ )
12 fsequb2 ⊢ ( 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 )
13 12 adantl ⊢ ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 )
14 ffn ⊢ ( 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ → 𝐹 Fn ( 𝑀 ... 𝑁 ) )
15 fnfvelrn ⊢ ( ( 𝐹 Fn ( 𝑀 ... 𝑁 ) ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝐾 ) ∈ ran 𝐹 )
16 15 ancoms ⊢ ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝐹 Fn ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝐾 ) ∈ ran 𝐹 )
17 14 16 sylan2 ⊢ ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ ) → ( 𝐹 ‘ 𝐾 ) ∈ ran 𝐹 )
18 2 11 13 17 suprubd ⊢ ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ ) → ( 𝐹 ‘ 𝐾 ) ≤ sup ( ran 𝐹 , ℝ , < ) )