esumfsup

Description: Formulating an extended sum over integers using the recursive sequence builder. (Contributed by Thierry Arnoux, 18-Oct-2017)

		Ref	Expression
	Hypothesis	esumfsup.1	$⊢ \underline{Ⅎ} k F$
	Assertion	esumfsup	$⊢ F : ℕ ⟶ [0, +∞] \to \underset{k \in ℕ}{\sum^{}} F (k) = sup (ran seq 1 (+_{𝑒}, F) ℝ^{} <)$

Proof

Step	Hyp	Ref	Expression
1		esumfsup.1	$⊢ \underline{Ⅎ} k F$
2		1z	$⊢ 1 \in ℤ$
3		seqfn	$⊢ 1 \in ℤ \to seq 1 (+_{𝑒}, F) Fn ℤ_{\geq 1}$
4	2 3	ax-mp	$⊢ seq 1 (+_{𝑒}, F) Fn ℤ_{\geq 1}$
5		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
6	5	fneq2i	$⊢ seq 1 (+_{𝑒}, F) Fn ℕ \leftrightarrow seq 1 (+_{𝑒}, F) Fn ℤ_{\geq 1}$
7	4 6	mpbir	$⊢ seq 1 (+_{𝑒}, F) Fn ℕ$
8		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
9	1	esumfzf	$⊢ (F : ℕ ⟶ [0, +∞] \land n \in ℕ) \to {\sum^{*}}_{k = 1}^{n} F (k) = seq 1 (+_{𝑒}, F) (n)$
10		ovex	$⊢ (1 \dots n) \in V$
11		nfcv	$⊢ \underline{Ⅎ} k ℕ$
12		nfcv	$⊢ \underline{Ⅎ} k [0, +∞]$
13	1 11 12	nff	$⊢ Ⅎ k F : ℕ ⟶ [0, +∞]$
14		nfv	$⊢ Ⅎ k n \in ℕ$
15	13 14	nfan	$⊢ Ⅎ k (F : ℕ ⟶ [0, +∞] \land n \in ℕ)$
16		simpll	$⊢ ((F : ℕ ⟶ [0, +∞] \land n \in ℕ) \land k \in (1 \dots n)) \to F : ℕ ⟶ [0, +∞]$
17		1nn	$⊢ 1 \in ℕ$
18		fzssnn	$⊢ 1 \in ℕ \to (1 \dots n) \subseteq ℕ$
19	17 18	mp1i	$⊢ ((F : ℕ ⟶ [0, +∞] \land n \in ℕ) \land k \in (1 \dots n)) \to (1 \dots n) \subseteq ℕ$
20		simpr	$⊢ ((F : ℕ ⟶ [0, +∞] \land n \in ℕ) \land k \in (1 \dots n)) \to k \in (1 \dots n)$
21	19 20	sseldd	$⊢ ((F : ℕ ⟶ [0, +∞] \land n \in ℕ) \land k \in (1 \dots n)) \to k \in ℕ$
22	16 21	ffvelrnd	$⊢ ((F : ℕ ⟶ [0, +∞] \land n \in ℕ) \land k \in (1 \dots n)) \to F (k) \in [0, +∞]$
23	22	ex	$⊢ (F : ℕ ⟶ [0, +∞] \land n \in ℕ) \to (k \in (1 \dots n) \to F (k) \in [0, +∞])$
24	15 23	ralrimi	$⊢ (F : ℕ ⟶ [0, +∞] \land n \in ℕ) \to \forall k \in (1 \dots n) F (k) \in [0, +∞]$
25		nfcv	$⊢ \underline{Ⅎ} k (1 \dots n)$
26	25	esumcl	$⊢ ((1 \dots n) \in V \land \forall k \in (1 \dots n) F (k) \in [0, +∞]) \to {\sum^{*}}_{k = 1}^{n} F (k) \in [0, +∞]$
27	10 24 26	sylancr	$⊢ (F : ℕ ⟶ [0, +∞] \land n \in ℕ) \to {\sum^{*}}_{k = 1}^{n} F (k) \in [0, +∞]$
28	9 27	eqeltrrd	$⊢ (F : ℕ ⟶ [0, +∞] \land n \in ℕ) \to seq 1 (+_{𝑒}, F) (n) \in [0, +∞]$
29	8 28	sselid	$⊢ (F : ℕ ⟶ [0, +∞] \land n \in ℕ) \to seq 1 (+_{𝑒}, F) (n) \in ℝ^{*}$
30	29	ralrimiva	$⊢ F : ℕ ⟶ [0, +∞] \to \forall n \in ℕ seq 1 (+_{𝑒}, F) (n) \in ℝ^{*}$
31		fnfvrnss	$⊢ (seq 1 (+_{𝑒}, F) Fn ℕ \land \forall n \in ℕ seq 1 (+_{𝑒}, F) (n) \in ℝ^{}) \to ran seq 1 (+_{𝑒}, F) \subseteq ℝ^{}$
32	7 30 31	sylancr	$⊢ F : ℕ ⟶ [0, +∞] \to ran seq 1 (+_{𝑒}, F) \subseteq ℝ^{*}$
33		nnex	$⊢ ℕ \in V$
34		ffvelrn	$⊢ (F : ℕ ⟶ [0, +∞] \land k \in ℕ) \to F (k) \in [0, +∞]$
35	34	ex	$⊢ F : ℕ ⟶ [0, +∞] \to (k \in ℕ \to F (k) \in [0, +∞])$
36	13 35	ralrimi	$⊢ F : ℕ ⟶ [0, +∞] \to \forall k \in ℕ F (k) \in [0, +∞]$
37	11	esumcl	$⊢ (ℕ \in V \land \forall k \in ℕ F (k) \in [0, +∞]) \to \underset{k \in ℕ}{\sum^{*}} F (k) \in [0, +∞]$
38	33 36 37	sylancr	$⊢ F : ℕ ⟶ [0, +∞] \to \underset{k \in ℕ}{\sum^{*}} F (k) \in [0, +∞]$
39	8 38	sselid	$⊢ F : ℕ ⟶ [0, +∞] \to \underset{k \in ℕ}{\sum^{}} F (k) \in ℝ^{}$
40		fvelrnb	$⊢ seq 1 (+_{𝑒}, F) Fn ℕ \to (x \in ran seq 1 (+_{𝑒}, F) \leftrightarrow \exists n \in ℕ seq 1 (+_{𝑒}, F) (n) = x)$
41	7 40	mp1i	$⊢ F : ℕ ⟶ [0, +∞] \to (x \in ran seq 1 (+_{𝑒}, F) \leftrightarrow \exists n \in ℕ seq 1 (+_{𝑒}, F) (n) = x)$
42		eqcom	$⊢ {\sum^{}}_{k = 1}^{n} F (k) = x \leftrightarrow x = {\sum^{}}_{k = 1}^{n} F (k)$
43	9	eqeq1d	$⊢ (F : ℕ ⟶ [0, +∞] \land n \in ℕ) \to ({\sum^{*}}_{k = 1}^{n} F (k) = x \leftrightarrow seq 1 (+_{𝑒}, F) (n) = x)$
44	42 43	bitr3id	$⊢ (F : ℕ ⟶ [0, +∞] \land n \in ℕ) \to (x = {\sum^{*}}_{k = 1}^{n} F (k) \leftrightarrow seq 1 (+_{𝑒}, F) (n) = x)$
45	44	rexbidva	$⊢ F : ℕ ⟶ [0, +∞] \to (\exists n \in ℕ x = {\sum^{*}}_{k = 1}^{n} F (k) \leftrightarrow \exists n \in ℕ seq 1 (+_{𝑒}, F) (n) = x)$
46	41 45	bitr4d	$⊢ F : ℕ ⟶ [0, +∞] \to (x \in ran seq 1 (+_{𝑒}, F) \leftrightarrow \exists n \in ℕ x = {\sum^{*}}_{k = 1}^{n} F (k))$
47	46	biimpa	$⊢ (F : ℕ ⟶ [0, +∞] \land x \in ran seq 1 (+_{𝑒}, F)) \to \exists n \in ℕ x = {\sum^{*}}_{k = 1}^{n} F (k)$
48	33	a1i	$⊢ (F : ℕ ⟶ [0, +∞] \land n \in ℕ) \to ℕ \in V$
49	34	adantlr	$⊢ ((F : ℕ ⟶ [0, +∞] \land n \in ℕ) \land k \in ℕ) \to F (k) \in [0, +∞]$
50	17 18	mp1i	$⊢ (F : ℕ ⟶ [0, +∞] \land n \in ℕ) \to (1 \dots n) \subseteq ℕ$
51	15 48 49 50	esummono	$⊢ (F : ℕ ⟶ [0, +∞] \land n \in ℕ) \to {\sum^{}}_{k = 1}^{n} F (k) \leq \underset{k \in ℕ}{\sum^{}} F (k)$
52	51	ralrimiva	$⊢ F : ℕ ⟶ [0, +∞] \to \forall n \in ℕ {\sum^{}}_{k = 1}^{n} F (k) \leq \underset{k \in ℕ}{\sum^{}} F (k)$
53	52	adantr	$⊢ (F : ℕ ⟶ [0, +∞] \land x \in ran seq 1 (+_{𝑒}, F)) \to \forall n \in ℕ {\sum^{}}_{k = 1}^{n} F (k) \leq \underset{k \in ℕ}{\sum^{}} F (k)$
54	47 53	jca	$⊢ (F : ℕ ⟶ [0, +∞] \land x \in ran seq 1 (+_{𝑒}, F)) \to (\exists n \in ℕ x = {\sum^{}}_{k = 1}^{n} F (k) \land \forall n \in ℕ {\sum^{}}_{k = 1}^{n} F (k) \leq \underset{k \in ℕ}{\sum^{*}} F (k))$
55		r19.29r	$⊢ (\exists n \in ℕ x = {\sum^{}}_{k = 1}^{n} F (k) \land \forall n \in ℕ {\sum^{}}_{k = 1}^{n} F (k) \leq \underset{k \in ℕ}{\sum^{}} F (k)) \to \exists n \in ℕ (x = {\sum^{}}_{k = 1}^{n} F (k) \land {\sum^{}}_{k = 1}^{n} F (k) \leq \underset{k \in ℕ}{\sum^{}} F (k))$
56		breq1	$⊢ x = {\sum^{}}_{k = 1}^{n} F (k) \to (x \leq \underset{k \in ℕ}{\sum^{}} F (k) \leftrightarrow {\sum^{}}_{k = 1}^{n} F (k) \leq \underset{k \in ℕ}{\sum^{}} F (k))$
57	56	biimpar	$⊢ (x = {\sum^{}}_{k = 1}^{n} F (k) \land {\sum^{}}_{k = 1}^{n} F (k) \leq \underset{k \in ℕ}{\sum^{}} F (k)) \to x \leq \underset{k \in ℕ}{\sum^{}} F (k)$
58	57	rexlimivw	$⊢ \exists n \in ℕ (x = {\sum^{}}_{k = 1}^{n} F (k) \land {\sum^{}}_{k = 1}^{n} F (k) \leq \underset{k \in ℕ}{\sum^{}} F (k)) \to x \leq \underset{k \in ℕ}{\sum^{}} F (k)$
59	54 55 58	3syl	$⊢ (F : ℕ ⟶ [0, +∞] \land x \in ran seq 1 (+_{𝑒}, F)) \to x \leq \underset{k \in ℕ}{\sum^{*}} F (k)$
60	59	ralrimiva	$⊢ F : ℕ ⟶ [0, +∞] \to \forall x \in ran seq 1 (+_{𝑒}, F) x \leq \underset{k \in ℕ}{\sum^{*}} F (k)$
61		nfv	$⊢ Ⅎ k x \in ℝ$
62	13 61	nfan	$⊢ Ⅎ k (F : ℕ ⟶ [0, +∞] \land x \in ℝ)$
63		nfcv	$⊢ \underline{Ⅎ} k x$
64		nfcv	$⊢ \underline{Ⅎ} k <$
65	11	nfesum1	$⊢ \underline{Ⅎ} k \underset{k \in ℕ}{\sum^{*}} F (k)$
66	63 64 65	nfbr	$⊢ Ⅎ k x < \underset{k \in ℕ}{\sum^{*}} F (k)$
67	62 66	nfan	$⊢ Ⅎ k ((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{*}} F (k))$
68	33	a1i	$⊢ ((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{*}} F (k)) \to ℕ \in V$
69		simplll	$⊢ (((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{*}} F (k)) \land k \in ℕ) \to F : ℕ ⟶ [0, +∞]$
70	69 34	sylancom	$⊢ (((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{*}} F (k)) \land k \in ℕ) \to F (k) \in [0, +∞]$
71		simplr	$⊢ ((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{*}} F (k)) \to x \in ℝ$
72	71	rexrd	$⊢ ((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{}} F (k)) \to x \in ℝ^{}$
73		simpr	$⊢ ((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{}} F (k)) \to x < \underset{k \in ℕ}{\sum^{}} F (k)$
74	67 68 70 72 73	esumlub	$⊢ ((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{}} F (k)) \to \exists a \in (𝒫 ℕ \cap Fin) x < \underset{k \in a}{\sum^{}} F (k)$
75		ssnnssfz	$⊢ a \in (𝒫 ℕ \cap Fin) \to \exists n \in ℕ a \subseteq (1 \dots n)$
76		r19.42v	$⊢ \exists n \in ℕ (((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{}} F (k)) \land a \subseteq (1 \dots n)) \leftrightarrow (((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{}} F (k)) \land \exists n \in ℕ a \subseteq (1 \dots n))$
77		nfv	$⊢ Ⅎ k a \subseteq (1 \dots n)$
78	67 77	nfan	$⊢ Ⅎ k (((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{*}} F (k)) \land a \subseteq (1 \dots n))$
79	10	a1i	$⊢ (((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{*}} F (k)) \land a \subseteq (1 \dots n)) \to (1 \dots n) \in V$
80		simp-4l	$⊢ ((((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{*}} F (k)) \land a \subseteq (1 \dots n)) \land k \in (1 \dots n)) \to F : ℕ ⟶ [0, +∞]$
81	17 18	ax-mp	$⊢ (1 \dots n) \subseteq ℕ$
82		simpr	$⊢ ((((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{*}} F (k)) \land a \subseteq (1 \dots n)) \land k \in (1 \dots n)) \to k \in (1 \dots n)$
83	81 82	sselid	$⊢ ((((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{*}} F (k)) \land a \subseteq (1 \dots n)) \land k \in (1 \dots n)) \to k \in ℕ$
84	80 83	ffvelrnd	$⊢ ((((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{*}} F (k)) \land a \subseteq (1 \dots n)) \land k \in (1 \dots n)) \to F (k) \in [0, +∞]$
85		simpr	$⊢ (((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{*}} F (k)) \land a \subseteq (1 \dots n)) \to a \subseteq (1 \dots n)$
86	78 79 84 85	esummono	$⊢ (((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{}} F (k)) \land a \subseteq (1 \dots n)) \to \underset{k \in a}{\sum^{}} F (k) \leq {\sum^{*}}_{k = 1}^{n} F (k)$
87	86	reximi	$⊢ \exists n \in ℕ (((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{}} F (k)) \land a \subseteq (1 \dots n)) \to \exists n \in ℕ \underset{k \in a}{\sum^{}} F (k) \leq {\sum^{*}}_{k = 1}^{n} F (k)$
88	76 87	sylbir	$⊢ (((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{}} F (k)) \land \exists n \in ℕ a \subseteq (1 \dots n)) \to \exists n \in ℕ \underset{k \in a}{\sum^{}} F (k) \leq {\sum^{*}}_{k = 1}^{n} F (k)$
89	75 88	sylan2	$⊢ (((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{}} F (k)) \land a \in (𝒫 ℕ \cap Fin)) \to \exists n \in ℕ \underset{k \in a}{\sum^{}} F (k) \leq {\sum^{*}}_{k = 1}^{n} F (k)$
90	89	ralrimiva	$⊢ ((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{}} F (k)) \to \forall a \in (𝒫 ℕ \cap Fin) \exists n \in ℕ \underset{k \in a}{\sum^{}} F (k) \leq {\sum^{*}}_{k = 1}^{n} F (k)$
91		r19.29r	$⊢ (\exists a \in (𝒫 ℕ \cap Fin) x < \underset{k \in a}{\sum^{}} F (k) \land \forall a \in (𝒫 ℕ \cap Fin) \exists n \in ℕ \underset{k \in a}{\sum^{}} F (k) \leq {\sum^{}}_{k = 1}^{n} F (k)) \to \exists a \in (𝒫 ℕ \cap Fin) (x < \underset{k \in a}{\sum^{}} F (k) \land \exists n \in ℕ \underset{k \in a}{\sum^{}} F (k) \leq {\sum^{}}_{k = 1}^{n} F (k))$
92		r19.42v	$⊢ \exists n \in ℕ (x < \underset{k \in a}{\sum^{}} F (k) \land \underset{k \in a}{\sum^{}} F (k) \leq {\sum^{}}_{k = 1}^{n} F (k)) \leftrightarrow (x < \underset{k \in a}{\sum^{}} F (k) \land \exists n \in ℕ \underset{k \in a}{\sum^{}} F (k) \leq {\sum^{}}_{k = 1}^{n} F (k))$
93	92	rexbii	$⊢ \exists a \in (𝒫 ℕ \cap Fin) \exists n \in ℕ (x < \underset{k \in a}{\sum^{}} F (k) \land \underset{k \in a}{\sum^{}} F (k) \leq {\sum^{}}_{k = 1}^{n} F (k)) \leftrightarrow \exists a \in (𝒫 ℕ \cap Fin) (x < \underset{k \in a}{\sum^{}} F (k) \land \exists n \in ℕ \underset{k \in a}{\sum^{}} F (k) \leq {\sum^{}}_{k = 1}^{n} F (k))$
94	91 93	sylibr	$⊢ (\exists a \in (𝒫 ℕ \cap Fin) x < \underset{k \in a}{\sum^{}} F (k) \land \forall a \in (𝒫 ℕ \cap Fin) \exists n \in ℕ \underset{k \in a}{\sum^{}} F (k) \leq {\sum^{}}_{k = 1}^{n} F (k)) \to \exists a \in (𝒫 ℕ \cap Fin) \exists n \in ℕ (x < \underset{k \in a}{\sum^{}} F (k) \land \underset{k \in a}{\sum^{}} F (k) \leq {\sum^{}}_{k = 1}^{n} F (k))$
95	74 90 94	syl2anc	$⊢ ((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{}} F (k)) \to \exists a \in (𝒫 ℕ \cap Fin) \exists n \in ℕ (x < \underset{k \in a}{\sum^{}} F (k) \land \underset{k \in a}{\sum^{}} F (k) \leq {\sum^{}}_{k = 1}^{n} F (k))$
96		simp-4r	$⊢ ((((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{*}} F (k)) \land a \in (𝒫 ℕ \cap Fin)) \land n \in ℕ) \to x \in ℝ$
97	96	rexrd	$⊢ ((((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{}} F (k)) \land a \in (𝒫 ℕ \cap Fin)) \land n \in ℕ) \to x \in ℝ^{}$
98		vex	$⊢ a \in V$
99		nfcv	$⊢ \underline{Ⅎ} k a$
100	99	nfel1	$⊢ Ⅎ k a \in (𝒫 ℕ \cap Fin)$
101	67 100	nfan	$⊢ Ⅎ k (((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{*}} F (k)) \land a \in (𝒫 ℕ \cap Fin))$
102	101 14	nfan	$⊢ Ⅎ k ((((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{*}} F (k)) \land a \in (𝒫 ℕ \cap Fin)) \land n \in ℕ)$
103		simp-5l	$⊢ (((((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{*}} F (k)) \land a \in (𝒫 ℕ \cap Fin)) \land n \in ℕ) \land k \in a) \to F : ℕ ⟶ [0, +∞]$
104		simpllr	$⊢ (((((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{*}} F (k)) \land a \in (𝒫 ℕ \cap Fin)) \land n \in ℕ) \land k \in a) \to a \in (𝒫 ℕ \cap Fin)$
105		inss1	$⊢ 𝒫 ℕ \cap Fin \subseteq 𝒫 ℕ$
106	105	sseli	$⊢ a \in (𝒫 ℕ \cap Fin) \to a \in 𝒫 ℕ$
107		elpwi	$⊢ a \in 𝒫 ℕ \to a \subseteq ℕ$
108	104 106 107	3syl	$⊢ (((((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{*}} F (k)) \land a \in (𝒫 ℕ \cap Fin)) \land n \in ℕ) \land k \in a) \to a \subseteq ℕ$
109		simpr	$⊢ (((((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{*}} F (k)) \land a \in (𝒫 ℕ \cap Fin)) \land n \in ℕ) \land k \in a) \to k \in a$
110	108 109	sseldd	$⊢ (((((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{*}} F (k)) \land a \in (𝒫 ℕ \cap Fin)) \land n \in ℕ) \land k \in a) \to k \in ℕ$
111	103 110	ffvelrnd	$⊢ (((((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{*}} F (k)) \land a \in (𝒫 ℕ \cap Fin)) \land n \in ℕ) \land k \in a) \to F (k) \in [0, +∞]$
112	111	ex	$⊢ ((((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{*}} F (k)) \land a \in (𝒫 ℕ \cap Fin)) \land n \in ℕ) \to (k \in a \to F (k) \in [0, +∞])$
113	102 112	ralrimi	$⊢ ((((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{*}} F (k)) \land a \in (𝒫 ℕ \cap Fin)) \land n \in ℕ) \to \forall k \in a F (k) \in [0, +∞]$
114	99	esumcl	$⊢ (a \in V \land \forall k \in a F (k) \in [0, +∞]) \to \underset{k \in a}{\sum^{*}} F (k) \in [0, +∞]$
115	98 113 114	sylancr	$⊢ ((((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{}} F (k)) \land a \in (𝒫 ℕ \cap Fin)) \land n \in ℕ) \to \underset{k \in a}{\sum^{}} F (k) \in [0, +∞]$
116	8 115	sselid	$⊢ ((((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{}} F (k)) \land a \in (𝒫 ℕ \cap Fin)) \land n \in ℕ) \to \underset{k \in a}{\sum^{}} F (k) \in ℝ^{*}$
117		simp-5l	$⊢ (((((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{*}} F (k)) \land a \in (𝒫 ℕ \cap Fin)) \land n \in ℕ) \land k \in (1 \dots n)) \to F : ℕ ⟶ [0, +∞]$
118		simpr	$⊢ (((((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{*}} F (k)) \land a \in (𝒫 ℕ \cap Fin)) \land n \in ℕ) \land k \in (1 \dots n)) \to k \in (1 \dots n)$
119	81 118	sselid	$⊢ (((((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{*}} F (k)) \land a \in (𝒫 ℕ \cap Fin)) \land n \in ℕ) \land k \in (1 \dots n)) \to k \in ℕ$
120	117 119	ffvelrnd	$⊢ (((((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{*}} F (k)) \land a \in (𝒫 ℕ \cap Fin)) \land n \in ℕ) \land k \in (1 \dots n)) \to F (k) \in [0, +∞]$
121	120	ex	$⊢ ((((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{*}} F (k)) \land a \in (𝒫 ℕ \cap Fin)) \land n \in ℕ) \to (k \in (1 \dots n) \to F (k) \in [0, +∞])$
122	102 121	ralrimi	$⊢ ((((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{*}} F (k)) \land a \in (𝒫 ℕ \cap Fin)) \land n \in ℕ) \to \forall k \in (1 \dots n) F (k) \in [0, +∞]$
123	10 122 26	sylancr	$⊢ ((((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{}} F (k)) \land a \in (𝒫 ℕ \cap Fin)) \land n \in ℕ) \to {\sum^{}}_{k = 1}^{n} F (k) \in [0, +∞]$
124	8 123	sselid	$⊢ ((((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{}} F (k)) \land a \in (𝒫 ℕ \cap Fin)) \land n \in ℕ) \to {\sum^{}}_{k = 1}^{n} F (k) \in ℝ^{*}$
125		xrltletr	$⊢ (x \in ℝ^{} \land \underset{k \in a}{\sum^{}} F (k) \in ℝ^{} \land {\sum^{}}_{k = 1}^{n} F (k) \in ℝ^{}) \to ((x < \underset{k \in a}{\sum^{}} F (k) \land \underset{k \in a}{\sum^{}} F (k) \leq {\sum^{}}_{k = 1}^{n} F (k)) \to x < {\sum^{*}}_{k = 1}^{n} F (k))$
126	97 116 124 125	syl3anc	$⊢ ((((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{}} F (k)) \land a \in (𝒫 ℕ \cap Fin)) \land n \in ℕ) \to ((x < \underset{k \in a}{\sum^{}} F (k) \land \underset{k \in a}{\sum^{}} F (k) \leq {\sum^{}}_{k = 1}^{n} F (k)) \to x < {\sum^{*}}_{k = 1}^{n} F (k))$
127	126	reximdva	$⊢ (((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{}} F (k)) \land a \in (𝒫 ℕ \cap Fin)) \to (\exists n \in ℕ (x < \underset{k \in a}{\sum^{}} F (k) \land \underset{k \in a}{\sum^{}} F (k) \leq {\sum^{}}_{k = 1}^{n} F (k)) \to \exists n \in ℕ x < {\sum^{*}}_{k = 1}^{n} F (k))$
128	127	rexlimdva	$⊢ ((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{}} F (k)) \to (\exists a \in (𝒫 ℕ \cap Fin) \exists n \in ℕ (x < \underset{k \in a}{\sum^{}} F (k) \land \underset{k \in a}{\sum^{}} F (k) \leq {\sum^{}}_{k = 1}^{n} F (k)) \to \exists n \in ℕ x < {\sum^{*}}_{k = 1}^{n} F (k))$
129	95 128	mpd	$⊢ ((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{}} F (k)) \to \exists n \in ℕ x < {\sum^{}}_{k = 1}^{n} F (k)$
130		fvelrnb	$⊢ seq 1 (+_{𝑒}, F) Fn ℕ \to (y \in ran seq 1 (+_{𝑒}, F) \leftrightarrow \exists n \in ℕ seq 1 (+_{𝑒}, F) (n) = y)$
131	7 130	mp1i	$⊢ F : ℕ ⟶ [0, +∞] \to (y \in ran seq 1 (+_{𝑒}, F) \leftrightarrow \exists n \in ℕ seq 1 (+_{𝑒}, F) (n) = y)$
132		eqcom	$⊢ {\sum^{}}_{k = 1}^{n} F (k) = y \leftrightarrow y = {\sum^{}}_{k = 1}^{n} F (k)$
133	9	eqeq1d	$⊢ (F : ℕ ⟶ [0, +∞] \land n \in ℕ) \to ({\sum^{*}}_{k = 1}^{n} F (k) = y \leftrightarrow seq 1 (+_{𝑒}, F) (n) = y)$
134	132 133	bitr3id	$⊢ (F : ℕ ⟶ [0, +∞] \land n \in ℕ) \to (y = {\sum^{*}}_{k = 1}^{n} F (k) \leftrightarrow seq 1 (+_{𝑒}, F) (n) = y)$
135	134	rexbidva	$⊢ F : ℕ ⟶ [0, +∞] \to (\exists n \in ℕ y = {\sum^{*}}_{k = 1}^{n} F (k) \leftrightarrow \exists n \in ℕ seq 1 (+_{𝑒}, F) (n) = y)$
136	131 135	bitr4d	$⊢ F : ℕ ⟶ [0, +∞] \to (y \in ran seq 1 (+_{𝑒}, F) \leftrightarrow \exists n \in ℕ y = {\sum^{*}}_{k = 1}^{n} F (k))$
137		simpr	$⊢ (F : ℕ ⟶ [0, +∞] \land y = {\sum^{}}_{k = 1}^{n} F (k)) \to y = {\sum^{}}_{k = 1}^{n} F (k)$
138	137	breq2d	$⊢ (F : ℕ ⟶ [0, +∞] \land y = {\sum^{}}_{k = 1}^{n} F (k)) \to (x < y \leftrightarrow x < {\sum^{}}_{k = 1}^{n} F (k))$
139	27 136 138	rexxfr2d	$⊢ F : ℕ ⟶ [0, +∞] \to (\exists y \in ran seq 1 (+_{𝑒}, F) x < y \leftrightarrow \exists n \in ℕ x < {\sum^{*}}_{k = 1}^{n} F (k))$
140	139	ad2antrr	$⊢ ((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{}} F (k)) \to (\exists y \in ran seq 1 (+_{𝑒}, F) x < y \leftrightarrow \exists n \in ℕ x < {\sum^{}}_{k = 1}^{n} F (k))$
141	129 140	mpbird	$⊢ ((F : ℕ ⟶ [0, +∞] \land x \in ℝ) \land x < \underset{k \in ℕ}{\sum^{*}} F (k)) \to \exists y \in ran seq 1 (+_{𝑒}, F) x < y$
142	141	ex	$⊢ (F : ℕ ⟶ [0, +∞] \land x \in ℝ) \to (x < \underset{k \in ℕ}{\sum^{*}} F (k) \to \exists y \in ran seq 1 (+_{𝑒}, F) x < y)$
143	142	ralrimiva	$⊢ F : ℕ ⟶ [0, +∞] \to \forall x \in ℝ (x < \underset{k \in ℕ}{\sum^{*}} F (k) \to \exists y \in ran seq 1 (+_{𝑒}, F) x < y)$
144		supxr2	$⊢ ((ran seq 1 (+_{𝑒}, F) \subseteq ℝ^{} \land \underset{k \in ℕ}{\sum^{}} F (k) \in ℝ^{}) \land (\forall x \in ran seq 1 (+_{𝑒}, F) x \leq \underset{k \in ℕ}{\sum^{}} F (k) \land \forall x \in ℝ (x < \underset{k \in ℕ}{\sum^{}} F (k) \to \exists y \in ran seq 1 (+_{𝑒}, F) x < y))) \to sup (ran seq 1 (+_{𝑒}, F) ℝ^{} <) = \underset{k \in ℕ}{\sum^{*}} F (k)$
145	32 39 60 143 144	syl22anc	$⊢ F : ℕ ⟶ [0, +∞] \to sup (ran seq 1 (+_{𝑒}, F) ℝ^{} <) = \underset{k \in ℕ}{\sum^{}} F (k)$
146	145	eqcomd	$⊢ F : ℕ ⟶ [0, +∞] \to \underset{k \in ℕ}{\sum^{}} F (k) = sup (ran seq 1 (+_{𝑒}, F) ℝ^{} <)$

Metamath Proof Explorer

Theorem esumfsup

Proof