sumnnodd

Description: A series indexed by NN with only odd terms. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	sumnnodd.1	$⊢ φ \to F : ℕ ⟶ ℂ$
	sumnnodd.even0	$⊢ (φ \land k \in ℕ \land \frac{k}{2} \in ℕ) \to F (k) = 0$
	sumnnodd.sc	$⊢ φ \to seq 1 (+ F) ⇝ B$
Assertion	sumnnodd	$⊢ φ \to (seq 1 (+ (k \in ℕ ⟼ F (2 k - 1))) ⇝ B \land \sum_{k \in ℕ} F (k) = \sum_{k \in ℕ} F (2 k - 1))$

Proof

Step	Hyp	Ref	Expression
1		sumnnodd.1	$⊢ φ \to F : ℕ ⟶ ℂ$
2		sumnnodd.even0	$⊢ (φ \land k \in ℕ \land \frac{k}{2} \in ℕ) \to F (k) = 0$
3		sumnnodd.sc	$⊢ φ \to seq 1 (+ F) ⇝ B$
4		nfv	$⊢ Ⅎ k φ$
5		nfcv	$⊢ \underline{Ⅎ} k seq 1 (+ F)$
6		nfcv	$⊢ \underline{Ⅎ} k 1$
7		nfcv	$⊢ \underline{Ⅎ} k +$
8		nfmpt1	$⊢ \underline{Ⅎ} k (k \in ℕ ⟼ F (2 k - 1))$
9	6 7 8	nfseq	$⊢ \underline{Ⅎ} k seq 1 (+ (k \in ℕ ⟼ F (2 k - 1)))$
10		nfmpt1	$⊢ \underline{Ⅎ} k (k \in ℕ ⟼ 2 k - 1)$
11		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
12		1zzd	$⊢ φ \to 1 \in ℤ$
13		seqex	$⊢ seq 1 (+ F) \in V$
14	13	a1i	$⊢ φ \to seq 1 (+ F) \in V$
15	1	ffvelcdmda	$⊢ (φ \land k \in ℕ) \to F (k) \in ℂ$
16	11 12 15	serf	$⊢ φ \to seq 1 (+ F) : ℕ ⟶ ℂ$
17	16	ffvelcdmda	$⊢ (φ \land k \in ℕ) \to seq 1 (+ F) (k) \in ℂ$
18		1nn	$⊢ 1 \in ℕ$
19		oveq2	$⊢ k = 1 \to 2 k = 2 \cdot 1$
20	19	oveq1d	$⊢ k = 1 \to 2 k - 1 = 2 \cdot 1 - 1$
21		eqid	$⊢ (k \in ℕ ⟼ 2 k - 1) = (k \in ℕ ⟼ 2 k - 1)$
22		ovex	$⊢ 2 \cdot 1 - 1 \in V$
23	20 21 22	fvmpt	$⊢ 1 \in ℕ \to (k \in ℕ ⟼ 2 k - 1) (1) = 2 \cdot 1 - 1$
24	18 23	ax-mp	$⊢ (k \in ℕ ⟼ 2 k - 1) (1) = 2 \cdot 1 - 1$
25		2t1e2	$⊢ 2 \cdot 1 = 2$
26	25	oveq1i	$⊢ 2 \cdot 1 - 1 = 2 - 1$
27		2m1e1	$⊢ 2 - 1 = 1$
28	24 26 27	3eqtri	$⊢ (k \in ℕ ⟼ 2 k - 1) (1) = 1$
29	28 18	eqeltri	$⊢ (k \in ℕ ⟼ 2 k - 1) (1) \in ℕ$
30	29	a1i	$⊢ φ \to (k \in ℕ ⟼ 2 k - 1) (1) \in ℕ$
31		2z	$⊢ 2 \in ℤ$
32	31	a1i	$⊢ k \in ℕ \to 2 \in ℤ$
33		nnz	$⊢ k \in ℕ \to k \in ℤ$
34	32 33	zmulcld	$⊢ k \in ℕ \to 2 k \in ℤ$
35	33	peano2zd	$⊢ k \in ℕ \to k + 1 \in ℤ$
36	32 35	zmulcld	$⊢ k \in ℕ \to 2 (k + 1) \in ℤ$
37		1zzd	$⊢ k \in ℕ \to 1 \in ℤ$
38	36 37	zsubcld	$⊢ k \in ℕ \to 2 (k + 1) - 1 \in ℤ$
39		2re	$⊢ 2 \in ℝ$
40	39	a1i	$⊢ k \in ℕ \to 2 \in ℝ$
41		nnre	$⊢ k \in ℕ \to k \in ℝ$
42	40 41	remulcld	$⊢ k \in ℕ \to 2 k \in ℝ$
43	42	lep1d	$⊢ k \in ℕ \to 2 k \leq 2 k + 1$
44		2cnd	$⊢ k \in ℕ \to 2 \in ℂ$
45		nncn	$⊢ k \in ℕ \to k \in ℂ$
46		1cnd	$⊢ k \in ℕ \to 1 \in ℂ$
47	44 45 46	adddid	$⊢ k \in ℕ \to 2 (k + 1) = 2 k + 2 \cdot 1$
48	25	oveq2i	$⊢ 2 k + 2 \cdot 1 = 2 k + 2$
49	47 48	eqtrdi	$⊢ k \in ℕ \to 2 (k + 1) = 2 k + 2$
50	49	oveq1d	$⊢ k \in ℕ \to 2 (k + 1) - 1 = 2 k + 2 - 1$
51	44 45	mulcld	$⊢ k \in ℕ \to 2 k \in ℂ$
52	51 44 46	addsubassd	$⊢ k \in ℕ \to 2 k + 2 - 1 = 2 k + 2 - 1$
53	27	oveq2i	$⊢ 2 k + 2 - 1 = 2 k + 1$
54	53	a1i	$⊢ k \in ℕ \to 2 k + 2 - 1 = 2 k + 1$
55	50 52 54	3eqtrrd	$⊢ k \in ℕ \to 2 k + 1 = 2 (k + 1) - 1$
56	43 55	breqtrd	$⊢ k \in ℕ \to 2 k \leq 2 (k + 1) - 1$
57		eluz2	$⊢ 2 (k + 1) - 1 \in ℤ_{\geq 2 k} \leftrightarrow (2 k \in ℤ \land 2 (k + 1) - 1 \in ℤ \land 2 k \leq 2 (k + 1) - 1)$
58	34 38 56 57	syl3anbrc	$⊢ k \in ℕ \to 2 (k + 1) - 1 \in ℤ_{\geq 2 k}$
59		oveq2	$⊢ k = j \to 2 k = 2 j$
60	59	oveq1d	$⊢ k = j \to 2 k - 1 = 2 j - 1$
61	60	cbvmptv	$⊢ (k \in ℕ ⟼ 2 k - 1) = (j \in ℕ ⟼ 2 j - 1)$
62		oveq2	$⊢ j = k + 1 \to 2 j = 2 (k + 1)$
63	62	oveq1d	$⊢ j = k + 1 \to 2 j - 1 = 2 (k + 1) - 1$
64		peano2nn	$⊢ k \in ℕ \to k + 1 \in ℕ$
65	61 63 64 38	fvmptd3	$⊢ k \in ℕ \to (k \in ℕ ⟼ 2 k - 1) (k + 1) = 2 (k + 1) - 1$
66	34 37	zsubcld	$⊢ k \in ℕ \to 2 k - 1 \in ℤ$
67		fvmpt4	$⊢ (k \in ℕ \land 2 k - 1 \in ℤ) \to (k \in ℕ ⟼ 2 k - 1) (k) = 2 k - 1$
68	66 67	mpdan	$⊢ k \in ℕ \to (k \in ℕ ⟼ 2 k - 1) (k) = 2 k - 1$
69	51 46 68	mvrrsubd	$⊢ k \in ℕ \to (k \in ℕ ⟼ 2 k - 1) (k) + 1 = 2 k$
70	69	fveq2d	$⊢ k \in ℕ \to ℤ_{\geq ((k \in ℕ ⟼ 2 k - 1) (k) + 1)} = ℤ_{\geq 2 k}$
71	58 65 70	3eltr4d	$⊢ k \in ℕ \to (k \in ℕ ⟼ 2 k - 1) (k + 1) \in ℤ_{\geq ((k \in ℕ ⟼ 2 k - 1) (k) + 1)}$
72	71	adantl	$⊢ (φ \land k \in ℕ) \to (k \in ℕ ⟼ 2 k - 1) (k + 1) \in ℤ_{\geq ((k \in ℕ ⟼ 2 k - 1) (k) + 1)}$
73		seqex	$⊢ seq 1 (+ (k \in ℕ ⟼ F (2 k - 1))) \in V$
74	73	a1i	$⊢ φ \to seq 1 (+ (k \in ℕ ⟼ F (2 k - 1))) \in V$
75		incom	$⊢ ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \cap ((1 \dots 2 k - 1) \cap \{n \in ℕ \| \frac{n}{2} \in ℕ\}) = ((1 \dots 2 k - 1) \cap \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \cap ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\})$
76		inss2	$⊢ (1 \dots 2 k - 1) \cap \{n \in ℕ \| \frac{n}{2} \in ℕ\} \subseteq \{n \in ℕ \| \frac{n}{2} \in ℕ\}$
77		ssrin	$⊢ (1 \dots 2 k - 1) \cap \{n \in ℕ \| \frac{n}{2} \in ℕ\} \subseteq \{n \in ℕ \| \frac{n}{2} \in ℕ\} \to ((1 \dots 2 k - 1) \cap \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \cap ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \subseteq \{n \in ℕ \| \frac{n}{2} \in ℕ\} \cap ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\})$
78	76 77	ax-mp	$⊢ ((1 \dots 2 k - 1) \cap \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \cap ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \subseteq \{n \in ℕ \| \frac{n}{2} \in ℕ\} \cap ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\})$
79	75 78	eqsstri	$⊢ ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \cap ((1 \dots 2 k - 1) \cap \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \subseteq \{n \in ℕ \| \frac{n}{2} \in ℕ\} \cap ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\})$
80		disjdif	$⊢ \{n \in ℕ \| \frac{n}{2} \in ℕ\} \cap ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}) = \emptyset$
81	79 80	sseqtri	$⊢ ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \cap ((1 \dots 2 k - 1) \cap \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \subseteq \emptyset$
82		ss0	$⊢ ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \cap ((1 \dots 2 k - 1) \cap \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \subseteq \emptyset \to ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \cap ((1 \dots 2 k - 1) \cap \{n \in ℕ \| \frac{n}{2} \in ℕ\}) = \emptyset$
83	81 82	mp1i	$⊢ (φ \land k \in ℕ) \to ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \cap ((1 \dots 2 k - 1) \cap \{n \in ℕ \| \frac{n}{2} \in ℕ\}) = \emptyset$
84		uncom	$⊢ ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \cup ((1 \dots 2 k - 1) \cap \{n \in ℕ \| \frac{n}{2} \in ℕ\}) = ((1 \dots 2 k - 1) \cap \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \cup ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\})$
85		inundif	$⊢ ((1 \dots 2 k - 1) \cap \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \cup ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}) = (1 \dots 2 k - 1)$
86	84 85	eqtr2i	$⊢ (1 \dots 2 k - 1) = ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \cup ((1 \dots 2 k - 1) \cap \{n \in ℕ \| \frac{n}{2} \in ℕ\})$
87	86	a1i	$⊢ (φ \land k \in ℕ) \to (1 \dots 2 k - 1) = ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \cup ((1 \dots 2 k - 1) \cap \{n \in ℕ \| \frac{n}{2} \in ℕ\})$
88		fzfid	$⊢ (φ \land k \in ℕ) \to (1 \dots 2 k - 1) \in Fin$
89	1	adantr	$⊢ (φ \land j \in (1 \dots 2 k - 1)) \to F : ℕ ⟶ ℂ$
90		elfznn	$⊢ j \in (1 \dots 2 k - 1) \to j \in ℕ$
91	90	adantl	$⊢ (φ \land j \in (1 \dots 2 k - 1)) \to j \in ℕ$
92	89 91	ffvelcdmd	$⊢ (φ \land j \in (1 \dots 2 k - 1)) \to F (j) \in ℂ$
93	92	adantlr	$⊢ ((φ \land k \in ℕ) \land j \in (1 \dots 2 k - 1)) \to F (j) \in ℂ$
94	83 87 88 93	fsumsplit	$⊢ (φ \land k \in ℕ) \to \sum_{j = 1}^{2 k - 1} F (j) = \sum_{j \in (1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}} F (j) + \sum_{j \in (1 \dots 2 k - 1) \cap \{n \in ℕ \| \frac{n}{2} \in ℕ\}} F (j)$
95		simpl	$⊢ (φ \land j \in ((1 \dots 2 k - 1) \cap \{n \in ℕ \| \frac{n}{2} \in ℕ\})) \to φ$
96		ssrab2	$⊢ \{n \in ℕ \| \frac{n}{2} \in ℕ\} \subseteq ℕ$
97	76	sseli	$⊢ j \in ((1 \dots 2 k - 1) \cap \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \to j \in \{n \in ℕ \| \frac{n}{2} \in ℕ\}$
98	96 97	sselid	$⊢ j \in ((1 \dots 2 k - 1) \cap \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \to j \in ℕ$
99	98	adantl	$⊢ (φ \land j \in ((1 \dots 2 k - 1) \cap \{n \in ℕ \| \frac{n}{2} \in ℕ\})) \to j \in ℕ$
100		oveq1	$⊢ k = j \to \frac{k}{2} = \frac{j}{2}$
101	100	eleq1d	$⊢ k = j \to (\frac{k}{2} \in ℕ \leftrightarrow \frac{j}{2} \in ℕ)$
102		oveq1	$⊢ n = k \to \frac{n}{2} = \frac{k}{2}$
103	102	eleq1d	$⊢ n = k \to (\frac{n}{2} \in ℕ \leftrightarrow \frac{k}{2} \in ℕ)$
104	103	elrab	$⊢ k \in \{n \in ℕ \| \frac{n}{2} \in ℕ\} \leftrightarrow (k \in ℕ \land \frac{k}{2} \in ℕ)$
105	104	simprbi	$⊢ k \in \{n \in ℕ \| \frac{n}{2} \in ℕ\} \to \frac{k}{2} \in ℕ$
106	101 105	vtoclga	$⊢ j \in \{n \in ℕ \| \frac{n}{2} \in ℕ\} \to \frac{j}{2} \in ℕ$
107	97 106	syl	$⊢ j \in ((1 \dots 2 k - 1) \cap \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \to \frac{j}{2} \in ℕ$
108	107	adantl	$⊢ (φ \land j \in ((1 \dots 2 k - 1) \cap \{n \in ℕ \| \frac{n}{2} \in ℕ\})) \to \frac{j}{2} \in ℕ$
109		eleq1w	$⊢ k = j \to (k \in ℕ \leftrightarrow j \in ℕ)$
110	109 101	3anbi23d	$⊢ k = j \to ((φ \land k \in ℕ \land \frac{k}{2} \in ℕ) \leftrightarrow (φ \land j \in ℕ \land \frac{j}{2} \in ℕ))$
111		fveqeq2	$⊢ k = j \to (F (k) = 0 \leftrightarrow F (j) = 0)$
112	110 111	imbi12d	$⊢ k = j \to (((φ \land k \in ℕ \land \frac{k}{2} \in ℕ) \to F (k) = 0) \leftrightarrow ((φ \land j \in ℕ \land \frac{j}{2} \in ℕ) \to F (j) = 0))$
113	112 2	chvarvv	$⊢ (φ \land j \in ℕ \land \frac{j}{2} \in ℕ) \to F (j) = 0$
114	95 99 108 113	syl3anc	$⊢ (φ \land j \in ((1 \dots 2 k - 1) \cap \{n \in ℕ \| \frac{n}{2} \in ℕ\})) \to F (j) = 0$
115	114	sumeq2dv	$⊢ φ \to \sum_{j \in (1 \dots 2 k - 1) \cap \{n \in ℕ \| \frac{n}{2} \in ℕ\}} F (j) = \sum_{j \in (1 \dots 2 k - 1) \cap \{n \in ℕ \| \frac{n}{2} \in ℕ\}} 0$
116		fzfid	$⊢ φ \to (1 \dots 2 k - 1) \in Fin$
117		inss1	$⊢ (1 \dots 2 k - 1) \cap \{n \in ℕ \| \frac{n}{2} \in ℕ\} \subseteq (1 \dots 2 k - 1)$
118	117	a1i	$⊢ φ \to (1 \dots 2 k - 1) \cap \{n \in ℕ \| \frac{n}{2} \in ℕ\} \subseteq (1 \dots 2 k - 1)$
119	116 118	ssfid	$⊢ φ \to (1 \dots 2 k - 1) \cap \{n \in ℕ \| \frac{n}{2} \in ℕ\} \in Fin$
120	119	olcd	$⊢ φ \to ((1 \dots 2 k - 1) \cap \{n \in ℕ \| \frac{n}{2} \in ℕ\} \subseteq ℤ_{\geq C} \lor (1 \dots 2 k - 1) \cap \{n \in ℕ \| \frac{n}{2} \in ℕ\} \in Fin)$
121		sumz	$⊢ ((1 \dots 2 k - 1) \cap \{n \in ℕ \| \frac{n}{2} \in ℕ\} \subseteq ℤ_{\geq C} \lor (1 \dots 2 k - 1) \cap \{n \in ℕ \| \frac{n}{2} \in ℕ\} \in Fin) \to \sum_{j \in (1 \dots 2 k - 1) \cap \{n \in ℕ \| \frac{n}{2} \in ℕ\}} 0 = 0$
122	120 121	syl	$⊢ φ \to \sum_{j \in (1 \dots 2 k - 1) \cap \{n \in ℕ \| \frac{n}{2} \in ℕ\}} 0 = 0$
123	115 122	eqtrd	$⊢ φ \to \sum_{j \in (1 \dots 2 k - 1) \cap \{n \in ℕ \| \frac{n}{2} \in ℕ\}} F (j) = 0$
124	123	adantr	$⊢ (φ \land k \in ℕ) \to \sum_{j \in (1 \dots 2 k - 1) \cap \{n \in ℕ \| \frac{n}{2} \in ℕ\}} F (j) = 0$
125	124	oveq2d	$⊢ (φ \land k \in ℕ) \to \sum_{j \in (1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}} F (j) + \sum_{j \in (1 \dots 2 k - 1) \cap \{n \in ℕ \| \frac{n}{2} \in ℕ\}} F (j) = \sum_{j \in (1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}} F (j) + 0$
126		fzfi	$⊢ (1 \dots 2 k - 1) \in Fin$
127		difss	$⊢ (1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\} \subseteq (1 \dots 2 k - 1)$
128		ssfi	$⊢ ((1 \dots 2 k - 1) \in Fin \land (1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\} \subseteq (1 \dots 2 k - 1)) \to (1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\} \in Fin$
129	126 127 128	mp2an	$⊢ (1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\} \in Fin$
130	129	a1i	$⊢ (φ \land k \in ℕ) \to (1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\} \in Fin$
131	127	sseli	$⊢ j \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \to j \in (1 \dots 2 k - 1)$
132	131 92	sylan2	$⊢ (φ \land j \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\})) \to F (j) \in ℂ$
133	132	adantlr	$⊢ ((φ \land k \in ℕ) \land j \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\})) \to F (j) \in ℂ$
134	130 133	fsumcl	$⊢ (φ \land k \in ℕ) \to \sum_{j \in (1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}} F (j) \in ℂ$
135	134	addridd	$⊢ (φ \land k \in ℕ) \to \sum_{j \in (1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}} F (j) + 0 = \sum_{j \in (1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}} F (j)$
136		fveq2	$⊢ j = i \to F (j) = F (i)$
137	136	cbvsumv	$⊢ \sum_{j \in (1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}} F (j) = \sum_{i \in (1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}} F (i)$
138	135 137	eqtrdi	$⊢ (φ \land k \in ℕ) \to \sum_{j \in (1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}} F (j) + 0 = \sum_{i \in (1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}} F (i)$
139	125 138	eqtrd	$⊢ (φ \land k \in ℕ) \to \sum_{j \in (1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}} F (j) + \sum_{j \in (1 \dots 2 k - 1) \cap \{n \in ℕ \| \frac{n}{2} \in ℕ\}} F (j) = \sum_{i \in (1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}} F (i)$
140		fveq2	$⊢ i = 2 j - 1 \to F (i) = F (2 j - 1)$
141		fzfid	$⊢ (φ \land k \in ℕ) \to (1 \dots k) \in Fin$
142		1zzd	$⊢ (k \in ℕ \land i \in (1 \dots k)) \to 1 \in ℤ$
143	66	adantr	$⊢ (k \in ℕ \land i \in (1 \dots k)) \to 2 k - 1 \in ℤ$
144	31	a1i	$⊢ i \in (1 \dots k) \to 2 \in ℤ$
145		elfzelz	$⊢ i \in (1 \dots k) \to i \in ℤ$
146	144 145	zmulcld	$⊢ i \in (1 \dots k) \to 2 i \in ℤ$
147		1zzd	$⊢ i \in (1 \dots k) \to 1 \in ℤ$
148	146 147	zsubcld	$⊢ i \in (1 \dots k) \to 2 i - 1 \in ℤ$
149	148	adantl	$⊢ (k \in ℕ \land i \in (1 \dots k)) \to 2 i - 1 \in ℤ$
150	26 27	eqtr2i	$⊢ 1 = 2 \cdot 1 - 1$
151		1re	$⊢ 1 \in ℝ$
152	39 151	remulcli	$⊢ 2 \cdot 1 \in ℝ$
153	152	a1i	$⊢ i \in (1 \dots k) \to 2 \cdot 1 \in ℝ$
154	146	zred	$⊢ i \in (1 \dots k) \to 2 i \in ℝ$
155		1red	$⊢ i \in (1 \dots k) \to 1 \in ℝ$
156	145	zred	$⊢ i \in (1 \dots k) \to i \in ℝ$
157	39	a1i	$⊢ i \in (1 \dots k) \to 2 \in ℝ$
158		0le2	$⊢ 0 \leq 2$
159	158	a1i	$⊢ i \in (1 \dots k) \to 0 \leq 2$
160		elfzle1	$⊢ i \in (1 \dots k) \to 1 \leq i$
161	155 156 157 159 160	lemul2ad	$⊢ i \in (1 \dots k) \to 2 \cdot 1 \leq 2 i$
162	153 154 155 161	lesub1dd	$⊢ i \in (1 \dots k) \to 2 \cdot 1 - 1 \leq 2 i - 1$
163	150 162	eqbrtrid	$⊢ i \in (1 \dots k) \to 1 \leq 2 i - 1$
164	163	adantl	$⊢ (k \in ℕ \land i \in (1 \dots k)) \to 1 \leq 2 i - 1$
165	154	adantl	$⊢ (k \in ℕ \land i \in (1 \dots k)) \to 2 i \in ℝ$
166	42	adantr	$⊢ (k \in ℕ \land i \in (1 \dots k)) \to 2 k \in ℝ$
167		1red	$⊢ (k \in ℕ \land i \in (1 \dots k)) \to 1 \in ℝ$
168	156	adantl	$⊢ (k \in ℕ \land i \in (1 \dots k)) \to i \in ℝ$
169	41	adantr	$⊢ (k \in ℕ \land i \in (1 \dots k)) \to k \in ℝ$
170	39	a1i	$⊢ (k \in ℕ \land i \in (1 \dots k)) \to 2 \in ℝ$
171	158	a1i	$⊢ (k \in ℕ \land i \in (1 \dots k)) \to 0 \leq 2$
172		elfzle2	$⊢ i \in (1 \dots k) \to i \leq k$
173	172	adantl	$⊢ (k \in ℕ \land i \in (1 \dots k)) \to i \leq k$
174	168 169 170 171 173	lemul2ad	$⊢ (k \in ℕ \land i \in (1 \dots k)) \to 2 i \leq 2 k$
175	165 166 167 174	lesub1dd	$⊢ (k \in ℕ \land i \in (1 \dots k)) \to 2 i - 1 \leq 2 k - 1$
176	142 143 149 164 175	elfzd	$⊢ (k \in ℕ \land i \in (1 \dots k)) \to 2 i - 1 \in (1 \dots 2 k - 1)$
177	146	zcnd	$⊢ i \in (1 \dots k) \to 2 i \in ℂ$
178		1cnd	$⊢ i \in (1 \dots k) \to 1 \in ℂ$
179		2cnd	$⊢ i \in (1 \dots k) \to 2 \in ℂ$
180		2ne0	$⊢ 2 \neq 0$
181	180	a1i	$⊢ i \in (1 \dots k) \to 2 \neq 0$
182	177 178 179 181	divsubdird	$⊢ i \in (1 \dots k) \to \frac{2 i - 1}{2} = (\frac{2 i}{2}) - (\frac{1}{2})$
183	145	zcnd	$⊢ i \in (1 \dots k) \to i \in ℂ$
184	183 179 181	divcan3d	$⊢ i \in (1 \dots k) \to \frac{2 i}{2} = i$
185	184	oveq1d	$⊢ i \in (1 \dots k) \to (\frac{2 i}{2}) - (\frac{1}{2}) = i - (\frac{1}{2})$
186	182 185	eqtrd	$⊢ i \in (1 \dots k) \to \frac{2 i - 1}{2} = i - (\frac{1}{2})$
187	145 147	zsubcld	$⊢ i \in (1 \dots k) \to i - 1 \in ℤ$
188	157 181	rereccld	$⊢ i \in (1 \dots k) \to \frac{1}{2} \in ℝ$
189		halflt1	$⊢ \frac{1}{2} < 1$
190	189	a1i	$⊢ i \in (1 \dots k) \to \frac{1}{2} < 1$
191	188 155 156 190	ltsub2dd	$⊢ i \in (1 \dots k) \to i - 1 < i - (\frac{1}{2})$
192		2rp	$⊢ 2 \in ℝ^{+}$
193		rpreccl	$⊢ 2 \in ℝ^{+} \to \frac{1}{2} \in ℝ^{+}$
194	192 193	mp1i	$⊢ i \in (1 \dots k) \to \frac{1}{2} \in ℝ^{+}$
195	156 194	ltsubrpd	$⊢ i \in (1 \dots k) \to i - (\frac{1}{2}) < i$
196	183 178	npcand	$⊢ i \in (1 \dots k) \to i - 1 + 1 = i$
197	195 196	breqtrrd	$⊢ i \in (1 \dots k) \to i - (\frac{1}{2}) < i - 1 + 1$
198		btwnnz	$⊢ (i - 1 \in ℤ \land i - 1 < i - (\frac{1}{2}) \land i - (\frac{1}{2}) < i - 1 + 1) \to \neg i - (\frac{1}{2}) \in ℤ$
199	187 191 197 198	syl3anc	$⊢ i \in (1 \dots k) \to \neg i - (\frac{1}{2}) \in ℤ$
200		nnz	$⊢ i - (\frac{1}{2}) \in ℕ \to i - (\frac{1}{2}) \in ℤ$
201	199 200	nsyl	$⊢ i \in (1 \dots k) \to \neg i - (\frac{1}{2}) \in ℕ$
202	186 201	eqneltrd	$⊢ i \in (1 \dots k) \to \neg \frac{2 i - 1}{2} \in ℕ$
203	202	intnand	$⊢ i \in (1 \dots k) \to \neg (2 i - 1 \in ℕ \land \frac{2 i - 1}{2} \in ℕ)$
204		oveq1	$⊢ n = 2 i - 1 \to \frac{n}{2} = \frac{2 i - 1}{2}$
205	204	eleq1d	$⊢ n = 2 i - 1 \to (\frac{n}{2} \in ℕ \leftrightarrow \frac{2 i - 1}{2} \in ℕ)$
206	205	elrab	$⊢ 2 i - 1 \in \{n \in ℕ \| \frac{n}{2} \in ℕ\} \leftrightarrow (2 i - 1 \in ℕ \land \frac{2 i - 1}{2} \in ℕ)$
207	203 206	sylnibr	$⊢ i \in (1 \dots k) \to \neg 2 i - 1 \in \{n \in ℕ \| \frac{n}{2} \in ℕ\}$
208	207	adantl	$⊢ (k \in ℕ \land i \in (1 \dots k)) \to \neg 2 i - 1 \in \{n \in ℕ \| \frac{n}{2} \in ℕ\}$
209	176 208	eldifd	$⊢ (k \in ℕ \land i \in (1 \dots k)) \to 2 i - 1 \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\})$
210	209	fmpttd	$⊢ k \in ℕ \to (i \in (1 \dots k) ⟼ 2 i - 1) : (1 \dots k) ⟶ (1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}$
211		oveq2	$⊢ i = x \to 2 i = 2 x$
212	211	oveq1d	$⊢ i = x \to 2 i - 1 = 2 x - 1$
213		eqidd	$⊢ x \in (1 \dots k) \to (i \in (1 \dots k) ⟼ 2 i - 1) = (i \in (1 \dots k) ⟼ 2 i - 1)$
214		id	$⊢ x \in (1 \dots k) \to x \in (1 \dots k)$
215		ovexd	$⊢ x \in (1 \dots k) \to 2 x - 1 \in V$
216	212 213 214 215	fvmptd4	$⊢ x \in (1 \dots k) \to (i \in (1 \dots k) ⟼ 2 i - 1) (x) = 2 x - 1$
217	216	eqcomd	$⊢ x \in (1 \dots k) \to 2 x - 1 = (i \in (1 \dots k) ⟼ 2 i - 1) (x)$
218	217	ad2antrr	$⊢ ((x \in (1 \dots k) \land y \in (1 \dots k)) \land (i \in (1 \dots k) ⟼ 2 i - 1) (x) = (i \in (1 \dots k) ⟼ 2 i - 1) (y)) \to 2 x - 1 = (i \in (1 \dots k) ⟼ 2 i - 1) (x)$
219		simpr	$⊢ ((x \in (1 \dots k) \land y \in (1 \dots k)) \land (i \in (1 \dots k) ⟼ 2 i - 1) (x) = (i \in (1 \dots k) ⟼ 2 i - 1) (y)) \to (i \in (1 \dots k) ⟼ 2 i - 1) (x) = (i \in (1 \dots k) ⟼ 2 i - 1) (y)$
220		oveq2	$⊢ i = y \to 2 i = 2 y$
221	220	oveq1d	$⊢ i = y \to 2 i - 1 = 2 y - 1$
222		eqidd	$⊢ y \in (1 \dots k) \to (i \in (1 \dots k) ⟼ 2 i - 1) = (i \in (1 \dots k) ⟼ 2 i - 1)$
223		id	$⊢ y \in (1 \dots k) \to y \in (1 \dots k)$
224		ovexd	$⊢ y \in (1 \dots k) \to 2 y - 1 \in V$
225	221 222 223 224	fvmptd4	$⊢ y \in (1 \dots k) \to (i \in (1 \dots k) ⟼ 2 i - 1) (y) = 2 y - 1$
226	225	ad2antlr	$⊢ ((x \in (1 \dots k) \land y \in (1 \dots k)) \land (i \in (1 \dots k) ⟼ 2 i - 1) (x) = (i \in (1 \dots k) ⟼ 2 i - 1) (y)) \to (i \in (1 \dots k) ⟼ 2 i - 1) (y) = 2 y - 1$
227	218 219 226	3eqtrd	$⊢ ((x \in (1 \dots k) \land y \in (1 \dots k)) \land (i \in (1 \dots k) ⟼ 2 i - 1) (x) = (i \in (1 \dots k) ⟼ 2 i - 1) (y)) \to 2 x - 1 = 2 y - 1$
228		2cnd	$⊢ x \in (1 \dots k) \to 2 \in ℂ$
229		elfzelz	$⊢ x \in (1 \dots k) \to x \in ℤ$
230	229	zcnd	$⊢ x \in (1 \dots k) \to x \in ℂ$
231	228 230	mulcld	$⊢ x \in (1 \dots k) \to 2 x \in ℂ$
232	231	ad2antrr	$⊢ ((x \in (1 \dots k) \land y \in (1 \dots k)) \land 2 x - 1 = 2 y - 1) \to 2 x \in ℂ$
233		2cnd	$⊢ y \in (1 \dots k) \to 2 \in ℂ$
234		elfzelz	$⊢ y \in (1 \dots k) \to y \in ℤ$
235	234	zcnd	$⊢ y \in (1 \dots k) \to y \in ℂ$
236	233 235	mulcld	$⊢ y \in (1 \dots k) \to 2 y \in ℂ$
237	236	ad2antlr	$⊢ ((x \in (1 \dots k) \land y \in (1 \dots k)) \land 2 x - 1 = 2 y - 1) \to 2 y \in ℂ$
238		1cnd	$⊢ ((x \in (1 \dots k) \land y \in (1 \dots k)) \land 2 x - 1 = 2 y - 1) \to 1 \in ℂ$
239		simpr	$⊢ ((x \in (1 \dots k) \land y \in (1 \dots k)) \land 2 x - 1 = 2 y - 1) \to 2 x - 1 = 2 y - 1$
240	232 237 238 239	subcan2d	$⊢ ((x \in (1 \dots k) \land y \in (1 \dots k)) \land 2 x - 1 = 2 y - 1) \to 2 x = 2 y$
241	230	ad2antrr	$⊢ ((x \in (1 \dots k) \land y \in (1 \dots k)) \land 2 x = 2 y) \to x \in ℂ$
242	235	ad2antlr	$⊢ ((x \in (1 \dots k) \land y \in (1 \dots k)) \land 2 x = 2 y) \to y \in ℂ$
243		2cnd	$⊢ ((x \in (1 \dots k) \land y \in (1 \dots k)) \land 2 x = 2 y) \to 2 \in ℂ$
244	180	a1i	$⊢ ((x \in (1 \dots k) \land y \in (1 \dots k)) \land 2 x = 2 y) \to 2 \neq 0$
245		simpr	$⊢ ((x \in (1 \dots k) \land y \in (1 \dots k)) \land 2 x = 2 y) \to 2 x = 2 y$
246	241 242 243 244 245	mulcanad	$⊢ ((x \in (1 \dots k) \land y \in (1 \dots k)) \land 2 x = 2 y) \to x = y$
247	240 246	syldan	$⊢ ((x \in (1 \dots k) \land y \in (1 \dots k)) \land 2 x - 1 = 2 y - 1) \to x = y$
248	227 247	syldan	$⊢ ((x \in (1 \dots k) \land y \in (1 \dots k)) \land (i \in (1 \dots k) ⟼ 2 i - 1) (x) = (i \in (1 \dots k) ⟼ 2 i - 1) (y)) \to x = y$
249	248	adantll	$⊢ ((k \in ℕ \land (x \in (1 \dots k) \land y \in (1 \dots k))) \land (i \in (1 \dots k) ⟼ 2 i - 1) (x) = (i \in (1 \dots k) ⟼ 2 i - 1) (y)) \to x = y$
250	249	ex	$⊢ (k \in ℕ \land (x \in (1 \dots k) \land y \in (1 \dots k))) \to ((i \in (1 \dots k) ⟼ 2 i - 1) (x) = (i \in (1 \dots k) ⟼ 2 i - 1) (y) \to x = y)$
251	250	ralrimivva	$⊢ k \in ℕ \to \forall x \in (1 \dots k) \forall y \in (1 \dots k) ((i \in (1 \dots k) ⟼ 2 i - 1) (x) = (i \in (1 \dots k) ⟼ 2 i - 1) (y) \to x = y)$
252		dff13	$⊢ (i \in (1 \dots k) ⟼ 2 i - 1) : (1 \dots k) \underset{1-1}{⟶} (1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\} \leftrightarrow ((i \in (1 \dots k) ⟼ 2 i - 1) : (1 \dots k) ⟶ (1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\} \land \forall x \in (1 \dots k) \forall y \in (1 \dots k) ((i \in (1 \dots k) ⟼ 2 i - 1) (x) = (i \in (1 \dots k) ⟼ 2 i - 1) (y) \to x = y))$
253	210 251 252	sylanbrc	$⊢ k \in ℕ \to (i \in (1 \dots k) ⟼ 2 i - 1) : (1 \dots k) \underset{1-1}{⟶} (1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}$
254		1zzd	$⊢ (k \in ℕ \land j \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\})) \to 1 \in ℤ$
255	33	adantr	$⊢ (k \in ℕ \land j \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\})) \to k \in ℤ$
256	131	elfzelzd	$⊢ j \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \to j \in ℤ$
257		zeo	$⊢ j \in ℤ \to (\frac{j}{2} \in ℤ \lor \frac{j + 1}{2} \in ℤ)$
258	256 257	syl	$⊢ j \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \to (\frac{j}{2} \in ℤ \lor \frac{j + 1}{2} \in ℤ)$
259	258	adantl	$⊢ (k \in ℕ \land j \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\})) \to (\frac{j}{2} \in ℤ \lor \frac{j + 1}{2} \in ℤ)$
260		eldifn	$⊢ j \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \to \neg j \in \{n \in ℕ \| \frac{n}{2} \in ℕ\}$
261		oveq1	$⊢ n = j \to \frac{n}{2} = \frac{j}{2}$
262	261	eleq1d	$⊢ n = j \to (\frac{n}{2} \in ℕ \leftrightarrow \frac{j}{2} \in ℕ)$
263	131 90	syl	$⊢ j \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \to j \in ℕ$
264	263	adantr	$⊢ (j \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \land \frac{j}{2} \in ℤ) \to j \in ℕ$
265		simpr	$⊢ (j \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \land \frac{j}{2} \in ℤ) \to \frac{j}{2} \in ℤ$
266	264	nnred	$⊢ (j \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \land \frac{j}{2} \in ℤ) \to j \in ℝ$
267	39	a1i	$⊢ (j \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \land \frac{j}{2} \in ℤ) \to 2 \in ℝ$
268	264	nngt0d	$⊢ (j \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \land \frac{j}{2} \in ℤ) \to 0 < j$
269		2pos	$⊢ 0 < 2$
270	269	a1i	$⊢ (j \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \land \frac{j}{2} \in ℤ) \to 0 < 2$
271	266 267 268 270	divgt0d	$⊢ (j \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \land \frac{j}{2} \in ℤ) \to 0 < \frac{j}{2}$
272		elnnz	$⊢ \frac{j}{2} \in ℕ \leftrightarrow (\frac{j}{2} \in ℤ \land 0 < \frac{j}{2})$
273	265 271 272	sylanbrc	$⊢ (j \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \land \frac{j}{2} \in ℤ) \to \frac{j}{2} \in ℕ$
274	262 264 273	elrabd	$⊢ (j \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \land \frac{j}{2} \in ℤ) \to j \in \{n \in ℕ \| \frac{n}{2} \in ℕ\}$
275	260 274	mtand	$⊢ j \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \to \neg \frac{j}{2} \in ℤ$
276	275	adantl	$⊢ (k \in ℕ \land j \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\})) \to \neg \frac{j}{2} \in ℤ$
277	259 276	orcnd	$⊢ (k \in ℕ \land j \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\})) \to \frac{j + 1}{2} \in ℤ$
278		1p1e2	$⊢ 1 + 1 = 2$
279	278	oveq1i	$⊢ \frac{1 + 1}{2} = \frac{2}{2}$
280		2div2e1	$⊢ \frac{2}{2} = 1$
281	279 280	eqtr2i	$⊢ 1 = \frac{1 + 1}{2}$
282		1red	$⊢ j \in (1 \dots 2 k - 1) \to 1 \in ℝ$
283	282 282	readdcld	$⊢ j \in (1 \dots 2 k - 1) \to 1 + 1 \in ℝ$
284	90	nnred	$⊢ j \in (1 \dots 2 k - 1) \to j \in ℝ$
285	284 282	readdcld	$⊢ j \in (1 \dots 2 k - 1) \to j + 1 \in ℝ$
286	192	a1i	$⊢ j \in (1 \dots 2 k - 1) \to 2 \in ℝ^{+}$
287		elfzle1	$⊢ j \in (1 \dots 2 k - 1) \to 1 \leq j$
288	282 284 282 287	leadd1dd	$⊢ j \in (1 \dots 2 k - 1) \to 1 + 1 \leq j + 1$
289	283 285 286 288	lediv1dd	$⊢ j \in (1 \dots 2 k - 1) \to \frac{1 + 1}{2} \leq \frac{j + 1}{2}$
290	281 289	eqbrtrid	$⊢ j \in (1 \dots 2 k - 1) \to 1 \leq \frac{j + 1}{2}$
291	131 290	syl	$⊢ j \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \to 1 \leq \frac{j + 1}{2}$
292	291	adantl	$⊢ (k \in ℕ \land j \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\})) \to 1 \leq \frac{j + 1}{2}$
293		elfzel2	$⊢ j \in (1 \dots 2 k - 1) \to 2 k - 1 \in ℤ$
294	293	zred	$⊢ j \in (1 \dots 2 k - 1) \to 2 k - 1 \in ℝ$
295	294 282	readdcld	$⊢ j \in (1 \dots 2 k - 1) \to 2 k - 1 + 1 \in ℝ$
296		elfzle2	$⊢ j \in (1 \dots 2 k - 1) \to j \leq 2 k - 1$
297	284 294 282 296	leadd1dd	$⊢ j \in (1 \dots 2 k - 1) \to j + 1 \leq 2 k - 1 + 1$
298	285 295 286 297	lediv1dd	$⊢ j \in (1 \dots 2 k - 1) \to \frac{j + 1}{2} \leq \frac{2 k - 1 + 1}{2}$
299	298	adantl	$⊢ (k \in ℕ \land j \in (1 \dots 2 k - 1)) \to \frac{j + 1}{2} \leq \frac{2 k - 1 + 1}{2}$
300	51	adantr	$⊢ (k \in ℕ \land j \in (1 \dots 2 k - 1)) \to 2 k \in ℂ$
301		1cnd	$⊢ (k \in ℕ \land j \in (1 \dots 2 k - 1)) \to 1 \in ℂ$
302	300 301	npcand	$⊢ (k \in ℕ \land j \in (1 \dots 2 k - 1)) \to 2 k - 1 + 1 = 2 k$
303	302	oveq1d	$⊢ (k \in ℕ \land j \in (1 \dots 2 k - 1)) \to \frac{2 k - 1 + 1}{2} = \frac{2 k}{2}$
304	180	a1i	$⊢ k \in ℕ \to 2 \neq 0$
305	45 44 304	divcan3d	$⊢ k \in ℕ \to \frac{2 k}{2} = k$
306	305	adantr	$⊢ (k \in ℕ \land j \in (1 \dots 2 k - 1)) \to \frac{2 k}{2} = k$
307	303 306	eqtrd	$⊢ (k \in ℕ \land j \in (1 \dots 2 k - 1)) \to \frac{2 k - 1 + 1}{2} = k$
308	299 307	breqtrd	$⊢ (k \in ℕ \land j \in (1 \dots 2 k - 1)) \to \frac{j + 1}{2} \leq k$
309	131 308	sylan2	$⊢ (k \in ℕ \land j \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\})) \to \frac{j + 1}{2} \leq k$
310	254 255 277 292 309	elfzd	$⊢ (k \in ℕ \land j \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\})) \to \frac{j + 1}{2} \in (1 \dots k)$
311	263	nncnd	$⊢ j \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \to j \in ℂ$
312		peano2cn	$⊢ j \in ℂ \to j + 1 \in ℂ$
313		2cnd	$⊢ j \in ℂ \to 2 \in ℂ$
314	180	a1i	$⊢ j \in ℂ \to 2 \neq 0$
315	312 313 314	divcan2d	$⊢ j \in ℂ \to 2 (\frac{j + 1}{2}) = j + 1$
316	315	oveq1d	$⊢ j \in ℂ \to 2 (\frac{j + 1}{2}) - 1 = j + 1 - 1$
317		pncan1	$⊢ j \in ℂ \to j + 1 - 1 = j$
318	316 317	eqtr2d	$⊢ j \in ℂ \to j = 2 (\frac{j + 1}{2}) - 1$
319	311 318	syl	$⊢ j \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \to j = 2 (\frac{j + 1}{2}) - 1$
320	319	adantl	$⊢ (k \in ℕ \land j \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\})) \to j = 2 (\frac{j + 1}{2}) - 1$
321		oveq2	$⊢ m = \frac{j + 1}{2} \to 2 m = 2 (\frac{j + 1}{2})$
322	321	oveq1d	$⊢ m = \frac{j + 1}{2} \to 2 m - 1 = 2 (\frac{j + 1}{2}) - 1$
323	322	rspceeqv	$⊢ (\frac{j + 1}{2} \in (1 \dots k) \land j = 2 (\frac{j + 1}{2}) - 1) \to \exists m \in (1 \dots k) j = 2 m - 1$
324	310 320 323	syl2anc	$⊢ (k \in ℕ \land j \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\})) \to \exists m \in (1 \dots k) j = 2 m - 1$
325		oveq2	$⊢ i = m \to 2 i = 2 m$
326	325	oveq1d	$⊢ i = m \to 2 i - 1 = 2 m - 1$
327		eqidd	$⊢ (m \in (1 \dots k) \land j = 2 m - 1) \to (i \in (1 \dots k) ⟼ 2 i - 1) = (i \in (1 \dots k) ⟼ 2 i - 1)$
328		simpl	$⊢ (m \in (1 \dots k) \land j = 2 m - 1) \to m \in (1 \dots k)$
329		ovexd	$⊢ (m \in (1 \dots k) \land j = 2 m - 1) \to 2 m - 1 \in V$
330	326 327 328 329	fvmptd4	$⊢ (m \in (1 \dots k) \land j = 2 m - 1) \to (i \in (1 \dots k) ⟼ 2 i - 1) (m) = 2 m - 1$
331		id	$⊢ j = 2 m - 1 \to j = 2 m - 1$
332	331	eqcomd	$⊢ j = 2 m - 1 \to 2 m - 1 = j$
333	332	adantl	$⊢ (m \in (1 \dots k) \land j = 2 m - 1) \to 2 m - 1 = j$
334	330 333	eqtr2d	$⊢ (m \in (1 \dots k) \land j = 2 m - 1) \to j = (i \in (1 \dots k) ⟼ 2 i - 1) (m)$
335	334	ex	$⊢ m \in (1 \dots k) \to (j = 2 m - 1 \to j = (i \in (1 \dots k) ⟼ 2 i - 1) (m))$
336	335	adantl	$⊢ ((k \in ℕ \land j \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\})) \land m \in (1 \dots k)) \to (j = 2 m - 1 \to j = (i \in (1 \dots k) ⟼ 2 i - 1) (m))$
337	336	reximdva	$⊢ (k \in ℕ \land j \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\})) \to (\exists m \in (1 \dots k) j = 2 m - 1 \to \exists m \in (1 \dots k) j = (i \in (1 \dots k) ⟼ 2 i - 1) (m))$
338	324 337	mpd	$⊢ (k \in ℕ \land j \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\})) \to \exists m \in (1 \dots k) j = (i \in (1 \dots k) ⟼ 2 i - 1) (m)$
339	338	ralrimiva	$⊢ k \in ℕ \to \forall j \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \exists m \in (1 \dots k) j = (i \in (1 \dots k) ⟼ 2 i - 1) (m)$
340		dffo3	$⊢ (i \in (1 \dots k) ⟼ 2 i - 1) : (1 \dots k) \underset{onto}{⟶} (1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\} \leftrightarrow ((i \in (1 \dots k) ⟼ 2 i - 1) : (1 \dots k) ⟶ (1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\} \land \forall j \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \exists m \in (1 \dots k) j = (i \in (1 \dots k) ⟼ 2 i - 1) (m))$
341	210 339 340	sylanbrc	$⊢ k \in ℕ \to (i \in (1 \dots k) ⟼ 2 i - 1) : (1 \dots k) \underset{onto}{⟶} (1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}$
342		df-f1o	$⊢ (i \in (1 \dots k) ⟼ 2 i - 1) : (1 \dots k) \underset{1-1 onto}{⟶} (1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\} \leftrightarrow ((i \in (1 \dots k) ⟼ 2 i - 1) : (1 \dots k) \underset{1-1}{⟶} (1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\} \land (i \in (1 \dots k) ⟼ 2 i - 1) : (1 \dots k) \underset{onto}{⟶} (1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\})$
343	253 341 342	sylanbrc	$⊢ k \in ℕ \to (i \in (1 \dots k) ⟼ 2 i - 1) : (1 \dots k) \underset{1-1 onto}{⟶} (1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}$
344	343	adantl	$⊢ (φ \land k \in ℕ) \to (i \in (1 \dots k) ⟼ 2 i - 1) : (1 \dots k) \underset{1-1 onto}{⟶} (1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}$
345		oveq2	$⊢ i = j \to 2 i = 2 j$
346	345	oveq1d	$⊢ i = j \to 2 i - 1 = 2 j - 1$
347		eqidd	$⊢ j \in (1 \dots k) \to (i \in (1 \dots k) ⟼ 2 i - 1) = (i \in (1 \dots k) ⟼ 2 i - 1)$
348		id	$⊢ j \in (1 \dots k) \to j \in (1 \dots k)$
349		ovexd	$⊢ j \in (1 \dots k) \to 2 j - 1 \in V$
350	346 347 348 349	fvmptd4	$⊢ j \in (1 \dots k) \to (i \in (1 \dots k) ⟼ 2 i - 1) (j) = 2 j - 1$
351	350	adantl	$⊢ ((φ \land k \in ℕ) \land j \in (1 \dots k)) \to (i \in (1 \dots k) ⟼ 2 i - 1) (j) = 2 j - 1$
352		eleq1w	$⊢ j = i \to (j \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}) \leftrightarrow i \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}))$
353	352	anbi2d	$⊢ j = i \to (((φ \land k \in ℕ) \land j \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\})) \leftrightarrow ((φ \land k \in ℕ) \land i \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\})))$
354	136	eleq1d	$⊢ j = i \to (F (j) \in ℂ \leftrightarrow F (i) \in ℂ)$
355	353 354	imbi12d	$⊢ j = i \to ((((φ \land k \in ℕ) \land j \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\})) \to F (j) \in ℂ) \leftrightarrow (((φ \land k \in ℕ) \land i \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\})) \to F (i) \in ℂ))$
356	355 133	chvarvv	$⊢ ((φ \land k \in ℕ) \land i \in ((1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\})) \to F (i) \in ℂ$
357	140 141 344 351 356	fsumf1o	$⊢ (φ \land k \in ℕ) \to \sum_{i \in (1 \dots 2 k - 1) ∖ \{n \in ℕ \| \frac{n}{2} \in ℕ\}} F (i) = \sum_{j = 1}^{k} F (2 j - 1)$
358	94 139 357	3eqtrrd	$⊢ (φ \land k \in ℕ) \to \sum_{j = 1}^{k} F (2 j - 1) = \sum_{j = 1}^{2 k - 1} F (j)$
359		ovex	$⊢ 2 k - 1 \in V$
360		fvmpt4	$⊢ (k \in ℕ \land 2 k - 1 \in V) \to (k \in ℕ ⟼ 2 k - 1) (k) = 2 k - 1$
361	359 360	mpan2	$⊢ k \in ℕ \to (k \in ℕ ⟼ 2 k - 1) (k) = 2 k - 1$
362	361	oveq2d	$⊢ k \in ℕ \to (1 \dots (k \in ℕ ⟼ 2 k - 1) (k)) = (1 \dots 2 k - 1)$
363	362	eqcomd	$⊢ k \in ℕ \to (1 \dots 2 k - 1) = (1 \dots (k \in ℕ ⟼ 2 k - 1) (k))$
364	363	sumeq1d	$⊢ k \in ℕ \to \sum_{j = 1}^{2 k - 1} F (j) = \sum_{j = 1}^{(k \in ℕ ⟼ 2 k - 1) (k)} F (j)$
365	364	adantl	$⊢ (φ \land k \in ℕ) \to \sum_{j = 1}^{2 k - 1} F (j) = \sum_{j = 1}^{(k \in ℕ ⟼ 2 k - 1) (k)} F (j)$
366	358 365	eqtrd	$⊢ (φ \land k \in ℕ) \to \sum_{j = 1}^{k} F (2 j - 1) = \sum_{j = 1}^{(k \in ℕ ⟼ 2 k - 1) (k)} F (j)$
367		elfznn	$⊢ j \in (1 \dots k) \to j \in ℕ$
368	1	adantr	$⊢ (φ \land j \in (1 \dots k)) \to F : ℕ ⟶ ℂ$
369	31	a1i	$⊢ j \in (1 \dots k) \to 2 \in ℤ$
370		elfzelz	$⊢ j \in (1 \dots k) \to j \in ℤ$
371	369 370	zmulcld	$⊢ j \in (1 \dots k) \to 2 j \in ℤ$
372		1zzd	$⊢ j \in (1 \dots k) \to 1 \in ℤ$
373	371 372	zsubcld	$⊢ j \in (1 \dots k) \to 2 j - 1 \in ℤ$
374		0red	$⊢ j \in (1 \dots k) \to 0 \in ℝ$
375	39	a1i	$⊢ j \in (1 \dots k) \to 2 \in ℝ$
376	25 375	eqeltrid	$⊢ j \in (1 \dots k) \to 2 \cdot 1 \in ℝ$
377		1red	$⊢ j \in (1 \dots k) \to 1 \in ℝ$
378	376 377	resubcld	$⊢ j \in (1 \dots k) \to 2 \cdot 1 - 1 \in ℝ$
379	373	zred	$⊢ j \in (1 \dots k) \to 2 j - 1 \in ℝ$
380		0lt1	$⊢ 0 < 1$
381	150	a1i	$⊢ j \in (1 \dots k) \to 1 = 2 \cdot 1 - 1$
382	380 381	breqtrid	$⊢ j \in (1 \dots k) \to 0 < 2 \cdot 1 - 1$
383	371	zred	$⊢ j \in (1 \dots k) \to 2 j \in ℝ$
384	367	nnred	$⊢ j \in (1 \dots k) \to j \in ℝ$
385	158	a1i	$⊢ j \in (1 \dots k) \to 0 \leq 2$
386		elfzle1	$⊢ j \in (1 \dots k) \to 1 \leq j$
387	377 384 375 385 386	lemul2ad	$⊢ j \in (1 \dots k) \to 2 \cdot 1 \leq 2 j$
388	376 383 377 387	lesub1dd	$⊢ j \in (1 \dots k) \to 2 \cdot 1 - 1 \leq 2 j - 1$
389	374 378 379 382 388	ltletrd	$⊢ j \in (1 \dots k) \to 0 < 2 j - 1$
390		elnnz	$⊢ 2 j - 1 \in ℕ \leftrightarrow (2 j - 1 \in ℤ \land 0 < 2 j - 1)$
391	373 389 390	sylanbrc	$⊢ j \in (1 \dots k) \to 2 j - 1 \in ℕ$
392	391	adantl	$⊢ (φ \land j \in (1 \dots k)) \to 2 j - 1 \in ℕ$
393	368 392	ffvelcdmd	$⊢ (φ \land j \in (1 \dots k)) \to F (2 j - 1) \in ℂ$
394	393	adantlr	$⊢ ((φ \land k \in ℕ) \land j \in (1 \dots k)) \to F (2 j - 1) \in ℂ$
395	60	fveq2d	$⊢ k = j \to F (2 k - 1) = F (2 j - 1)$
396	395	cbvmptv	$⊢ (k \in ℕ ⟼ F (2 k - 1)) = (j \in ℕ ⟼ F (2 j - 1))$
397	396	fvmpt2	$⊢ (j \in ℕ \land F (2 j - 1) \in ℂ) \to (k \in ℕ ⟼ F (2 k - 1)) (j) = F (2 j - 1)$
398	367 394 397	syl2an2	$⊢ ((φ \land k \in ℕ) \land j \in (1 \dots k)) \to (k \in ℕ ⟼ F (2 k - 1)) (j) = F (2 j - 1)$
399		simpr	$⊢ (φ \land k \in ℕ) \to k \in ℕ$
400	399 11	eleqtrdi	$⊢ (φ \land k \in ℕ) \to k \in ℤ_{\geq 1}$
401	398 400 394	fsumser	$⊢ (φ \land k \in ℕ) \to \sum_{j = 1}^{k} F (2 j - 1) = seq 1 (+ (k \in ℕ ⟼ F (2 k - 1))) (k)$
402		eqidd	$⊢ ((φ \land k \in ℕ) \land j \in (1 \dots (k \in ℕ ⟼ 2 k - 1) (k))) \to F (j) = F (j)$
403	152	a1i	$⊢ k \in ℕ \to 2 \cdot 1 \in ℝ$
404		1red	$⊢ k \in ℕ \to 1 \in ℝ$
405	158	a1i	$⊢ k \in ℕ \to 0 \leq 2$
406		nnge1	$⊢ k \in ℕ \to 1 \leq k$
407	404 41 40 405 406	lemul2ad	$⊢ k \in ℕ \to 2 \cdot 1 \leq 2 k$
408	403 42 404 407	lesub1dd	$⊢ k \in ℕ \to 2 \cdot 1 - 1 \leq 2 k - 1$
409	150 408	eqbrtrid	$⊢ k \in ℕ \to 1 \leq 2 k - 1$
410		eluz2	$⊢ 2 k - 1 \in ℤ_{\geq 1} \leftrightarrow (1 \in ℤ \land 2 k - 1 \in ℤ \land 1 \leq 2 k - 1)$
411	37 66 409 410	syl3anbrc	$⊢ k \in ℕ \to 2 k - 1 \in ℤ_{\geq 1}$
412	68 411	eqeltrd	$⊢ k \in ℕ \to (k \in ℕ ⟼ 2 k - 1) (k) \in ℤ_{\geq 1}$
413	412	adantl	$⊢ (φ \land k \in ℕ) \to (k \in ℕ ⟼ 2 k - 1) (k) \in ℤ_{\geq 1}$
414		simpll	$⊢ ((φ \land k \in ℕ) \land j \in (1 \dots (k \in ℕ ⟼ 2 k - 1) (k))) \to φ$
415		simpr	$⊢ (k \in ℕ \land j \in (1 \dots (k \in ℕ ⟼ 2 k - 1) (k))) \to j \in (1 \dots (k \in ℕ ⟼ 2 k - 1) (k))$
416	362	adantr	$⊢ (k \in ℕ \land j \in (1 \dots (k \in ℕ ⟼ 2 k - 1) (k))) \to (1 \dots (k \in ℕ ⟼ 2 k - 1) (k)) = (1 \dots 2 k - 1)$
417	415 416	eleqtrd	$⊢ (k \in ℕ \land j \in (1 \dots (k \in ℕ ⟼ 2 k - 1) (k))) \to j \in (1 \dots 2 k - 1)$
418	417	adantll	$⊢ ((φ \land k \in ℕ) \land j \in (1 \dots (k \in ℕ ⟼ 2 k - 1) (k))) \to j \in (1 \dots 2 k - 1)$
419	414 418 92	syl2anc	$⊢ ((φ \land k \in ℕ) \land j \in (1 \dots (k \in ℕ ⟼ 2 k - 1) (k))) \to F (j) \in ℂ$
420	402 413 419	fsumser	$⊢ (φ \land k \in ℕ) \to \sum_{j = 1}^{(k \in ℕ ⟼ 2 k - 1) (k)} F (j) = seq 1 (+ F) ((k \in ℕ ⟼ 2 k - 1) (k))$
421	366 401 420	3eqtr3d	$⊢ (φ \land k \in ℕ) \to seq 1 (+ (k \in ℕ ⟼ F (2 k - 1))) (k) = seq 1 (+ F) ((k \in ℕ ⟼ 2 k - 1) (k))$
422	4 5 9 10 11 12 14 17 3 30 72 74 421	climsuse	$⊢ φ \to seq 1 (+ (k \in ℕ ⟼ F (2 k - 1))) ⇝ B$
423		eqidd	$⊢ (φ \land k \in ℕ) \to F (k) = F (k)$
424	11 12 423 15	isum	$⊢ φ \to \sum_{k \in ℕ} F (k) = ⇝ (seq 1 (+ F))$
425		climrel	$⊢ Rel ⇝$
426	425	releldmi	$⊢ seq 1 (+ F) ⇝ B \to seq 1 (+ F) \in dom ⇝$
427	3 426	syl	$⊢ φ \to seq 1 (+ F) \in dom ⇝$
428		climdm	$⊢ seq 1 (+ F) \in dom ⇝ \leftrightarrow seq 1 (+ F) ⇝ ⇝ (seq 1 (+ F))$
429	427 428	sylib	$⊢ φ \to seq 1 (+ F) ⇝ ⇝ (seq 1 (+ F))$
430		climuni	$⊢ (seq 1 (+ F) ⇝ ⇝ (seq 1 (+ F)) \land seq 1 (+ F) ⇝ B) \to ⇝ (seq 1 (+ F)) = B$
431	429 3 430	syl2anc	$⊢ φ \to ⇝ (seq 1 (+ F)) = B$
432	425	a1i	$⊢ φ \to Rel ⇝$
433		releldm	$⊢ (Rel ⇝ \land seq 1 (+ (k \in ℕ ⟼ F (2 k - 1))) ⇝ B) \to seq 1 (+ (k \in ℕ ⟼ F (2 k - 1))) \in dom ⇝$
434	432 422 433	syl2anc	$⊢ φ \to seq 1 (+ (k \in ℕ ⟼ F (2 k - 1))) \in dom ⇝$
435		climdm	$⊢ seq 1 (+ (k \in ℕ ⟼ F (2 k - 1))) \in dom ⇝ \leftrightarrow seq 1 (+ (k \in ℕ ⟼ F (2 k - 1))) ⇝ ⇝ (seq 1 (+ (k \in ℕ ⟼ F (2 k - 1))))$
436	434 435	sylib	$⊢ φ \to seq 1 (+ (k \in ℕ ⟼ F (2 k - 1))) ⇝ ⇝ (seq 1 (+ (k \in ℕ ⟼ F (2 k - 1))))$
437	396	a1i	$⊢ φ \to (k \in ℕ ⟼ F (2 k - 1)) = (j \in ℕ ⟼ F (2 j - 1))$
438	437	seqeq3d	$⊢ φ \to seq 1 (+ (k \in ℕ ⟼ F (2 k - 1))) = seq 1 (+ (j \in ℕ ⟼ F (2 j - 1)))$
439	438	fveq2d	$⊢ φ \to ⇝ (seq 1 (+ (k \in ℕ ⟼ F (2 k - 1)))) = ⇝ (seq 1 (+ (j \in ℕ ⟼ F (2 j - 1))))$
440	436 439	breqtrd	$⊢ φ \to seq 1 (+ (k \in ℕ ⟼ F (2 k - 1))) ⇝ ⇝ (seq 1 (+ (j \in ℕ ⟼ F (2 j - 1))))$
441		climuni	$⊢ (seq 1 (+ (k \in ℕ ⟼ F (2 k - 1))) ⇝ B \land seq 1 (+ (k \in ℕ ⟼ F (2 k - 1))) ⇝ ⇝ (seq 1 (+ (j \in ℕ ⟼ F (2 j - 1))))) \to B = ⇝ (seq 1 (+ (j \in ℕ ⟼ F (2 j - 1))))$
442	422 440 441	syl2anc	$⊢ φ \to B = ⇝ (seq 1 (+ (j \in ℕ ⟼ F (2 j - 1))))$
443		eqcom	$⊢ k = j \leftrightarrow j = k$
444		eqcom	$⊢ F (2 k - 1) = F (2 j - 1) \leftrightarrow F (2 j - 1) = F (2 k - 1)$
445	395 443 444	3imtr3i	$⊢ j = k \to F (2 j - 1) = F (2 k - 1)$
446		eqidd	$⊢ (φ \land k \in ℕ) \to (j \in ℕ ⟼ F (2 j - 1)) = (j \in ℕ ⟼ F (2 j - 1))$
447	1	adantr	$⊢ (φ \land k \in ℕ) \to F : ℕ ⟶ ℂ$
448	11 37 66 409	eluzd	$⊢ k \in ℕ \to 2 k - 1 \in ℕ$
449	448	adantl	$⊢ (φ \land k \in ℕ) \to 2 k - 1 \in ℕ$
450	447 449	ffvelcdmd	$⊢ (φ \land k \in ℕ) \to F (2 k - 1) \in ℂ$
451	445 446 399 450	fvmptd4	$⊢ (φ \land k \in ℕ) \to (j \in ℕ ⟼ F (2 j - 1)) (k) = F (2 k - 1)$
452	11 12 451 450	isum	$⊢ φ \to \sum_{k \in ℕ} F (2 k - 1) = ⇝ (seq 1 (+ (j \in ℕ ⟼ F (2 j - 1))))$
453	442 452	eqtr4d	$⊢ φ \to B = \sum_{k \in ℕ} F (2 k - 1)$
454	424 431 453	3eqtrd	$⊢ φ \to \sum_{k \in ℕ} F (k) = \sum_{k \in ℕ} F (2 k - 1)$
455	422 454	jca	$⊢ φ \to (seq 1 (+ (k \in ℕ ⟼ F (2 k - 1))) ⇝ B \land \sum_{k \in ℕ} F (k) = \sum_{k \in ℕ} F (2 k - 1))$

Metamath Proof Explorer

Theorem sumnnodd

Proof