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		simpl	$⊢ (N \in ℤ_{\geq M} \land F : (M \dots N) ⟶ ℝ) \to N \in ℤ_{\geq M}$
13		fzn0	$⊢ (M \dots N) \neq \emptyset \leftrightarrow N \in ℤ_{\geq M}$
14	12 13	sylibr	$⊢ (N \in ℤ_{\geq M} \land F : (M \dots N) ⟶ ℝ) \to (M \dots N) \neq \emptyset$
15	11 14	eqnetrd	$⊢ (N \in ℤ_{\geq M} \land F : (M \dots N) ⟶ ℝ) \to dom F \neq \emptyset$
16		dm0rn0	$⊢ dom F = \emptyset \leftrightarrow ran F = \emptyset$
17	16	necon3bii	$⊢ dom F \neq \emptyset \leftrightarrow ran F \neq \emptyset$
18	15 17	sylib	$⊢ (N \in ℤ_{\geq M} \land F : (M \dots N) ⟶ ℝ) \to ran F \neq \emptyset$
19		ltso	$⊢ < Or ℝ$
20		fisupcl	$⊢ (< Or ℝ \land (ran F \in Fin \land ran F \neq \emptyset \land ran F \subseteq ℝ)) \to sup (ran F ℝ <) \in ran F$
21	19 20	mpan	$⊢ (ran F \in Fin \land ran F \neq \emptyset \land ran F \subseteq ℝ) \to sup (ran F ℝ <) \in ran F$
22	9 18 2 21	syl3anc	$⊢ (N \in ℤ_{\geq M} \land F : (M \dots N) ⟶ ℝ) \to sup (ran F ℝ <) \in ran F$
23	2 22	sseldd	$⊢ (N \in ℤ_{\geq M} \land F : (M \dots N) ⟶ ℝ) \to sup (ran F ℝ <) \in ℝ$

Metamath Proof Explorer

Theorem fseqsupcl

Proof