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	$⊢ (N \in ℤ_{\geq M} \land F : (M \dots N) ⟶ ℝ) \to sup (ran F ℝ <) \in ℝ$

Proof

Step	Hyp	Ref	Expression
1		frn	$⊢ F : (M \dots N) ⟶ ℝ \to ran F \subseteq ℝ$
2	1	adantl	$⊢ (N \in ℤ_{\geq M} \land F : (M \dots N) ⟶ ℝ) \to ran F \subseteq ℝ$
3		fzfi	$⊢ (M \dots N) \in Fin$
4		ffn	$⊢ F : (M \dots N) ⟶ ℝ \to F Fn (M \dots N)$
5	4	adantl	$⊢ (N \in ℤ_{\geq M} \land F : (M \dots N) ⟶ ℝ) \to F Fn (M \dots N)$
6		dffn4	$⊢ F Fn (M \dots N) \leftrightarrow F : (M \dots N) \underset{onto}{⟶} ran F$
7	5 6	sylib	$⊢ (N \in ℤ_{\geq M} \land F : (M \dots N) ⟶ ℝ) \to F : (M \dots N) \underset{onto}{⟶} ran F$
8		fofi	$⊢ ((M \dots N) \in Fin \land F : (M \dots N) \underset{onto}{⟶} ran F) \to ran F \in Fin$
9	3 7 8	sylancr	$⊢ (N \in ℤ_{\geq M} \land F : (M \dots N) ⟶ ℝ) \to ran F \in Fin$
10		fdm	$⊢ F : (M \dots N) ⟶ ℝ \to dom F = (M \dots N)$
11	10	adantl	$⊢ (N \in ℤ_{\geq M} \land F : (M \dots N) ⟶ ℝ) \to dom F = (M \dots N)$
12		fzn0	$⊢ (M \dots N) \neq \emptyset \leftrightarrow N \in ℤ_{\geq M}$
13	12	biranri	$⊢ (N \in ℤ_{\geq M} \land F : (M \dots N) ⟶ ℝ) \to (M \dots N) \neq \emptyset$
14	11 13	eqnetrd	$⊢ (N \in ℤ_{\geq M} \land F : (M \dots N) ⟶ ℝ) \to dom F \neq \emptyset$
15		dm0rn0	$⊢ dom F = \emptyset \leftrightarrow ran F = \emptyset$
16	15	necon3bii	$⊢ dom F \neq \emptyset \leftrightarrow ran F \neq \emptyset$
17	14 16	sylib	$⊢ (N \in ℤ_{\geq M} \land F : (M \dots N) ⟶ ℝ) \to ran F \neq \emptyset$
18		ltso	$⊢ < Or ℝ$
19		fisupcl	$⊢ (< Or ℝ \land (ran F \in Fin \land ran F \neq \emptyset \land ran F \subseteq ℝ)) \to sup (ran F ℝ <) \in ran F$
20	18 19	mpan	$⊢ (ran F \in Fin \land ran F \neq \emptyset \land ran F \subseteq ℝ) \to sup (ran F ℝ <) \in ran F$
21	9 17 2 20	syl3anc	$⊢ (N \in ℤ_{\geq M} \land F : (M \dots N) ⟶ ℝ) \to sup (ran F ℝ <) \in ran F$
22	2 21	sseldd	$⊢ (N \in ℤ_{\geq M} \land F : (M \dots N) ⟶ ℝ) \to sup (ran F ℝ <) \in ℝ$

Metamath Proof Explorer

Theorem fseqsupcl

Proof