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