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