esumpcvgval

Description: The value of the extended sum when the corresponding series sum is convergent. (Contributed by Thierry Arnoux, 31-Jul-2017)

	Ref	Expression
Hypotheses	esumpcvgval.1	$⊢ (φ \land k \in ℕ) \to A \in [0, +∞)$
	esumpcvgval.2	$⊢ k = l \to A = B$
	esumpcvgval.3	$⊢ φ \to (n \in ℕ ⟼ \sum_{k = 1}^{n} A) \in dom ⇝$
Assertion	esumpcvgval	$⊢ φ \to \underset{k \in ℕ}{\sum^{*}} A = \sum_{k \in ℕ} A$

Proof

Step	Hyp	Ref	Expression
1		esumpcvgval.1	$⊢ (φ \land k \in ℕ) \to A \in [0, +∞)$
2		esumpcvgval.2	$⊢ k = l \to A = B$
3		esumpcvgval.3	$⊢ φ \to (n \in ℕ ⟼ \sum_{k = 1}^{n} A) \in dom ⇝$
4		xrltso	$⊢ < Or ℝ^{*}$
5	4	a1i	$⊢ φ \to < Or ℝ^{*}$
6		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
7		1zzd	$⊢ φ \to 1 \in ℤ$
8		eqcom	$⊢ k = l \leftrightarrow l = k$
9		eqcom	$⊢ A = B \leftrightarrow B = A$
10	2 8 9	3imtr3i	$⊢ l = k \to B = A$
11	10	cbvmptv	$⊢ (l \in ℕ ⟼ B) = (k \in ℕ ⟼ A)$
12	1 11	fmptd	$⊢ φ \to (l \in ℕ ⟼ B) : ℕ ⟶ [0, +∞)$
13	12	ffvelcdmda	$⊢ (φ \land x \in ℕ) \to (l \in ℕ ⟼ B) (x) \in [0, +∞)$
14		elrege0	$⊢ (l \in ℕ ⟼ B) (x) \in [0, +∞) \leftrightarrow ((l \in ℕ ⟼ B) (x) \in ℝ \land 0 \leq (l \in ℕ ⟼ B) (x))$
15	14	simplbi	$⊢ (l \in ℕ ⟼ B) (x) \in [0, +∞) \to (l \in ℕ ⟼ B) (x) \in ℝ$
16	13 15	syl	$⊢ (φ \land x \in ℕ) \to (l \in ℕ ⟼ B) (x) \in ℝ$
17	6 7 16	serfre	$⊢ φ \to seq 1 (+ (l \in ℕ ⟼ B)) : ℕ ⟶ ℝ$
18	12	adantr	$⊢ (φ \land n \in ℕ) \to (l \in ℕ ⟼ B) : ℕ ⟶ [0, +∞)$
19		simpr	$⊢ (φ \land n \in ℕ) \to n \in ℕ$
20	19	peano2nnd	$⊢ (φ \land n \in ℕ) \to n + 1 \in ℕ$
21	18 20	ffvelcdmd	$⊢ (φ \land n \in ℕ) \to (l \in ℕ ⟼ B) (n + 1) \in [0, +∞)$
22		elrege0	$⊢ (l \in ℕ ⟼ B) (n + 1) \in [0, +∞) \leftrightarrow ((l \in ℕ ⟼ B) (n + 1) \in ℝ \land 0 \leq (l \in ℕ ⟼ B) (n + 1))$
23	22	simprbi	$⊢ (l \in ℕ ⟼ B) (n + 1) \in [0, +∞) \to 0 \leq (l \in ℕ ⟼ B) (n + 1)$
24	21 23	syl	$⊢ (φ \land n \in ℕ) \to 0 \leq (l \in ℕ ⟼ B) (n + 1)$
25	17	ffvelcdmda	$⊢ (φ \land n \in ℕ) \to seq 1 (+ (l \in ℕ ⟼ B)) (n) \in ℝ$
26	22	simplbi	$⊢ (l \in ℕ ⟼ B) (n + 1) \in [0, +∞) \to (l \in ℕ ⟼ B) (n + 1) \in ℝ$
27	21 26	syl	$⊢ (φ \land n \in ℕ) \to (l \in ℕ ⟼ B) (n + 1) \in ℝ$
28	25 27	addge01d	$⊢ (φ \land n \in ℕ) \to (0 \leq (l \in ℕ ⟼ B) (n + 1) \leftrightarrow seq 1 (+ (l \in ℕ ⟼ B)) (n) \leq seq 1 (+ (l \in ℕ ⟼ B)) (n) + (l \in ℕ ⟼ B) (n + 1))$
29	24 28	mpbid	$⊢ (φ \land n \in ℕ) \to seq 1 (+ (l \in ℕ ⟼ B)) (n) \leq seq 1 (+ (l \in ℕ ⟼ B)) (n) + (l \in ℕ ⟼ B) (n + 1)$
30	19 6	eleqtrdi	$⊢ (φ \land n \in ℕ) \to n \in ℤ_{\geq 1}$
31		seqp1	$⊢ n \in ℤ_{\geq 1} \to seq 1 (+ (l \in ℕ ⟼ B)) (n + 1) = seq 1 (+ (l \in ℕ ⟼ B)) (n) + (l \in ℕ ⟼ B) (n + 1)$
32	30 31	syl	$⊢ (φ \land n \in ℕ) \to seq 1 (+ (l \in ℕ ⟼ B)) (n + 1) = seq 1 (+ (l \in ℕ ⟼ B)) (n) + (l \in ℕ ⟼ B) (n + 1)$
33	29 32	breqtrrd	$⊢ (φ \land n \in ℕ) \to seq 1 (+ (l \in ℕ ⟼ B)) (n) \leq seq 1 (+ (l \in ℕ ⟼ B)) (n + 1)$
34		simpr	$⊢ (φ \land k \in ℕ) \to k \in ℕ$
35	11	fvmpt2	$⊢ (k \in ℕ \land A \in [0, +∞)) \to (l \in ℕ ⟼ B) (k) = A$
36	34 1 35	syl2anc	$⊢ (φ \land k \in ℕ) \to (l \in ℕ ⟼ B) (k) = A$
37		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
38	37 1	sselid	$⊢ (φ \land k \in ℕ) \to A \in ℝ$
39	17	feqmptd	$⊢ φ \to seq 1 (+ (l \in ℕ ⟼ B)) = (n \in ℕ ⟼ seq 1 (+ (l \in ℕ ⟼ B)) (n))$
40		simpll	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to φ$
41		elfznn	$⊢ k \in (1 \dots n) \to k \in ℕ$
42	41	adantl	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to k \in ℕ$
43	40 42 36	syl2anc	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to (l \in ℕ ⟼ B) (k) = A$
44	38	recnd	$⊢ (φ \land k \in ℕ) \to A \in ℂ$
45	40 42 44	syl2anc	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to A \in ℂ$
46	43 30 45	fsumser	$⊢ (φ \land n \in ℕ) \to \sum_{k = 1}^{n} A = seq 1 (+ (l \in ℕ ⟼ B)) (n)$
47	46	eqcomd	$⊢ (φ \land n \in ℕ) \to seq 1 (+ (l \in ℕ ⟼ B)) (n) = \sum_{k = 1}^{n} A$
48	47	mpteq2dva	$⊢ φ \to (n \in ℕ ⟼ seq 1 (+ (l \in ℕ ⟼ B)) (n)) = (n \in ℕ ⟼ \sum_{k = 1}^{n} A)$
49	39 48	eqtr2d	$⊢ φ \to (n \in ℕ ⟼ \sum_{k = 1}^{n} A) = seq 1 (+ (l \in ℕ ⟼ B))$
50	49 3	eqeltrrd	$⊢ φ \to seq 1 (+ (l \in ℕ ⟼ B)) \in dom ⇝$
51	6 7 36 38 50	isumrecl	$⊢ φ \to \sum_{k \in ℕ} A \in ℝ$
52		1zzd	$⊢ (φ \land n \in ℕ) \to 1 \in ℤ$
53		fzfid	$⊢ (φ \land n \in ℕ) \to (1 \dots n) \in Fin$
54		fzssuz	$⊢ (1 \dots n) \subseteq ℤ_{\geq 1}$
55	54 6	sseqtrri	$⊢ (1 \dots n) \subseteq ℕ$
56	55	a1i	$⊢ (φ \land n \in ℕ) \to (1 \dots n) \subseteq ℕ$
57	36	adantlr	$⊢ ((φ \land n \in ℕ) \land k \in ℕ) \to (l \in ℕ ⟼ B) (k) = A$
58	38	adantlr	$⊢ ((φ \land n \in ℕ) \land k \in ℕ) \to A \in ℝ$
59	1	adantlr	$⊢ ((φ \land n \in ℕ) \land k \in ℕ) \to A \in [0, +∞)$
60		elrege0	$⊢ A \in [0, +∞) \leftrightarrow (A \in ℝ \land 0 \leq A)$
61	60	simprbi	$⊢ A \in [0, +∞) \to 0 \leq A$
62	59 61	syl	$⊢ ((φ \land n \in ℕ) \land k \in ℕ) \to 0 \leq A$
63	50	adantr	$⊢ (φ \land n \in ℕ) \to seq 1 (+ (l \in ℕ ⟼ B)) \in dom ⇝$
64	6 52 53 56 57 58 62 63	isumless	$⊢ (φ \land n \in ℕ) \to \sum_{k = 1}^{n} A \leq \sum_{k \in ℕ} A$
65	46 64	eqbrtrrd	$⊢ (φ \land n \in ℕ) \to seq 1 (+ (l \in ℕ ⟼ B)) (n) \leq \sum_{k \in ℕ} A$
66	65	ralrimiva	$⊢ φ \to \forall n \in ℕ seq 1 (+ (l \in ℕ ⟼ B)) (n) \leq \sum_{k \in ℕ} A$
67		brralrspcev	$⊢ (\sum_{k \in ℕ} A \in ℝ \land \forall n \in ℕ seq 1 (+ (l \in ℕ ⟼ B)) (n) \leq \sum_{k \in ℕ} A) \to \exists s \in ℝ \forall n \in ℕ seq 1 (+ (l \in ℕ ⟼ B)) (n) \leq s$
68	51 66 67	syl2anc	$⊢ φ \to \exists s \in ℝ \forall n \in ℕ seq 1 (+ (l \in ℕ ⟼ B)) (n) \leq s$
69	6 7 17 33 68	climsup	$⊢ φ \to seq 1 (+ (l \in ℕ ⟼ B)) ⇝ sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <)$
70	6 7 69 25	climrecl	$⊢ φ \to sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <) \in ℝ$
71	70	rexrd	$⊢ φ \to sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <) \in ℝ^{*}$
72		eqid	$⊢ (b \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in b} A) = (b \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in b} A)$
73		sumex	$⊢ \sum_{k \in b} A \in V$
74	72 73	elrnmpti	$⊢ x \in ran (b \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in b} A) \leftrightarrow \exists b \in (𝒫 ℕ \cap Fin) x = \sum_{k \in b} A$
75		ssnnssfz	$⊢ b \in (𝒫 ℕ \cap Fin) \to \exists m \in ℕ b \subseteq (1 \dots m)$
76		fzfid	$⊢ (φ \land b \subseteq (1 \dots m)) \to (1 \dots m) \in Fin$
77		elfznn	$⊢ k \in (1 \dots m) \to k \in ℕ$
78	77 1	sylan2	$⊢ (φ \land k \in (1 \dots m)) \to A \in [0, +∞)$
79	60	simplbi	$⊢ A \in [0, +∞) \to A \in ℝ$
80	78 79	syl	$⊢ (φ \land k \in (1 \dots m)) \to A \in ℝ$
81	80	adantlr	$⊢ ((φ \land b \subseteq (1 \dots m)) \land k \in (1 \dots m)) \to A \in ℝ$
82	78 61	syl	$⊢ (φ \land k \in (1 \dots m)) \to 0 \leq A$
83	82	adantlr	$⊢ ((φ \land b \subseteq (1 \dots m)) \land k \in (1 \dots m)) \to 0 \leq A$
84		simpr	$⊢ (φ \land b \subseteq (1 \dots m)) \to b \subseteq (1 \dots m)$
85	76 81 83 84	fsumless	$⊢ (φ \land b \subseteq (1 \dots m)) \to \sum_{k \in b} A \leq \sum_{k = 1}^{m} A$
86	85	ex	$⊢ φ \to (b \subseteq (1 \dots m) \to \sum_{k \in b} A \leq \sum_{k = 1}^{m} A)$
87	86	reximdv	$⊢ φ \to (\exists m \in ℕ b \subseteq (1 \dots m) \to \exists m \in ℕ \sum_{k \in b} A \leq \sum_{k = 1}^{m} A)$
88	87	imp	$⊢ (φ \land \exists m \in ℕ b \subseteq (1 \dots m)) \to \exists m \in ℕ \sum_{k \in b} A \leq \sum_{k = 1}^{m} A$
89	75 88	sylan2	$⊢ (φ \land b \in (𝒫 ℕ \cap Fin)) \to \exists m \in ℕ \sum_{k \in b} A \leq \sum_{k = 1}^{m} A$
90		breq1	$⊢ x = \sum_{k \in b} A \to (x \leq \sum_{k = 1}^{m} A \leftrightarrow \sum_{k \in b} A \leq \sum_{k = 1}^{m} A)$
91	90	rexbidv	$⊢ x = \sum_{k \in b} A \to (\exists m \in ℕ x \leq \sum_{k = 1}^{m} A \leftrightarrow \exists m \in ℕ \sum_{k \in b} A \leq \sum_{k = 1}^{m} A)$
92	89 91	syl5ibrcom	$⊢ (φ \land b \in (𝒫 ℕ \cap Fin)) \to (x = \sum_{k \in b} A \to \exists m \in ℕ x \leq \sum_{k = 1}^{m} A)$
93	92	rexlimdva	$⊢ φ \to (\exists b \in (𝒫 ℕ \cap Fin) x = \sum_{k \in b} A \to \exists m \in ℕ x \leq \sum_{k = 1}^{m} A)$
94	93	imp	$⊢ (φ \land \exists b \in (𝒫 ℕ \cap Fin) x = \sum_{k \in b} A) \to \exists m \in ℕ x \leq \sum_{k = 1}^{m} A$
95	74 94	sylan2b	$⊢ (φ \land x \in ran (b \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in b} A)) \to \exists m \in ℕ x \leq \sum_{k = 1}^{m} A$
96		simpr	$⊢ ((φ \land b \in (𝒫 ℕ \cap Fin)) \land x = \sum_{k \in b} A) \to x = \sum_{k \in b} A$
97		inss2	$⊢ 𝒫 ℕ \cap Fin \subseteq Fin$
98		simpr	$⊢ (φ \land b \in (𝒫 ℕ \cap Fin)) \to b \in (𝒫 ℕ \cap Fin)$
99	97 98	sselid	$⊢ (φ \land b \in (𝒫 ℕ \cap Fin)) \to b \in Fin$
100		simpll	$⊢ ((φ \land b \in (𝒫 ℕ \cap Fin)) \land k \in b) \to φ$
101		inss1	$⊢ 𝒫 ℕ \cap Fin \subseteq 𝒫 ℕ$
102		simplr	$⊢ ((φ \land b \in (𝒫 ℕ \cap Fin)) \land k \in b) \to b \in (𝒫 ℕ \cap Fin)$
103	101 102	sselid	$⊢ ((φ \land b \in (𝒫 ℕ \cap Fin)) \land k \in b) \to b \in 𝒫 ℕ$
104	103	elpwid	$⊢ ((φ \land b \in (𝒫 ℕ \cap Fin)) \land k \in b) \to b \subseteq ℕ$
105		simpr	$⊢ ((φ \land b \in (𝒫 ℕ \cap Fin)) \land k \in b) \to k \in b$
106	104 105	sseldd	$⊢ ((φ \land b \in (𝒫 ℕ \cap Fin)) \land k \in b) \to k \in ℕ$
107	100 106 1	syl2anc	$⊢ ((φ \land b \in (𝒫 ℕ \cap Fin)) \land k \in b) \to A \in [0, +∞)$
108	107 79	syl	$⊢ ((φ \land b \in (𝒫 ℕ \cap Fin)) \land k \in b) \to A \in ℝ$
109	99 108	fsumrecl	$⊢ (φ \land b \in (𝒫 ℕ \cap Fin)) \to \sum_{k \in b} A \in ℝ$
110	109	adantr	$⊢ ((φ \land b \in (𝒫 ℕ \cap Fin)) \land x = \sum_{k \in b} A) \to \sum_{k \in b} A \in ℝ$
111	96 110	eqeltrd	$⊢ ((φ \land b \in (𝒫 ℕ \cap Fin)) \land x = \sum_{k \in b} A) \to x \in ℝ$
112	111	r19.29an	$⊢ (φ \land \exists b \in (𝒫 ℕ \cap Fin) x = \sum_{k \in b} A) \to x \in ℝ$
113	74 112	sylan2b	$⊢ (φ \land x \in ran (b \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in b} A)) \to x \in ℝ$
114	113	adantr	$⊢ ((φ \land x \in ran (b \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in b} A)) \land (m \in ℕ \land x \leq \sum_{k = 1}^{m} A)) \to x \in ℝ$
115		fzfid	$⊢ φ \to (1 \dots m) \in Fin$
116	115 80	fsumrecl	$⊢ φ \to \sum_{k = 1}^{m} A \in ℝ$
117	116	ad2antrr	$⊢ ((φ \land x \in ran (b \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in b} A)) \land (m \in ℕ \land x \leq \sum_{k = 1}^{m} A)) \to \sum_{k = 1}^{m} A \in ℝ$
118	70	ad2antrr	$⊢ ((φ \land x \in ran (b \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in b} A)) \land (m \in ℕ \land x \leq \sum_{k = 1}^{m} A)) \to sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <) \in ℝ$
119		simprr	$⊢ ((φ \land x \in ran (b \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in b} A)) \land (m \in ℕ \land x \leq \sum_{k = 1}^{m} A)) \to x \leq \sum_{k = 1}^{m} A$
120	17	frnd	$⊢ φ \to ran seq 1 (+ (l \in ℕ ⟼ B)) \subseteq ℝ$
121	120	ad2antrr	$⊢ ((φ \land x \in ran (b \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in b} A)) \land (m \in ℕ \land x \leq \sum_{k = 1}^{m} A)) \to ran seq 1 (+ (l \in ℕ ⟼ B)) \subseteq ℝ$
122		1nn	$⊢ 1 \in ℕ$
123	122	ne0ii	$⊢ ℕ \neq \emptyset$
124		dm0rn0	$⊢ dom seq 1 (+ (l \in ℕ ⟼ B)) = \emptyset \leftrightarrow ran seq 1 (+ (l \in ℕ ⟼ B)) = \emptyset$
125	17	fdmd	$⊢ φ \to dom seq 1 (+ (l \in ℕ ⟼ B)) = ℕ$
126	125	eqeq1d	$⊢ φ \to (dom seq 1 (+ (l \in ℕ ⟼ B)) = \emptyset \leftrightarrow ℕ = \emptyset)$
127	124 126	bitr3id	$⊢ φ \to (ran seq 1 (+ (l \in ℕ ⟼ B)) = \emptyset \leftrightarrow ℕ = \emptyset)$
128	127	necon3bid	$⊢ φ \to (ran seq 1 (+ (l \in ℕ ⟼ B)) \neq \emptyset \leftrightarrow ℕ \neq \emptyset)$
129	123 128	mpbiri	$⊢ φ \to ran seq 1 (+ (l \in ℕ ⟼ B)) \neq \emptyset$
130	129	ad2antrr	$⊢ ((φ \land x \in ran (b \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in b} A)) \land (m \in ℕ \land x \leq \sum_{k = 1}^{m} A)) \to ran seq 1 (+ (l \in ℕ ⟼ B)) \neq \emptyset$
131		1z	$⊢ 1 \in ℤ$
132		seqfn	$⊢ 1 \in ℤ \to seq 1 (+ (l \in ℕ ⟼ B)) Fn ℤ_{\geq 1}$
133	131 132	ax-mp	$⊢ seq 1 (+ (l \in ℕ ⟼ B)) Fn ℤ_{\geq 1}$
134	6	fneq2i	$⊢ seq 1 (+ (l \in ℕ ⟼ B)) Fn ℕ \leftrightarrow seq 1 (+ (l \in ℕ ⟼ B)) Fn ℤ_{\geq 1}$
135	133 134	mpbir	$⊢ seq 1 (+ (l \in ℕ ⟼ B)) Fn ℕ$
136		dffn5	$⊢ seq 1 (+ (l \in ℕ ⟼ B)) Fn ℕ \leftrightarrow seq 1 (+ (l \in ℕ ⟼ B)) = (n \in ℕ ⟼ seq 1 (+ (l \in ℕ ⟼ B)) (n))$
137	135 136	mpbi	$⊢ seq 1 (+ (l \in ℕ ⟼ B)) = (n \in ℕ ⟼ seq 1 (+ (l \in ℕ ⟼ B)) (n))$
138		fvex	$⊢ seq 1 (+ (l \in ℕ ⟼ B)) (n) \in V$
139	137 138	elrnmpti	$⊢ z \in ran seq 1 (+ (l \in ℕ ⟼ B)) \leftrightarrow \exists n \in ℕ z = seq 1 (+ (l \in ℕ ⟼ B)) (n)$
140		r19.29	$⊢ (\forall n \in ℕ seq 1 (+ (l \in ℕ ⟼ B)) (n) \leq s \land \exists n \in ℕ z = seq 1 (+ (l \in ℕ ⟼ B)) (n)) \to \exists n \in ℕ (seq 1 (+ (l \in ℕ ⟼ B)) (n) \leq s \land z = seq 1 (+ (l \in ℕ ⟼ B)) (n))$
141		breq1	$⊢ z = seq 1 (+ (l \in ℕ ⟼ B)) (n) \to (z \leq s \leftrightarrow seq 1 (+ (l \in ℕ ⟼ B)) (n) \leq s)$
142	141	biimparc	$⊢ (seq 1 (+ (l \in ℕ ⟼ B)) (n) \leq s \land z = seq 1 (+ (l \in ℕ ⟼ B)) (n)) \to z \leq s$
143	142	rexlimivw	$⊢ \exists n \in ℕ (seq 1 (+ (l \in ℕ ⟼ B)) (n) \leq s \land z = seq 1 (+ (l \in ℕ ⟼ B)) (n)) \to z \leq s$
144	140 143	syl	$⊢ (\forall n \in ℕ seq 1 (+ (l \in ℕ ⟼ B)) (n) \leq s \land \exists n \in ℕ z = seq 1 (+ (l \in ℕ ⟼ B)) (n)) \to z \leq s$
145	139 144	sylan2b	$⊢ (\forall n \in ℕ seq 1 (+ (l \in ℕ ⟼ B)) (n) \leq s \land z \in ran seq 1 (+ (l \in ℕ ⟼ B))) \to z \leq s$
146	145	ralrimiva	$⊢ \forall n \in ℕ seq 1 (+ (l \in ℕ ⟼ B)) (n) \leq s \to \forall z \in ran seq 1 (+ (l \in ℕ ⟼ B)) z \leq s$
147	146	reximi	$⊢ \exists s \in ℝ \forall n \in ℕ seq 1 (+ (l \in ℕ ⟼ B)) (n) \leq s \to \exists s \in ℝ \forall z \in ran seq 1 (+ (l \in ℕ ⟼ B)) z \leq s$
148	68 147	syl	$⊢ φ \to \exists s \in ℝ \forall z \in ran seq 1 (+ (l \in ℕ ⟼ B)) z \leq s$
149	148	ad2antrr	$⊢ ((φ \land x \in ran (b \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in b} A)) \land (m \in ℕ \land x \leq \sum_{k = 1}^{m} A)) \to \exists s \in ℝ \forall z \in ran seq 1 (+ (l \in ℕ ⟼ B)) z \leq s$
150		simpr	$⊢ (φ \land m \in ℕ) \to m \in ℕ$
151		simpll	$⊢ ((φ \land m \in ℕ) \land k \in (1 \dots m)) \to φ$
152	77	adantl	$⊢ ((φ \land m \in ℕ) \land k \in (1 \dots m)) \to k \in ℕ$
153	151 152 36	syl2anc	$⊢ ((φ \land m \in ℕ) \land k \in (1 \dots m)) \to (l \in ℕ ⟼ B) (k) = A$
154	150 6	eleqtrdi	$⊢ (φ \land m \in ℕ) \to m \in ℤ_{\geq 1}$
155	151 152 1	syl2anc	$⊢ ((φ \land m \in ℕ) \land k \in (1 \dots m)) \to A \in [0, +∞)$
156	155 79	syl	$⊢ ((φ \land m \in ℕ) \land k \in (1 \dots m)) \to A \in ℝ$
157	156	recnd	$⊢ ((φ \land m \in ℕ) \land k \in (1 \dots m)) \to A \in ℂ$
158	153 154 157	fsumser	$⊢ (φ \land m \in ℕ) \to \sum_{k = 1}^{m} A = seq 1 (+ (l \in ℕ ⟼ B)) (m)$
159		fveq2	$⊢ n = m \to seq 1 (+ (l \in ℕ ⟼ B)) (n) = seq 1 (+ (l \in ℕ ⟼ B)) (m)$
160	159	rspceeqv	$⊢ (m \in ℕ \land \sum_{k = 1}^{m} A = seq 1 (+ (l \in ℕ ⟼ B)) (m)) \to \exists n \in ℕ \sum_{k = 1}^{m} A = seq 1 (+ (l \in ℕ ⟼ B)) (n)$
161	150 158 160	syl2anc	$⊢ (φ \land m \in ℕ) \to \exists n \in ℕ \sum_{k = 1}^{m} A = seq 1 (+ (l \in ℕ ⟼ B)) (n)$
162	137 138	elrnmpti	$⊢ \sum_{k = 1}^{m} A \in ran seq 1 (+ (l \in ℕ ⟼ B)) \leftrightarrow \exists n \in ℕ \sum_{k = 1}^{m} A = seq 1 (+ (l \in ℕ ⟼ B)) (n)$
163	161 162	sylibr	$⊢ (φ \land m \in ℕ) \to \sum_{k = 1}^{m} A \in ran seq 1 (+ (l \in ℕ ⟼ B))$
164	163	ad2ant2r	$⊢ ((φ \land x \in ran (b \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in b} A)) \land (m \in ℕ \land x \leq \sum_{k = 1}^{m} A)) \to \sum_{k = 1}^{m} A \in ran seq 1 (+ (l \in ℕ ⟼ B))$
165		suprub	$⊢ ((ran seq 1 (+ (l \in ℕ ⟼ B)) \subseteq ℝ \land ran seq 1 (+ (l \in ℕ ⟼ B)) \neq \emptyset \land \exists s \in ℝ \forall z \in ran seq 1 (+ (l \in ℕ ⟼ B)) z \leq s) \land \sum_{k = 1}^{m} A \in ran seq 1 (+ (l \in ℕ ⟼ B))) \to \sum_{k = 1}^{m} A \leq sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <)$
166	121 130 149 164 165	syl31anc	$⊢ ((φ \land x \in ran (b \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in b} A)) \land (m \in ℕ \land x \leq \sum_{k = 1}^{m} A)) \to \sum_{k = 1}^{m} A \leq sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <)$
167	114 117 118 119 166	letrd	$⊢ ((φ \land x \in ran (b \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in b} A)) \land (m \in ℕ \land x \leq \sum_{k = 1}^{m} A)) \to x \leq sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <)$
168	95 167	rexlimddv	$⊢ (φ \land x \in ran (b \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in b} A)) \to x \leq sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <)$
169	70	adantr	$⊢ (φ \land x \in ran (b \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in b} A)) \to sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <) \in ℝ$
170	113 169	lenltd	$⊢ (φ \land x \in ran (b \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in b} A)) \to (x \leq sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <) \leftrightarrow \neg sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <) < x)$
171	168 170	mpbid	$⊢ (φ \land x \in ran (b \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in b} A)) \to \neg sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <) < x$
172		simpr1r	$⊢ (φ \land ((x \in ℝ^{*} \land x < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <)) \land 0 \leq x \land x = +∞)) \to x < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <)$
173	172	3anassrs	$⊢ (((φ \land (x \in ℝ^{*} \land x < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <))) \land 0 \leq x) \land x = +∞) \to x < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <)$
174	71	ad3antrrr	$⊢ (((φ \land (x \in ℝ^{} \land x < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <))) \land 0 \leq x) \land x = +∞) \to sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <) \in ℝ^{}$
175		pnfnlt	$⊢ sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <) \in ℝ^{*} \to \neg +∞ < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <)$
176	174 175	syl	$⊢ (((φ \land (x \in ℝ^{*} \land x < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <))) \land 0 \leq x) \land x = +∞) \to \neg +∞ < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <)$
177		breq1	$⊢ x = +∞ \to (x < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <) \leftrightarrow +∞ < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <))$
178	177	notbid	$⊢ x = +∞ \to (\neg x < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <) \leftrightarrow \neg +∞ < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <))$
179	178	adantl	$⊢ (((φ \land (x \in ℝ^{*} \land x < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <))) \land 0 \leq x) \land x = +∞) \to (\neg x < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <) \leftrightarrow \neg +∞ < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <))$
180	176 179	mpbird	$⊢ (((φ \land (x \in ℝ^{*} \land x < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <))) \land 0 \leq x) \land x = +∞) \to \neg x < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <)$
181	173 180	pm2.21dd	$⊢ (((φ \land (x \in ℝ^{*} \land x < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <))) \land 0 \leq x) \land x = +∞) \to \exists y \in ran (b \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in b} A) x < y$
182		simplll	$⊢ (((φ \land (x \in ℝ^{*} \land x < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <))) \land 0 \leq x) \land x < +∞) \to φ$
183		simpr1l	$⊢ (φ \land ((x \in ℝ^{} \land x < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <)) \land 0 \leq x \land x < +∞)) \to x \in ℝ^{}$
184	183	3anassrs	$⊢ (((φ \land (x \in ℝ^{} \land x < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <))) \land 0 \leq x) \land x < +∞) \to x \in ℝ^{}$
185		simplr	$⊢ (((φ \land (x \in ℝ^{*} \land x < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <))) \land 0 \leq x) \land x < +∞) \to 0 \leq x$
186		simpr	$⊢ (((φ \land (x \in ℝ^{*} \land x < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <))) \land 0 \leq x) \land x < +∞) \to x < +∞$
187		0xr	$⊢ 0 \in ℝ^{*}$
188		pnfxr	$⊢ +∞ \in ℝ^{*}$
189		elico1	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{}) \to (x \in [0, +∞) \leftrightarrow (x \in ℝ^{*} \land 0 \leq x \land x < +∞))$
190	187 188 189	mp2an	$⊢ x \in [0, +∞) \leftrightarrow (x \in ℝ^{*} \land 0 \leq x \land x < +∞)$
191	184 185 186 190	syl3anbrc	$⊢ (((φ \land (x \in ℝ^{*} \land x < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <))) \land 0 \leq x) \land x < +∞) \to x \in [0, +∞)$
192		simpr1r	$⊢ (φ \land ((x \in ℝ^{*} \land x < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <)) \land 0 \leq x \land x < +∞)) \to x < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <)$
193	192	3anassrs	$⊢ (((φ \land (x \in ℝ^{*} \land x < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <))) \land 0 \leq x) \land x < +∞) \to x < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <)$
194	120	adantr	$⊢ (φ \land (x \in [0, +∞) \land x < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <))) \to ran seq 1 (+ (l \in ℕ ⟼ B)) \subseteq ℝ$
195	129	adantr	$⊢ (φ \land (x \in [0, +∞) \land x < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <))) \to ran seq 1 (+ (l \in ℕ ⟼ B)) \neq \emptyset$
196	148	adantr	$⊢ (φ \land (x \in [0, +∞) \land x < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <))) \to \exists s \in ℝ \forall z \in ran seq 1 (+ (l \in ℕ ⟼ B)) z \leq s$
197	194 195 196	3jca	$⊢ (φ \land (x \in [0, +∞) \land x < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <))) \to (ran seq 1 (+ (l \in ℕ ⟼ B)) \subseteq ℝ \land ran seq 1 (+ (l \in ℕ ⟼ B)) \neq \emptyset \land \exists s \in ℝ \forall z \in ran seq 1 (+ (l \in ℕ ⟼ B)) z \leq s)$
198		simprl	$⊢ (φ \land (x \in [0, +∞) \land x < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <))) \to x \in [0, +∞)$
199	37 198	sselid	$⊢ (φ \land (x \in [0, +∞) \land x < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <))) \to x \in ℝ$
200		simprr	$⊢ (φ \land (x \in [0, +∞) \land x < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <))) \to x < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <)$
201		suprlub	$⊢ ((ran seq 1 (+ (l \in ℕ ⟼ B)) \subseteq ℝ \land ran seq 1 (+ (l \in ℕ ⟼ B)) \neq \emptyset \land \exists s \in ℝ \forall z \in ran seq 1 (+ (l \in ℕ ⟼ B)) z \leq s) \land x \in ℝ) \to (x < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <) \leftrightarrow \exists y \in ran seq 1 (+ (l \in ℕ ⟼ B)) x < y)$
202	201	biimpa	$⊢ (((ran seq 1 (+ (l \in ℕ ⟼ B)) \subseteq ℝ \land ran seq 1 (+ (l \in ℕ ⟼ B)) \neq \emptyset \land \exists s \in ℝ \forall z \in ran seq 1 (+ (l \in ℕ ⟼ B)) z \leq s) \land x \in ℝ) \land x < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <)) \to \exists y \in ran seq 1 (+ (l \in ℕ ⟼ B)) x < y$
203	197 199 200 202	syl21anc	$⊢ (φ \land (x \in [0, +∞) \land x < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <))) \to \exists y \in ran seq 1 (+ (l \in ℕ ⟼ B)) x < y$
204	41	ssriv	$⊢ (1 \dots n) \subseteq ℕ$
205		ovex	$⊢ (1 \dots n) \in V$
206	205	elpw	$⊢ (1 \dots n) \in 𝒫 ℕ \leftrightarrow (1 \dots n) \subseteq ℕ$
207	204 206	mpbir	$⊢ (1 \dots n) \in 𝒫 ℕ$
208		fzfi	$⊢ (1 \dots n) \in Fin$
209		elin	$⊢ (1 \dots n) \in (𝒫 ℕ \cap Fin) \leftrightarrow ((1 \dots n) \in 𝒫 ℕ \land (1 \dots n) \in Fin)$
210	207 208 209	mpbir2an	$⊢ (1 \dots n) \in (𝒫 ℕ \cap Fin)$
211	210	a1i	$⊢ ((φ \land n \in ℕ) \land y = seq 1 (+ (l \in ℕ ⟼ B)) (n)) \to (1 \dots n) \in (𝒫 ℕ \cap Fin)$
212		simpr	$⊢ ((φ \land n \in ℕ) \land y = seq 1 (+ (l \in ℕ ⟼ B)) (n)) \to y = seq 1 (+ (l \in ℕ ⟼ B)) (n)$
213	46	adantr	$⊢ ((φ \land n \in ℕ) \land y = seq 1 (+ (l \in ℕ ⟼ B)) (n)) \to \sum_{k = 1}^{n} A = seq 1 (+ (l \in ℕ ⟼ B)) (n)$
214	212 213	eqtr4d	$⊢ ((φ \land n \in ℕ) \land y = seq 1 (+ (l \in ℕ ⟼ B)) (n)) \to y = \sum_{k = 1}^{n} A$
215		sumeq1	$⊢ b = (1 \dots n) \to \sum_{k \in b} A = \sum_{k = 1}^{n} A$
216	215	rspceeqv	$⊢ ((1 \dots n) \in (𝒫 ℕ \cap Fin) \land y = \sum_{k = 1}^{n} A) \to \exists b \in (𝒫 ℕ \cap Fin) y = \sum_{k \in b} A$
217	211 214 216	syl2anc	$⊢ ((φ \land n \in ℕ) \land y = seq 1 (+ (l \in ℕ ⟼ B)) (n)) \to \exists b \in (𝒫 ℕ \cap Fin) y = \sum_{k \in b} A$
218	217	ex	$⊢ (φ \land n \in ℕ) \to (y = seq 1 (+ (l \in ℕ ⟼ B)) (n) \to \exists b \in (𝒫 ℕ \cap Fin) y = \sum_{k \in b} A)$
219	218	rexlimdva	$⊢ φ \to (\exists n \in ℕ y = seq 1 (+ (l \in ℕ ⟼ B)) (n) \to \exists b \in (𝒫 ℕ \cap Fin) y = \sum_{k \in b} A)$
220	137 138	elrnmpti	$⊢ y \in ran seq 1 (+ (l \in ℕ ⟼ B)) \leftrightarrow \exists n \in ℕ y = seq 1 (+ (l \in ℕ ⟼ B)) (n)$
221	72 73	elrnmpti	$⊢ y \in ran (b \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in b} A) \leftrightarrow \exists b \in (𝒫 ℕ \cap Fin) y = \sum_{k \in b} A$
222	219 220 221	3imtr4g	$⊢ φ \to (y \in ran seq 1 (+ (l \in ℕ ⟼ B)) \to y \in ran (b \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in b} A))$
223	222	ssrdv	$⊢ φ \to ran seq 1 (+ (l \in ℕ ⟼ B)) \subseteq ran (b \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in b} A)$
224		ssrexv	$⊢ ran seq 1 (+ (l \in ℕ ⟼ B)) \subseteq ran (b \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in b} A) \to (\exists y \in ran seq 1 (+ (l \in ℕ ⟼ B)) x < y \to \exists y \in ran (b \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in b} A) x < y)$
225	223 224	syl	$⊢ φ \to (\exists y \in ran seq 1 (+ (l \in ℕ ⟼ B)) x < y \to \exists y \in ran (b \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in b} A) x < y)$
226	225	imp	$⊢ (φ \land \exists y \in ran seq 1 (+ (l \in ℕ ⟼ B)) x < y) \to \exists y \in ran (b \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in b} A) x < y$
227	203 226	syldan	$⊢ (φ \land (x \in [0, +∞) \land x < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <))) \to \exists y \in ran (b \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in b} A) x < y$
228	182 191 193 227	syl12anc	$⊢ (((φ \land (x \in ℝ^{*} \land x < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <))) \land 0 \leq x) \land x < +∞) \to \exists y \in ran (b \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in b} A) x < y$
229		simplrl	$⊢ ((φ \land (x \in ℝ^{} \land x < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <))) \land 0 \leq x) \to x \in ℝ^{}$
230		xrlelttric	$⊢ (+∞ \in ℝ^{} \land x \in ℝ^{}) \to (+∞ \leq x \lor x < +∞)$
231	188 230	mpan	$⊢ x \in ℝ^{*} \to (+∞ \leq x \lor x < +∞)$
232		xgepnf	$⊢ x \in ℝ^{*} \to (+∞ \leq x \leftrightarrow x = +∞)$
233	232	orbi1d	$⊢ x \in ℝ^{*} \to ((+∞ \leq x \lor x < +∞) \leftrightarrow (x = +∞ \lor x < +∞))$
234	231 233	mpbid	$⊢ x \in ℝ^{*} \to (x = +∞ \lor x < +∞)$
235	229 234	syl	$⊢ ((φ \land (x \in ℝ^{*} \land x < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <))) \land 0 \leq x) \to (x = +∞ \lor x < +∞)$
236	181 228 235	mpjaodan	$⊢ ((φ \land (x \in ℝ^{*} \land x < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <))) \land 0 \leq x) \to \exists y \in ran (b \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in b} A) x < y$
237		0elpw	$⊢ \emptyset \in 𝒫 ℕ$
238		0fin	$⊢ \emptyset \in Fin$
239		elin	$⊢ \emptyset \in (𝒫 ℕ \cap Fin) \leftrightarrow (\emptyset \in 𝒫 ℕ \land \emptyset \in Fin)$
240	237 238 239	mpbir2an	$⊢ \emptyset \in (𝒫 ℕ \cap Fin)$
241		sum0	$⊢ \sum_{k \in \emptyset} A = 0$
242	241	eqcomi	$⊢ 0 = \sum_{k \in \emptyset} A$
243		sumeq1	$⊢ b = \emptyset \to \sum_{k \in b} A = \sum_{k \in \emptyset} A$
244	243	rspceeqv	$⊢ (\emptyset \in (𝒫 ℕ \cap Fin) \land 0 = \sum_{k \in \emptyset} A) \to \exists b \in (𝒫 ℕ \cap Fin) 0 = \sum_{k \in b} A$
245	240 242 244	mp2an	$⊢ \exists b \in (𝒫 ℕ \cap Fin) 0 = \sum_{k \in b} A$
246	72 73	elrnmpti	$⊢ 0 \in ran (b \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in b} A) \leftrightarrow \exists b \in (𝒫 ℕ \cap Fin) 0 = \sum_{k \in b} A$
247	245 246	mpbir	$⊢ 0 \in ran (b \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in b} A)$
248		breq2	$⊢ y = 0 \to (x < y \leftrightarrow x < 0)$
249	248	rspcev	$⊢ (0 \in ran (b \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in b} A) \land x < 0) \to \exists y \in ran (b \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in b} A) x < y$
250	247 249	mpan	$⊢ x < 0 \to \exists y \in ran (b \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in b} A) x < y$
251	250	adantl	$⊢ ((φ \land (x \in ℝ^{*} \land x < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <))) \land x < 0) \to \exists y \in ran (b \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in b} A) x < y$
252		xrlelttric	$⊢ (0 \in ℝ^{} \land x \in ℝ^{}) \to (0 \leq x \lor x < 0)$
253	187 252	mpan	$⊢ x \in ℝ^{*} \to (0 \leq x \lor x < 0)$
254	253	ad2antrl	$⊢ (φ \land (x \in ℝ^{*} \land x < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <))) \to (0 \leq x \lor x < 0)$
255	236 251 254	mpjaodan	$⊢ (φ \land (x \in ℝ^{*} \land x < sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <))) \to \exists y \in ran (b \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in b} A) x < y$
256	5 71 171 255	eqsupd	$⊢ φ \to sup (ran (b \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in b} A) ℝ^{*} <) = sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <)$
257		nfv	$⊢ Ⅎ k φ$
258		nfcv	$⊢ \underline{Ⅎ} k ℕ$
259		nnex	$⊢ ℕ \in V$
260	259	a1i	$⊢ φ \to ℕ \in V$
261		icossicc	$⊢ [0, +∞) \subseteq [0, +∞]$
262	261 1	sselid	$⊢ (φ \land k \in ℕ) \to A \in [0, +∞]$
263		elex	$⊢ b \in (𝒫 ℕ \cap Fin) \to b \in V$
264	263	adantl	$⊢ (φ \land b \in (𝒫 ℕ \cap Fin)) \to b \in V$
265	107	fmpttd	$⊢ (φ \land b \in (𝒫 ℕ \cap Fin)) \to (k \in b ⟼ A) : b ⟶ [0, +∞)$
266		esumpfinvallem	$⊢ (b \in V \land (k \in b ⟼ A) : b ⟶ [0, +∞)) \to \underset{k \in b}{\sum_{ℂ_{fld}}} A = \underset{k \in b}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} A$
267	264 265 266	syl2anc	$⊢ (φ \land b \in (𝒫 ℕ \cap Fin)) \to \underset{k \in b}{\sum_{ℂ_{fld}}} A = \underset{k \in b}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} A$
268	108	recnd	$⊢ ((φ \land b \in (𝒫 ℕ \cap Fin)) \land k \in b) \to A \in ℂ$
269	99 268	gsumfsum	$⊢ (φ \land b \in (𝒫 ℕ \cap Fin)) \to \underset{k \in b}{\sum_{ℂ_{fld}}} A = \sum_{k \in b} A$
270	267 269	eqtr3d	$⊢ (φ \land b \in (𝒫 ℕ \cap Fin)) \to \underset{k \in b}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} A = \sum_{k \in b} A$
271	257 258 260 262 270	esumval	$⊢ φ \to \underset{k \in ℕ}{\sum^{}} A = sup (ran (b \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in b} A) ℝ^{} <)$
272	6 7 36 44 69	isumclim	$⊢ φ \to \sum_{k \in ℕ} A = sup (ran seq 1 (+ (l \in ℕ ⟼ B)) ℝ <)$
273	256 271 272	3eqtr4d	$⊢ φ \to \underset{k \in ℕ}{\sum^{*}} A = \sum_{k \in ℕ} A$

Metamath Proof Explorer

Theorem esumpcvgval

Proof