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 𝐹 , ℝ , < ) )