sumnnodd - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > sumnnodd		Structured version Visualization version GIF version

Theorem sumnnodd 44797

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

**Hypotheses**
Ref	Expression
sumnnodd.1	⊢ (𝜑 → 𝐹:ℕ⟶ℂ)
sumnnodd.even0	⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ (𝑘 / 2) ∈ ℕ) → (𝐹‘𝑘) = 0)
sumnnodd.sc	⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝐵)

**Assertion**
Ref	Expression
sumnnodd	⊢ (𝜑 → (seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ 𝐵 ∧ Σ𝑘 ∈ ℕ (𝐹‘𝑘) = Σ𝑘 ∈ ℕ (𝐹‘((2 · 𝑘) − 1))))

Distinct variable groups: 𝑘,𝐹 𝜑,𝑘 Allowed substitution hint: 𝐵(𝑘)

Proof of Theorem sumnnodd Dummy variables 𝐶 𝑗 𝑖 𝑛 𝑚 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1909	. . 3 ⊢ Ⅎ𝑘𝜑
2		nfcv 2895	. . 3 ⊢ Ⅎ𝑘seq1( + , 𝐹)
3		nfcv 2895	. . . 4 ⊢ Ⅎ𝑘1
4		nfcv 2895	. . . 4 ⊢ Ⅎ𝑘 +
5		nfmpt1 5246	. . . 4 ⊢ Ⅎ𝑘(𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))
6	3, 4, 5	nfseq 13972	. . 3 ⊢ Ⅎ𝑘seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))))
7		nfmpt1 5246	. . 3 ⊢ Ⅎ𝑘(𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))
8		nnuz 12861	. . 3 ⊢ ℕ = (ℤ_≥‘1)
9		1zzd 12589	. . 3 ⊢ (𝜑 → 1 ∈ ℤ)
10		seqex 13964	. . . 4 ⊢ seq1( + , 𝐹) ∈ V
11	10	a1i 11	. . 3 ⊢ (𝜑 → seq1( + , 𝐹) ∈ V)
12		sumnnodd.1	. . . . . 6 ⊢ (𝜑 → 𝐹:ℕ⟶ℂ)
13	12	ffvelcdmda 7076	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ)
14	8, 9, 13	serf 13992	. . . 4 ⊢ (𝜑 → seq1( + , 𝐹):ℕ⟶ℂ)
15	14	ffvelcdmda 7076	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , 𝐹)‘𝑘) ∈ ℂ)
16		sumnnodd.sc	. . 3 ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝐵)
17		1nn 12219	. . . . . . 7 ⊢ 1 ∈ ℕ
18		oveq2 7409	. . . . . . . . 9 ⊢ (𝑘 = 1 → (2 · 𝑘) = (2 · 1))
19	18	oveq1d 7416	. . . . . . . 8 ⊢ (𝑘 = 1 → ((2 · 𝑘) − 1) = ((2 · 1) − 1))
20		eqid 2724	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1)) = (𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))
21		ovex 7434	. . . . . . . 8 ⊢ ((2 · 1) − 1) ∈ V
22	19, 20, 21	fvmpt 6988	. . . . . . 7 ⊢ (1 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘1) = ((2 · 1) − 1))
23	17, 22	ax-mp 5	. . . . . 6 ⊢ ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘1) = ((2 · 1) − 1)
24		2t1e2 12371	. . . . . . 7 ⊢ (2 · 1) = 2
25	24	oveq1i 7411	. . . . . 6 ⊢ ((2 · 1) − 1) = (2 − 1)
26		2m1e1 12334	. . . . . 6 ⊢ (2 − 1) = 1
27	23, 25, 26	3eqtri 2756	. . . . 5 ⊢ ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘1) = 1
28	27, 17	eqeltri 2821	. . . 4 ⊢ ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘1) ∈ ℕ
29	28	a1i 11	. . 3 ⊢ (𝜑 → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘1) ∈ ℕ)
30		2z 12590	. . . . . . . 8 ⊢ 2 ∈ ℤ
31	30	a1i 11	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → 2 ∈ ℤ)
32		nnz 12575	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
33	31, 32	zmulcld 12668	. . . . . 6 ⊢ (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℤ)
34	32	peano2zd 12665	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℤ)
35	31, 34	zmulcld 12668	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → (2 · (𝑘 + 1)) ∈ ℤ)
36		1zzd 12589	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → 1 ∈ ℤ)
37	35, 36	zsubcld 12667	. . . . . 6 ⊢ (𝑘 ∈ ℕ → ((2 · (𝑘 + 1)) − 1) ∈ ℤ)
38		2re 12282	. . . . . . . . . 10 ⊢ 2 ∈ ℝ
39	38	a1i 11	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → 2 ∈ ℝ)
40		nnre 12215	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
41	39, 40	remulcld 11240	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℝ)
42	41	lep1d 12141	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → (2 · 𝑘) ≤ ((2 · 𝑘) + 1))
43		2cnd 12286	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 2 ∈ ℂ)
44		nncn 12216	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
45		1cnd 11205	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 1 ∈ ℂ)
46	43, 44, 45	adddid 11234	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → (2 · (𝑘 + 1)) = ((2 · 𝑘) + (2 · 1)))
47	24	oveq2i 7412	. . . . . . . . . 10 ⊢ ((2 · 𝑘) + (2 · 1)) = ((2 · 𝑘) + 2)
48	46, 47	eqtrdi 2780	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (2 · (𝑘 + 1)) = ((2 · 𝑘) + 2))
49	48	oveq1d 7416	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → ((2 · (𝑘 + 1)) − 1) = (((2 · 𝑘) + 2) − 1))
50	43, 44	mulcld 11230	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℂ)
51	50, 43, 45	addsubassd 11587	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (((2 · 𝑘) + 2) − 1) = ((2 · 𝑘) + (2 − 1)))
52	26	oveq2i 7412	. . . . . . . . 9 ⊢ ((2 · 𝑘) + (2 − 1)) = ((2 · 𝑘) + 1)
53	52	a1i 11	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → ((2 · 𝑘) + (2 − 1)) = ((2 · 𝑘) + 1))
54	49, 51, 53	3eqtrrd 2769	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) = ((2 · (𝑘 + 1)) − 1))
55	42, 54	breqtrd 5164	. . . . . 6 ⊢ (𝑘 ∈ ℕ → (2 · 𝑘) ≤ ((2 · (𝑘 + 1)) − 1))
56		eluz2 12824	. . . . . 6 ⊢ (((2 · (𝑘 + 1)) − 1) ∈ (ℤ_≥‘(2 · 𝑘)) ↔ ((2 · 𝑘) ∈ ℤ ∧ ((2 · (𝑘 + 1)) − 1) ∈ ℤ ∧ (2 · 𝑘) ≤ ((2 · (𝑘 + 1)) − 1)))
57	33, 37, 55, 56	syl3anbrc 1340	. . . . 5 ⊢ (𝑘 ∈ ℕ → ((2 · (𝑘 + 1)) − 1) ∈ (ℤ_≥‘(2 · 𝑘)))
58		oveq2 7409	. . . . . . . 8 ⊢ (𝑘 = 𝑗 → (2 · 𝑘) = (2 · 𝑗))
59	58	oveq1d 7416	. . . . . . 7 ⊢ (𝑘 = 𝑗 → ((2 · 𝑘) − 1) = ((2 · 𝑗) − 1))
60	59	cbvmptv 5251	. . . . . 6 ⊢ (𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1)) = (𝑗 ∈ ℕ ↦ ((2 · 𝑗) − 1))
61		oveq2 7409	. . . . . . 7 ⊢ (𝑗 = (𝑘 + 1) → (2 · 𝑗) = (2 · (𝑘 + 1)))
62	61	oveq1d 7416	. . . . . 6 ⊢ (𝑗 = (𝑘 + 1) → ((2 · 𝑗) − 1) = ((2 · (𝑘 + 1)) − 1))
63		peano2nn 12220	. . . . . 6 ⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
64	60, 62, 63, 37	fvmptd3 7011	. . . . 5 ⊢ (𝑘 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘(𝑘 + 1)) = ((2 · (𝑘 + 1)) − 1))
65	33, 36	zsubcld 12667	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → ((2 · 𝑘) − 1) ∈ ℤ)
66	20	fvmpt2 6999	. . . . . . . . 9 ⊢ ((𝑘 ∈ ℕ ∧ ((2 · 𝑘) − 1) ∈ ℤ) → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) = ((2 · 𝑘) − 1))
67	65, 66	mpdan 684	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) = ((2 · 𝑘) − 1))
68	67	oveq1d 7416	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → (((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) + 1) = (((2 · 𝑘) − 1) + 1))
69	50, 45	npcand 11571	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → (((2 · 𝑘) − 1) + 1) = (2 · 𝑘))
70	68, 69	eqtrd 2764	. . . . . 6 ⊢ (𝑘 ∈ ℕ → (((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) + 1) = (2 · 𝑘))
71	70	fveq2d 6885	. . . . 5 ⊢ (𝑘 ∈ ℕ → (ℤ_≥‘(((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) + 1)) = (ℤ_≥‘(2 · 𝑘)))
72	57, 64, 71	3eltr4d 2840	. . . 4 ⊢ (𝑘 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘(𝑘 + 1)) ∈ (ℤ_≥‘(((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) + 1)))
73	72	adantl 481	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘(𝑘 + 1)) ∈ (ℤ_≥‘(((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) + 1)))
74		seqex 13964	. . . 4 ⊢ seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ∈ V
75	74	a1i 11	. . 3 ⊢ (𝜑 → seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ∈ V)
76		incom 4193	. . . . . . . . . 10 ⊢ (((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) = (((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
77		inss2 4221	. . . . . . . . . . 11 ⊢ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}
78		ssrin 4225	. . . . . . . . . . 11 ⊢ (((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} → (((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) ⊆ ({𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} ∩ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})))
79	77, 78	ax-mp 5	. . . . . . . . . 10 ⊢ (((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) ⊆ ({𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} ∩ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
80	76, 79	eqsstri 4008	. . . . . . . . 9 ⊢ (((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) ⊆ ({𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} ∩ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
81		disjdif 4463	. . . . . . . . 9 ⊢ ({𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} ∩ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) = ∅
82	80, 81	sseqtri 4010	. . . . . . . 8 ⊢ (((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) ⊆ ∅
83		ss0 4390	. . . . . . . 8 ⊢ ((((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) ⊆ ∅ → (((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) = ∅)
84	82, 83	mp1i 13	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) = ∅)
85		uncom 4145	. . . . . . . . 9 ⊢ (((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∪ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) = (((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∪ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
86		inundif 4470	. . . . . . . . 9 ⊢ (((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∪ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) = (1...((2 · 𝑘) − 1))
87	85, 86	eqtr2i 2753	. . . . . . . 8 ⊢ (1...((2 · 𝑘) − 1)) = (((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∪ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
88	87	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1...((2 · 𝑘) − 1)) = (((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∪ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})))
89		fzfid 13934	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1...((2 · 𝑘) − 1)) ∈ Fin)
90	12	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → 𝐹:ℕ⟶ℂ)
91		elfznn 13526	. . . . . . . . . 10 ⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → 𝑗 ∈ ℕ)
92	91	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → 𝑗 ∈ ℕ)
93	90, 92	ffvelcdmd 7077	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → (𝐹‘𝑗) ∈ ℂ)
94	93	adantlr 712	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → (𝐹‘𝑗) ∈ ℂ)
95	84, 88, 89, 94	fsumsplit 15683	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...((2 · 𝑘) − 1))(𝐹‘𝑗) = (Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗) + Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗)))
96		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → 𝜑)
97		ssrab2 4069	. . . . . . . . . . . . . 14 ⊢ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} ⊆ ℕ
98	77	sseli 3970	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → 𝑗 ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})
99	97, 98	sselid 3972	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → 𝑗 ∈ ℕ)
100	99	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → 𝑗 ∈ ℕ)
101		oveq1 7408	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑗 → (𝑘 / 2) = (𝑗 / 2))
102	101	eleq1d 2810	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑗 → ((𝑘 / 2) ∈ ℕ ↔ (𝑗 / 2) ∈ ℕ))
103		oveq1 7408	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑘 → (𝑛 / 2) = (𝑘 / 2))
104	103	eleq1d 2810	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑘 → ((𝑛 / 2) ∈ ℕ ↔ (𝑘 / 2) ∈ ℕ))
105	104	elrab 3675	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} ↔ (𝑘 ∈ ℕ ∧ (𝑘 / 2) ∈ ℕ))
106	105	simprbi 496	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} → (𝑘 / 2) ∈ ℕ)
107	102, 106	vtoclga 3558	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} → (𝑗 / 2) ∈ ℕ)
108	98, 107	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → (𝑗 / 2) ∈ ℕ)
109	108	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (𝑗 / 2) ∈ ℕ)
110		eleq1w 2808	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑗 → (𝑘 ∈ ℕ ↔ 𝑗 ∈ ℕ))
111	110, 102	3anbi23d 1435	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑗 → ((𝜑 ∧ 𝑘 ∈ ℕ ∧ (𝑘 / 2) ∈ ℕ) ↔ (𝜑 ∧ 𝑗 ∈ ℕ ∧ (𝑗 / 2) ∈ ℕ)))
112		fveqeq2 6890	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑗 → ((𝐹‘𝑘) = 0 ↔ (𝐹‘𝑗) = 0))
113	111, 112	imbi12d 344	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑗 → (((𝜑 ∧ 𝑘 ∈ ℕ ∧ (𝑘 / 2) ∈ ℕ) → (𝐹‘𝑘) = 0) ↔ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ (𝑗 / 2) ∈ ℕ) → (𝐹‘𝑗) = 0)))
114		sumnnodd.even0	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ (𝑘 / 2) ∈ ℕ) → (𝐹‘𝑘) = 0)
115	113, 114	chvarvv 1994	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ (𝑗 / 2) ∈ ℕ) → (𝐹‘𝑗) = 0)
116	96, 100, 109, 115	syl3anc 1368	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (𝐹‘𝑗) = 0)
117	116	sumeq2dv 15645	. . . . . . . . . 10 ⊢ (𝜑 → Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗) = Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})0)
118		fzfid 13934	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1...((2 · 𝑘) − 1)) ∈ Fin)
119		inss1 4220	. . . . . . . . . . . . . 14 ⊢ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ (1...((2 · 𝑘) − 1))
120	119	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ (1...((2 · 𝑘) − 1)))
121		ssfi 9168	. . . . . . . . . . . . 13 ⊢ (((1...((2 · 𝑘) − 1)) ∈ Fin ∧ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ (1...((2 · 𝑘) − 1))) → ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∈ Fin)
122	118, 120, 121	syl2anc 583	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∈ Fin)
123	122	olcd 871	. . . . . . . . . . 11 ⊢ (𝜑 → (((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ (ℤ_≥‘𝐶) ∨ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∈ Fin))
124		sumz 15664	. . . . . . . . . . 11 ⊢ ((((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ (ℤ_≥‘𝐶) ∨ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∈ Fin) → Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})0 = 0)
125	123, 124	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})0 = 0)
126	117, 125	eqtrd 2764	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗) = 0)
127	126	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗) = 0)
128	127	oveq2d 7417	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗) + Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗)) = (Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗) + 0))
129		fzfi 13933	. . . . . . . . . . . 12 ⊢ (1...((2 · 𝑘) − 1)) ∈ Fin
130		difss 4123	. . . . . . . . . . . 12 ⊢ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ (1...((2 · 𝑘) − 1))
131		ssfi 9168	. . . . . . . . . . . 12 ⊢ (((1...((2 · 𝑘) − 1)) ∈ Fin ∧ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ (1...((2 · 𝑘) − 1))) → ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∈ Fin)
132	129, 130, 131	mp2an 689	. . . . . . . . . . 11 ⊢ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∈ Fin
133	132	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∈ Fin)
134	130	sseli 3970	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → 𝑗 ∈ (1...((2 · 𝑘) − 1)))
135	134, 93	sylan2 592	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (𝐹‘𝑗) ∈ ℂ)
136	135	adantlr 712	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (𝐹‘𝑗) ∈ ℂ)
137	133, 136	fsumcl 15675	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗) ∈ ℂ)
138	137	addridd 11410	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗) + 0) = Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗))
139		fveq2 6881	. . . . . . . . 9 ⊢ (𝑗 = 𝑖 → (𝐹‘𝑗) = (𝐹‘𝑖))
140	139	cbvsumv 15638	. . . . . . . 8 ⊢ Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗) = Σ𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑖)
141	138, 140	eqtrdi 2780	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗) + 0) = Σ𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑖))
142	128, 141	eqtrd 2764	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗) + Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗)) = Σ𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑖))
143		fveq2 6881	. . . . . . 7 ⊢ (𝑖 = ((2 · 𝑗) − 1) → (𝐹‘𝑖) = (𝐹‘((2 · 𝑗) − 1)))
144		fzfid 13934	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1...𝑘) ∈ Fin)
145		1zzd 12589	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 1 ∈ ℤ)
146	65	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → ((2 · 𝑘) − 1) ∈ ℤ)
147	30	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (1...𝑘) → 2 ∈ ℤ)
148		elfzelz 13497	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (1...𝑘) → 𝑖 ∈ ℤ)
149	147, 148	zmulcld 12668	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (1...𝑘) → (2 · 𝑖) ∈ ℤ)
150		1zzd 12589	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (1...𝑘) → 1 ∈ ℤ)
151	149, 150	zsubcld 12667	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (1...𝑘) → ((2 · 𝑖) − 1) ∈ ℤ)
152	151	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → ((2 · 𝑖) − 1) ∈ ℤ)
153	25, 26	eqtr2i 2753	. . . . . . . . . . . . . . 15 ⊢ 1 = ((2 · 1) − 1)
154		1re 11210	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℝ
155	38, 154	remulcli 11226	. . . . . . . . . . . . . . . . 17 ⊢ (2 · 1) ∈ ℝ
156	155	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (1...𝑘) → (2 · 1) ∈ ℝ)
157	149	zred 12662	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (1...𝑘) → (2 · 𝑖) ∈ ℝ)
158		1red 11211	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (1...𝑘) → 1 ∈ ℝ)
159	148	zred 12662	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ (1...𝑘) → 𝑖 ∈ ℝ)
160	38	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ (1...𝑘) → 2 ∈ ℝ)
161		0le2 12310	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ≤ 2
162	161	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ (1...𝑘) → 0 ≤ 2)
163		elfzle1 13500	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ (1...𝑘) → 1 ≤ 𝑖)
164	158, 159, 160, 162, 163	lemul2ad 12150	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (1...𝑘) → (2 · 1) ≤ (2 · 𝑖))
165	156, 157, 158, 164	lesub1dd 11826	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (1...𝑘) → ((2 · 1) − 1) ≤ ((2 · 𝑖) − 1))
166	153, 165	eqbrtrid 5173	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (1...𝑘) → 1 ≤ ((2 · 𝑖) − 1))
167	166	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 1 ≤ ((2 · 𝑖) − 1))
168	157	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → (2 · 𝑖) ∈ ℝ)
169	41	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → (2 · 𝑘) ∈ ℝ)
170		1red 11211	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 1 ∈ ℝ)
171	159	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 𝑖 ∈ ℝ)
172	40	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 𝑘 ∈ ℝ)
173	38	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 2 ∈ ℝ)
174	161	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 0 ≤ 2)
175		elfzle2 13501	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (1...𝑘) → 𝑖 ≤ 𝑘)
176	175	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 𝑖 ≤ 𝑘)
177	171, 172, 173, 174, 176	lemul2ad 12150	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → (2 · 𝑖) ≤ (2 · 𝑘))
178	168, 169, 170, 177	lesub1dd 11826	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → ((2 · 𝑖) − 1) ≤ ((2 · 𝑘) − 1))
179	145, 146, 152, 167, 178	elfzd 13488	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → ((2 · 𝑖) − 1) ∈ (1...((2 · 𝑘) − 1)))
180	149	zcnd 12663	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ (1...𝑘) → (2 · 𝑖) ∈ ℂ)
181		1cnd 11205	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ (1...𝑘) → 1 ∈ ℂ)
182		2cnd 12286	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ (1...𝑘) → 2 ∈ ℂ)
183		2ne0 12312	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ≠ 0
184	183	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ (1...𝑘) → 2 ≠ 0)
185	180, 181, 182, 184	divsubdird 12025	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ (1...𝑘) → (((2 · 𝑖) − 1) / 2) = (((2 · 𝑖) / 2) − (1 / 2)))
186	148	zcnd 12663	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ (1...𝑘) → 𝑖 ∈ ℂ)
187	186, 182, 184	divcan3d 11991	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ (1...𝑘) → ((2 · 𝑖) / 2) = 𝑖)
188	187	oveq1d 7416	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ (1...𝑘) → (((2 · 𝑖) / 2) − (1 / 2)) = (𝑖 − (1 / 2)))
189	185, 188	eqtrd 2764	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (1...𝑘) → (((2 · 𝑖) − 1) / 2) = (𝑖 − (1 / 2)))
190	148, 150	zsubcld 12667	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ (1...𝑘) → (𝑖 − 1) ∈ ℤ)
191	160, 184	rereccld 12037	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ (1...𝑘) → (1 / 2) ∈ ℝ)
192		halflt1 12426	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 / 2) < 1
193	192	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ (1...𝑘) → (1 / 2) < 1)
194	191, 158, 159, 193	ltsub2dd 11823	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ (1...𝑘) → (𝑖 − 1) < (𝑖 − (1 / 2)))
195		2rp 12975	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 2 ∈ ℝ⁺
196		rpreccl 12996	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (2 ∈ ℝ⁺ → (1 / 2) ∈ ℝ⁺)
197	195, 196	mp1i 13	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (1...𝑘) → (1 / 2) ∈ ℝ⁺)
198	159, 197	ltsubrpd 13044	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ (1...𝑘) → (𝑖 − (1 / 2)) < 𝑖)
199	186, 181	npcand 11571	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ (1...𝑘) → ((𝑖 − 1) + 1) = 𝑖)
200	198, 199	breqtrrd 5166	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ (1...𝑘) → (𝑖 − (1 / 2)) < ((𝑖 − 1) + 1))
201		btwnnz 12634	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 − 1) ∈ ℤ ∧ (𝑖 − 1) < (𝑖 − (1 / 2)) ∧ (𝑖 − (1 / 2)) < ((𝑖 − 1) + 1)) → ¬ (𝑖 − (1 / 2)) ∈ ℤ)
202	190, 194, 200, 201	syl3anc 1368	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ (1...𝑘) → ¬ (𝑖 − (1 / 2)) ∈ ℤ)
203		nnz 12575	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 − (1 / 2)) ∈ ℕ → (𝑖 − (1 / 2)) ∈ ℤ)
204	202, 203	nsyl 140	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (1...𝑘) → ¬ (𝑖 − (1 / 2)) ∈ ℕ)
205	189, 204	eqneltrd 2845	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (1...𝑘) → ¬ (((2 · 𝑖) − 1) / 2) ∈ ℕ)
206	205	intnand 488	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (1...𝑘) → ¬ (((2 · 𝑖) − 1) ∈ ℕ ∧ (((2 · 𝑖) − 1) / 2) ∈ ℕ))
207		oveq1 7408	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = ((2 · 𝑖) − 1) → (𝑛 / 2) = (((2 · 𝑖) − 1) / 2))
208	207	eleq1d 2810	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = ((2 · 𝑖) − 1) → ((𝑛 / 2) ∈ ℕ ↔ (((2 · 𝑖) − 1) / 2) ∈ ℕ))
209	208	elrab 3675	. . . . . . . . . . . . . 14 ⊢ (((2 · 𝑖) − 1) ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} ↔ (((2 · 𝑖) − 1) ∈ ℕ ∧ (((2 · 𝑖) − 1) / 2) ∈ ℕ))
210	206, 209	sylnibr 329	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (1...𝑘) → ¬ ((2 · 𝑖) − 1) ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})
211	210	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → ¬ ((2 · 𝑖) − 1) ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})
212	179, 211	eldifd 3951	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → ((2 · 𝑖) − 1) ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
213	212	fmpttd 7106	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)⟶((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
214		eqidd 2725	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (1...𝑘) → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)) = (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)))
215		oveq2 7409	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 𝑥 → (2 · 𝑖) = (2 · 𝑥))
216	215	oveq1d 7416	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑥 → ((2 · 𝑖) − 1) = ((2 · 𝑥) − 1))
217	216	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ (1...𝑘) ∧ 𝑖 = 𝑥) → ((2 · 𝑖) − 1) = ((2 · 𝑥) − 1))
218		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (1...𝑘) → 𝑥 ∈ (1...𝑘))
219		ovexd 7436	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (1...𝑘) → ((2 · 𝑥) − 1) ∈ V)
220	214, 217, 218, 219	fvmptd 6995	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (1...𝑘) → ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((2 · 𝑥) − 1))
221	220	eqcomd 2730	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (1...𝑘) → ((2 · 𝑥) − 1) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥))
222	221	ad2antrr 723	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦)) → ((2 · 𝑥) − 1) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥))
223		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦)) → ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦))
224		eqidd 2725	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (1...𝑘) → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)) = (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)))
225		oveq2 7409	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑦 → (2 · 𝑖) = (2 · 𝑦))
226	225	oveq1d 7416	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑦 → ((2 · 𝑖) − 1) = ((2 · 𝑦) − 1))
227	226	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ (1...𝑘) ∧ 𝑖 = 𝑦) → ((2 · 𝑖) − 1) = ((2 · 𝑦) − 1))
228		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (1...𝑘) → 𝑦 ∈ (1...𝑘))
229		ovexd 7436	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (1...𝑘) → ((2 · 𝑦) − 1) ∈ V)
230	224, 227, 228, 229	fvmptd 6995	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ (1...𝑘) → ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦) = ((2 · 𝑦) − 1))
231	230	ad2antlr 724	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦)) → ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦) = ((2 · 𝑦) − 1))
232	222, 223, 231	3eqtrd 2768	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦)) → ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1))
233		2cnd 12286	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (1...𝑘) → 2 ∈ ℂ)
234		elfzelz 13497	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (1...𝑘) → 𝑥 ∈ ℤ)
235	234	zcnd 12663	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (1...𝑘) → 𝑥 ∈ ℂ)
236	233, 235	mulcld 11230	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (1...𝑘) → (2 · 𝑥) ∈ ℂ)
237	236	ad2antrr 723	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1)) → (2 · 𝑥) ∈ ℂ)
238		2cnd 12286	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (1...𝑘) → 2 ∈ ℂ)
239		elfzelz 13497	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (1...𝑘) → 𝑦 ∈ ℤ)
240	239	zcnd 12663	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (1...𝑘) → 𝑦 ∈ ℂ)
241	238, 240	mulcld 11230	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (1...𝑘) → (2 · 𝑦) ∈ ℂ)
242	241	ad2antlr 724	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1)) → (2 · 𝑦) ∈ ℂ)
243		1cnd 11205	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1)) → 1 ∈ ℂ)
244		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1)) → ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1))
245	237, 242, 243, 244	subcan2d 11609	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1)) → (2 · 𝑥) = (2 · 𝑦))
246	235	ad2antrr 723	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ (2 · 𝑥) = (2 · 𝑦)) → 𝑥 ∈ ℂ)
247	240	ad2antlr 724	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ (2 · 𝑥) = (2 · 𝑦)) → 𝑦 ∈ ℂ)
248		2cnd 12286	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ (2 · 𝑥) = (2 · 𝑦)) → 2 ∈ ℂ)
249	183	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ (2 · 𝑥) = (2 · 𝑦)) → 2 ≠ 0)
250		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ (2 · 𝑥) = (2 · 𝑦)) → (2 · 𝑥) = (2 · 𝑦))
251	246, 247, 248, 249, 250	mulcanad 11845	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ (2 · 𝑥) = (2 · 𝑦)) → 𝑥 = 𝑦)
252	245, 251	syldan 590	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1)) → 𝑥 = 𝑦)
253	232, 252	syldan 590	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦)) → 𝑥 = 𝑦)
254	253	adantll 711	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ℕ ∧ (𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘))) ∧ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦)) → 𝑥 = 𝑦)
255	254	ex 412	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ ∧ (𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘))) → (((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦) → 𝑥 = 𝑦))
256	255	ralrimivva 3192	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → ∀𝑥 ∈ (1...𝑘)∀𝑦 ∈ (1...𝑘)(((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦) → 𝑥 = 𝑦))
257		dff13 7246	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)–1-1→((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ↔ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)⟶((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ ∀𝑥 ∈ (1...𝑘)∀𝑦 ∈ (1...𝑘)(((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦) → 𝑥 = 𝑦)))
258	213, 256, 257	sylanbrc 582	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)–1-1→((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
259		1zzd 12589	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → 1 ∈ ℤ)
260	32	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → 𝑘 ∈ ℤ)
261	134	elfzelzd 13498	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → 𝑗 ∈ ℤ)
262		zeo 12644	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ ℤ → ((𝑗 / 2) ∈ ℤ ∨ ((𝑗 + 1) / 2) ∈ ℤ))
263	261, 262	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → ((𝑗 / 2) ∈ ℤ ∨ ((𝑗 + 1) / 2) ∈ ℤ))
264	263	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → ((𝑗 / 2) ∈ ℤ ∨ ((𝑗 + 1) / 2) ∈ ℤ))
265		eldifn 4119	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → ¬ 𝑗 ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})
266	134, 91	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → 𝑗 ∈ ℕ)
267	266	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → 𝑗 ∈ ℕ)
268		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → (𝑗 / 2) ∈ ℤ)
269	267	nnred 12223	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → 𝑗 ∈ ℝ)
270	38	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → 2 ∈ ℝ)
271	267	nngt0d 12257	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → 0 < 𝑗)
272		2pos 12311	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 < 2
273	272	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → 0 < 2)
274	269, 270, 271, 273	divgt0d 12145	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → 0 < (𝑗 / 2))
275		elnnz 12564	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 / 2) ∈ ℕ ↔ ((𝑗 / 2) ∈ ℤ ∧ 0 < (𝑗 / 2)))
276	268, 274, 275	sylanbrc 582	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → (𝑗 / 2) ∈ ℕ)
277		oveq1 7408	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑗 → (𝑛 / 2) = (𝑗 / 2))
278	277	eleq1d 2810	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑗 → ((𝑛 / 2) ∈ ℕ ↔ (𝑗 / 2) ∈ ℕ))
279	278	elrab 3675	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} ↔ (𝑗 ∈ ℕ ∧ (𝑗 / 2) ∈ ℕ))
280	267, 276, 279	sylanbrc 582	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → 𝑗 ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})
281	265, 280	mtand 813	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → ¬ (𝑗 / 2) ∈ ℤ)
282	281	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → ¬ (𝑗 / 2) ∈ ℤ)
283		pm2.53 848	. . . . . . . . . . . . . . 15 ⊢ (((𝑗 / 2) ∈ ℤ ∨ ((𝑗 + 1) / 2) ∈ ℤ) → (¬ (𝑗 / 2) ∈ ℤ → ((𝑗 + 1) / 2) ∈ ℤ))
284	264, 282, 283	sylc 65	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → ((𝑗 + 1) / 2) ∈ ℤ)
285		1p1e2 12333	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 + 1) = 2
286	285	oveq1i 7411	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 + 1) / 2) = (2 / 2)
287		2div2e1 12349	. . . . . . . . . . . . . . . . . 18 ⊢ (2 / 2) = 1
288	286, 287	eqtr2i 2753	. . . . . . . . . . . . . . . . 17 ⊢ 1 = ((1 + 1) / 2)
289		1red 11211	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → 1 ∈ ℝ)
290	289, 289	readdcld 11239	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → (1 + 1) ∈ ℝ)
291	91	nnred 12223	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → 𝑗 ∈ ℝ)
292	291, 289	readdcld 11239	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → (𝑗 + 1) ∈ ℝ)
293	195	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → 2 ∈ ℝ⁺)
294		elfzle1 13500	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → 1 ≤ 𝑗)
295	289, 291, 289, 294	leadd1dd 11824	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → (1 + 1) ≤ (𝑗 + 1))
296	290, 292, 293, 295	lediv1dd 13070	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → ((1 + 1) / 2) ≤ ((𝑗 + 1) / 2))
297	288, 296	eqbrtrid 5173	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → 1 ≤ ((𝑗 + 1) / 2))
298	134, 297	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → 1 ≤ ((𝑗 + 1) / 2))
299	298	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → 1 ≤ ((𝑗 + 1) / 2))
300		elfzel2 13495	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → ((2 · 𝑘) − 1) ∈ ℤ)
301	300	zred 12662	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → ((2 · 𝑘) − 1) ∈ ℝ)
302	301, 289	readdcld 11239	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → (((2 · 𝑘) − 1) + 1) ∈ ℝ)
303		elfzle2 13501	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → 𝑗 ≤ ((2 · 𝑘) − 1))
304	291, 301, 289, 303	leadd1dd 11824	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → (𝑗 + 1) ≤ (((2 · 𝑘) − 1) + 1))
305	292, 302, 293, 304	lediv1dd 13070	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → ((𝑗 + 1) / 2) ≤ ((((2 · 𝑘) − 1) + 1) / 2))
306	305	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → ((𝑗 + 1) / 2) ≤ ((((2 · 𝑘) − 1) + 1) / 2))
307	50	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → (2 · 𝑘) ∈ ℂ)
308		1cnd 11205	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → 1 ∈ ℂ)
309	307, 308	npcand 11571	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → (((2 · 𝑘) − 1) + 1) = (2 · 𝑘))
310	309	oveq1d 7416	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → ((((2 · 𝑘) − 1) + 1) / 2) = ((2 · 𝑘) / 2))
311	183	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℕ → 2 ≠ 0)
312	44, 43, 311	divcan3d 11991	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ → ((2 · 𝑘) / 2) = 𝑘)
313	312	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → ((2 · 𝑘) / 2) = 𝑘)
314	310, 313	eqtrd 2764	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → ((((2 · 𝑘) − 1) + 1) / 2) = 𝑘)
315	306, 314	breqtrd 5164	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → ((𝑗 + 1) / 2) ≤ 𝑘)
316	134, 315	sylan2 592	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → ((𝑗 + 1) / 2) ≤ 𝑘)
317	259, 260, 284, 299, 316	elfzd 13488	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → ((𝑗 + 1) / 2) ∈ (1...𝑘))
318	266	nncnd 12224	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → 𝑗 ∈ ℂ)
319		peano2cn 11382	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ ℂ → (𝑗 + 1) ∈ ℂ)
320		2cnd 12286	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ ℂ → 2 ∈ ℂ)
321	183	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ ℂ → 2 ≠ 0)
322	319, 320, 321	divcan2d 11988	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ ℂ → (2 · ((𝑗 + 1) / 2)) = (𝑗 + 1))
323	322	oveq1d 7416	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ℂ → ((2 · ((𝑗 + 1) / 2)) − 1) = ((𝑗 + 1) − 1))
324		pncan1 11634	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ℂ → ((𝑗 + 1) − 1) = 𝑗)
325	323, 324	eqtr2d 2765	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℂ → 𝑗 = ((2 · ((𝑗 + 1) / 2)) − 1))
326	318, 325	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → 𝑗 = ((2 · ((𝑗 + 1) / 2)) − 1))
327	326	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → 𝑗 = ((2 · ((𝑗 + 1) / 2)) − 1))
328		oveq2 7409	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = ((𝑗 + 1) / 2) → (2 · 𝑚) = (2 · ((𝑗 + 1) / 2)))
329	328	oveq1d 7416	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ((𝑗 + 1) / 2) → ((2 · 𝑚) − 1) = ((2 · ((𝑗 + 1) / 2)) − 1))
330	329	rspceeqv 3625	. . . . . . . . . . . . 13 ⊢ ((((𝑗 + 1) / 2) ∈ (1...𝑘) ∧ 𝑗 = ((2 · ((𝑗 + 1) / 2)) − 1)) → ∃𝑚 ∈ (1...𝑘)𝑗 = ((2 · 𝑚) − 1))
331	317, 327, 330	syl2anc 583	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → ∃𝑚 ∈ (1...𝑘)𝑗 = ((2 · 𝑚) − 1))
332		eqidd 2725	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑚 ∈ (1...𝑘) ∧ 𝑗 = ((2 · 𝑚) − 1)) → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)) = (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)))
333		oveq2 7409	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑚 → (2 · 𝑖) = (2 · 𝑚))
334	333	oveq1d 7416	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑚 → ((2 · 𝑖) − 1) = ((2 · 𝑚) − 1))
335	334	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑚 ∈ (1...𝑘) ∧ 𝑗 = ((2 · 𝑚) − 1)) ∧ 𝑖 = 𝑚) → ((2 · 𝑖) − 1) = ((2 · 𝑚) − 1))
336		simpl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑚 ∈ (1...𝑘) ∧ 𝑗 = ((2 · 𝑚) − 1)) → 𝑚 ∈ (1...𝑘))
337		ovexd 7436	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑚 ∈ (1...𝑘) ∧ 𝑗 = ((2 · 𝑚) − 1)) → ((2 · 𝑚) − 1) ∈ V)
338	332, 335, 336, 337	fvmptd 6995	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 ∈ (1...𝑘) ∧ 𝑗 = ((2 · 𝑚) − 1)) → ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚) = ((2 · 𝑚) − 1))
339		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = ((2 · 𝑚) − 1) → 𝑗 = ((2 · 𝑚) − 1))
340	339	eqcomd 2730	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = ((2 · 𝑚) − 1) → ((2 · 𝑚) − 1) = 𝑗)
341	340	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 ∈ (1...𝑘) ∧ 𝑗 = ((2 · 𝑚) − 1)) → ((2 · 𝑚) − 1) = 𝑗)
342	338, 341	eqtr2d 2765	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 ∈ (1...𝑘) ∧ 𝑗 = ((2 · 𝑚) − 1)) → 𝑗 = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚))
343	342	ex 412	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (1...𝑘) → (𝑗 = ((2 · 𝑚) − 1) → 𝑗 = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚)))
344	343	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) ∧ 𝑚 ∈ (1...𝑘)) → (𝑗 = ((2 · 𝑚) − 1) → 𝑗 = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚)))
345	344	reximdva 3160	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (∃𝑚 ∈ (1...𝑘)𝑗 = ((2 · 𝑚) − 1) → ∃𝑚 ∈ (1...𝑘)𝑗 = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚)))
346	331, 345	mpd 15	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → ∃𝑚 ∈ (1...𝑘)𝑗 = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚))
347	346	ralrimiva 3138	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → ∀𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})∃𝑚 ∈ (1...𝑘)𝑗 = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚))
348		dffo3 7093	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)–onto→((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ↔ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)⟶((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ ∀𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})∃𝑚 ∈ (1...𝑘)𝑗 = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚)))
349	213, 347, 348	sylanbrc 582	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)–onto→((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
350		df-f1o 6540	. . . . . . . . 9 ⊢ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)–1-1-onto→((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ↔ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)–1-1→((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)–onto→((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})))
351	258, 349, 350	sylanbrc 582	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)–1-1-onto→((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
352	351	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)–1-1-onto→((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
353		eqidd 2725	. . . . . . . . 9 ⊢ (𝑗 ∈ (1...𝑘) → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)) = (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)))
354		oveq2 7409	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑗 → (2 · 𝑖) = (2 · 𝑗))
355	354	oveq1d 7416	. . . . . . . . . 10 ⊢ (𝑖 = 𝑗 → ((2 · 𝑖) − 1) = ((2 · 𝑗) − 1))
356	355	adantl 481	. . . . . . . . 9 ⊢ ((𝑗 ∈ (1...𝑘) ∧ 𝑖 = 𝑗) → ((2 · 𝑖) − 1) = ((2 · 𝑗) − 1))
357		id 22	. . . . . . . . 9 ⊢ (𝑗 ∈ (1...𝑘) → 𝑗 ∈ (1...𝑘))
358		ovexd 7436	. . . . . . . . 9 ⊢ (𝑗 ∈ (1...𝑘) → ((2 · 𝑗) − 1) ∈ V)
359	353, 356, 357, 358	fvmptd 6995	. . . . . . . 8 ⊢ (𝑗 ∈ (1...𝑘) → ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑗) = ((2 · 𝑗) − 1))
360	359	adantl 481	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑘)) → ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑗) = ((2 · 𝑗) − 1))
361		eleq1w 2808	. . . . . . . . . 10 ⊢ (𝑗 = 𝑖 → (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ↔ 𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})))
362	361	anbi2d 628	. . . . . . . . 9 ⊢ (𝑗 = 𝑖 → (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) ↔ ((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))))
363	139	eleq1d 2810	. . . . . . . . 9 ⊢ (𝑗 = 𝑖 → ((𝐹‘𝑗) ∈ ℂ ↔ (𝐹‘𝑖) ∈ ℂ))
364	362, 363	imbi12d 344	. . . . . . . 8 ⊢ (𝑗 = 𝑖 → ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (𝐹‘𝑗) ∈ ℂ) ↔ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (𝐹‘𝑖) ∈ ℂ)))
365	364, 136	chvarvv 1994	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (𝐹‘𝑖) ∈ ℂ)
366	143, 144, 352, 360, 365	fsumf1o 15665	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑖) = Σ𝑗 ∈ (1...𝑘)(𝐹‘((2 · 𝑗) − 1)))
367	95, 142, 366	3eqtrrd 2769	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...𝑘)(𝐹‘((2 · 𝑗) − 1)) = Σ𝑗 ∈ (1...((2 · 𝑘) − 1))(𝐹‘𝑗))
368		ovex 7434	. . . . . . . . . 10 ⊢ ((2 · 𝑘) − 1) ∈ V
369	20	fvmpt2 6999	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ ∧ ((2 · 𝑘) − 1) ∈ V) → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) = ((2 · 𝑘) − 1))
370	368, 369	mpan2 688	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) = ((2 · 𝑘) − 1))
371	370	oveq2d 7417	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘)) = (1...((2 · 𝑘) − 1)))
372	371	eqcomd 2730	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → (1...((2 · 𝑘) − 1)) = (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘)))
373	372	sumeq1d 15643	. . . . . 6 ⊢ (𝑘 ∈ ℕ → Σ𝑗 ∈ (1...((2 · 𝑘) − 1))(𝐹‘𝑗) = Σ𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))(𝐹‘𝑗))
374	373	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...((2 · 𝑘) − 1))(𝐹‘𝑗) = Σ𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))(𝐹‘𝑗))
375	367, 374	eqtrd 2764	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...𝑘)(𝐹‘((2 · 𝑗) − 1)) = Σ𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))(𝐹‘𝑗))
376		elfznn 13526	. . . . . . 7 ⊢ (𝑗 ∈ (1...𝑘) → 𝑗 ∈ ℕ)
377	376	adantl 481	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑘)) → 𝑗 ∈ ℕ)
378	12	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑘)) → 𝐹:ℕ⟶ℂ)
379	30	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (1...𝑘) → 2 ∈ ℤ)
380		elfzelz 13497	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (1...𝑘) → 𝑗 ∈ ℤ)
381	379, 380	zmulcld 12668	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (1...𝑘) → (2 · 𝑗) ∈ ℤ)
382		1zzd 12589	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (1...𝑘) → 1 ∈ ℤ)
383	381, 382	zsubcld 12667	. . . . . . . . . 10 ⊢ (𝑗 ∈ (1...𝑘) → ((2 · 𝑗) − 1) ∈ ℤ)
384		0red 11213	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (1...𝑘) → 0 ∈ ℝ)
385	38	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (1...𝑘) → 2 ∈ ℝ)
386	24, 385	eqeltrid 2829	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (1...𝑘) → (2 · 1) ∈ ℝ)
387		1red 11211	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (1...𝑘) → 1 ∈ ℝ)
388	386, 387	resubcld 11638	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (1...𝑘) → ((2 · 1) − 1) ∈ ℝ)
389	383	zred 12662	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (1...𝑘) → ((2 · 𝑗) − 1) ∈ ℝ)
390		0lt1 11732	. . . . . . . . . . . 12 ⊢ 0 < 1
391	153	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (1...𝑘) → 1 = ((2 · 1) − 1))
392	390, 391	breqtrid 5175	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (1...𝑘) → 0 < ((2 · 1) − 1))
393	381	zred 12662	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (1...𝑘) → (2 · 𝑗) ∈ ℝ)
394	376	nnred 12223	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (1...𝑘) → 𝑗 ∈ ℝ)
395	161	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (1...𝑘) → 0 ≤ 2)
396		elfzle1 13500	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (1...𝑘) → 1 ≤ 𝑗)
397	387, 394, 385, 395, 396	lemul2ad 12150	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (1...𝑘) → (2 · 1) ≤ (2 · 𝑗))
398	386, 393, 387, 397	lesub1dd 11826	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (1...𝑘) → ((2 · 1) − 1) ≤ ((2 · 𝑗) − 1))
399	384, 388, 389, 392, 398	ltletrd 11370	. . . . . . . . . 10 ⊢ (𝑗 ∈ (1...𝑘) → 0 < ((2 · 𝑗) − 1))
400		elnnz 12564	. . . . . . . . . 10 ⊢ (((2 · 𝑗) − 1) ∈ ℕ ↔ (((2 · 𝑗) − 1) ∈ ℤ ∧ 0 < ((2 · 𝑗) − 1)))
401	383, 399, 400	sylanbrc 582	. . . . . . . . 9 ⊢ (𝑗 ∈ (1...𝑘) → ((2 · 𝑗) − 1) ∈ ℕ)
402	401	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑘)) → ((2 · 𝑗) − 1) ∈ ℕ)
403	378, 402	ffvelcdmd 7077	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑘)) → (𝐹‘((2 · 𝑗) − 1)) ∈ ℂ)
404	403	adantlr 712	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑘)) → (𝐹‘((2 · 𝑗) − 1)) ∈ ℂ)
405	59	fveq2d 6885	. . . . . . . 8 ⊢ (𝑘 = 𝑗 → (𝐹‘((2 · 𝑘) − 1)) = (𝐹‘((2 · 𝑗) − 1)))
406	405	cbvmptv 5251	. . . . . . 7 ⊢ (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))) = (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1)))
407	406	fvmpt2 6999	. . . . . 6 ⊢ ((𝑗 ∈ ℕ ∧ (𝐹‘((2 · 𝑗) − 1)) ∈ ℂ) → ((𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))‘𝑗) = (𝐹‘((2 · 𝑗) − 1)))
408	377, 404, 407	syl2anc 583	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑘)) → ((𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))‘𝑗) = (𝐹‘((2 · 𝑗) − 1)))
409		simpr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
410	409, 8	eleqtrdi 2835	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ (ℤ_≥‘1))
411	408, 410, 404	fsumser 15672	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...𝑘)(𝐹‘((2 · 𝑗) − 1)) = (seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))))‘𝑘))
412		eqidd 2725	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))) → (𝐹‘𝑗) = (𝐹‘𝑗))
413	155	a1i 11	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → (2 · 1) ∈ ℝ)
414		1red 11211	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 1 ∈ ℝ)
415	161	a1i 11	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 0 ≤ 2)
416		nnge1 12236	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 1 ≤ 𝑘)
417	414, 40, 39, 415, 416	lemul2ad 12150	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → (2 · 1) ≤ (2 · 𝑘))
418	413, 41, 414, 417	lesub1dd 11826	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → ((2 · 1) − 1) ≤ ((2 · 𝑘) − 1))
419	153, 418	eqbrtrid 5173	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → 1 ≤ ((2 · 𝑘) − 1))
420		eluz2 12824	. . . . . . . 8 ⊢ (((2 · 𝑘) − 1) ∈ (ℤ_≥‘1) ↔ (1 ∈ ℤ ∧ ((2 · 𝑘) − 1) ∈ ℤ ∧ 1 ≤ ((2 · 𝑘) − 1)))
421	36, 65, 419, 420	syl3anbrc 1340	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → ((2 · 𝑘) − 1) ∈ (ℤ_≥‘1))
422	67, 421	eqeltrd 2825	. . . . . 6 ⊢ (𝑘 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) ∈ (ℤ_≥‘1))
423	422	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) ∈ (ℤ_≥‘1))
424		simpll 764	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))) → 𝜑)
425		simpr 484	. . . . . . . 8 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))) → 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘)))
426	371	adantr 480	. . . . . . . 8 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))) → (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘)) = (1...((2 · 𝑘) − 1)))
427	425, 426	eleqtrd 2827	. . . . . . 7 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))) → 𝑗 ∈ (1...((2 · 𝑘) − 1)))
428	427	adantll 711	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))) → 𝑗 ∈ (1...((2 · 𝑘) − 1)))
429	424, 428, 93	syl2anc 583	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))) → (𝐹‘𝑗) ∈ ℂ)
430	412, 423, 429	fsumser 15672	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))(𝐹‘𝑗) = (seq1( + , 𝐹)‘((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘)))
431	375, 411, 430	3eqtr3d 2772	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))))‘𝑘) = (seq1( + , 𝐹)‘((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘)))
432	1, 2, 6, 7, 8, 9, 11, 15, 16, 29, 73, 75, 431	climsuse 44775	. 2 ⊢ (𝜑 → seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ 𝐵)
433		eqidd 2725	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = (𝐹‘𝑘))
434	8, 9, 433, 13	isum 15661	. . 3 ⊢ (𝜑 → Σ𝑘 ∈ ℕ (𝐹‘𝑘) = ( ⇝ ‘seq1( + , 𝐹)))
435		climrel 15432	. . . . . . 7 ⊢ Rel ⇝
436	435	releldmi 5937	. . . . . 6 ⊢ (seq1( + , 𝐹) ⇝ 𝐵 → seq1( + , 𝐹) ∈ dom ⇝ )
437	16, 436	syl 17	. . . . 5 ⊢ (𝜑 → seq1( + , 𝐹) ∈ dom ⇝ )
438		climdm 15494	. . . . 5 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ ↔ seq1( + , 𝐹) ⇝ ( ⇝ ‘seq1( + , 𝐹)))
439	437, 438	sylib 217	. . . 4 ⊢ (𝜑 → seq1( + , 𝐹) ⇝ ( ⇝ ‘seq1( + , 𝐹)))
440		climuni 15492	. . . 4 ⊢ ((seq1( + , 𝐹) ⇝ ( ⇝ ‘seq1( + , 𝐹)) ∧ seq1( + , 𝐹) ⇝ 𝐵) → ( ⇝ ‘seq1( + , 𝐹)) = 𝐵)
441	439, 16, 440	syl2anc 583	. . 3 ⊢ (𝜑 → ( ⇝ ‘seq1( + , 𝐹)) = 𝐵)
442	435	a1i 11	. . . . . . . 8 ⊢ (𝜑 → Rel ⇝ )
443		releldm 5933	. . . . . . . 8 ⊢ ((Rel ⇝ ∧ seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ 𝐵) → seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ∈ dom ⇝ )
444	442, 432, 443	syl2anc 583	. . . . . . 7 ⊢ (𝜑 → seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ∈ dom ⇝ )
445		climdm 15494	. . . . . . 7 ⊢ (seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ∈ dom ⇝ ↔ seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ ( ⇝ ‘seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))))))
446	444, 445	sylib 217	. . . . . 6 ⊢ (𝜑 → seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ ( ⇝ ‘seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))))))
447	406	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))) = (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1))))
448	447	seqeq3d 13970	. . . . . . 7 ⊢ (𝜑 → seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) = seq1( + , (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1)))))
449	448	fveq2d 6885	. . . . . 6 ⊢ (𝜑 → ( ⇝ ‘seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))))) = ( ⇝ ‘seq1( + , (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1))))))
450	446, 449	breqtrd 5164	. . . . 5 ⊢ (𝜑 → seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ ( ⇝ ‘seq1( + , (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1))))))
451		climuni 15492	. . . . 5 ⊢ ((seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ 𝐵 ∧ seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ ( ⇝ ‘seq1( + , (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1)))))) → 𝐵 = ( ⇝ ‘seq1( + , (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1))))))
452	432, 450, 451	syl2anc 583	. . . 4 ⊢ (𝜑 → 𝐵 = ( ⇝ ‘seq1( + , (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1))))))
453		eqidd 2725	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1))) = (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1))))
454		eqcom 2731	. . . . . . . 8 ⊢ (𝑘 = 𝑗 ↔ 𝑗 = 𝑘)
455		eqcom 2731	. . . . . . . 8 ⊢ ((𝐹‘((2 · 𝑘) − 1)) = (𝐹‘((2 · 𝑗) − 1)) ↔ (𝐹‘((2 · 𝑗) − 1)) = (𝐹‘((2 · 𝑘) − 1)))
456	405, 454, 455	3imtr3i 291	. . . . . . 7 ⊢ (𝑗 = 𝑘 → (𝐹‘((2 · 𝑗) − 1)) = (𝐹‘((2 · 𝑘) − 1)))
457	456	adantl 481	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 = 𝑘) → (𝐹‘((2 · 𝑗) − 1)) = (𝐹‘((2 · 𝑘) − 1)))
458	12	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐹:ℕ⟶ℂ)
459	421, 8	eleqtrrdi 2836	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → ((2 · 𝑘) − 1) ∈ ℕ)
460	459	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) − 1) ∈ ℕ)
461	458, 460	ffvelcdmd 7077	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘((2 · 𝑘) − 1)) ∈ ℂ)
462	453, 457, 409, 461	fvmptd 6995	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1)))‘𝑘) = (𝐹‘((2 · 𝑘) − 1)))
463	8, 9, 462, 461	isum 15661	. . . 4 ⊢ (𝜑 → Σ𝑘 ∈ ℕ (𝐹‘((2 · 𝑘) − 1)) = ( ⇝ ‘seq1( + , (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1))))))
464	452, 463	eqtr4d 2767	. . 3 ⊢ (𝜑 → 𝐵 = Σ𝑘 ∈ ℕ (𝐹‘((2 · 𝑘) − 1)))
465	434, 441, 464	3eqtrd 2768	. 2 ⊢ (𝜑 → Σ𝑘 ∈ ℕ (𝐹‘𝑘) = Σ𝑘 ∈ ℕ (𝐹‘((2 · 𝑘) − 1)))
466	432, 465	jca 511	1 ⊢ (𝜑 → (seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ 𝐵 ∧ Σ𝑘 ∈ ℕ (𝐹‘𝑘) = Σ𝑘 ∈ ℕ (𝐹‘((2 · 𝑘) − 1))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∨ wo 844 ∧ w3a 1084 = wceq 1533 ∈ wcel 2098 ≠ wne 2932 ∀wral 3053 ∃wrex 3062 {crab 3424 Vcvv 3466 ∖ cdif 3937 ∪ cun 3938 ∩ cin 3939 ⊆ wss 3940 ∅c0 4314 class class class wbr 5138 ↦ cmpt 5221 dom cdm 5666 Rel wrel 5671 ⟶wf 6529 –1-1→wf1 6530 –onto→wfo 6531 –1-1-onto→wf1o 6532 ‘cfv 6533 (class class class)co 7401 Fincfn 8934 ℂcc 11103 ℝcr 11104 0cc0 11105 1c1 11106 + caddc 11108 · cmul 11110 < clt 11244 ≤ cle 11245 − cmin 11440 / cdiv 11867 ℕcn 12208 2c2 12263 ℤcz 12554 ℤ_≥cuz 12818 ℝ⁺crp 12970 ...cfz 13480 seqcseq 13962 ⇝ cli 15424 Σcsu 15628

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2695 ax-rep 5275 ax-sep 5289 ax-nul 5296 ax-pow 5353 ax-pr 5417 ax-un 7718 ax-inf2 9631 ax-cnex 11161 ax-resscn 11162 ax-1cn 11163 ax-icn 11164 ax-addcl 11165 ax-addrcl 11166 ax-mulcl 11167 ax-mulrcl 11168 ax-mulcom 11169 ax-addass 11170 ax-mulass 11171 ax-distr 11172 ax-i2m1 11173 ax-1ne0 11174 ax-1rid 11175 ax-rnegex 11176 ax-rrecex 11177 ax-cnre 11178 ax-pre-lttri 11179 ax-pre-lttrn 11180 ax-pre-ltadd 11181 ax-pre-mulgt0 11182 ax-pre-sup 11183

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2526 df-eu 2555 df-clab 2702 df-cleq 2716 df-clel 2802 df-nfc 2877 df-ne 2933 df-nel 3039 df-ral 3054 df-rex 3063 df-rmo 3368 df-reu 3369 df-rab 3425 df-v 3468 df-sbc 3770 df-csb 3886 df-dif 3943 df-un 3945 df-in 3947 df-ss 3957 df-pss 3959 df-nul 4315 df-if 4521 df-pw 4596 df-sn 4621 df-pr 4623 df-op 4627 df-uni 4900 df-int 4941 df-iun 4989 df-br 5139 df-opab 5201 df-mpt 5222 df-tr 5256 df-id 5564 df-eprel 5570 df-po 5578 df-so 5579 df-fr 5621 df-se 5622 df-we 5623 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-pred 6290 df-ord 6357 df-on 6358 df-lim 6359 df-suc 6360 df-iota 6485 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-isom 6542 df-riota 7357 df-ov 7404 df-oprab 7405 df-mpo 7406 df-om 7849 df-1st 7968 df-2nd 7969 df-frecs 8261 df-wrecs 8292 df-recs 8366 df-rdg 8405 df-1o 8461 df-er 8698 df-en 8935 df-dom 8936 df-sdom 8937 df-fin 8938 df-sup 9432 df-oi 9500 df-card 9929 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11442 df-neg 11443 df-div 11868 df-nn 12209 df-2 12271 df-3 12272 df-n0 12469 df-z 12555 df-uz 12819 df-rp 12971 df-fz 13481 df-fzo 13624 df-seq 13963 df-exp 14024 df-hash 14287 df-cj 15042 df-re 15043 df-im 15044 df-sqrt 15178 df-abs 15179 df-clim 15428 df-sum 15629

This theorem is referenced by: fouriersw 45398

W3C validator