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	ffvelrnda	$⊢ (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	biimpi	$⊢ seq 1 (+ F) \in dom ⇝ \to seq 1 (+ F) ⇝ ⇝ (seq 1 (+ F))$
22	21	adantl	$⊢ (F : ℕ ⟶ [0, +∞) \land seq 1 (+ F) \in dom ⇝) \to seq 1 (+ F) ⇝ ⇝ (seq 1 (+ F))$
23	7	adantr	$⊢ (F : ℕ ⟶ [0, +∞) \land seq 1 (+ F) \in dom ⇝) \to seq 1 (+ F) : ℕ ⟶ ℝ$
24	23	ffvelrnda	$⊢ ((F : ℕ ⟶ [0, +∞) \land seq 1 (+ F) \in dom ⇝) \land k \in ℕ) \to seq 1 (+ F) (k) \in ℝ$
25	1 19 22 24	climrecl	$⊢ (F : ℕ ⟶ [0, +∞) \land seq 1 (+ F) \in dom ⇝) \to ⇝ (seq 1 (+ F)) \in ℝ$
26		simpr	$⊢ ((F : ℕ ⟶ [0, +∞) \land seq 1 (+ F) \in dom ⇝) \land k \in ℕ) \to k \in ℕ$
27	22	adantr	$⊢ ((F : ℕ ⟶ [0, +∞) \land seq 1 (+ F) \in dom ⇝) \land k \in ℕ) \to seq 1 (+ F) ⇝ ⇝ (seq 1 (+ F))$
28		simplll	$⊢ (((F : ℕ ⟶ [0, +∞) \land seq 1 (+ F) \in dom ⇝) \land k \in ℕ) \land j \in ℕ) \to F : ℕ ⟶ [0, +∞)$
29		ffvelrn	$⊢ (F : ℕ ⟶ [0, +∞) \land j \in ℕ) \to F (j) \in [0, +∞)$
30	3 29	sselid	$⊢ (F : ℕ ⟶ [0, +∞) \land j \in ℕ) \to F (j) \in ℝ$
31	28 30	sylancom	$⊢ (((F : ℕ ⟶ [0, +∞) \land seq 1 (+ F) \in dom ⇝) \land k \in ℕ) \land j \in ℕ) \to F (j) \in ℝ$
32		elrege0	$⊢ F (j) \in [0, +∞) \leftrightarrow (F (j) \in ℝ \land 0 \leq F (j))$
33	32	simprbi	$⊢ F (j) \in [0, +∞) \to 0 \leq F (j)$
34	29 33	syl	$⊢ (F : ℕ ⟶ [0, +∞) \land j \in ℕ) \to 0 \leq F (j)$
35	34	adantlr	$⊢ ((F : ℕ ⟶ [0, +∞) \land seq 1 (+ F) \in dom ⇝) \land j \in ℕ) \to 0 \leq F (j)$
36	35	adantlr	$⊢ (((F : ℕ ⟶ [0, +∞) \land seq 1 (+ F) \in dom ⇝) \land k \in ℕ) \land j \in ℕ) \to 0 \leq F (j)$
37	1 26 27 31 36	climserle	$⊢ ((F : ℕ ⟶ [0, +∞) \land seq 1 (+ F) \in dom ⇝) \land k \in ℕ) \to seq 1 (+ F) (k) \leq ⇝ (seq 1 (+ F))$
38	37	ralrimiva	$⊢ (F : ℕ ⟶ [0, +∞) \land seq 1 (+ F) \in dom ⇝) \to \forall k \in ℕ seq 1 (+ F) (k) \leq ⇝ (seq 1 (+ F))$
39		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$
40	25 38 39	syl2anc	$⊢ (F : ℕ ⟶ [0, +∞) \land seq 1 (+ F) \in dom ⇝) \to \exists x \in ℝ \forall k \in ℕ seq 1 (+ F) (k) \leq x$
41		ffn	$⊢ seq 1 (+ F) : ℕ ⟶ ℝ \to seq 1 (+ F) Fn ℕ$
42		breq1	$⊢ z = seq 1 (+ F) (k) \to (z \leq x \leftrightarrow seq 1 (+ F) (k) \leq x)$
43	42	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)$
44	7 41 43	3syl	$⊢ F : ℕ ⟶ [0, +∞) \to (\forall z \in ran seq 1 (+ F) z \leq x \leftrightarrow \forall k \in ℕ seq 1 (+ F) (k) \leq x)$
45	44	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)$
46	45	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)$
47	40 46	mpbird	$⊢ (F : ℕ ⟶ [0, +∞) \land seq 1 (+ F) \in dom ⇝) \to \exists x \in ℝ \forall z \in ran seq 1 (+ F) z \leq x$
48		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 ℝ$
49	9 18 47 48	syl3anc	$⊢ (F : ℕ ⟶ [0, +∞) \land seq 1 (+ F) \in dom ⇝) \to sup (ran seq 1 (+ F) ℝ <) \in ℝ$

Metamath Proof Explorer

Theorem rge0scvg

Proof