esumcvg

Description: The sequence of partial sums of an extended sum converges to the whole sum. cf. fsumcvg2 . (Contributed by Thierry Arnoux, 5-Sep-2017)

	Ref	Expression
Hypotheses	esumcvg.j	$⊢ J = TopOpen (ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])$
	esumcvg.f	$⊢ F = (n \in ℕ ⟼ {\sum^{*}}_{k = 1}^{n} A)$
	esumcvg.a	$⊢ (φ \land k \in ℕ) \to A \in [0, +∞]$
	esumcvg.m	$⊢ k = m \to A = B$
Assertion	esumcvg	$⊢ φ \to F \underset{t}{⇝} (J) \underset{k \in ℕ}{\sum^{*}} A$

Proof

Step	Hyp	Ref	Expression
1		esumcvg.j	$⊢ J = TopOpen (ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])$
2		esumcvg.f	$⊢ F = (n \in ℕ ⟼ {\sum^{*}}_{k = 1}^{n} A)$
3		esumcvg.a	$⊢ (φ \land k \in ℕ) \to A \in [0, +∞]$
4		esumcvg.m	$⊢ k = m \to A = B$
5		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
6		1zzd	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land F \in dom ⇝) \to 1 \in ℤ$
7		simpr	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land F \in dom ⇝) \to F \in dom ⇝$
8		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
9		ax-resscn	$⊢ ℝ \subseteq ℂ$
10	8 9	sstri	$⊢ [0, +∞) \subseteq ℂ$
11	4	eleq1d	$⊢ k = m \to (A \in [0, +∞) \leftrightarrow B \in [0, +∞))$
12	11	cbvralvw	$⊢ \forall k \in ℕ A \in [0, +∞) \leftrightarrow \forall m \in ℕ B \in [0, +∞)$
13		rsp	$⊢ \forall k \in ℕ A \in [0, +∞) \to (k \in ℕ \to A \in [0, +∞))$
14	12 13	sylbir	$⊢ \forall m \in ℕ B \in [0, +∞) \to (k \in ℕ \to A \in [0, +∞))$
15	14	adantl	$⊢ (φ \land \forall m \in ℕ B \in [0, +∞)) \to (k \in ℕ \to A \in [0, +∞))$
16	15	imp	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land k \in ℕ) \to A \in [0, +∞)$
17	10 16	sseldi	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land k \in ℕ) \to A \in ℂ$
18	17	adantlr	$⊢ (((φ \land \forall m \in ℕ B \in [0, +∞)) \land F \in dom ⇝) \land k \in ℕ) \to A \in ℂ$
19		fzfid	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land n \in ℕ) \to (1 \dots n) \in Fin$
20		elfznn	$⊢ k \in (1 \dots n) \to k \in ℕ$
21	20 16	sylan2	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land k \in (1 \dots n)) \to A \in [0, +∞)$
22	21	adantlr	$⊢ (((φ \land \forall m \in ℕ B \in [0, +∞)) \land n \in ℕ) \land k \in (1 \dots n)) \to A \in [0, +∞)$
23	19 22	esumpfinval	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land n \in ℕ) \to {\sum^{*}}_{k = 1}^{n} A = \sum_{k = 1}^{n} A$
24	23	mpteq2dva	$⊢ (φ \land \forall m \in ℕ B \in [0, +∞)) \to (n \in ℕ ⟼ {\sum^{*}}_{k = 1}^{n} A) = (n \in ℕ ⟼ \sum_{k = 1}^{n} A)$
25	2 24	syl5eq	$⊢ (φ \land \forall m \in ℕ B \in [0, +∞)) \to F = (n \in ℕ ⟼ \sum_{k = 1}^{n} A)$
26	10 22	sseldi	$⊢ (((φ \land \forall m \in ℕ B \in [0, +∞)) \land n \in ℕ) \land k \in (1 \dots n)) \to A \in ℂ$
27	19 26	fsumcl	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land n \in ℕ) \to \sum_{k = 1}^{n} A \in ℂ$
28	25 27	fvmpt2d	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land n \in ℕ) \to F (n) = \sum_{k = 1}^{n} A$
29	28	adantlr	$⊢ (((φ \land \forall m \in ℕ B \in [0, +∞)) \land F \in dom ⇝) \land n \in ℕ) \to F (n) = \sum_{k = 1}^{n} A$
30	5 6 7 18 29	isumclim3	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land F \in dom ⇝) \to F ⇝ \sum_{k \in ℕ} A$
31	19 22	fsumrp0cl	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land n \in ℕ) \to \sum_{k = 1}^{n} A \in [0, +∞)$
32	23 31	eqeltrd	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land n \in ℕ) \to {\sum^{*}}_{k = 1}^{n} A \in [0, +∞)$
33	32 2	fmptd	$⊢ (φ \land \forall m \in ℕ B \in [0, +∞)) \to F : ℕ ⟶ [0, +∞)$
34	33	adantr	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land F \in dom ⇝) \to F : ℕ ⟶ [0, +∞)$
35		simplll	$⊢ (((φ \land \forall m \in ℕ B \in [0, +∞)) \land F \in dom ⇝) \land k \in ℕ) \to φ$
36		eqidd	$⊢ (φ \land k \in ℕ) \to (m \in ℕ ⟼ B) = (m \in ℕ ⟼ B)$
37		eqcom	$⊢ k = m \leftrightarrow m = k$
38		eqcom	$⊢ A = B \leftrightarrow B = A$
39	4 37 38	3imtr3i	$⊢ m = k \to B = A$
40	39	adantl	$⊢ ((φ \land k \in ℕ) \land m = k) \to B = A$
41		simpr	$⊢ (φ \land k \in ℕ) \to k \in ℕ$
42	36 40 41 3	fvmptd	$⊢ (φ \land k \in ℕ) \to (m \in ℕ ⟼ B) (k) = A$
43	35 42	sylancom	$⊢ (((φ \land \forall m \in ℕ B \in [0, +∞)) \land F \in dom ⇝) \land k \in ℕ) \to (m \in ℕ ⟼ B) (k) = A$
44	16	adantlr	$⊢ (((φ \land \forall m \in ℕ B \in [0, +∞)) \land F \in dom ⇝) \land k \in ℕ) \to A \in [0, +∞)$
45		elrege0	$⊢ A \in [0, +∞) \leftrightarrow (A \in ℝ \land 0 \leq A)$
46	44 45	sylib	$⊢ (((φ \land \forall m \in ℕ B \in [0, +∞)) \land F \in dom ⇝) \land k \in ℕ) \to (A \in ℝ \land 0 \leq A)$
47	46	simpld	$⊢ (((φ \land \forall m \in ℕ B \in [0, +∞)) \land F \in dom ⇝) \land k \in ℕ) \to A \in ℝ$
48		ovex	$⊢ (1 \dots n) \in V$
49		simpll	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to φ$
50	20	adantl	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to k \in ℕ$
51	49 50 3	syl2anc	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to A \in [0, +∞]$
52	51	ralrimiva	$⊢ (φ \land n \in ℕ) \to \forall k \in (1 \dots n) A \in [0, +∞]$
53		nfcv	$⊢ \underline{Ⅎ} k (1 \dots n)$
54	53	esumcl	$⊢ ((1 \dots n) \in V \land \forall k \in (1 \dots n) A \in [0, +∞]) \to {\sum^{*}}_{k = 1}^{n} A \in [0, +∞]$
55	48 52 54	sylancr	$⊢ (φ \land n \in ℕ) \to {\sum^{*}}_{k = 1}^{n} A \in [0, +∞]$
56	55 2	fmptd	$⊢ φ \to F : ℕ ⟶ [0, +∞]$
57	56	ffnd	$⊢ φ \to F Fn ℕ$
58	57	adantr	$⊢ (φ \land \forall m \in ℕ B \in [0, +∞)) \to F Fn ℕ$
59		1z	$⊢ 1 \in ℤ$
60		seqfn	$⊢ 1 \in ℤ \to seq 1 (+ (m \in ℕ ⟼ B)) Fn ℤ_{\geq 1}$
61	59 60	ax-mp	$⊢ seq 1 (+ (m \in ℕ ⟼ B)) Fn ℤ_{\geq 1}$
62	5	fneq2i	$⊢ seq 1 (+ (m \in ℕ ⟼ B)) Fn ℕ \leftrightarrow seq 1 (+ (m \in ℕ ⟼ B)) Fn ℤ_{\geq 1}$
63	61 62	mpbir	$⊢ seq 1 (+ (m \in ℕ ⟼ B)) Fn ℕ$
64	63	a1i	$⊢ (φ \land \forall m \in ℕ B \in [0, +∞)) \to seq 1 (+ (m \in ℕ ⟼ B)) Fn ℕ$
65		simplll	$⊢ (((φ \land \forall m \in ℕ B \in [0, +∞)) \land n \in ℕ) \land k \in (1 \dots n)) \to φ$
66	20 42	sylan2	$⊢ (φ \land k \in (1 \dots n)) \to (m \in ℕ ⟼ B) (k) = A$
67	65 66	sylancom	$⊢ (((φ \land \forall m \in ℕ B \in [0, +∞)) \land n \in ℕ) \land k \in (1 \dots n)) \to (m \in ℕ ⟼ B) (k) = A$
68		simpr	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land n \in ℕ) \to n \in ℕ$
69	68 5	eleqtrdi	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land n \in ℕ) \to n \in ℤ_{\geq 1}$
70	67 69 26	fsumser	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land n \in ℕ) \to \sum_{k = 1}^{n} A = seq 1 (+ (m \in ℕ ⟼ B)) (n)$
71	28 70	eqtrd	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land n \in ℕ) \to F (n) = seq 1 (+ (m \in ℕ ⟼ B)) (n)$
72	58 64 71	eqfnfvd	$⊢ (φ \land \forall m \in ℕ B \in [0, +∞)) \to F = seq 1 (+ (m \in ℕ ⟼ B))$
73	72	adantr	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land F \in dom ⇝) \to F = seq 1 (+ (m \in ℕ ⟼ B))$
74	73 7	eqeltrrd	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land F \in dom ⇝) \to seq 1 (+ (m \in ℕ ⟼ B)) \in dom ⇝$
75	5 6 43 47 74	isumrecl	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land F \in dom ⇝) \to \sum_{k \in ℕ} A \in ℝ$
76	46	simprd	$⊢ (((φ \land \forall m \in ℕ B \in [0, +∞)) \land F \in dom ⇝) \land k \in ℕ) \to 0 \leq A$
77	5 6 43 47 74 76	isumge0	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land F \in dom ⇝) \to 0 \leq \sum_{k \in ℕ} A$
78		elrege0	$⊢ \sum_{k \in ℕ} A \in [0, +∞) \leftrightarrow (\sum_{k \in ℕ} A \in ℝ \land 0 \leq \sum_{k \in ℕ} A)$
79	75 77 78	sylanbrc	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land F \in dom ⇝) \to \sum_{k \in ℕ} A \in [0, +∞)$
80		ssid	$⊢ [0, +∞) \subseteq [0, +∞)$
81	1 34 79 80	lmlimxrge0	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land F \in dom ⇝) \to (F \underset{t}{⇝} (J) \sum_{k \in ℕ} A \leftrightarrow F ⇝ \sum_{k \in ℕ} A)$
82	30 81	mpbird	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land F \in dom ⇝) \to F \underset{t}{⇝} (J) \sum_{k \in ℕ} A$
83	2 7	eqeltrrid	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land F \in dom ⇝) \to (n \in ℕ ⟼ {\sum^{*}}_{k = 1}^{n} A) \in dom ⇝$
84	24	eleq1d	$⊢ (φ \land \forall m \in ℕ B \in [0, +∞)) \to ((n \in ℕ ⟼ {\sum^{*}}_{k = 1}^{n} A) \in dom ⇝ \leftrightarrow (n \in ℕ ⟼ \sum_{k = 1}^{n} A) \in dom ⇝)$
85	84	adantr	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land F \in dom ⇝) \to ((n \in ℕ ⟼ {\sum^{*}}_{k = 1}^{n} A) \in dom ⇝ \leftrightarrow (n \in ℕ ⟼ \sum_{k = 1}^{n} A) \in dom ⇝)$
86	83 85	mpbid	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land F \in dom ⇝) \to (n \in ℕ ⟼ \sum_{k = 1}^{n} A) \in dom ⇝$
87	44 4 86	esumpcvgval	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land F \in dom ⇝) \to \underset{k \in ℕ}{\sum^{*}} A = \sum_{k \in ℕ} A$
88	82 87	breqtrrd	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land F \in dom ⇝) \to F \underset{t}{⇝} (J) \underset{k \in ℕ}{\sum^{*}} A$
89	33	adantr	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \to F : ℕ ⟶ [0, +∞)$
90		simpr	$⊢ (((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land n \in ℕ) \to n \in ℕ$
91	90	nnzd	$⊢ (((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land n \in ℕ) \to n \in ℤ$
92		uzid	$⊢ n \in ℤ \to n \in ℤ_{\geq n}$
93		peano2uz	$⊢ n \in ℤ_{\geq n} \to n + 1 \in ℤ_{\geq n}$
94	91 92 93	3syl	$⊢ (((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land n \in ℕ) \to n + 1 \in ℤ_{\geq n}$
95		simplll	$⊢ ((((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land n \in ℕ) \land k \in ℕ) \to (φ \land \forall m \in ℕ B \in [0, +∞))$
96	95 16	sylancom	$⊢ ((((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land n \in ℕ) \land k \in ℕ) \to A \in [0, +∞)$
97	90 94 96	esumpmono	$⊢ (((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land n \in ℕ) \to {\sum^{}}_{k = 1}^{n} A \leq {\sum^{}}_{k = 1}^{n + 1} A$
98	28 23	eqtr4d	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land n \in ℕ) \to F (n) = {\sum^{*}}_{k = 1}^{n} A$
99	98	adantlr	$⊢ (((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land n \in ℕ) \to F (n) = {\sum^{*}}_{k = 1}^{n} A$
100		oveq2	$⊢ l = n \to (1 \dots l) = (1 \dots n)$
101		esumeq1	$⊢ (1 \dots l) = (1 \dots n) \to {\sum^{}}_{k = 1}^{l} A = {\sum^{}}_{k = 1}^{n} A$
102	100 101	syl	$⊢ l = n \to {\sum^{}}_{k = 1}^{l} A = {\sum^{}}_{k = 1}^{n} A$
103	102	cbvmptv	$⊢ (l \in ℕ ⟼ {\sum^{}}_{k = 1}^{l} A) = (n \in ℕ ⟼ {\sum^{}}_{k = 1}^{n} A)$
104	2 103	eqtr4i	$⊢ F = (l \in ℕ ⟼ {\sum^{*}}_{k = 1}^{l} A)$
105	104	a1i	$⊢ (((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land n \in ℕ) \to F = (l \in ℕ ⟼ {\sum^{*}}_{k = 1}^{l} A)$
106		simpr3	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land (\neg F \in dom ⇝ \land n \in ℕ \land l = n + 1)) \to l = n + 1$
107		oveq2	$⊢ l = n + 1 \to (1 \dots l) = (1 \dots n + 1)$
108		esumeq1	$⊢ (1 \dots l) = (1 \dots n + 1) \to {\sum^{}}_{k = 1}^{l} A = {\sum^{}}_{k = 1}^{n + 1} A$
109	106 107 108	3syl	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land (\neg F \in dom ⇝ \land n \in ℕ \land l = n + 1)) \to {\sum^{}}_{k = 1}^{l} A = {\sum^{}}_{k = 1}^{n + 1} A$
110	109	3anassrs	$⊢ ((((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land n \in ℕ) \land l = n + 1) \to {\sum^{}}_{k = 1}^{l} A = {\sum^{}}_{k = 1}^{n + 1} A$
111	90	peano2nnd	$⊢ (((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land n \in ℕ) \to n + 1 \in ℕ$
112		ovex	$⊢ (1 \dots n + 1) \in V$
113		simp-4l	$⊢ ((((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land n \in ℕ) \land k \in (1 \dots n + 1)) \to φ$
114		elfznn	$⊢ k \in (1 \dots n + 1) \to k \in ℕ$
115	114	adantl	$⊢ ((((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land n \in ℕ) \land k \in (1 \dots n + 1)) \to k \in ℕ$
116	113 115 3	syl2anc	$⊢ ((((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land n \in ℕ) \land k \in (1 \dots n + 1)) \to A \in [0, +∞]$
117	116	ralrimiva	$⊢ (((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land n \in ℕ) \to \forall k \in (1 \dots n + 1) A \in [0, +∞]$
118		nfcv	$⊢ \underline{Ⅎ} k (1 \dots n + 1)$
119	118	esumcl	$⊢ ((1 \dots n + 1) \in V \land \forall k \in (1 \dots n + 1) A \in [0, +∞]) \to {\sum^{*}}_{k = 1}^{n + 1} A \in [0, +∞]$
120	112 117 119	sylancr	$⊢ (((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land n \in ℕ) \to {\sum^{*}}_{k = 1}^{n + 1} A \in [0, +∞]$
121	105 110 111 120	fvmptd	$⊢ (((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land n \in ℕ) \to F (n + 1) = {\sum^{*}}_{k = 1}^{n + 1} A$
122	97 99 121	3brtr4d	$⊢ (((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land n \in ℕ) \to F (n) \leq F (n + 1)$
123		simpr	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \to \neg F \in dom ⇝$
124	1 89 122 123	lmdvglim	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \to F \underset{t}{⇝} (J) +∞$
125		nfv	$⊢ Ⅎ k (φ \land \forall m \in ℕ B \in [0, +∞))$
126		nfcv	$⊢ \underline{Ⅎ} k ℕ$
127		nnex	$⊢ ℕ \in V$
128	127	a1i	$⊢ (φ \land \forall m \in ℕ B \in [0, +∞)) \to ℕ \in V$
129	3	adantlr	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land k \in ℕ) \to A \in [0, +∞]$
130		simpr	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land x \in (𝒫 ℕ \cap Fin)) \to x \in (𝒫 ℕ \cap Fin)$
131		simpll	$⊢ (((φ \land \forall m \in ℕ B \in [0, +∞)) \land x \in (𝒫 ℕ \cap Fin)) \land k \in x) \to (φ \land \forall m \in ℕ B \in [0, +∞))$
132		inss1	$⊢ 𝒫 ℕ \cap Fin \subseteq 𝒫 ℕ$
133		simplr	$⊢ (((φ \land \forall m \in ℕ B \in [0, +∞)) \land x \in (𝒫 ℕ \cap Fin)) \land k \in x) \to x \in (𝒫 ℕ \cap Fin)$
134	132 133	sseldi	$⊢ (((φ \land \forall m \in ℕ B \in [0, +∞)) \land x \in (𝒫 ℕ \cap Fin)) \land k \in x) \to x \in 𝒫 ℕ$
135	134	elpwid	$⊢ (((φ \land \forall m \in ℕ B \in [0, +∞)) \land x \in (𝒫 ℕ \cap Fin)) \land k \in x) \to x \subseteq ℕ$
136		simpr	$⊢ (((φ \land \forall m \in ℕ B \in [0, +∞)) \land x \in (𝒫 ℕ \cap Fin)) \land k \in x) \to k \in x$
137	135 136	sseldd	$⊢ (((φ \land \forall m \in ℕ B \in [0, +∞)) \land x \in (𝒫 ℕ \cap Fin)) \land k \in x) \to k \in ℕ$
138	131 137 16	syl2anc	$⊢ (((φ \land \forall m \in ℕ B \in [0, +∞)) \land x \in (𝒫 ℕ \cap Fin)) \land k \in x) \to A \in [0, +∞)$
139	138	fmpttd	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land x \in (𝒫 ℕ \cap Fin)) \to (k \in x ⟼ A) : x ⟶ [0, +∞)$
140		esumpfinvallem	$⊢ (x \in (𝒫 ℕ \cap Fin) \land (k \in x ⟼ A) : x ⟶ [0, +∞)) \to \underset{k \in x}{\sum_{ℂ_{fld}}} A = \underset{k \in x}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} A$
141	130 139 140	syl2anc	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land x \in (𝒫 ℕ \cap Fin)) \to \underset{k \in x}{\sum_{ℂ_{fld}}} A = \underset{k \in x}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} A$
142		inss2	$⊢ 𝒫 ℕ \cap Fin \subseteq Fin$
143	142 130	sseldi	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land x \in (𝒫 ℕ \cap Fin)) \to x \in Fin$
144	131 137 17	syl2anc	$⊢ (((φ \land \forall m \in ℕ B \in [0, +∞)) \land x \in (𝒫 ℕ \cap Fin)) \land k \in x) \to A \in ℂ$
145	143 144	gsumfsum	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land x \in (𝒫 ℕ \cap Fin)) \to \underset{k \in x}{\sum_{ℂ_{fld}}} A = \sum_{k \in x} A$
146	141 145	eqtr3d	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land x \in (𝒫 ℕ \cap Fin)) \to \underset{k \in x}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} A = \sum_{k \in x} A$
147	125 126 128 129 146	esumval	$⊢ (φ \land \forall m \in ℕ B \in [0, +∞)) \to \underset{k \in ℕ}{\sum^{}} A = sup (ran (x \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in x} A) ℝ^{} <)$
148	147	adantr	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \to \underset{k \in ℕ}{\sum^{}} A = sup (ran (x \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in x} A) ℝ^{} <)$
149	89 122 123	lmdvg	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \to \forall y \in ℝ \exists l \in ℕ \forall n \in ℤ_{\geq l} y < F (n)$
150	149	r19.21bi	$⊢ (((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land y \in ℝ) \to \exists l \in ℕ \forall n \in ℤ_{\geq l} y < F (n)$
151		nnz	$⊢ l \in ℕ \to l \in ℤ$
152		uzid	$⊢ l \in ℤ \to l \in ℤ_{\geq l}$
153	151 152	syl	$⊢ l \in ℕ \to l \in ℤ_{\geq l}$
154		simpr	$⊢ (l \in ℕ \land n = l) \to n = l$
155	154	fveq2d	$⊢ (l \in ℕ \land n = l) \to F (n) = F (l)$
156	155	breq2d	$⊢ (l \in ℕ \land n = l) \to (y < F (n) \leftrightarrow y < F (l))$
157	153 156	rspcdv	$⊢ l \in ℕ \to (\forall n \in ℤ_{\geq l} y < F (n) \to y < F (l))$
158	157	reximia	$⊢ \exists l \in ℕ \forall n \in ℤ_{\geq l} y < F (n) \to \exists l \in ℕ y < F (l)$
159	150 158	syl	$⊢ (((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land y \in ℝ) \to \exists l \in ℕ y < F (l)$
160		simplr	$⊢ ((((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land y \in ℝ) \land l \in ℕ) \to y \in ℝ$
161	89	ad2antrr	$⊢ ((((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land y \in ℝ) \land l \in ℕ) \to F : ℕ ⟶ [0, +∞)$
162		simpr	$⊢ ((((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land y \in ℝ) \land l \in ℕ) \to l \in ℕ$
163	161 162	ffvelrnd	$⊢ ((((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land y \in ℝ) \land l \in ℕ) \to F (l) \in [0, +∞)$
164	8 163	sseldi	$⊢ ((((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land y \in ℝ) \land l \in ℕ) \to F (l) \in ℝ$
165		ltle	$⊢ (y \in ℝ \land F (l) \in ℝ) \to (y < F (l) \to y \leq F (l))$
166	160 164 165	syl2anc	$⊢ ((((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land y \in ℝ) \land l \in ℕ) \to (y < F (l) \to y \leq F (l))$
167		oveq2	$⊢ n = l \to (1 \dots n) = (1 \dots l)$
168		esumeq1	$⊢ (1 \dots n) = (1 \dots l) \to {\sum^{}}_{k = 1}^{n} A = {\sum^{}}_{k = 1}^{l} A$
169	167 168	syl	$⊢ n = l \to {\sum^{}}_{k = 1}^{n} A = {\sum^{}}_{k = 1}^{l} A$
170		esumex	$⊢ {\sum^{*}}_{k = 1}^{l} A \in V$
171	170	a1i	$⊢ ((((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land y \in ℝ) \land l \in ℕ) \to {\sum^{*}}_{k = 1}^{l} A \in V$
172	2 169 162 171	fvmptd3	$⊢ ((((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land y \in ℝ) \land l \in ℕ) \to F (l) = {\sum^{*}}_{k = 1}^{l} A$
173		fzfid	$⊢ ((((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land y \in ℝ) \land l \in ℕ) \to (1 \dots l) \in Fin$
174		simp-4l	$⊢ (((((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land y \in ℝ) \land l \in ℕ) \land k \in (1 \dots l)) \to (φ \land \forall m \in ℕ B \in [0, +∞))$
175		elfznn	$⊢ k \in (1 \dots l) \to k \in ℕ$
176	175	adantl	$⊢ (((((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land y \in ℝ) \land l \in ℕ) \land k \in (1 \dots l)) \to k \in ℕ$
177	174 176 16	syl2anc	$⊢ (((((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land y \in ℝ) \land l \in ℕ) \land k \in (1 \dots l)) \to A \in [0, +∞)$
178	173 177	esumpfinval	$⊢ ((((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land y \in ℝ) \land l \in ℕ) \to {\sum^{*}}_{k = 1}^{l} A = \sum_{k = 1}^{l} A$
179	172 178	eqtrd	$⊢ ((((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land y \in ℝ) \land l \in ℕ) \to F (l) = \sum_{k = 1}^{l} A$
180	179	breq2d	$⊢ ((((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land y \in ℝ) \land l \in ℕ) \to (y \leq F (l) \leftrightarrow y \leq \sum_{k = 1}^{l} A)$
181	166 180	sylibd	$⊢ ((((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land y \in ℝ) \land l \in ℕ) \to (y < F (l) \to y \leq \sum_{k = 1}^{l} A)$
182	181	reximdva	$⊢ (((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land y \in ℝ) \to (\exists l \in ℕ y < F (l) \to \exists l \in ℕ y \leq \sum_{k = 1}^{l} A)$
183	159 182	mpd	$⊢ (((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land y \in ℝ) \to \exists l \in ℕ y \leq \sum_{k = 1}^{l} A$
184		fzssuz	$⊢ (1 \dots l) \subseteq ℤ_{\geq 1}$
185	184 5	sseqtrri	$⊢ (1 \dots l) \subseteq ℕ$
186		ovex	$⊢ (1 \dots l) \in V$
187	186	elpw	$⊢ (1 \dots l) \in 𝒫 ℕ \leftrightarrow (1 \dots l) \subseteq ℕ$
188	185 187	mpbir	$⊢ (1 \dots l) \in 𝒫 ℕ$
189		fzfi	$⊢ (1 \dots l) \in Fin$
190		elin	$⊢ (1 \dots l) \in (𝒫 ℕ \cap Fin) \leftrightarrow ((1 \dots l) \in 𝒫 ℕ \land (1 \dots l) \in Fin)$
191	188 189 190	mpbir2an	$⊢ (1 \dots l) \in (𝒫 ℕ \cap Fin)$
192		sumex	$⊢ \sum_{k = 1}^{l} A \in V$
193		eqid	$⊢ (x \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in x} A) = (x \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in x} A)$
194		sumeq1	$⊢ x = (1 \dots l) \to \sum_{k \in x} A = \sum_{k = 1}^{l} A$
195	193 194	elrnmpt1s	$⊢ ((1 \dots l) \in (𝒫 ℕ \cap Fin) \land \sum_{k = 1}^{l} A \in V) \to \sum_{k = 1}^{l} A \in ran (x \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in x} A)$
196	191 192 195	mp2an	$⊢ \sum_{k = 1}^{l} A \in ran (x \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in x} A)$
197		nfv	$⊢ Ⅎ z y \leq \sum_{k = 1}^{l} A$
198		breq2	$⊢ z = \sum_{k = 1}^{l} A \to (y \leq z \leftrightarrow y \leq \sum_{k = 1}^{l} A)$
199	197 198	rspce	$⊢ (\sum_{k = 1}^{l} A \in ran (x \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in x} A) \land y \leq \sum_{k = 1}^{l} A) \to \exists z \in ran (x \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in x} A) y \leq z$
200	196 199	mpan	$⊢ y \leq \sum_{k = 1}^{l} A \to \exists z \in ran (x \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in x} A) y \leq z$
201	200	rexlimivw	$⊢ \exists l \in ℕ y \leq \sum_{k = 1}^{l} A \to \exists z \in ran (x \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in x} A) y \leq z$
202	183 201	syl	$⊢ (((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land y \in ℝ) \to \exists z \in ran (x \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in x} A) y \leq z$
203	202	ralrimiva	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \to \forall y \in ℝ \exists z \in ran (x \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in x} A) y \leq z$
204		simpr	$⊢ (((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land x \in (𝒫 ℕ \cap Fin)) \to x \in (𝒫 ℕ \cap Fin)$
205	142 204	sseldi	$⊢ (((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land x \in (𝒫 ℕ \cap Fin)) \to x \in Fin$
206	138	adantllr	$⊢ ((((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land x \in (𝒫 ℕ \cap Fin)) \land k \in x) \to A \in [0, +∞)$
207	8 206	sseldi	$⊢ ((((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land x \in (𝒫 ℕ \cap Fin)) \land k \in x) \to A \in ℝ$
208	205 207	fsumrecl	$⊢ (((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land x \in (𝒫 ℕ \cap Fin)) \to \sum_{k \in x} A \in ℝ$
209	208	rexrd	$⊢ (((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \land x \in (𝒫 ℕ \cap Fin)) \to \sum_{k \in x} A \in ℝ^{*}$
210	209	fmpttd	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \to (x \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in x} A) : 𝒫 ℕ \cap Fin ⟶ ℝ^{*}$
211		frn	$⊢ (x \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in x} A) : 𝒫 ℕ \cap Fin ⟶ ℝ^{} \to ran (x \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in x} A) \subseteq ℝ^{}$
212		supxrunb1	$⊢ ran (x \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in x} A) \subseteq ℝ^{} \to (\forall y \in ℝ \exists z \in ran (x \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in x} A) y \leq z \leftrightarrow sup (ran (x \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in x} A) ℝ^{} <) = +∞)$
213	210 211 212	3syl	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \to (\forall y \in ℝ \exists z \in ran (x \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in x} A) y \leq z \leftrightarrow sup (ran (x \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in x} A) ℝ^{*} <) = +∞)$
214	203 213	mpbid	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \to sup (ran (x \in (𝒫 ℕ \cap Fin) ⟼ \sum_{k \in x} A) ℝ^{*} <) = +∞$
215	148 214	eqtrd	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \to \underset{k \in ℕ}{\sum^{*}} A = +∞$
216	124 215	breqtrrd	$⊢ ((φ \land \forall m \in ℕ B \in [0, +∞)) \land \neg F \in dom ⇝) \to F \underset{t}{⇝} (J) \underset{k \in ℕ}{\sum^{*}} A$
217	88 216	pm2.61dan	$⊢ (φ \land \forall m \in ℕ B \in [0, +∞)) \to F \underset{t}{⇝} (J) \underset{k \in ℕ}{\sum^{*}} A$
218	2	reseq1i	$⊢ {F ↾}_{ℤ_{\geq k}} = {(n \in ℕ ⟼ {\sum^{*}}_{k = 1}^{n} A) ↾}_{ℤ_{\geq k}}$
219		eleq1w	$⊢ l = k \to (l \in ℕ \leftrightarrow k \in ℕ)$
220	219	anbi2d	$⊢ l = k \to ((φ \land l \in ℕ) \leftrightarrow (φ \land k \in ℕ))$
221		sbequ12r	$⊢ l = k \to ([l/ k] A = +∞ \leftrightarrow A = +∞)$
222	220 221	anbi12d	$⊢ l = k \to (((φ \land l \in ℕ) \land [l/ k] A = +∞) \leftrightarrow ((φ \land k \in ℕ) \land A = +∞))$
223		fveq2	$⊢ l = k \to ℤ_{\geq l} = ℤ_{\geq k}$
224	223	reseq2d	$⊢ l = k \to {(n \in ℕ ⟼ {\sum^{}}_{k = 1}^{n} A) ↾}_{ℤ_{\geq l}} = {(n \in ℕ ⟼ {\sum^{}}_{k = 1}^{n} A) ↾}_{ℤ_{\geq k}}$
225	223	xpeq1d	$⊢ l = k \to ℤ_{\geq l} \times \{+∞\} = ℤ_{\geq k} \times \{+∞\}$
226	224 225	eqeq12d	$⊢ l = k \to ({(n \in ℕ ⟼ {\sum^{}}_{k = 1}^{n} A) ↾}_{ℤ_{\geq l}} = ℤ_{\geq l} \times \{+∞\} \leftrightarrow {(n \in ℕ ⟼ {\sum^{}}_{k = 1}^{n} A) ↾}_{ℤ_{\geq k}} = ℤ_{\geq k} \times \{+∞\})$
227	222 226	imbi12d	$⊢ l = k \to ((((φ \land l \in ℕ) \land [l/ k] A = +∞) \to {(n \in ℕ ⟼ {\sum^{}}_{k = 1}^{n} A) ↾}_{ℤ_{\geq l}} = ℤ_{\geq l} \times \{+∞\}) \leftrightarrow (((φ \land k \in ℕ) \land A = +∞) \to {(n \in ℕ ⟼ {\sum^{}}_{k = 1}^{n} A) ↾}_{ℤ_{\geq k}} = ℤ_{\geq k} \times \{+∞\}))$
228		nfv	$⊢ Ⅎ k (φ \land l \in ℕ)$
229		nfs1v	$⊢ Ⅎ k [l/ k] A = +∞$
230	228 229	nfan	$⊢ Ⅎ k ((φ \land l \in ℕ) \land [l/ k] A = +∞)$
231		nfv	$⊢ Ⅎ k n \in ℤ_{\geq l}$
232	230 231	nfan	$⊢ Ⅎ k (((φ \land l \in ℕ) \land [l/ k] A = +∞) \land n \in ℤ_{\geq l})$
233		ovexd	$⊢ (((φ \land l \in ℕ) \land [l/ k] A = +∞) \land n \in ℤ_{\geq l}) \to (1 \dots n) \in V$
234		simp-4l	$⊢ ((((φ \land l \in ℕ) \land [l/ k] A = +∞) \land n \in ℤ_{\geq l}) \land k \in (1 \dots n)) \to φ$
235	20	adantl	$⊢ ((((φ \land l \in ℕ) \land [l/ k] A = +∞) \land n \in ℤ_{\geq l}) \land k \in (1 \dots n)) \to k \in ℕ$
236	234 235 3	syl2anc	$⊢ ((((φ \land l \in ℕ) \land [l/ k] A = +∞) \land n \in ℤ_{\geq l}) \land k \in (1 \dots n)) \to A \in [0, +∞]$
237		simpllr	$⊢ (((φ \land l \in ℕ) \land [l/ k] A = +∞) \land n \in ℤ_{\geq l}) \to l \in ℕ$
238		elnnuz	$⊢ l \in ℕ \leftrightarrow l \in ℤ_{\geq 1}$
239		eluzfz	$⊢ (l \in ℤ_{\geq 1} \land n \in ℤ_{\geq l}) \to l \in (1 \dots n)$
240	238 239	sylanb	$⊢ (l \in ℕ \land n \in ℤ_{\geq l}) \to l \in (1 \dots n)$
241	237 240	sylancom	$⊢ (((φ \land l \in ℕ) \land [l/ k] A = +∞) \land n \in ℤ_{\geq l}) \to l \in (1 \dots n)$
242		simplr	$⊢ (((φ \land l \in ℕ) \land [l/ k] A = +∞) \land n \in ℤ_{\geq l}) \to [l/ k] A = +∞$
243		sbequ12	$⊢ k = l \to (A = +∞ \leftrightarrow [l/ k] A = +∞)$
244	229 243	rspce	$⊢ (l \in (1 \dots n) \land [l/ k] A = +∞) \to \exists k \in (1 \dots n) A = +∞$
245	241 242 244	syl2anc	$⊢ (((φ \land l \in ℕ) \land [l/ k] A = +∞) \land n \in ℤ_{\geq l}) \to \exists k \in (1 \dots n) A = +∞$
246	232 233 236 245	esumpinfval	$⊢ (((φ \land l \in ℕ) \land [l/ k] A = +∞) \land n \in ℤ_{\geq l}) \to {\sum^{*}}_{k = 1}^{n} A = +∞$
247	246	ralrimiva	$⊢ ((φ \land l \in ℕ) \land [l/ k] A = +∞) \to \forall n \in ℤ_{\geq l} {\sum^{*}}_{k = 1}^{n} A = +∞$
248		eqidd	$⊢ ((φ \land l \in ℕ) \land [l/ k] A = +∞) \to ℤ_{\geq l} = ℤ_{\geq l}$
249		mpteq12	$⊢ (ℤ_{\geq l} = ℤ_{\geq l} \land \forall n \in ℤ_{\geq l} {\sum^{}}_{k = 1}^{n} A = +∞) \to (n \in ℤ_{\geq l} ⟼ {\sum^{}}_{k = 1}^{n} A) = (n \in ℤ_{\geq l} ⟼ +∞)$
250	248 249	sylan	$⊢ (((φ \land l \in ℕ) \land [l/ k] A = +∞) \land \forall n \in ℤ_{\geq l} {\sum^{}}_{k = 1}^{n} A = +∞) \to (n \in ℤ_{\geq l} ⟼ {\sum^{}}_{k = 1}^{n} A) = (n \in ℤ_{\geq l} ⟼ +∞)$
251		simplr	$⊢ ((φ \land l \in ℕ) \land [l/ k] A = +∞) \to l \in ℕ$
252		uznnssnn	$⊢ l \in ℕ \to ℤ_{\geq l} \subseteq ℕ$
253		resmpt	$⊢ ℤ_{\geq l} \subseteq ℕ \to {(n \in ℕ ⟼ {\sum^{}}_{k = 1}^{n} A) ↾}_{ℤ_{\geq l}} = (n \in ℤ_{\geq l} ⟼ {\sum^{}}_{k = 1}^{n} A)$
254	251 252 253	3syl	$⊢ ((φ \land l \in ℕ) \land [l/ k] A = +∞) \to {(n \in ℕ ⟼ {\sum^{}}_{k = 1}^{n} A) ↾}_{ℤ_{\geq l}} = (n \in ℤ_{\geq l} ⟼ {\sum^{}}_{k = 1}^{n} A)$
255	254	adantr	$⊢ (((φ \land l \in ℕ) \land [l/ k] A = +∞) \land \forall n \in ℤ_{\geq l} {\sum^{}}_{k = 1}^{n} A = +∞) \to {(n \in ℕ ⟼ {\sum^{}}_{k = 1}^{n} A) ↾}_{ℤ_{\geq l}} = (n \in ℤ_{\geq l} ⟼ {\sum^{*}}_{k = 1}^{n} A)$
256		fconstmpt	$⊢ ℤ_{\geq l} \times \{+∞\} = (n \in ℤ_{\geq l} ⟼ +∞)$
257	256	a1i	$⊢ (((φ \land l \in ℕ) \land [l/ k] A = +∞) \land \forall n \in ℤ_{\geq l} {\sum^{*}}_{k = 1}^{n} A = +∞) \to ℤ_{\geq l} \times \{+∞\} = (n \in ℤ_{\geq l} ⟼ +∞)$
258	250 255 257	3eqtr4d	$⊢ (((φ \land l \in ℕ) \land [l/ k] A = +∞) \land \forall n \in ℤ_{\geq l} {\sum^{}}_{k = 1}^{n} A = +∞) \to {(n \in ℕ ⟼ {\sum^{}}_{k = 1}^{n} A) ↾}_{ℤ_{\geq l}} = ℤ_{\geq l} \times \{+∞\}$
259	247 258	mpdan	$⊢ ((φ \land l \in ℕ) \land [l/ k] A = +∞) \to {(n \in ℕ ⟼ {\sum^{*}}_{k = 1}^{n} A) ↾}_{ℤ_{\geq l}} = ℤ_{\geq l} \times \{+∞\}$
260	227 259	chvarvv	$⊢ ((φ \land k \in ℕ) \land A = +∞) \to {(n \in ℕ ⟼ {\sum^{*}}_{k = 1}^{n} A) ↾}_{ℤ_{\geq k}} = ℤ_{\geq k} \times \{+∞\}$
261	218 260	syl5eq	$⊢ ((φ \land k \in ℕ) \land A = +∞) \to {F ↾}_{ℤ_{\geq k}} = ℤ_{\geq k} \times \{+∞\}$
262	261	ex	$⊢ (φ \land k \in ℕ) \to (A = +∞ \to {F ↾}_{ℤ_{\geq k}} = ℤ_{\geq k} \times \{+∞\})$
263	262	reximdva	$⊢ φ \to (\exists k \in ℕ A = +∞ \to \exists k \in ℕ {F ↾}_{ℤ_{\geq k}} = ℤ_{\geq k} \times \{+∞\})$
264	263	imp	$⊢ (φ \land \exists k \in ℕ A = +∞) \to \exists k \in ℕ {F ↾}_{ℤ_{\geq k}} = ℤ_{\geq k} \times \{+∞\}$
265		xrge0topn	$⊢ TopOpen (ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]) = ordTop (\leq) ↾_{𝑡} [0, +∞]$
266	1 265	eqtri	$⊢ J = ordTop (\leq) ↾_{𝑡} [0, +∞]$
267		letopon	$⊢ ordTop (\leq) \in TopOn (ℝ^{*})$
268		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
269		resttopon	$⊢ (ordTop (\leq) \in TopOn (ℝ^{}) \land [0, +∞] \subseteq ℝ^{}) \to ordTop (\leq) ↾_{𝑡} [0, +∞] \in TopOn ([0, +∞])$
270	267 268 269	mp2an	$⊢ ordTop (\leq) ↾_{𝑡} [0, +∞] \in TopOn ([0, +∞])$
271	266 270	eqeltri	$⊢ J \in TopOn ([0, +∞])$
272	271	a1i	$⊢ (φ \land k \in ℕ) \to J \in TopOn ([0, +∞])$
273		0xr	$⊢ 0 \in ℝ^{*}$
274		pnfxr	$⊢ +∞ \in ℝ^{*}$
275		0lepnf	$⊢ 0 \leq +∞$
276		ubicc2	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{} \land 0 \leq +∞) \to +∞ \in [0, +∞]$
277	273 274 275 276	mp3an	$⊢ +∞ \in [0, +∞]$
278	277	a1i	$⊢ (φ \land k \in ℕ) \to +∞ \in [0, +∞]$
279	41	nnzd	$⊢ (φ \land k \in ℕ) \to k \in ℤ$
280		eqid	$⊢ ℤ_{\geq k} = ℤ_{\geq k}$
281	280	lmconst	$⊢ (J \in TopOn ([0, +∞]) \land +∞ \in [0, +∞] \land k \in ℤ) \to (ℤ_{\geq k} \times \{+∞\}) \underset{t}{⇝} (J) +∞$
282	272 278 279 281	syl3anc	$⊢ (φ \land k \in ℕ) \to (ℤ_{\geq k} \times \{+∞\}) \underset{t}{⇝} (J) +∞$
283		breq1	$⊢ {F ↾}_{ℤ_{\geq k}} = ℤ_{\geq k} \times \{+∞\} \to (({F ↾}_{ℤ_{\geq k}}) \underset{t}{⇝} (J) +∞ \leftrightarrow (ℤ_{\geq k} \times \{+∞\}) \underset{t}{⇝} (J) +∞)$
284	283	biimprd	$⊢ {F ↾}_{ℤ_{\geq k}} = ℤ_{\geq k} \times \{+∞\} \to ((ℤ_{\geq k} \times \{+∞\}) \underset{t}{⇝} (J) +∞ \to ({F ↾}_{ℤ_{\geq k}}) \underset{t}{⇝} (J) +∞)$
285	282 284	mpan9	$⊢ ((φ \land k \in ℕ) \land {F ↾}_{ℤ_{\geq k}} = ℤ_{\geq k} \times \{+∞\}) \to ({F ↾}_{ℤ_{\geq k}}) \underset{t}{⇝} (J) +∞$
286		ovexd	$⊢ (φ \land k \in ℕ) \to [0, +∞] \in V$
287		cnex	$⊢ ℂ \in V$
288	287	a1i	$⊢ (φ \land k \in ℕ) \to ℂ \in V$
289	56	adantr	$⊢ (φ \land k \in ℕ) \to F : ℕ ⟶ [0, +∞]$
290		nnsscn	$⊢ ℕ \subseteq ℂ$
291	290	a1i	$⊢ (φ \land k \in ℕ) \to ℕ \subseteq ℂ$
292		elpm2r	$⊢ (([0, +∞] \in V \land ℂ \in V) \land (F : ℕ ⟶ [0, +∞] \land ℕ \subseteq ℂ)) \to F \in ([0, +∞] ↑_{𝑝𝑚} ℂ)$
293	286 288 289 291 292	syl22anc	$⊢ (φ \land k \in ℕ) \to F \in ([0, +∞] ↑_{𝑝𝑚} ℂ)$
294	272 293 279	lmres	$⊢ (φ \land k \in ℕ) \to (F \underset{t}{⇝} (J) +∞ \leftrightarrow ({F ↾}_{ℤ_{\geq k}}) \underset{t}{⇝} (J) +∞)$
295	294	biimpar	$⊢ ((φ \land k \in ℕ) \land ({F ↾}_{ℤ_{\geq k}}) \underset{t}{⇝} (J) +∞) \to F \underset{t}{⇝} (J) +∞$
296	285 295	syldan	$⊢ ((φ \land k \in ℕ) \land {F ↾}_{ℤ_{\geq k}} = ℤ_{\geq k} \times \{+∞\}) \to F \underset{t}{⇝} (J) +∞$
297	296	r19.29an	$⊢ (φ \land \exists k \in ℕ {F ↾}_{ℤ_{\geq k}} = ℤ_{\geq k} \times \{+∞\}) \to F \underset{t}{⇝} (J) +∞$
298	264 297	syldan	$⊢ (φ \land \exists k \in ℕ A = +∞) \to F \underset{t}{⇝} (J) +∞$
299		nfv	$⊢ Ⅎ k φ$
300		nfre1	$⊢ Ⅎ k \exists k \in ℕ A = +∞$
301	299 300	nfan	$⊢ Ⅎ k (φ \land \exists k \in ℕ A = +∞)$
302	127	a1i	$⊢ (φ \land \exists k \in ℕ A = +∞) \to ℕ \in V$
303	3	adantlr	$⊢ ((φ \land \exists k \in ℕ A = +∞) \land k \in ℕ) \to A \in [0, +∞]$
304		simpr	$⊢ (φ \land \exists k \in ℕ A = +∞) \to \exists k \in ℕ A = +∞$
305	301 302 303 304	esumpinfval	$⊢ (φ \land \exists k \in ℕ A = +∞) \to \underset{k \in ℕ}{\sum^{*}} A = +∞$
306	298 305	breqtrrd	$⊢ (φ \land \exists k \in ℕ A = +∞) \to F \underset{t}{⇝} (J) \underset{k \in ℕ}{\sum^{*}} A$
307		eleq1w	$⊢ k = m \to (k \in ℕ \leftrightarrow m \in ℕ)$
308	307	anbi2d	$⊢ k = m \to ((φ \land k \in ℕ) \leftrightarrow (φ \land m \in ℕ))$
309	4	eleq1d	$⊢ k = m \to (A \in [0, +∞] \leftrightarrow B \in [0, +∞])$
310	308 309	imbi12d	$⊢ k = m \to (((φ \land k \in ℕ) \to A \in [0, +∞]) \leftrightarrow ((φ \land m \in ℕ) \to B \in [0, +∞]))$
311	310 3	chvarvv	$⊢ (φ \land m \in ℕ) \to B \in [0, +∞]$
312		eliccelico	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{} \land 0 \leq +∞) \to (B \in [0, +∞] \leftrightarrow (B \in [0, +∞) \lor B = +∞))$
313	273 274 275 312	mp3an	$⊢ B \in [0, +∞] \leftrightarrow (B \in [0, +∞) \lor B = +∞)$
314	311 313	sylib	$⊢ (φ \land m \in ℕ) \to (B \in [0, +∞) \lor B = +∞)$
315	314	ralrimiva	$⊢ φ \to \forall m \in ℕ (B \in [0, +∞) \lor B = +∞)$
316		r19.30	$⊢ \forall m \in ℕ (B \in [0, +∞) \lor B = +∞) \to (\forall m \in ℕ B \in [0, +∞) \lor \exists m \in ℕ B = +∞)$
317	315 316	syl	$⊢ φ \to (\forall m \in ℕ B \in [0, +∞) \lor \exists m \in ℕ B = +∞)$
318	4	eqeq1d	$⊢ k = m \to (A = +∞ \leftrightarrow B = +∞)$
319	318	cbvrexvw	$⊢ \exists k \in ℕ A = +∞ \leftrightarrow \exists m \in ℕ B = +∞$
320	319	orbi2i	$⊢ (\forall m \in ℕ B \in [0, +∞) \lor \exists k \in ℕ A = +∞) \leftrightarrow (\forall m \in ℕ B \in [0, +∞) \lor \exists m \in ℕ B = +∞)$
321	317 320	sylibr	$⊢ φ \to (\forall m \in ℕ B \in [0, +∞) \lor \exists k \in ℕ A = +∞)$
322	217 306 321	mpjaodan	$⊢ φ \to F \underset{t}{⇝} (J) \underset{k \in ℕ}{\sum^{*}} A$

Metamath Proof Explorer

Theorem esumcvg

Proof