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 46611

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 1947	. . 3 ⊢ Ⅎ𝑘𝜑
2		nfcv 2923	. . 3 ⊢ Ⅎ𝑘seq1( + , 𝐹)
3		nfcv 2923	. . . 4 ⊢ Ⅎ𝑘1
4		nfcv 2923	. . . 4 ⊢ Ⅎ𝑘 +
5		nfmpt1 5204	. . . 4 ⊢ Ⅎ𝑘(𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))
6	3, 4, 5	nfseq 14147	. . 3 ⊢ Ⅎ𝑘seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))))
7		nfmpt1 5204	. . 3 ⊢ Ⅎ𝑘(𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))
8		nnuz 12997	. . 3 ⊢ ℕ = (ℤ_≥‘1)
9		1zzd 12720	. . 3 ⊢ (𝜑 → 1 ∈ ℤ)
10		seqex 14139	. . . 4 ⊢ seq1( + , 𝐹) ∈ V
11	10	a1i 11	. . 3 ⊢ (𝜑 → seq1( + , 𝐹) ∈ V)
12		sumnnodd.1	. . . . . 6 ⊢ (𝜑 → 𝐹:ℕ⟶ℂ)
13	12	ffvelcdmda 7082	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ)
14	8, 9, 13	serf 14166	. . . 4 ⊢ (𝜑 → seq1( + , 𝐹):ℕ⟶ℂ)
15	14	ffvelcdmda 7082	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , 𝐹)‘𝑘) ∈ ℂ)
16		sumnnodd.sc	. . 3 ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝐵)
17		1nn 12339	. . . . . . 7 ⊢ 1 ∈ ℕ
18		oveq2 7426	. . . . . . . . 9 ⊢ (𝑘 = 1 → (2 · 𝑘) = (2 · 1))
19	18	oveq1d 7433	. . . . . . . 8 ⊢ (𝑘 = 1 → ((2 · 𝑘) − 1) = ((2 · 1) − 1))
20		eqid 2761	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1)) = (𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))
21		ovex 7451	. . . . . . . 8 ⊢ ((2 · 1) − 1) ∈ V
22	19, 20, 21	fvmpt 6991	. . . . . . 7 ⊢ (1 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘1) = ((2 · 1) − 1))
23	17, 22	ax-mp 5	. . . . . 6 ⊢ ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘1) = ((2 · 1) − 1)
24		2t1e2 12498	. . . . . . 7 ⊢ (2 · 1) = 2
25	24	oveq1i 7428	. . . . . 6 ⊢ ((2 · 1) − 1) = (2 − 1)
26		2m1e1 12460	. . . . . 6 ⊢ (2 − 1) = 1
27	23, 25, 26	3eqtri 2788	. . . . 5 ⊢ ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘1) = 1
28	27, 17	eqeltri 2857	. . . 4 ⊢ ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘1) ∈ ℕ
29	28	a1i 11	. . 3 ⊢ (𝜑 → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘1) ∈ ℕ)
30		2z 12721	. . . . . . . 8 ⊢ 2 ∈ ℤ
31	30	a1i 11	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → 2 ∈ ℤ)
32		nnz 12707	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
33	31, 32	zmulcld 12802	. . . . . 6 ⊢ (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℤ)
34	32	peano2zd 12799	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℤ)
35	31, 34	zmulcld 12802	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → (2 · (𝑘 + 1)) ∈ ℤ)
36		1zzd 12720	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → 1 ∈ ℤ)
37	35, 36	zsubcld 12801	. . . . . 6 ⊢ (𝑘 ∈ ℕ → ((2 · (𝑘 + 1)) − 1) ∈ ℤ)
38		2re 12410	. . . . . . . . . 10 ⊢ 2 ∈ ℝ
39	38	a1i 11	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → 2 ∈ ℝ)
40		nnre 12335	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
41	39, 40	remulcld 11332	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℝ)
42	41	lep1d 12241	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → (2 · 𝑘) ≤ ((2 · 𝑘) + 1))
43		2cnd 12414	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 2 ∈ ℂ)
44		nncn 12336	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
45		1cnd 11295	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 1 ∈ ℂ)
46	43, 44, 45	adddid 11326	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → (2 · (𝑘 + 1)) = ((2 · 𝑘) + (2 · 1)))
47	24	oveq2i 7429	. . . . . . . . . 10 ⊢ ((2 · 𝑘) + (2 · 1)) = ((2 · 𝑘) + 2)
48	46, 47	eqtrdi 2812	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (2 · (𝑘 + 1)) = ((2 · 𝑘) + 2))
49	48	oveq1d 7433	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → ((2 · (𝑘 + 1)) − 1) = (((2 · 𝑘) + 2) − 1))
50	43, 44	mulcld 11322	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℂ)
51	50, 43, 45	addsubassd 11682	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (((2 · 𝑘) + 2) − 1) = ((2 · 𝑘) + (2 − 1)))
52	26	oveq2i 7429	. . . . . . . . 9 ⊢ ((2 · 𝑘) + (2 − 1)) = ((2 · 𝑘) + 1)
53	52	a1i 11	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → ((2 · 𝑘) + (2 − 1)) = ((2 · 𝑘) + 1))
54	49, 51, 53	3eqtrrd 2801	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) = ((2 · (𝑘 + 1)) − 1))
55	42, 54	breqtrd 5131	. . . . . 6 ⊢ (𝑘 ∈ ℕ → (2 · 𝑘) ≤ ((2 · (𝑘 + 1)) − 1))
56		eluz2 12964	. . . . . 6 ⊢ (((2 · (𝑘 + 1)) − 1) ∈ (ℤ_≥‘(2 · 𝑘)) ↔ ((2 · 𝑘) ∈ ℤ ∧ ((2 · (𝑘 + 1)) − 1) ∈ ℤ ∧ (2 · 𝑘) ≤ ((2 · (𝑘 + 1)) − 1)))
57	33, 37, 55, 56	syl3anbrc 1362	. . . . 5 ⊢ (𝑘 ∈ ℕ → ((2 · (𝑘 + 1)) − 1) ∈ (ℤ_≥‘(2 · 𝑘)))
58		oveq2 7426	. . . . . . . 8 ⊢ (𝑘 = 𝑗 → (2 · 𝑘) = (2 · 𝑗))
59	58	oveq1d 7433	. . . . . . 7 ⊢ (𝑘 = 𝑗 → ((2 · 𝑘) − 1) = ((2 · 𝑗) − 1))
60	59	cbvmptv 5209	. . . . . 6 ⊢ (𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1)) = (𝑗 ∈ ℕ ↦ ((2 · 𝑗) − 1))
61		oveq2 7426	. . . . . . 7 ⊢ (𝑗 = (𝑘 + 1) → (2 · 𝑗) = (2 · (𝑘 + 1)))
62	61	oveq1d 7433	. . . . . 6 ⊢ (𝑗 = (𝑘 + 1) → ((2 · 𝑗) − 1) = ((2 · (𝑘 + 1)) − 1))
63		peano2nn 12340	. . . . . 6 ⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
64	60, 62, 63, 37	fvmptd3 7015	. . . . 5 ⊢ (𝑘 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘(𝑘 + 1)) = ((2 · (𝑘 + 1)) − 1))
65	33, 36	zsubcld 12801	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → ((2 · 𝑘) − 1) ∈ ℤ)
66		fvmpt4 46219	. . . . . . . 8 ⊢ ((𝑘 ∈ ℕ ∧ ((2 · 𝑘) − 1) ∈ ℤ) → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) = ((2 · 𝑘) − 1))
67	65, 66	mpdan 700	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) = ((2 · 𝑘) − 1))
68	50, 45, 67	mvrrsubd 11722	. . . . . 6 ⊢ (𝑘 ∈ ℕ → (((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) + 1) = (2 · 𝑘))
69	68	fveq2d 6887	. . . . 5 ⊢ (𝑘 ∈ ℕ → (ℤ_≥‘(((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) + 1)) = (ℤ_≥‘(2 · 𝑘)))
70	57, 64, 69	3eltr4d 2876	. . . 4 ⊢ (𝑘 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘(𝑘 + 1)) ∈ (ℤ_≥‘(((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) + 1)))
71	70	adantl 487	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘(𝑘 + 1)) ∈ (ℤ_≥‘(((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) + 1)))
72		seqex 14139	. . . 4 ⊢ seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ∈ V
73	72	a1i 11	. . 3 ⊢ (𝜑 → seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ∈ V)
74		incom 4155	. . . . . . . . . 10 ⊢ (((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) = (((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
75		inss2 4183	. . . . . . . . . . 11 ⊢ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}
76		ssrin 4187	. . . . . . . . . . 11 ⊢ (((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} → (((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) ⊆ ({𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} ∩ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})))
77	75, 76	ax-mp 5	. . . . . . . . . 10 ⊢ (((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) ⊆ ({𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} ∩ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
78	74, 77	eqsstri 3977	. . . . . . . . 9 ⊢ (((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) ⊆ ({𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} ∩ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
79		disjdif 4426	. . . . . . . . 9 ⊢ ({𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} ∩ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) = ∅
80	78, 79	sseqtri 3979	. . . . . . . 8 ⊢ (((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) ⊆ ∅
81		ss0 4352	. . . . . . . 8 ⊢ ((((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) ⊆ ∅ → (((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) = ∅)
82	80, 81	mp1i 14	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) = ∅)
83		uncom 4105	. . . . . . . . 9 ⊢ (((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∪ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) = (((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∪ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
84		inundif 4435	. . . . . . . . 9 ⊢ (((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∪ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) = (1...((2 · 𝑘) − 1))
85	83, 84	eqtr2i 2785	. . . . . . . 8 ⊢ (1...((2 · 𝑘) − 1)) = (((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∪ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
86	85	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1...((2 · 𝑘) − 1)) = (((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∪ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})))
87		fzfid 14109	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1...((2 · 𝑘) − 1)) ∈ Fin)
88	12	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → 𝐹:ℕ⟶ℂ)
89		elfznn 13680	. . . . . . . . . 10 ⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → 𝑗 ∈ ℕ)
90	89	adantl 487	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → 𝑗 ∈ ℕ)
91	88, 90	ffvelcdmd 7083	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → (𝐹‘𝑗) ∈ ℂ)
92	91	adantlr 728	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → (𝐹‘𝑗) ∈ ℂ)
93	82, 86, 87, 92	fsumsplit 15900	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...((2 · 𝑘) − 1))(𝐹‘𝑗) = (Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗) + Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗)))
94		simpl 488	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → 𝜑)
95		ssrab2 4028	. . . . . . . . . . . . . 14 ⊢ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} ⊆ ℕ
96	75	sseli 3927	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → 𝑗 ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})
97	95, 96	sselid 3929	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → 𝑗 ∈ ℕ)
98	97	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → 𝑗 ∈ ℕ)
99		oveq1 7425	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑗 → (𝑘 / 2) = (𝑗 / 2))
100	99	eleq1d 2846	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑗 → ((𝑘 / 2) ∈ ℕ ↔ (𝑗 / 2) ∈ ℕ))
101		oveq1 7425	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑘 → (𝑛 / 2) = (𝑘 / 2))
102	101	eleq1d 2846	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑘 → ((𝑛 / 2) ∈ ℕ ↔ (𝑘 / 2) ∈ ℕ))
103	102	elrab 3645	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} ↔ (𝑘 ∈ ℕ ∧ (𝑘 / 2) ∈ ℕ))
104	103	simprbi 503	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} → (𝑘 / 2) ∈ ℕ)
105	100, 104	vtoclga 3537	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} → (𝑗 / 2) ∈ ℕ)
106	96, 105	syl 18	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → (𝑗 / 2) ∈ ℕ)
107	106	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (𝑗 / 2) ∈ ℕ)
108		eleq1w 2844	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑗 → (𝑘 ∈ ℕ ↔ 𝑗 ∈ ℕ))
109	108, 100	3anbi23d 1467	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑗 → ((𝜑 ∧ 𝑘 ∈ ℕ ∧ (𝑘 / 2) ∈ ℕ) ↔ (𝜑 ∧ 𝑗 ∈ ℕ ∧ (𝑗 / 2) ∈ ℕ)))
110		fveqeq2 6892	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑗 → ((𝐹‘𝑘) = 0 ↔ (𝐹‘𝑗) = 0))
111	109, 110	imbi12d 347	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑗 → (((𝜑 ∧ 𝑘 ∈ ℕ ∧ (𝑘 / 2) ∈ ℕ) → (𝐹‘𝑘) = 0) ↔ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ (𝑗 / 2) ∈ ℕ) → (𝐹‘𝑗) = 0)))
112		sumnnodd.even0	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ (𝑘 / 2) ∈ ℕ) → (𝐹‘𝑘) = 0)
113	111, 112	chvarvv 2022	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ (𝑗 / 2) ∈ ℕ) → (𝐹‘𝑗) = 0)
114	94, 98, 107, 113	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (𝐹‘𝑗) = 0)
115	114	sumeq2dv 15862	. . . . . . . . . 10 ⊢ (𝜑 → Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗) = Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})0)
116		fzfid 14109	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1...((2 · 𝑘) − 1)) ∈ Fin)
117		inss1 4182	. . . . . . . . . . . . . 14 ⊢ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ (1...((2 · 𝑘) − 1))
118	117	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ (1...((2 · 𝑘) − 1)))
119	116, 118	ssfid 9253	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∈ Fin)
120	119	olcd 888	. . . . . . . . . . 11 ⊢ (𝜑 → (((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ (ℤ_≥‘𝐶) ∨ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∈ Fin))
121		sumz 15881	. . . . . . . . . . 11 ⊢ ((((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ (ℤ_≥‘𝐶) ∨ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∈ Fin) → Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})0 = 0)
122	120, 121	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})0 = 0)
123	115, 122	eqtrd 2796	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗) = 0)
124	123	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗) = 0)
125	124	oveq2d 7434	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗) + Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗)) = (Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗) + 0))
126		fzfi 14108	. . . . . . . . . . . 12 ⊢ (1...((2 · 𝑘) − 1)) ∈ Fin
127		difss 4083	. . . . . . . . . . . 12 ⊢ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ (1...((2 · 𝑘) − 1))
128		ssfi 9181	. . . . . . . . . . . 12 ⊢ (((1...((2 · 𝑘) − 1)) ∈ Fin ∧ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ (1...((2 · 𝑘) − 1))) → ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∈ Fin)
129	126, 127, 128	mp2an 705	. . . . . . . . . . 11 ⊢ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∈ Fin
130	129	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∈ Fin)
131	127	sseli 3927	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → 𝑗 ∈ (1...((2 · 𝑘) − 1)))
132	131, 91	sylan2 605	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (𝐹‘𝑗) ∈ ℂ)
133	132	adantlr 728	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (𝐹‘𝑗) ∈ ℂ)
134	130, 133	fsumcl 15892	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗) ∈ ℂ)
135	134	addridd 11503	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗) + 0) = Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗))
136		fveq2 6883	. . . . . . . . 9 ⊢ (𝑗 = 𝑖 → (𝐹‘𝑗) = (𝐹‘𝑖))
137	136	cbvsumv 15856	. . . . . . . 8 ⊢ Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗) = Σ𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑖)
138	135, 137	eqtrdi 2812	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗) + 0) = Σ𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑖))
139	125, 138	eqtrd 2796	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗) + Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗)) = Σ𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑖))
140		fveq2 6883	. . . . . . 7 ⊢ (𝑖 = ((2 · 𝑗) − 1) → (𝐹‘𝑖) = (𝐹‘((2 · 𝑗) − 1)))
141		fzfid 14109	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1...𝑘) ∈ Fin)
142		1zzd 12720	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 1 ∈ ℤ)
143	65	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → ((2 · 𝑘) − 1) ∈ ℤ)
144	30	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (1...𝑘) → 2 ∈ ℤ)
145		elfzelz 13649	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (1...𝑘) → 𝑖 ∈ ℤ)
146	144, 145	zmulcld 12802	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (1...𝑘) → (2 · 𝑖) ∈ ℤ)
147		1zzd 12720	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (1...𝑘) → 1 ∈ ℤ)
148	146, 147	zsubcld 12801	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (1...𝑘) → ((2 · 𝑖) − 1) ∈ ℤ)
149	148	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → ((2 · 𝑖) − 1) ∈ ℤ)
150	25, 26	eqtr2i 2785	. . . . . . . . . . . . . . 15 ⊢ 1 = ((2 · 1) − 1)
151		1re 11301	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℝ
152	38, 151	remulcli 11318	. . . . . . . . . . . . . . . . 17 ⊢ (2 · 1) ∈ ℝ
153	152	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (1...𝑘) → (2 · 1) ∈ ℝ)
154	146	zred 12796	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (1...𝑘) → (2 · 𝑖) ∈ ℝ)
155		1red 11302	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (1...𝑘) → 1 ∈ ℝ)
156	145	zred 12796	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ (1...𝑘) → 𝑖 ∈ ℝ)
157	38	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ (1...𝑘) → 2 ∈ ℝ)
158		0le2 12438	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ≤ 2
159	158	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ (1...𝑘) → 0 ≤ 2)
160		elfzle1 13653	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ (1...𝑘) → 1 ≤ 𝑖)
161	155, 156, 157, 159, 160	lemul2ad 12250	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (1...𝑘) → (2 · 1) ≤ (2 · 𝑖))
162	153, 154, 155, 161	lesub1dd 11925	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (1...𝑘) → ((2 · 1) − 1) ≤ ((2 · 𝑖) − 1))
163	150, 162	eqbrtrid 5140	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (1...𝑘) → 1 ≤ ((2 · 𝑖) − 1))
164	163	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 1 ≤ ((2 · 𝑖) − 1))
165	154	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → (2 · 𝑖) ∈ ℝ)
166	41	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → (2 · 𝑘) ∈ ℝ)
167		1red 11302	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 1 ∈ ℝ)
168	156	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 𝑖 ∈ ℝ)
169	40	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 𝑘 ∈ ℝ)
170	38	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 2 ∈ ℝ)
171	158	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 0 ≤ 2)
172		elfzle2 13654	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (1...𝑘) → 𝑖 ≤ 𝑘)
173	172	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 𝑖 ≤ 𝑘)
174	168, 169, 170, 171, 173	lemul2ad 12250	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → (2 · 𝑖) ≤ (2 · 𝑘))
175	165, 166, 167, 174	lesub1dd 11925	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → ((2 · 𝑖) − 1) ≤ ((2 · 𝑘) − 1))
176	142, 143, 149, 164, 175	elfzd 13640	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → ((2 · 𝑖) − 1) ∈ (1...((2 · 𝑘) − 1)))
177	146	zcnd 12797	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ (1...𝑘) → (2 · 𝑖) ∈ ℂ)
178		1cnd 11295	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ (1...𝑘) → 1 ∈ ℂ)
179		2cnd 12414	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ (1...𝑘) → 2 ∈ ℂ)
180		2ne0 12442	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ≠ 0
181	180	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ (1...𝑘) → 2 ≠ 0)
182	177, 178, 179, 181	divsubdird 12125	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ (1...𝑘) → (((2 · 𝑖) − 1) / 2) = (((2 · 𝑖) / 2) − (1 / 2)))
183	145	zcnd 12797	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ (1...𝑘) → 𝑖 ∈ ℂ)
184	183, 179, 181	divcan3d 12091	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ (1...𝑘) → ((2 · 𝑖) / 2) = 𝑖)
185	184	oveq1d 7433	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ (1...𝑘) → (((2 · 𝑖) / 2) − (1 / 2)) = (𝑖 − (1 / 2)))
186	182, 185	eqtrd 2796	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (1...𝑘) → (((2 · 𝑖) − 1) / 2) = (𝑖 − (1 / 2)))
187	145, 147	zsubcld 12801	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ (1...𝑘) → (𝑖 − 1) ∈ ℤ)
188	157, 181	rereccld 12137	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ (1...𝑘) → (1 / 2) ∈ ℝ)
189		halflt1 12556	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 / 2) < 1
190	189	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ (1...𝑘) → (1 / 2) < 1)
191	188, 155, 156, 190	ltsub2dd 11922	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ (1...𝑘) → (𝑖 − 1) < (𝑖 − (1 / 2)))
192		2rp 13118	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 2 ∈ ℝ⁺
193		rpreccl 13141	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (2 ∈ ℝ⁺ → (1 / 2) ∈ ℝ⁺)
194	192, 193	mp1i 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (1...𝑘) → (1 / 2) ∈ ℝ⁺)
195	156, 194	ltsubrpd 13189	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ (1...𝑘) → (𝑖 − (1 / 2)) < 𝑖)
196	183, 178	npcand 11666	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ (1...𝑘) → ((𝑖 − 1) + 1) = 𝑖)
197	195, 196	breqtrrd 5133	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ (1...𝑘) → (𝑖 − (1 / 2)) < ((𝑖 − 1) + 1))
198		btwnnz 12768	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 − 1) ∈ ℤ ∧ (𝑖 − 1) < (𝑖 − (1 / 2)) ∧ (𝑖 − (1 / 2)) < ((𝑖 − 1) + 1)) → ¬ (𝑖 − (1 / 2)) ∈ ℤ)
199	187, 191, 197, 198	syl3anc 1398	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ (1...𝑘) → ¬ (𝑖 − (1 / 2)) ∈ ℤ)
200		nnz 12707	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 − (1 / 2)) ∈ ℕ → (𝑖 − (1 / 2)) ∈ ℤ)
201	199, 200	nsyl 141	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (1...𝑘) → ¬ (𝑖 − (1 / 2)) ∈ ℕ)
202	186, 201	eqneltrd 2881	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (1...𝑘) → ¬ (((2 · 𝑖) − 1) / 2) ∈ ℕ)
203	202	intnand 494	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (1...𝑘) → ¬ (((2 · 𝑖) − 1) ∈ ℕ ∧ (((2 · 𝑖) − 1) / 2) ∈ ℕ))
204		oveq1 7425	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = ((2 · 𝑖) − 1) → (𝑛 / 2) = (((2 · 𝑖) − 1) / 2))
205	204	eleq1d 2846	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = ((2 · 𝑖) − 1) → ((𝑛 / 2) ∈ ℕ ↔ (((2 · 𝑖) − 1) / 2) ∈ ℕ))
206	205	elrab 3645	. . . . . . . . . . . . . 14 ⊢ (((2 · 𝑖) − 1) ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} ↔ (((2 · 𝑖) − 1) ∈ ℕ ∧ (((2 · 𝑖) − 1) / 2) ∈ ℕ))
207	203, 206	sylnibr 332	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (1...𝑘) → ¬ ((2 · 𝑖) − 1) ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})
208	207	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → ¬ ((2 · 𝑖) − 1) ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})
209	176, 208	eldifd 3910	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → ((2 · 𝑖) − 1) ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
210	209	fmpttd 7113	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)⟶((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
211		oveq2 7426	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑥 → (2 · 𝑖) = (2 · 𝑥))
212	211	oveq1d 7433	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑥 → ((2 · 𝑖) − 1) = ((2 · 𝑥) − 1))
213		eqidd 2762	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (1...𝑘) → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)) = (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)))
214		id 23	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (1...𝑘) → 𝑥 ∈ (1...𝑘))
215		ovexd 7453	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (1...𝑘) → ((2 · 𝑥) − 1) ∈ V)
216	212, 213, 214, 215	fvmptd4 7016	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (1...𝑘) → ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((2 · 𝑥) − 1))
217	216	eqcomd 2767	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (1...𝑘) → ((2 · 𝑥) − 1) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥))
218	217	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦)) → ((2 · 𝑥) − 1) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥))
219		simpr 490	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦)) → ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦))
220		oveq2 7426	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑦 → (2 · 𝑖) = (2 · 𝑦))
221	220	oveq1d 7433	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑦 → ((2 · 𝑖) − 1) = ((2 · 𝑦) − 1))
222		eqidd 2762	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (1...𝑘) → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)) = (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)))
223		id 23	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (1...𝑘) → 𝑦 ∈ (1...𝑘))
224		ovexd 7453	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (1...𝑘) → ((2 · 𝑦) − 1) ∈ V)
225	221, 222, 223, 224	fvmptd4 7016	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ (1...𝑘) → ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦) = ((2 · 𝑦) − 1))
226	225	ad2antlr 740	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦)) → ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦) = ((2 · 𝑦) − 1))
227	218, 219, 226	3eqtrd 2800	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦)) → ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1))
228		2cnd 12414	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (1...𝑘) → 2 ∈ ℂ)
229		elfzelz 13649	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (1...𝑘) → 𝑥 ∈ ℤ)
230	229	zcnd 12797	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (1...𝑘) → 𝑥 ∈ ℂ)
231	228, 230	mulcld 11322	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (1...𝑘) → (2 · 𝑥) ∈ ℂ)
232	231	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1)) → (2 · 𝑥) ∈ ℂ)
233		2cnd 12414	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (1...𝑘) → 2 ∈ ℂ)
234		elfzelz 13649	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (1...𝑘) → 𝑦 ∈ ℤ)
235	234	zcnd 12797	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (1...𝑘) → 𝑦 ∈ ℂ)
236	233, 235	mulcld 11322	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (1...𝑘) → (2 · 𝑦) ∈ ℂ)
237	236	ad2antlr 740	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1)) → (2 · 𝑦) ∈ ℂ)
238		1cnd 11295	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1)) → 1 ∈ ℂ)
239		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1)) → ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1))
240	232, 237, 238, 239	subcan2d 11704	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1)) → (2 · 𝑥) = (2 · 𝑦))
241	230	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ (2 · 𝑥) = (2 · 𝑦)) → 𝑥 ∈ ℂ)
242	235	ad2antlr 740	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ (2 · 𝑥) = (2 · 𝑦)) → 𝑦 ∈ ℂ)
243		2cnd 12414	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ (2 · 𝑥) = (2 · 𝑦)) → 2 ∈ ℂ)
244	180	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ (2 · 𝑥) = (2 · 𝑦)) → 2 ≠ 0)
245		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ (2 · 𝑥) = (2 · 𝑦)) → (2 · 𝑥) = (2 · 𝑦))
246	241, 242, 243, 244, 245	mulcanad 11944	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ (2 · 𝑥) = (2 · 𝑦)) → 𝑥 = 𝑦)
247	240, 246	syldan 603	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1)) → 𝑥 = 𝑦)
248	227, 247	syldan 603	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦)) → 𝑥 = 𝑦)
249	248	adantll 727	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ℕ ∧ (𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘))) ∧ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦)) → 𝑥 = 𝑦)
250	249	ex 418	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ ∧ (𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘))) → (((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦) → 𝑥 = 𝑦))
251	250	ralrimivva 3206	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → ∀𝑥 ∈ (1...𝑘)∀𝑦 ∈ (1...𝑘)(((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦) → 𝑥 = 𝑦))
252		dff13 7256	. . . . . . . . . 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))‘𝑦) → 𝑥 = 𝑦)))
253	210, 251, 252	sylanbrc 595	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)–1-1→((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
254		1zzd 12720	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → 1 ∈ ℤ)
255	32	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → 𝑘 ∈ ℤ)
256	131	elfzelzd 13650	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → 𝑗 ∈ ℤ)
257		zeo 12778	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ ℤ → ((𝑗 / 2) ∈ ℤ ∨ ((𝑗 + 1) / 2) ∈ ℤ))
258	256, 257	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → ((𝑗 / 2) ∈ ℤ ∨ ((𝑗 + 1) / 2) ∈ ℤ))
259	258	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → ((𝑗 / 2) ∈ ℤ ∨ ((𝑗 + 1) / 2) ∈ ℤ))
260		eldifn 4079	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → ¬ 𝑗 ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})
261		oveq1 7425	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑗 → (𝑛 / 2) = (𝑗 / 2))
262	261	eleq1d 2846	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑗 → ((𝑛 / 2) ∈ ℕ ↔ (𝑗 / 2) ∈ ℕ))
263	131, 89	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → 𝑗 ∈ ℕ)
264	263	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → 𝑗 ∈ ℕ)
265		simpr 490	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → (𝑗 / 2) ∈ ℤ)
266	264	nnred 12343	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → 𝑗 ∈ ℝ)
267	38	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → 2 ∈ ℝ)
268	264	nngt0d 12380	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → 0 < 𝑗)
269		2pos 12440	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 < 2
270	269	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → 0 < 2)
271	266, 267, 268, 270	divgt0d 12245	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → 0 < (𝑗 / 2))
272		elnnz 12696	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 / 2) ∈ ℕ ↔ ((𝑗 / 2) ∈ ℤ ∧ 0 < (𝑗 / 2)))
273	265, 271, 272	sylanbrc 595	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → (𝑗 / 2) ∈ ℕ)
274	262, 264, 273	elrabd 3647	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → 𝑗 ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})
275	260, 274	mtand 828	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → ¬ (𝑗 / 2) ∈ ℤ)
276	275	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → ¬ (𝑗 / 2) ∈ ℤ)
277	259, 276	orcnd 892	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → ((𝑗 + 1) / 2) ∈ ℤ)
278		1p1e2 12459	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 + 1) = 2
279	278	oveq1i 7428	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 + 1) / 2) = (2 / 2)
280		2div2e1 12476	. . . . . . . . . . . . . . . . . 18 ⊢ (2 / 2) = 1
281	279, 280	eqtr2i 2785	. . . . . . . . . . . . . . . . 17 ⊢ 1 = ((1 + 1) / 2)
282		1red 11302	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → 1 ∈ ℝ)
283	282, 282	readdcld 11331	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → (1 + 1) ∈ ℝ)
284	89	nnred 12343	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → 𝑗 ∈ ℝ)
285	284, 282	readdcld 11331	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → (𝑗 + 1) ∈ ℝ)
286	192	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → 2 ∈ ℝ⁺)
287		elfzle1 13653	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → 1 ≤ 𝑗)
288	282, 284, 282, 287	leadd1dd 11923	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → (1 + 1) ≤ (𝑗 + 1))
289	283, 285, 286, 288	lediv1dd 13215	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → ((1 + 1) / 2) ≤ ((𝑗 + 1) / 2))
290	281, 289	eqbrtrid 5140	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → 1 ≤ ((𝑗 + 1) / 2))
291	131, 290	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → 1 ≤ ((𝑗 + 1) / 2))
292	291	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → 1 ≤ ((𝑗 + 1) / 2))
293		elfzel2 13647	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → ((2 · 𝑘) − 1) ∈ ℤ)
294	293	zred 12796	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → ((2 · 𝑘) − 1) ∈ ℝ)
295	294, 282	readdcld 11331	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → (((2 · 𝑘) − 1) + 1) ∈ ℝ)
296		elfzle2 13654	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → 𝑗 ≤ ((2 · 𝑘) − 1))
297	284, 294, 282, 296	leadd1dd 11923	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → (𝑗 + 1) ≤ (((2 · 𝑘) − 1) + 1))
298	285, 295, 286, 297	lediv1dd 13215	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → ((𝑗 + 1) / 2) ≤ ((((2 · 𝑘) − 1) + 1) / 2))
299	298	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → ((𝑗 + 1) / 2) ≤ ((((2 · 𝑘) − 1) + 1) / 2))
300	50	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → (2 · 𝑘) ∈ ℂ)
301		1cnd 11295	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → 1 ∈ ℂ)
302	300, 301	npcand 11666	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → (((2 · 𝑘) − 1) + 1) = (2 · 𝑘))
303	302	oveq1d 7433	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → ((((2 · 𝑘) − 1) + 1) / 2) = ((2 · 𝑘) / 2))
304	180	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℕ → 2 ≠ 0)
305	44, 43, 304	divcan3d 12091	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ → ((2 · 𝑘) / 2) = 𝑘)
306	305	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → ((2 · 𝑘) / 2) = 𝑘)
307	303, 306	eqtrd 2796	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → ((((2 · 𝑘) − 1) + 1) / 2) = 𝑘)
308	299, 307	breqtrd 5131	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → ((𝑗 + 1) / 2) ≤ 𝑘)
309	131, 308	sylan2 605	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → ((𝑗 + 1) / 2) ≤ 𝑘)
310	254, 255, 277, 292, 309	elfzd 13640	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → ((𝑗 + 1) / 2) ∈ (1...𝑘))
311	263	nncnd 12344	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → 𝑗 ∈ ℂ)
312		peano2cn 11475	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ ℂ → (𝑗 + 1) ∈ ℂ)
313		2cnd 12414	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ ℂ → 2 ∈ ℂ)
314	180	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ ℂ → 2 ≠ 0)
315	312, 313, 314	divcan2d 12088	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ ℂ → (2 · ((𝑗 + 1) / 2)) = (𝑗 + 1))
316	315	oveq1d 7433	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ℂ → ((2 · ((𝑗 + 1) / 2)) − 1) = ((𝑗 + 1) − 1))
317		pncan1 11733	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ℂ → ((𝑗 + 1) − 1) = 𝑗)
318	316, 317	eqtr2d 2797	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℂ → 𝑗 = ((2 · ((𝑗 + 1) / 2)) − 1))
319	311, 318	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → 𝑗 = ((2 · ((𝑗 + 1) / 2)) − 1))
320	319	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → 𝑗 = ((2 · ((𝑗 + 1) / 2)) − 1))
321		oveq2 7426	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = ((𝑗 + 1) / 2) → (2 · 𝑚) = (2 · ((𝑗 + 1) / 2)))
322	321	oveq1d 7433	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ((𝑗 + 1) / 2) → ((2 · 𝑚) − 1) = ((2 · ((𝑗 + 1) / 2)) − 1))
323	322	rspceeqv 3599	. . . . . . . . . . . . 13 ⊢ ((((𝑗 + 1) / 2) ∈ (1...𝑘) ∧ 𝑗 = ((2 · ((𝑗 + 1) / 2)) − 1)) → ∃𝑚 ∈ (1...𝑘)𝑗 = ((2 · 𝑚) − 1))
324	310, 320, 323	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → ∃𝑚 ∈ (1...𝑘)𝑗 = ((2 · 𝑚) − 1))
325		oveq2 7426	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑚 → (2 · 𝑖) = (2 · 𝑚))
326	325	oveq1d 7433	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑚 → ((2 · 𝑖) − 1) = ((2 · 𝑚) − 1))
327		eqidd 2762	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑚 ∈ (1...𝑘) ∧ 𝑗 = ((2 · 𝑚) − 1)) → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)) = (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)))
328		simpl 488	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑚 ∈ (1...𝑘) ∧ 𝑗 = ((2 · 𝑚) − 1)) → 𝑚 ∈ (1...𝑘))
329		ovexd 7453	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑚 ∈ (1...𝑘) ∧ 𝑗 = ((2 · 𝑚) − 1)) → ((2 · 𝑚) − 1) ∈ V)
330	326, 327, 328, 329	fvmptd4 7016	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 ∈ (1...𝑘) ∧ 𝑗 = ((2 · 𝑚) − 1)) → ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚) = ((2 · 𝑚) − 1))
331		id 23	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = ((2 · 𝑚) − 1) → 𝑗 = ((2 · 𝑚) − 1))
332	331	eqcomd 2767	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = ((2 · 𝑚) − 1) → ((2 · 𝑚) − 1) = 𝑗)
333	332	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 ∈ (1...𝑘) ∧ 𝑗 = ((2 · 𝑚) − 1)) → ((2 · 𝑚) − 1) = 𝑗)
334	330, 333	eqtr2d 2797	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 ∈ (1...𝑘) ∧ 𝑗 = ((2 · 𝑚) − 1)) → 𝑗 = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚))
335	334	ex 418	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (1...𝑘) → (𝑗 = ((2 · 𝑚) − 1) → 𝑗 = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚)))
336	335	adantl 487	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) ∧ 𝑚 ∈ (1...𝑘)) → (𝑗 = ((2 · 𝑚) − 1) → 𝑗 = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚)))
337	336	reximdva 3176	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (∃𝑚 ∈ (1...𝑘)𝑗 = ((2 · 𝑚) − 1) → ∃𝑚 ∈ (1...𝑘)𝑗 = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚)))
338	324, 337	mpd 16	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → ∃𝑚 ∈ (1...𝑘)𝑗 = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚))
339	338	ralrimiva 3155	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → ∀𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})∃𝑚 ∈ (1...𝑘)𝑗 = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚))
340		dffo3 7100	. . . . . . . . . 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))‘𝑚)))
341	210, 339, 340	sylanbrc 595	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)–onto→((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
342		df-f1o 6544	. . . . . . . . 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) ∈ ℕ})))
343	253, 341, 342	sylanbrc 595	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)–1-1-onto→((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
344	343	adantl 487	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)–1-1-onto→((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
345		oveq2 7426	. . . . . . . . . 10 ⊢ (𝑖 = 𝑗 → (2 · 𝑖) = (2 · 𝑗))
346	345	oveq1d 7433	. . . . . . . . 9 ⊢ (𝑖 = 𝑗 → ((2 · 𝑖) − 1) = ((2 · 𝑗) − 1))
347		eqidd 2762	. . . . . . . . 9 ⊢ (𝑗 ∈ (1...𝑘) → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)) = (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)))
348		id 23	. . . . . . . . 9 ⊢ (𝑗 ∈ (1...𝑘) → 𝑗 ∈ (1...𝑘))
349		ovexd 7453	. . . . . . . . 9 ⊢ (𝑗 ∈ (1...𝑘) → ((2 · 𝑗) − 1) ∈ V)
350	346, 347, 348, 349	fvmptd4 7016	. . . . . . . 8 ⊢ (𝑗 ∈ (1...𝑘) → ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑗) = ((2 · 𝑗) − 1))
351	350	adantl 487	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑘)) → ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑗) = ((2 · 𝑗) − 1))
352		eleq1w 2844	. . . . . . . . . 10 ⊢ (𝑗 = 𝑖 → (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ↔ 𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})))
353	352	anbi2d 642	. . . . . . . . 9 ⊢ (𝑗 = 𝑖 → (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) ↔ ((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))))
354	136	eleq1d 2846	. . . . . . . . 9 ⊢ (𝑗 = 𝑖 → ((𝐹‘𝑗) ∈ ℂ ↔ (𝐹‘𝑖) ∈ ℂ))
355	353, 354	imbi12d 347	. . . . . . . 8 ⊢ (𝑗 = 𝑖 → ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (𝐹‘𝑗) ∈ ℂ) ↔ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (𝐹‘𝑖) ∈ ℂ)))
356	355, 133	chvarvv 2022	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (𝐹‘𝑖) ∈ ℂ)
357	140, 141, 344, 351, 356	fsumf1o 15882	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑖) = Σ𝑗 ∈ (1...𝑘)(𝐹‘((2 · 𝑗) − 1)))
358	93, 139, 357	3eqtrrd 2801	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...𝑘)(𝐹‘((2 · 𝑗) − 1)) = Σ𝑗 ∈ (1...((2 · 𝑘) − 1))(𝐹‘𝑗))
359		ovex 7451	. . . . . . . . . 10 ⊢ ((2 · 𝑘) − 1) ∈ V
360		fvmpt4 46219	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ ∧ ((2 · 𝑘) − 1) ∈ V) → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) = ((2 · 𝑘) − 1))
361	359, 360	mpan2 704	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) = ((2 · 𝑘) − 1))
362	361	oveq2d 7434	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘)) = (1...((2 · 𝑘) − 1)))
363	362	eqcomd 2767	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → (1...((2 · 𝑘) − 1)) = (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘)))
364	363	sumeq1d 15860	. . . . . 6 ⊢ (𝑘 ∈ ℕ → Σ𝑗 ∈ (1...((2 · 𝑘) − 1))(𝐹‘𝑗) = Σ𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))(𝐹‘𝑗))
365	364	adantl 487	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...((2 · 𝑘) − 1))(𝐹‘𝑗) = Σ𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))(𝐹‘𝑗))
366	358, 365	eqtrd 2796	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...𝑘)(𝐹‘((2 · 𝑗) − 1)) = Σ𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))(𝐹‘𝑗))
367		elfznn 13680	. . . . . 6 ⊢ (𝑗 ∈ (1...𝑘) → 𝑗 ∈ ℕ)
368	12	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑘)) → 𝐹:ℕ⟶ℂ)
369	30	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (1...𝑘) → 2 ∈ ℤ)
370		elfzelz 13649	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (1...𝑘) → 𝑗 ∈ ℤ)
371	369, 370	zmulcld 12802	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (1...𝑘) → (2 · 𝑗) ∈ ℤ)
372		1zzd 12720	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (1...𝑘) → 1 ∈ ℤ)
373	371, 372	zsubcld 12801	. . . . . . . . . 10 ⊢ (𝑗 ∈ (1...𝑘) → ((2 · 𝑗) − 1) ∈ ℤ)
374		0red 11304	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (1...𝑘) → 0 ∈ ℝ)
375	38	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (1...𝑘) → 2 ∈ ℝ)
376	24, 375	eqeltrid 2865	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (1...𝑘) → (2 · 1) ∈ ℝ)
377		1red 11302	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (1...𝑘) → 1 ∈ ℝ)
378	376, 377	resubcld 11737	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (1...𝑘) → ((2 · 1) − 1) ∈ ℝ)
379	373	zred 12796	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (1...𝑘) → ((2 · 𝑗) − 1) ∈ ℝ)
380		0lt1 11831	. . . . . . . . . . . 12 ⊢ 0 < 1
381	150	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (1...𝑘) → 1 = ((2 · 1) − 1))
382	380, 381	breqtrid 5142	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (1...𝑘) → 0 < ((2 · 1) − 1))
383	371	zred 12796	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (1...𝑘) → (2 · 𝑗) ∈ ℝ)
384	367	nnred 12343	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (1...𝑘) → 𝑗 ∈ ℝ)
385	158	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (1...𝑘) → 0 ≤ 2)
386		elfzle1 13653	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (1...𝑘) → 1 ≤ 𝑗)
387	377, 384, 375, 385, 386	lemul2ad 12250	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (1...𝑘) → (2 · 1) ≤ (2 · 𝑗))
388	376, 383, 377, 387	lesub1dd 11925	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (1...𝑘) → ((2 · 1) − 1) ≤ ((2 · 𝑗) − 1))
389	374, 378, 379, 382, 388	ltletrd 11463	. . . . . . . . . 10 ⊢ (𝑗 ∈ (1...𝑘) → 0 < ((2 · 𝑗) − 1))
390		elnnz 12696	. . . . . . . . . 10 ⊢ (((2 · 𝑗) − 1) ∈ ℕ ↔ (((2 · 𝑗) − 1) ∈ ℤ ∧ 0 < ((2 · 𝑗) − 1)))
391	373, 389, 390	sylanbrc 595	. . . . . . . . 9 ⊢ (𝑗 ∈ (1...𝑘) → ((2 · 𝑗) − 1) ∈ ℕ)
392	391	adantl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑘)) → ((2 · 𝑗) − 1) ∈ ℕ)
393	368, 392	ffvelcdmd 7083	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑘)) → (𝐹‘((2 · 𝑗) − 1)) ∈ ℂ)
394	393	adantlr 728	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑘)) → (𝐹‘((2 · 𝑗) − 1)) ∈ ℂ)
395	59	fveq2d 6887	. . . . . . . 8 ⊢ (𝑘 = 𝑗 → (𝐹‘((2 · 𝑘) − 1)) = (𝐹‘((2 · 𝑗) − 1)))
396	395	cbvmptv 5209	. . . . . . 7 ⊢ (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))) = (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1)))
397	396	fvmpt2 7003	. . . . . 6 ⊢ ((𝑗 ∈ ℕ ∧ (𝐹‘((2 · 𝑗) − 1)) ∈ ℂ) → ((𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))‘𝑗) = (𝐹‘((2 · 𝑗) − 1)))
398	367, 394, 397	syl2an2 699	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑘)) → ((𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))‘𝑗) = (𝐹‘((2 · 𝑗) − 1)))
399		simpr 490	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
400	399, 8	eleqtrdi 2871	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ (ℤ_≥‘1))
401	398, 400, 394	fsumser 15889	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...𝑘)(𝐹‘((2 · 𝑗) − 1)) = (seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))))‘𝑘))
402		eqidd 2762	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))) → (𝐹‘𝑗) = (𝐹‘𝑗))
403	152	a1i 11	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → (2 · 1) ∈ ℝ)
404		1red 11302	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 1 ∈ ℝ)
405	158	a1i 11	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 0 ≤ 2)
406		nnge1 12359	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 1 ≤ 𝑘)
407	404, 40, 39, 405, 406	lemul2ad 12250	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → (2 · 1) ≤ (2 · 𝑘))
408	403, 41, 404, 407	lesub1dd 11925	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → ((2 · 1) − 1) ≤ ((2 · 𝑘) − 1))
409	150, 408	eqbrtrid 5140	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → 1 ≤ ((2 · 𝑘) − 1))
410		eluz2 12964	. . . . . . . 8 ⊢ (((2 · 𝑘) − 1) ∈ (ℤ_≥‘1) ↔ (1 ∈ ℤ ∧ ((2 · 𝑘) − 1) ∈ ℤ ∧ 1 ≤ ((2 · 𝑘) − 1)))
411	36, 65, 409, 410	syl3anbrc 1362	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → ((2 · 𝑘) − 1) ∈ (ℤ_≥‘1))
412	67, 411	eqeltrd 2861	. . . . . 6 ⊢ (𝑘 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) ∈ (ℤ_≥‘1))
413	412	adantl 487	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) ∈ (ℤ_≥‘1))
414		simpll 779	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))) → 𝜑)
415		simpr 490	. . . . . . . 8 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))) → 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘)))
416	362	adantr 486	. . . . . . . 8 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))) → (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘)) = (1...((2 · 𝑘) − 1)))
417	415, 416	eleqtrd 2863	. . . . . . 7 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))) → 𝑗 ∈ (1...((2 · 𝑘) − 1)))
418	417	adantll 727	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))) → 𝑗 ∈ (1...((2 · 𝑘) − 1)))
419	414, 418, 91	syl2anc 596	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))) → (𝐹‘𝑗) ∈ ℂ)
420	402, 413, 419	fsumser 15889	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))(𝐹‘𝑗) = (seq1( + , 𝐹)‘((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘)))
421	366, 401, 420	3eqtr3d 2804	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))))‘𝑘) = (seq1( + , 𝐹)‘((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘)))
422	1, 2, 6, 7, 8, 9, 11, 15, 16, 29, 71, 73, 421	climsuse 46589	. 2 ⊢ (𝜑 → seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ 𝐵)
423		eqidd 2762	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = (𝐹‘𝑘))
424	8, 9, 423, 13	isum 15878	. . 3 ⊢ (𝜑 → Σ𝑘 ∈ ℕ (𝐹‘𝑘) = ( ⇝ ‘seq1( + , 𝐹)))
425		climrel 15652	. . . . . . 7 ⊢ Rel ⇝
426	425	releldmi 5930	. . . . . 6 ⊢ (seq1( + , 𝐹) ⇝ 𝐵 → seq1( + , 𝐹) ∈ dom ⇝ )
427	16, 426	syl 18	. . . . 5 ⊢ (𝜑 → seq1( + , 𝐹) ∈ dom ⇝ )
428		climdm 15714	. . . . 5 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ ↔ seq1( + , 𝐹) ⇝ ( ⇝ ‘seq1( + , 𝐹)))
429	427, 428	sylib 221	. . . 4 ⊢ (𝜑 → seq1( + , 𝐹) ⇝ ( ⇝ ‘seq1( + , 𝐹)))
430		climuni 15712	. . . 4 ⊢ ((seq1( + , 𝐹) ⇝ ( ⇝ ‘seq1( + , 𝐹)) ∧ seq1( + , 𝐹) ⇝ 𝐵) → ( ⇝ ‘seq1( + , 𝐹)) = 𝐵)
431	429, 16, 430	syl2anc 596	. . 3 ⊢ (𝜑 → ( ⇝ ‘seq1( + , 𝐹)) = 𝐵)
432	425	a1i 11	. . . . . . . 8 ⊢ (𝜑 → Rel ⇝ )
433		releldm 5926	. . . . . . . 8 ⊢ ((Rel ⇝ ∧ seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ 𝐵) → seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ∈ dom ⇝ )
434	432, 422, 433	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ∈ dom ⇝ )
435		climdm 15714	. . . . . . 7 ⊢ (seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ∈ dom ⇝ ↔ seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ ( ⇝ ‘seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))))))
436	434, 435	sylib 221	. . . . . 6 ⊢ (𝜑 → seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ ( ⇝ ‘seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))))))
437	396	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))) = (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1))))
438	437	seqeq3d 14145	. . . . . . 7 ⊢ (𝜑 → seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) = seq1( + , (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1)))))
439	438	fveq2d 6887	. . . . . 6 ⊢ (𝜑 → ( ⇝ ‘seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))))) = ( ⇝ ‘seq1( + , (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1))))))
440	436, 439	breqtrd 5131	. . . . 5 ⊢ (𝜑 → seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ ( ⇝ ‘seq1( + , (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1))))))
441		climuni 15712	. . . . 5 ⊢ ((seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ 𝐵 ∧ seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ ( ⇝ ‘seq1( + , (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1)))))) → 𝐵 = ( ⇝ ‘seq1( + , (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1))))))
442	422, 440, 441	syl2anc 596	. . . 4 ⊢ (𝜑 → 𝐵 = ( ⇝ ‘seq1( + , (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1))))))
443		eqcom 2768	. . . . . . 7 ⊢ (𝑘 = 𝑗 ↔ 𝑗 = 𝑘)
444		eqcom 2768	. . . . . . 7 ⊢ ((𝐹‘((2 · 𝑘) − 1)) = (𝐹‘((2 · 𝑗) − 1)) ↔ (𝐹‘((2 · 𝑗) − 1)) = (𝐹‘((2 · 𝑘) − 1)))
445	395, 443, 444	3imtr3i 294	. . . . . 6 ⊢ (𝑗 = 𝑘 → (𝐹‘((2 · 𝑗) − 1)) = (𝐹‘((2 · 𝑘) − 1)))
446		eqidd 2762	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1))) = (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1))))
447	12	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐹:ℕ⟶ℂ)
448	8, 36, 65, 409	eluzd 46388	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → ((2 · 𝑘) − 1) ∈ ℕ)
449	448	adantl 487	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) − 1) ∈ ℕ)
450	447, 449	ffvelcdmd 7083	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘((2 · 𝑘) − 1)) ∈ ℂ)
451	445, 446, 399, 450	fvmptd4 7016	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1)))‘𝑘) = (𝐹‘((2 · 𝑘) − 1)))
452	8, 9, 451, 450	isum 15878	. . . 4 ⊢ (𝜑 → Σ𝑘 ∈ ℕ (𝐹‘((2 · 𝑘) − 1)) = ( ⇝ ‘seq1( + , (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1))))))
453	442, 452	eqtr4d 2799	. . 3 ⊢ (𝜑 → 𝐵 = Σ𝑘 ∈ ℕ (𝐹‘((2 · 𝑘) − 1)))
454	424, 431, 453	3eqtrd 2800	. 2 ⊢ (𝜑 → Σ𝑘 ∈ ℕ (𝐹‘𝑘) = Σ𝑘 ∈ ℕ (𝐹‘((2 · 𝑘) − 1)))
455	422, 454	jca 521	1 ⊢ (𝜑 → (seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ 𝐵 ∧ Σ𝑘 ∈ ℕ (𝐹‘𝑘) = Σ𝑘 ∈ ℕ (𝐹‘((2 · 𝑘) − 1))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ≠ wne 2956 ∀wral 3077 ∃wrex 3087 {crab 3413 Vcvv 3451 ∖ cdif 3896 ∪ cun 3897 ∩ cin 3898 ⊆ wss 3899 ∅c0 4279 class class class wbr 5103 ↦ cmpt 5186 dom cdm 5651 Rel wrel 5656 ⟶wf 6533 –1-1→wf1 6534 –onto→wfo 6535 –1-1-onto→wf1o 6536 ‘cfv 6537 (class class class)co 7418 Fincfn 8966 ℂcc 11191 ℝcr 11192 0cc0 11193 1c1 11194 + caddc 11196 · cmul 11198 < clt 11336 ≤ cle 11337 − cmin 11534 / cdiv 11966 ℕcn 12328 2c2 12390 ℤcz 12686 ℤ_≥cuz 12958 ℝ⁺crp 13113 ...cfz 13632 seqcseq 14137 ⇝ cli 15644 Σcsu 15846

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7749 ax-inf2 9635 ax-cnex 11249 ax-resscn 11250 ax-1cn 11251 ax-icn 11252 ax-addcl 11253 ax-addrcl 11254 ax-mulcl 11255 ax-mulrcl 11256 ax-mulcom 11257 ax-addass 11258 ax-mulass 11259 ax-distr 11260 ax-i2m1 11261 ax-1ne0 11262 ax-1rid 11263 ax-rnegex 11264 ax-rrecex 11265 ax-cnre 11266 ax-pre-lttri 11267 ax-pre-lttrn 11268 ax-pre-ltadd 11269 ax-pre-mulgt0 11270 ax-pre-sup 11271

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7375 df-ov 7421 df-oprab 7422 df-mpo 7423 df-om 7876 df-1st 7999 df-2nd 8000 df-frecs 8292 df-wrecs 8323 df-recs 8372 df-rdg 8411 df-1o 8469 df-er 8710 df-en 8967 df-dom 8968 df-sdom 8969 df-fin 8970 df-sup 9427 df-oi 9497 df-card 10013 df-pnf 11338 df-mnf 11339 df-xr 11340 df-ltxr 11341 df-le 11342 df-sub 11536 df-neg 11537 df-div 11967 df-nn 12329 df-2 12398 df-3 12399 df-n0 12600 df-z 12687 df-uz 12959 df-rp 13114 df-fz 13633 df-fzo 13782 df-seq 14138 df-exp 14198 df-hash 14468 df-cj 15259 df-re 15260 df-im 15261 df-sqrt 15395 df-abs 15396 df-clim 15648 df-sum 15847

This theorem is used by: fouriersw 47210

W3C validator