esumfzf

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

		Ref	Expression
	Hypothesis	esumfzf.1	$⊢ \underline{Ⅎ} k F$
	Assertion	esumfzf	$⊢ (F : ℕ ⟶ [0, +∞] \land N \in ℕ) \to {\sum^{*}}_{k = 1}^{N} F (k) = seq 1 (+_{𝑒}, F) (N)$

Proof

Step	Hyp	Ref	Expression
1		esumfzf.1	$⊢ \underline{Ⅎ} k F$
2		nfv	$⊢ Ⅎ k i = 1$
3		oveq2	$⊢ i = 1 \to (1 \dots i) = (1 \dots 1)$
4	2 3	esumeq1d	$⊢ i = 1 \to {\sum^{}}_{k = 1}^{i} F (k) = {\sum^{}}_{k = 1}^{1} F (k)$
5		fveq2	$⊢ i = 1 \to seq 1 (+_{𝑒}, F) (i) = seq 1 (+_{𝑒}, F) (1)$
6	4 5	eqeq12d	$⊢ i = 1 \to ({\sum^{}}_{k = 1}^{i} F (k) = seq 1 (+_{𝑒}, F) (i) \leftrightarrow {\sum^{}}_{k = 1}^{1} F (k) = seq 1 (+_{𝑒}, F) (1))$
7	6	imbi2d	$⊢ i = 1 \to ((F : ℕ ⟶ [0, +∞] \to {\sum^{}}_{k = 1}^{i} F (k) = seq 1 (+_{𝑒}, F) (i)) \leftrightarrow (F : ℕ ⟶ [0, +∞] \to {\sum^{}}_{k = 1}^{1} F (k) = seq 1 (+_{𝑒}, F) (1)))$
8		nfv	$⊢ Ⅎ k i = n$
9		oveq2	$⊢ i = n \to (1 \dots i) = (1 \dots n)$
10	8 9	esumeq1d	$⊢ i = n \to {\sum^{}}_{k = 1}^{i} F (k) = {\sum^{}}_{k = 1}^{n} F (k)$
11		fveq2	$⊢ i = n \to seq 1 (+_{𝑒}, F) (i) = seq 1 (+_{𝑒}, F) (n)$
12	10 11	eqeq12d	$⊢ i = n \to ({\sum^{}}_{k = 1}^{i} F (k) = seq 1 (+_{𝑒}, F) (i) \leftrightarrow {\sum^{}}_{k = 1}^{n} F (k) = seq 1 (+_{𝑒}, F) (n))$
13	12	imbi2d	$⊢ i = n \to ((F : ℕ ⟶ [0, +∞] \to {\sum^{}}_{k = 1}^{i} F (k) = seq 1 (+_{𝑒}, F) (i)) \leftrightarrow (F : ℕ ⟶ [0, +∞] \to {\sum^{}}_{k = 1}^{n} F (k) = seq 1 (+_{𝑒}, F) (n)))$
14		nfv	$⊢ Ⅎ k i = n + 1$
15		oveq2	$⊢ i = n + 1 \to (1 \dots i) = (1 \dots n + 1)$
16	14 15	esumeq1d	$⊢ i = n + 1 \to {\sum^{}}_{k = 1}^{i} F (k) = {\sum^{}}_{k = 1}^{n + 1} F (k)$
17		fveq2	$⊢ i = n + 1 \to seq 1 (+_{𝑒}, F) (i) = seq 1 (+_{𝑒}, F) (n + 1)$
18	16 17	eqeq12d	$⊢ i = n + 1 \to ({\sum^{}}_{k = 1}^{i} F (k) = seq 1 (+_{𝑒}, F) (i) \leftrightarrow {\sum^{}}_{k = 1}^{n + 1} F (k) = seq 1 (+_{𝑒}, F) (n + 1))$
19	18	imbi2d	$⊢ i = n + 1 \to ((F : ℕ ⟶ [0, +∞] \to {\sum^{}}_{k = 1}^{i} F (k) = seq 1 (+_{𝑒}, F) (i)) \leftrightarrow (F : ℕ ⟶ [0, +∞] \to {\sum^{}}_{k = 1}^{n + 1} F (k) = seq 1 (+_{𝑒}, F) (n + 1)))$
20		nfv	$⊢ Ⅎ k i = N$
21		oveq2	$⊢ i = N \to (1 \dots i) = (1 \dots N)$
22	20 21	esumeq1d	$⊢ i = N \to {\sum^{}}_{k = 1}^{i} F (k) = {\sum^{}}_{k = 1}^{N} F (k)$
23		fveq2	$⊢ i = N \to seq 1 (+_{𝑒}, F) (i) = seq 1 (+_{𝑒}, F) (N)$
24	22 23	eqeq12d	$⊢ i = N \to ({\sum^{}}_{k = 1}^{i} F (k) = seq 1 (+_{𝑒}, F) (i) \leftrightarrow {\sum^{}}_{k = 1}^{N} F (k) = seq 1 (+_{𝑒}, F) (N))$
25	24	imbi2d	$⊢ i = N \to ((F : ℕ ⟶ [0, +∞] \to {\sum^{}}_{k = 1}^{i} F (k) = seq 1 (+_{𝑒}, F) (i)) \leftrightarrow (F : ℕ ⟶ [0, +∞] \to {\sum^{}}_{k = 1}^{N} F (k) = seq 1 (+_{𝑒}, F) (N)))$
26		fveq2	$⊢ k = x \to F (k) = F (x)$
27		nfcv	$⊢ \underline{Ⅎ} x \{1\}$
28		nfcv	$⊢ \underline{Ⅎ} k \{1\}$
29		nfcv	$⊢ \underline{Ⅎ} x F (k)$
30		nfcv	$⊢ \underline{Ⅎ} k x$
31	1 30	nffv	$⊢ \underline{Ⅎ} k F (x)$
32	26 27 28 29 31	cbvesum	$⊢ \underset{k \in \{1\}}{\sum^{}} F (k) = \underset{x \in \{1\}}{\sum^{}} F (x)$
33		simpr	$⊢ (F : ℕ ⟶ [0, +∞] \land x = 1) \to x = 1$
34	33	fveq2d	$⊢ (F : ℕ ⟶ [0, +∞] \land x = 1) \to F (x) = F (1)$
35		1z	$⊢ 1 \in ℤ$
36	35	a1i	$⊢ F : ℕ ⟶ [0, +∞] \to 1 \in ℤ$
37		1nn	$⊢ 1 \in ℕ$
38		ffvelcdm	$⊢ (F : ℕ ⟶ [0, +∞] \land 1 \in ℕ) \to F (1) \in [0, +∞]$
39	37 38	mpan2	$⊢ F : ℕ ⟶ [0, +∞] \to F (1) \in [0, +∞]$
40	34 36 39	esumsn	$⊢ F : ℕ ⟶ [0, +∞] \to \underset{x \in \{1\}}{\sum^{*}} F (x) = F (1)$
41	32 40	eqtrid	$⊢ F : ℕ ⟶ [0, +∞] \to \underset{k \in \{1\}}{\sum^{*}} F (k) = F (1)$
42		fzsn	$⊢ 1 \in ℤ \to (1 \dots 1) = \{1\}$
43	35 42	ax-mp	$⊢ (1 \dots 1) = \{1\}$
44		esumeq1	$⊢ (1 \dots 1) = \{1\} \to {\sum^{}}_{k = 1}^{1} F (k) = \underset{k \in \{1\}}{\sum^{}} F (k)$
45	43 44	ax-mp	$⊢ {\sum^{}}_{k = 1}^{1} F (k) = \underset{k \in \{1\}}{\sum^{}} F (k)$
46		seq1	$⊢ 1 \in ℤ \to seq 1 (+_{𝑒}, F) (1) = F (1)$
47	35 46	ax-mp	$⊢ seq 1 (+_{𝑒}, F) (1) = F (1)$
48	41 45 47	3eqtr4g	$⊢ F : ℕ ⟶ [0, +∞] \to {\sum^{*}}_{k = 1}^{1} F (k) = seq 1 (+_{𝑒}, F) (1)$
49		simpl	$⊢ (n \in ℕ \land F : ℕ ⟶ [0, +∞]) \to n \in ℕ$
50		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
51	49 50	eleqtrdi	$⊢ (n \in ℕ \land F : ℕ ⟶ [0, +∞]) \to n \in ℤ_{\geq 1}$
52		seqp1	$⊢ n \in ℤ_{\geq 1} \to seq 1 (+_{𝑒}, F) (n + 1) = seq 1 (+_{𝑒}, F) (n) +_{𝑒} F (n + 1)$
53	51 52	syl	$⊢ (n \in ℕ \land F : ℕ ⟶ [0, +∞]) \to seq 1 (+_{𝑒}, F) (n + 1) = seq 1 (+_{𝑒}, F) (n) +_{𝑒} F (n + 1)$
54	53	adantr	$⊢ ((n \in ℕ \land F : ℕ ⟶ [0, +∞]) \land {\sum^{*}}_{k = 1}^{n} F (k) = seq 1 (+_{𝑒}, F) (n)) \to seq 1 (+_{𝑒}, F) (n + 1) = seq 1 (+_{𝑒}, F) (n) +_{𝑒} F (n + 1)$
55		simpr	$⊢ ((n \in ℕ \land F : ℕ ⟶ [0, +∞]) \land {\sum^{}}_{k = 1}^{n} F (k) = seq 1 (+_{𝑒}, F) (n)) \to {\sum^{}}_{k = 1}^{n} F (k) = seq 1 (+_{𝑒}, F) (n)$
56	55	oveq1d	$⊢ ((n \in ℕ \land F : ℕ ⟶ [0, +∞]) \land {\sum^{}}_{k = 1}^{n} F (k) = seq 1 (+_{𝑒}, F) (n)) \to {\sum^{}}_{k = 1}^{n} F (k) +_{𝑒} F (n + 1) = seq 1 (+_{𝑒}, F) (n) +_{𝑒} F (n + 1)$
57		nfv	$⊢ Ⅎ k n \in ℕ$
58	57	nfci	$⊢ \underline{Ⅎ} k ℕ$
59		nfcv	$⊢ \underline{Ⅎ} k [0, +∞]$
60	1 58 59	nff	$⊢ Ⅎ k F : ℕ ⟶ [0, +∞]$
61	57 60	nfan	$⊢ Ⅎ k (n \in ℕ \land F : ℕ ⟶ [0, +∞])$
62		fzsuc	$⊢ n \in ℤ_{\geq 1} \to (1 \dots n + 1) = (1 \dots n) \cup \{n + 1\}$
63	51 62	syl	$⊢ (n \in ℕ \land F : ℕ ⟶ [0, +∞]) \to (1 \dots n + 1) = (1 \dots n) \cup \{n + 1\}$
64	61 63	esumeq1d	$⊢ (n \in ℕ \land F : ℕ ⟶ [0, +∞]) \to {\sum^{}}_{k = 1}^{n + 1} F (k) = \underset{k \in (1 \dots n) \cup \{n + 1\}}{\sum^{}} F (k)$
65		nfcv	$⊢ \underline{Ⅎ} k (1 \dots n)$
66		nfcv	$⊢ \underline{Ⅎ} k \{n + 1\}$
67		ovexd	$⊢ (n \in ℕ \land F : ℕ ⟶ [0, +∞]) \to (1 \dots n) \in V$
68		snex	$⊢ \{n + 1\} \in V$
69	68	a1i	$⊢ (n \in ℕ \land F : ℕ ⟶ [0, +∞]) \to \{n + 1\} \in V$
70		fzp1disj	$⊢ (1 \dots n) \cap \{n + 1\} = \emptyset$
71	70	a1i	$⊢ (n \in ℕ \land F : ℕ ⟶ [0, +∞]) \to (1 \dots n) \cap \{n + 1\} = \emptyset$
72		simplr	$⊢ ((n \in ℕ \land F : ℕ ⟶ [0, +∞]) \land k \in (1 \dots n)) \to F : ℕ ⟶ [0, +∞]$
73		fzssnn	$⊢ 1 \in ℕ \to (1 \dots n) \subseteq ℕ$
74	37 73	ax-mp	$⊢ (1 \dots n) \subseteq ℕ$
75		simpr	$⊢ ((n \in ℕ \land F : ℕ ⟶ [0, +∞]) \land k \in (1 \dots n)) \to k \in (1 \dots n)$
76	74 75	sselid	$⊢ ((n \in ℕ \land F : ℕ ⟶ [0, +∞]) \land k \in (1 \dots n)) \to k \in ℕ$
77	72 76	ffvelcdmd	$⊢ ((n \in ℕ \land F : ℕ ⟶ [0, +∞]) \land k \in (1 \dots n)) \to F (k) \in [0, +∞]$
78		simplr	$⊢ ((n \in ℕ \land F : ℕ ⟶ [0, +∞]) \land k \in \{n + 1\}) \to F : ℕ ⟶ [0, +∞]$
79		simpr	$⊢ ((n \in ℕ \land F : ℕ ⟶ [0, +∞]) \land k \in \{n + 1\}) \to k \in \{n + 1\}$
80		velsn	$⊢ k \in \{n + 1\} \leftrightarrow k = n + 1$
81	79 80	sylib	$⊢ ((n \in ℕ \land F : ℕ ⟶ [0, +∞]) \land k \in \{n + 1\}) \to k = n + 1$
82		simpll	$⊢ ((n \in ℕ \land F : ℕ ⟶ [0, +∞]) \land k \in \{n + 1\}) \to n \in ℕ$
83	82	peano2nnd	$⊢ ((n \in ℕ \land F : ℕ ⟶ [0, +∞]) \land k \in \{n + 1\}) \to n + 1 \in ℕ$
84	81 83	eqeltrd	$⊢ ((n \in ℕ \land F : ℕ ⟶ [0, +∞]) \land k \in \{n + 1\}) \to k \in ℕ$
85	78 84	ffvelcdmd	$⊢ ((n \in ℕ \land F : ℕ ⟶ [0, +∞]) \land k \in \{n + 1\}) \to F (k) \in [0, +∞]$
86	61 65 66 67 69 71 77 85	esumsplit	$⊢ (n \in ℕ \land F : ℕ ⟶ [0, +∞]) \to \underset{k \in (1 \dots n) \cup \{n + 1\}}{\sum^{}} F (k) = {\sum^{}}_{k = 1}^{n} F (k) +_{𝑒} \underset{k \in \{n + 1\}}{\sum^{*}} F (k)$
87		nfcv	$⊢ \underline{Ⅎ} x \{n + 1\}$
88	26 87 66 29 31	cbvesum	$⊢ \underset{k \in \{n + 1\}}{\sum^{}} F (k) = \underset{x \in \{n + 1\}}{\sum^{}} F (x)$
89		simpr	$⊢ ((n \in ℕ \land F : ℕ ⟶ [0, +∞]) \land x = n + 1) \to x = n + 1$
90	89	fveq2d	$⊢ ((n \in ℕ \land F : ℕ ⟶ [0, +∞]) \land x = n + 1) \to F (x) = F (n + 1)$
91	49	peano2nnd	$⊢ (n \in ℕ \land F : ℕ ⟶ [0, +∞]) \to n + 1 \in ℕ$
92		simpr	$⊢ (n \in ℕ \land F : ℕ ⟶ [0, +∞]) \to F : ℕ ⟶ [0, +∞]$
93	92 91	ffvelcdmd	$⊢ (n \in ℕ \land F : ℕ ⟶ [0, +∞]) \to F (n + 1) \in [0, +∞]$
94	90 91 93	esumsn	$⊢ (n \in ℕ \land F : ℕ ⟶ [0, +∞]) \to \underset{x \in \{n + 1\}}{\sum^{*}} F (x) = F (n + 1)$
95	88 94	eqtrid	$⊢ (n \in ℕ \land F : ℕ ⟶ [0, +∞]) \to \underset{k \in \{n + 1\}}{\sum^{*}} F (k) = F (n + 1)$
96	95	oveq2d	$⊢ (n \in ℕ \land F : ℕ ⟶ [0, +∞]) \to {\sum^{}}_{k = 1}^{n} F (k) +_{𝑒} \underset{k \in \{n + 1\}}{\sum^{}} F (k) = {\sum^{*}}_{k = 1}^{n} F (k) +_{𝑒} F (n + 1)$
97	64 86 96	3eqtrrd	$⊢ (n \in ℕ \land F : ℕ ⟶ [0, +∞]) \to {\sum^{}}_{k = 1}^{n} F (k) +_{𝑒} F (n + 1) = {\sum^{}}_{k = 1}^{n + 1} F (k)$
98	97	adantr	$⊢ ((n \in ℕ \land F : ℕ ⟶ [0, +∞]) \land {\sum^{}}_{k = 1}^{n} F (k) = seq 1 (+_{𝑒}, F) (n)) \to {\sum^{}}_{k = 1}^{n} F (k) +_{𝑒} F (n + 1) = {\sum^{*}}_{k = 1}^{n + 1} F (k)$
99	54 56 98	3eqtr2rd	$⊢ ((n \in ℕ \land F : ℕ ⟶ [0, +∞]) \land {\sum^{}}_{k = 1}^{n} F (k) = seq 1 (+_{𝑒}, F) (n)) \to {\sum^{}}_{k = 1}^{n + 1} F (k) = seq 1 (+_{𝑒}, F) (n + 1)$
100	99	exp31	$⊢ n \in ℕ \to (F : ℕ ⟶ [0, +∞] \to ({\sum^{}}_{k = 1}^{n} F (k) = seq 1 (+_{𝑒}, F) (n) \to {\sum^{}}_{k = 1}^{n + 1} F (k) = seq 1 (+_{𝑒}, F) (n + 1)))$
101	100	a2d	$⊢ n \in ℕ \to ((F : ℕ ⟶ [0, +∞] \to {\sum^{}}_{k = 1}^{n} F (k) = seq 1 (+_{𝑒}, F) (n)) \to (F : ℕ ⟶ [0, +∞] \to {\sum^{}}_{k = 1}^{n + 1} F (k) = seq 1 (+_{𝑒}, F) (n + 1)))$
102	7 13 19 25 48 101	nnind	$⊢ N \in ℕ \to (F : ℕ ⟶ [0, +∞] \to {\sum^{*}}_{k = 1}^{N} F (k) = seq 1 (+_{𝑒}, F) (N))$
103	102	impcom	$⊢ (F : ℕ ⟶ [0, +∞] \land N \in ℕ) \to {\sum^{*}}_{k = 1}^{N} F (k) = seq 1 (+_{𝑒}, F) (N)$

Metamath Proof Explorer

Theorem esumfzf

Proof