fseqsupubi

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

		Ref	Expression
	Assertion	fseqsupubi	$⊢ (K \in (M \dots N) \land F : (M \dots N) ⟶ ℝ) \to F (K) \leq sup (ran F ℝ <)$

Step	Hyp	Ref	Expression
1		frn	$⊢ F : (M \dots N) ⟶ ℝ \to ran F \subseteq ℝ$
2	1	adantl	$⊢ (K \in (M \dots N) \land F : (M \dots N) ⟶ ℝ) \to ran F \subseteq ℝ$
3		fdm	$⊢ F : (M \dots N) ⟶ ℝ \to dom F = (M \dots N)$
4		ne0i	$⊢ K \in (M \dots N) \to (M \dots N) \neq \emptyset$
5		dm0rn0	$⊢ dom F = \emptyset \leftrightarrow ran F = \emptyset$
6		eqeq1	$⊢ dom F = (M \dots N) \to (dom F = \emptyset \leftrightarrow (M \dots N) = \emptyset)$
7	6	biimpd	$⊢ dom F = (M \dots N) \to (dom F = \emptyset \to (M \dots N) = \emptyset)$
8	5 7	syl5bir	$⊢ dom F = (M \dots N) \to (ran F = \emptyset \to (M \dots N) = \emptyset)$
9	8	necon3d	$⊢ dom F = (M \dots N) \to ((M \dots N) \neq \emptyset \to ran F \neq \emptyset)$
10	4 9	mpan9	$⊢ (K \in (M \dots N) \land dom F = (M \dots N)) \to ran F \neq \emptyset$
11	3 10	sylan2	$⊢ (K \in (M \dots N) \land F : (M \dots N) ⟶ ℝ) \to ran F \neq \emptyset$
12		fsequb2	$⊢ F : (M \dots N) ⟶ ℝ \to \exists x \in ℝ \forall y \in ran F y \leq x$
13	12	adantl	$⊢ (K \in (M \dots N) \land F : (M \dots N) ⟶ ℝ) \to \exists x \in ℝ \forall y \in ran F y \leq x$
14		ffn	$⊢ F : (M \dots N) ⟶ ℝ \to F Fn (M \dots N)$
15		fnfvelrn	$⊢ (F Fn (M \dots N) \land K \in (M \dots N)) \to F (K) \in ran F$
16	15	ancoms	$⊢ (K \in (M \dots N) \land F Fn (M \dots N)) \to F (K) \in ran F$
17	14 16	sylan2	$⊢ (K \in (M \dots N) \land F : (M \dots N) ⟶ ℝ) \to F (K) \in ran F$
18	2 11 13 17	suprubd	$⊢ (K \in (M \dots N) \land F : (M \dots N) ⟶ ℝ) \to F (K) \leq sup (ran F ℝ <)$

Metamath Proof Explorer