rge0scvg

Description: Implication of convergence for a nonnegative series. This could be used to shorten prmreclem6 . (Contributed by Thierry Arnoux, 28-Jul-2017)

		Ref	Expression
	Assertion	rge0scvg	$⊢ (F : ℕ ⟶ [0, +∞) \land seq 1 (+ F) \in dom ⇝) \to sup (ran seq 1 (+ F) ℝ <) \in ℝ$

Proof

Step	Hyp	Ref	Expression
1		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
2		1zzd	$⊢ F : ℕ ⟶ [0, +∞) \to 1 \in ℤ$
3		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
4		fss	$⊢ (F : ℕ ⟶ [0, +∞) \land [0, +∞) \subseteq ℝ) \to F : ℕ ⟶ ℝ$
5	3 4	mpan2	$⊢ F : ℕ ⟶ [0, +∞) \to F : ℕ ⟶ ℝ$
6	5	ffvelcdmda	$⊢ (F : ℕ ⟶ [0, +∞) \land j \in ℕ) \to F (j) \in ℝ$
7	1 2 6	serfre	$⊢ F : ℕ ⟶ [0, +∞) \to seq 1 (+ F) : ℕ ⟶ ℝ$
8	7	frnd	$⊢ F : ℕ ⟶ [0, +∞) \to ran seq 1 (+ F) \subseteq ℝ$
9	8	adantr	$⊢ (F : ℕ ⟶ [0, +∞) \land seq 1 (+ F) \in dom ⇝) \to ran seq 1 (+ F) \subseteq ℝ$
10		1nn	$⊢ 1 \in ℕ$
11		fdm	$⊢ seq 1 (+ F) : ℕ ⟶ ℝ \to dom seq 1 (+ F) = ℕ$
12	10 11	eleqtrrid	$⊢ seq 1 (+ F) : ℕ ⟶ ℝ \to 1 \in dom seq 1 (+ F)$
13		ne0i	$⊢ 1 \in dom seq 1 (+ F) \to dom seq 1 (+ F) \neq \emptyset$
14		dm0rn0	$⊢ dom seq 1 (+ F) = \emptyset \leftrightarrow ran seq 1 (+ F) = \emptyset$
15	14	necon3bii	$⊢ dom seq 1 (+ F) \neq \emptyset \leftrightarrow ran seq 1 (+ F) \neq \emptyset$
16	13 15	sylib	$⊢ 1 \in dom seq 1 (+ F) \to ran seq 1 (+ F) \neq \emptyset$
17	7 12 16	3syl	$⊢ F : ℕ ⟶ [0, +∞) \to ran seq 1 (+ F) \neq \emptyset$
18	17	adantr	$⊢ (F : ℕ ⟶ [0, +∞) \land seq 1 (+ F) \in dom ⇝) \to ran seq 1 (+ F) \neq \emptyset$
19		1zzd	$⊢ (F : ℕ ⟶ [0, +∞) \land seq 1 (+ F) \in dom ⇝) \to 1 \in ℤ$
20		climdm	$⊢ seq 1 (+ F) \in dom ⇝ \leftrightarrow seq 1 (+ F) ⇝ ⇝ (seq 1 (+ F))$
21	20	bilani	$⊢ (F : ℕ ⟶ [0, +∞) \land seq 1 (+ F) \in dom ⇝) \to seq 1 (+ F) ⇝ ⇝ (seq 1 (+ F))$
22	7	adantr	$⊢ (F : ℕ ⟶ [0, +∞) \land seq 1 (+ F) \in dom ⇝) \to seq 1 (+ F) : ℕ ⟶ ℝ$
23	22	ffvelcdmda	$⊢ ((F : ℕ ⟶ [0, +∞) \land seq 1 (+ F) \in dom ⇝) \land k \in ℕ) \to seq 1 (+ F) (k) \in ℝ$
24	1 19 21 23	climrecl	$⊢ (F : ℕ ⟶ [0, +∞) \land seq 1 (+ F) \in dom ⇝) \to ⇝ (seq 1 (+ F)) \in ℝ$
25		simpr	$⊢ ((F : ℕ ⟶ [0, +∞) \land seq 1 (+ F) \in dom ⇝) \land k \in ℕ) \to k \in ℕ$
26	21	adantr	$⊢ ((F : ℕ ⟶ [0, +∞) \land seq 1 (+ F) \in dom ⇝) \land k \in ℕ) \to seq 1 (+ F) ⇝ ⇝ (seq 1 (+ F))$
27		simplll	$⊢ (((F : ℕ ⟶ [0, +∞) \land seq 1 (+ F) \in dom ⇝) \land k \in ℕ) \land j \in ℕ) \to F : ℕ ⟶ [0, +∞)$
28		ffvelcdm	$⊢ (F : ℕ ⟶ [0, +∞) \land j \in ℕ) \to F (j) \in [0, +∞)$
29	3 28	sselid	$⊢ (F : ℕ ⟶ [0, +∞) \land j \in ℕ) \to F (j) \in ℝ$
30	27 29	sylancom	$⊢ (((F : ℕ ⟶ [0, +∞) \land seq 1 (+ F) \in dom ⇝) \land k \in ℕ) \land j \in ℕ) \to F (j) \in ℝ$
31		elrege0	$⊢ F (j) \in [0, +∞) \leftrightarrow (F (j) \in ℝ \land 0 \leq F (j))$
32	31	simprbi	$⊢ F (j) \in [0, +∞) \to 0 \leq F (j)$
33	28 32	syl	$⊢ (F : ℕ ⟶ [0, +∞) \land j \in ℕ) \to 0 \leq F (j)$
34	33	adantlr	$⊢ ((F : ℕ ⟶ [0, +∞) \land seq 1 (+ F) \in dom ⇝) \land j \in ℕ) \to 0 \leq F (j)$
35	34	adantlr	$⊢ (((F : ℕ ⟶ [0, +∞) \land seq 1 (+ F) \in dom ⇝) \land k \in ℕ) \land j \in ℕ) \to 0 \leq F (j)$
36	1 25 26 30 35	climserle	$⊢ ((F : ℕ ⟶ [0, +∞) \land seq 1 (+ F) \in dom ⇝) \land k \in ℕ) \to seq 1 (+ F) (k) \leq ⇝ (seq 1 (+ F))$
37	36	ralrimiva	$⊢ (F : ℕ ⟶ [0, +∞) \land seq 1 (+ F) \in dom ⇝) \to \forall k \in ℕ seq 1 (+ F) (k) \leq ⇝ (seq 1 (+ F))$
38		brralrspcev	$⊢ (⇝ (seq 1 (+ F)) \in ℝ \land \forall k \in ℕ seq 1 (+ F) (k) \leq ⇝ (seq 1 (+ F))) \to \exists x \in ℝ \forall k \in ℕ seq 1 (+ F) (k) \leq x$
39	24 37 38	syl2anc	$⊢ (F : ℕ ⟶ [0, +∞) \land seq 1 (+ F) \in dom ⇝) \to \exists x \in ℝ \forall k \in ℕ seq 1 (+ F) (k) \leq x$
40		ffn	$⊢ seq 1 (+ F) : ℕ ⟶ ℝ \to seq 1 (+ F) Fn ℕ$
41		breq1	$⊢ z = seq 1 (+ F) (k) \to (z \leq x \leftrightarrow seq 1 (+ F) (k) \leq x)$
42	41	ralrn	$⊢ seq 1 (+ F) Fn ℕ \to (\forall z \in ran seq 1 (+ F) z \leq x \leftrightarrow \forall k \in ℕ seq 1 (+ F) (k) \leq x)$
43	7 40 42	3syl	$⊢ F : ℕ ⟶ [0, +∞) \to (\forall z \in ran seq 1 (+ F) z \leq x \leftrightarrow \forall k \in ℕ seq 1 (+ F) (k) \leq x)$
44	43	rexbidv	$⊢ F : ℕ ⟶ [0, +∞) \to (\exists x \in ℝ \forall z \in ran seq 1 (+ F) z \leq x \leftrightarrow \exists x \in ℝ \forall k \in ℕ seq 1 (+ F) (k) \leq x)$
45	44	adantr	$⊢ (F : ℕ ⟶ [0, +∞) \land seq 1 (+ F) \in dom ⇝) \to (\exists x \in ℝ \forall z \in ran seq 1 (+ F) z \leq x \leftrightarrow \exists x \in ℝ \forall k \in ℕ seq 1 (+ F) (k) \leq x)$
46	39 45	mpbird	$⊢ (F : ℕ ⟶ [0, +∞) \land seq 1 (+ F) \in dom ⇝) \to \exists x \in ℝ \forall z \in ran seq 1 (+ F) z \leq x$
47		suprcl	$⊢ (ran seq 1 (+ F) \subseteq ℝ \land ran seq 1 (+ F) \neq \emptyset \land \exists x \in ℝ \forall z \in ran seq 1 (+ F) z \leq x) \to sup (ran seq 1 (+ F) ℝ <) \in ℝ$
48	9 18 46 47	syl3anc	$⊢ (F : ℕ ⟶ [0, +∞) \land seq 1 (+ F) \in dom ⇝) \to sup (ran seq 1 (+ F) ℝ <) \in ℝ$

Metamath Proof Explorer

Theorem rge0scvg

Proof