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

Theorem sumnnodd 43861
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.
StepHypRef Expression
1 nfv 1917 . . 3 𝑘𝜑
2 nfcv 2907 . . 3 𝑘seq1( + , 𝐹)
3 nfcv 2907 . . . 4 𝑘1
4 nfcv 2907 . . . 4 𝑘 +
5 nfmpt1 5213 . . . 4 𝑘(𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))
63, 4, 5nfseq 13916 . . 3 𝑘seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))))
7 nfmpt1 5213 . . 3 𝑘(𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))
8 nnuz 12806 . . 3 ℕ = (ℤ‘1)
9 1zzd 12534 . . 3 (𝜑 → 1 ∈ ℤ)
10 seqex 13908 . . . 4 seq1( + , 𝐹) ∈ V
1110a1i 11 . . 3 (𝜑 → seq1( + , 𝐹) ∈ V)
12 sumnnodd.1 . . . . . 6 (𝜑𝐹:ℕ⟶ℂ)
1312ffvelcdmda 7035 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ℂ)
148, 9, 13serf 13936 . . . 4 (𝜑 → seq1( + , 𝐹):ℕ⟶ℂ)
1514ffvelcdmda 7035 . . 3 ((𝜑𝑘 ∈ ℕ) → (seq1( + , 𝐹)‘𝑘) ∈ ℂ)
16 sumnnodd.sc . . 3 (𝜑 → seq1( + , 𝐹) ⇝ 𝐵)
17 1nn 12164 . . . . . . 7 1 ∈ ℕ
18 oveq2 7365 . . . . . . . . 9 (𝑘 = 1 → (2 · 𝑘) = (2 · 1))
1918oveq1d 7372 . . . . . . . 8 (𝑘 = 1 → ((2 · 𝑘) − 1) = ((2 · 1) − 1))
20 eqid 2736 . . . . . . . 8 (𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1)) = (𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))
21 ovex 7390 . . . . . . . 8 ((2 · 1) − 1) ∈ V
2219, 20, 21fvmpt 6948 . . . . . . 7 (1 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘1) = ((2 · 1) − 1))
2317, 22ax-mp 5 . . . . . 6 ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘1) = ((2 · 1) − 1)
24 2t1e2 12316 . . . . . . 7 (2 · 1) = 2
2524oveq1i 7367 . . . . . 6 ((2 · 1) − 1) = (2 − 1)
26 2m1e1 12279 . . . . . 6 (2 − 1) = 1
2723, 25, 263eqtri 2768 . . . . 5 ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘1) = 1
2827, 17eqeltri 2834 . . . 4 ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘1) ∈ ℕ
2928a1i 11 . . 3 (𝜑 → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘1) ∈ ℕ)
30 2z 12535 . . . . . . . 8 2 ∈ ℤ
3130a1i 11 . . . . . . 7 (𝑘 ∈ ℕ → 2 ∈ ℤ)
32 nnz 12520 . . . . . . 7 (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
3331, 32zmulcld 12613 . . . . . 6 (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℤ)
3432peano2zd 12610 . . . . . . . 8 (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℤ)
3531, 34zmulcld 12613 . . . . . . 7 (𝑘 ∈ ℕ → (2 · (𝑘 + 1)) ∈ ℤ)
36 1zzd 12534 . . . . . . 7 (𝑘 ∈ ℕ → 1 ∈ ℤ)
3735, 36zsubcld 12612 . . . . . 6 (𝑘 ∈ ℕ → ((2 · (𝑘 + 1)) − 1) ∈ ℤ)
38 2re 12227 . . . . . . . . . 10 2 ∈ ℝ
3938a1i 11 . . . . . . . . 9 (𝑘 ∈ ℕ → 2 ∈ ℝ)
40 nnre 12160 . . . . . . . . 9 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
4139, 40remulcld 11185 . . . . . . . 8 (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℝ)
4241lep1d 12086 . . . . . . 7 (𝑘 ∈ ℕ → (2 · 𝑘) ≤ ((2 · 𝑘) + 1))
43 2cnd 12231 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 2 ∈ ℂ)
44 nncn 12161 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
45 1cnd 11150 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 1 ∈ ℂ)
4643, 44, 45adddid 11179 . . . . . . . . . 10 (𝑘 ∈ ℕ → (2 · (𝑘 + 1)) = ((2 · 𝑘) + (2 · 1)))
4724oveq2i 7368 . . . . . . . . . 10 ((2 · 𝑘) + (2 · 1)) = ((2 · 𝑘) + 2)
4846, 47eqtrdi 2792 . . . . . . . . 9 (𝑘 ∈ ℕ → (2 · (𝑘 + 1)) = ((2 · 𝑘) + 2))
4948oveq1d 7372 . . . . . . . 8 (𝑘 ∈ ℕ → ((2 · (𝑘 + 1)) − 1) = (((2 · 𝑘) + 2) − 1))
5043, 44mulcld 11175 . . . . . . . . 9 (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℂ)
5150, 43, 45addsubassd 11532 . . . . . . . 8 (𝑘 ∈ ℕ → (((2 · 𝑘) + 2) − 1) = ((2 · 𝑘) + (2 − 1)))
5226oveq2i 7368 . . . . . . . . 9 ((2 · 𝑘) + (2 − 1)) = ((2 · 𝑘) + 1)
5352a1i 11 . . . . . . . 8 (𝑘 ∈ ℕ → ((2 · 𝑘) + (2 − 1)) = ((2 · 𝑘) + 1))
5449, 51, 533eqtrrd 2781 . . . . . . 7 (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) = ((2 · (𝑘 + 1)) − 1))
5542, 54breqtrd 5131 . . . . . 6 (𝑘 ∈ ℕ → (2 · 𝑘) ≤ ((2 · (𝑘 + 1)) − 1))
56 eluz2 12769 . . . . . 6 (((2 · (𝑘 + 1)) − 1) ∈ (ℤ‘(2 · 𝑘)) ↔ ((2 · 𝑘) ∈ ℤ ∧ ((2 · (𝑘 + 1)) − 1) ∈ ℤ ∧ (2 · 𝑘) ≤ ((2 · (𝑘 + 1)) − 1)))
5733, 37, 55, 56syl3anbrc 1343 . . . . 5 (𝑘 ∈ ℕ → ((2 · (𝑘 + 1)) − 1) ∈ (ℤ‘(2 · 𝑘)))
58 oveq2 7365 . . . . . . . 8 (𝑘 = 𝑗 → (2 · 𝑘) = (2 · 𝑗))
5958oveq1d 7372 . . . . . . 7 (𝑘 = 𝑗 → ((2 · 𝑘) − 1) = ((2 · 𝑗) − 1))
6059cbvmptv 5218 . . . . . 6 (𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1)) = (𝑗 ∈ ℕ ↦ ((2 · 𝑗) − 1))
61 oveq2 7365 . . . . . . 7 (𝑗 = (𝑘 + 1) → (2 · 𝑗) = (2 · (𝑘 + 1)))
6261oveq1d 7372 . . . . . 6 (𝑗 = (𝑘 + 1) → ((2 · 𝑗) − 1) = ((2 · (𝑘 + 1)) − 1))
63 peano2nn 12165 . . . . . 6 (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
6460, 62, 63, 37fvmptd3 6971 . . . . 5 (𝑘 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘(𝑘 + 1)) = ((2 · (𝑘 + 1)) − 1))
6533, 36zsubcld 12612 . . . . . . . . 9 (𝑘 ∈ ℕ → ((2 · 𝑘) − 1) ∈ ℤ)
6620fvmpt2 6959 . . . . . . . . 9 ((𝑘 ∈ ℕ ∧ ((2 · 𝑘) − 1) ∈ ℤ) → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) = ((2 · 𝑘) − 1))
6765, 66mpdan 685 . . . . . . . 8 (𝑘 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) = ((2 · 𝑘) − 1))
6867oveq1d 7372 . . . . . . 7 (𝑘 ∈ ℕ → (((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) + 1) = (((2 · 𝑘) − 1) + 1))
6950, 45npcand 11516 . . . . . . 7 (𝑘 ∈ ℕ → (((2 · 𝑘) − 1) + 1) = (2 · 𝑘))
7068, 69eqtrd 2776 . . . . . 6 (𝑘 ∈ ℕ → (((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) + 1) = (2 · 𝑘))
7170fveq2d 6846 . . . . 5 (𝑘 ∈ ℕ → (ℤ‘(((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) + 1)) = (ℤ‘(2 · 𝑘)))
7257, 64, 713eltr4d 2853 . . . 4 (𝑘 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘(𝑘 + 1)) ∈ (ℤ‘(((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) + 1)))
7372adantl 482 . . 3 ((𝜑𝑘 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘(𝑘 + 1)) ∈ (ℤ‘(((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) + 1)))
74 seqex 13908 . . . 4 seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ∈ V
7574a1i 11 . . 3 (𝜑 → seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ∈ V)
76 incom 4161 . . . . . . . . . 10 (((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) = (((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
77 inss2 4189 . . . . . . . . . . 11 ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}
78 ssrin 4193 . . . . . . . . . . 11 (((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} → (((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) ⊆ ({𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} ∩ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})))
7977, 78ax-mp 5 . . . . . . . . . 10 (((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) ⊆ ({𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} ∩ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
8076, 79eqsstri 3978 . . . . . . . . 9 (((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) ⊆ ({𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} ∩ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
81 disjdif 4431 . . . . . . . . 9 ({𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} ∩ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) = ∅
8280, 81sseqtri 3980 . . . . . . . 8 (((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) ⊆ ∅
83 ss0 4358 . . . . . . . 8 ((((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) ⊆ ∅ → (((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) = ∅)
8482, 83mp1i 13 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) = ∅)
85 uncom 4113 . . . . . . . . 9 (((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∪ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) = (((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∪ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
86 inundif 4438 . . . . . . . . 9 (((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∪ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) = (1...((2 · 𝑘) − 1))
8785, 86eqtr2i 2765 . . . . . . . 8 (1...((2 · 𝑘) − 1)) = (((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∪ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
8887a1i 11 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (1...((2 · 𝑘) − 1)) = (((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∪ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})))
89 fzfid 13878 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (1...((2 · 𝑘) − 1)) ∈ Fin)
9012adantr 481 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...((2 · 𝑘) − 1))) → 𝐹:ℕ⟶ℂ)
91 elfznn 13470 . . . . . . . . . 10 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → 𝑗 ∈ ℕ)
9291adantl 482 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...((2 · 𝑘) − 1))) → 𝑗 ∈ ℕ)
9390, 92ffvelcdmd 7036 . . . . . . . 8 ((𝜑𝑗 ∈ (1...((2 · 𝑘) − 1))) → (𝐹𝑗) ∈ ℂ)
9493adantlr 713 . . . . . . 7 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → (𝐹𝑗) ∈ ℂ)
9584, 88, 89, 94fsumsplit 15626 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...((2 · 𝑘) − 1))(𝐹𝑗) = (Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗) + Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗)))
96 simpl 483 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → 𝜑)
97 ssrab2 4037 . . . . . . . . . . . . . 14 {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} ⊆ ℕ
9877sseli 3940 . . . . . . . . . . . . . 14 (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → 𝑗 ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})
9997, 98sselid 3942 . . . . . . . . . . . . 13 (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → 𝑗 ∈ ℕ)
10099adantl 482 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → 𝑗 ∈ ℕ)
101 oveq1 7364 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑗 → (𝑘 / 2) = (𝑗 / 2))
102101eleq1d 2822 . . . . . . . . . . . . . . 15 (𝑘 = 𝑗 → ((𝑘 / 2) ∈ ℕ ↔ (𝑗 / 2) ∈ ℕ))
103 oveq1 7364 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑘 → (𝑛 / 2) = (𝑘 / 2))
104103eleq1d 2822 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑘 → ((𝑛 / 2) ∈ ℕ ↔ (𝑘 / 2) ∈ ℕ))
105104elrab 3645 . . . . . . . . . . . . . . . 16 (𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} ↔ (𝑘 ∈ ℕ ∧ (𝑘 / 2) ∈ ℕ))
106105simprbi 497 . . . . . . . . . . . . . . 15 (𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} → (𝑘 / 2) ∈ ℕ)
107102, 106vtoclga 3534 . . . . . . . . . . . . . 14 (𝑗 ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} → (𝑗 / 2) ∈ ℕ)
10898, 107syl 17 . . . . . . . . . . . . 13 (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → (𝑗 / 2) ∈ ℕ)
109108adantl 482 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (𝑗 / 2) ∈ ℕ)
110 eleq1w 2820 . . . . . . . . . . . . . . 15 (𝑘 = 𝑗 → (𝑘 ∈ ℕ ↔ 𝑗 ∈ ℕ))
111110, 1023anbi23d 1439 . . . . . . . . . . . . . 14 (𝑘 = 𝑗 → ((𝜑𝑘 ∈ ℕ ∧ (𝑘 / 2) ∈ ℕ) ↔ (𝜑𝑗 ∈ ℕ ∧ (𝑗 / 2) ∈ ℕ)))
112 fveqeq2 6851 . . . . . . . . . . . . . 14 (𝑘 = 𝑗 → ((𝐹𝑘) = 0 ↔ (𝐹𝑗) = 0))
113111, 112imbi12d 344 . . . . . . . . . . . . 13 (𝑘 = 𝑗 → (((𝜑𝑘 ∈ ℕ ∧ (𝑘 / 2) ∈ ℕ) → (𝐹𝑘) = 0) ↔ ((𝜑𝑗 ∈ ℕ ∧ (𝑗 / 2) ∈ ℕ) → (𝐹𝑗) = 0)))
114 sumnnodd.even0 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ ∧ (𝑘 / 2) ∈ ℕ) → (𝐹𝑘) = 0)
115113, 114chvarvv 2002 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ ∧ (𝑗 / 2) ∈ ℕ) → (𝐹𝑗) = 0)
11696, 100, 109, 115syl3anc 1371 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (𝐹𝑗) = 0)
117116sumeq2dv 15588 . . . . . . . . . 10 (𝜑 → Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗) = Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})0)
118 fzfid 13878 . . . . . . . . . . . . 13 (𝜑 → (1...((2 · 𝑘) − 1)) ∈ Fin)
119 inss1 4188 . . . . . . . . . . . . . 14 ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ (1...((2 · 𝑘) − 1))
120119a1i 11 . . . . . . . . . . . . 13 (𝜑 → ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ (1...((2 · 𝑘) − 1)))
121 ssfi 9117 . . . . . . . . . . . . 13 (((1...((2 · 𝑘) − 1)) ∈ Fin ∧ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ (1...((2 · 𝑘) − 1))) → ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∈ Fin)
122118, 120, 121syl2anc 584 . . . . . . . . . . . 12 (𝜑 → ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∈ Fin)
123122olcd 872 . . . . . . . . . . 11 (𝜑 → (((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ (ℤ𝐶) ∨ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∈ Fin))
124 sumz 15607 . . . . . . . . . . 11 ((((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ (ℤ𝐶) ∨ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∈ Fin) → Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})0 = 0)
125123, 124syl 17 . . . . . . . . . 10 (𝜑 → Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})0 = 0)
126117, 125eqtrd 2776 . . . . . . . . 9 (𝜑 → Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗) = 0)
127126adantr 481 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗) = 0)
128127oveq2d 7373 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗) + Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗)) = (Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗) + 0))
129 fzfi 13877 . . . . . . . . . . . 12 (1...((2 · 𝑘) − 1)) ∈ Fin
130 difss 4091 . . . . . . . . . . . 12 ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ (1...((2 · 𝑘) − 1))
131 ssfi 9117 . . . . . . . . . . . 12 (((1...((2 · 𝑘) − 1)) ∈ Fin ∧ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ (1...((2 · 𝑘) − 1))) → ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∈ Fin)
132129, 130, 131mp2an 690 . . . . . . . . . . 11 ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∈ Fin
133132a1i 11 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∈ Fin)
134130sseli 3940 . . . . . . . . . . . 12 (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → 𝑗 ∈ (1...((2 · 𝑘) − 1)))
135134, 93sylan2 593 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (𝐹𝑗) ∈ ℂ)
136135adantlr 713 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (𝐹𝑗) ∈ ℂ)
137133, 136fsumcl 15618 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗) ∈ ℂ)
138137addid1d 11355 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗) + 0) = Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗))
139 fveq2 6842 . . . . . . . . 9 (𝑗 = 𝑖 → (𝐹𝑗) = (𝐹𝑖))
140139cbvsumv 15581 . . . . . . . 8 Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗) = Σ𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑖)
141138, 140eqtrdi 2792 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗) + 0) = Σ𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑖))
142128, 141eqtrd 2776 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → (Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗) + Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗)) = Σ𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑖))
143 fveq2 6842 . . . . . . 7 (𝑖 = ((2 · 𝑗) − 1) → (𝐹𝑖) = (𝐹‘((2 · 𝑗) − 1)))
144 fzfid 13878 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (1...𝑘) ∈ Fin)
145 1zzd 12534 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 1 ∈ ℤ)
14665adantr 481 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → ((2 · 𝑘) − 1) ∈ ℤ)
14730a1i 11 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...𝑘) → 2 ∈ ℤ)
148 elfzelz 13441 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...𝑘) → 𝑖 ∈ ℤ)
149147, 148zmulcld 12613 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1...𝑘) → (2 · 𝑖) ∈ ℤ)
150 1zzd 12534 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1...𝑘) → 1 ∈ ℤ)
151149, 150zsubcld 12612 . . . . . . . . . . . . . 14 (𝑖 ∈ (1...𝑘) → ((2 · 𝑖) − 1) ∈ ℤ)
152151adantl 482 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → ((2 · 𝑖) − 1) ∈ ℤ)
15325, 26eqtr2i 2765 . . . . . . . . . . . . . . 15 1 = ((2 · 1) − 1)
154 1re 11155 . . . . . . . . . . . . . . . . . 18 1 ∈ ℝ
15538, 154remulcli 11171 . . . . . . . . . . . . . . . . 17 (2 · 1) ∈ ℝ
156155a1i 11 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...𝑘) → (2 · 1) ∈ ℝ)
157149zred 12607 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...𝑘) → (2 · 𝑖) ∈ ℝ)
158 1red 11156 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...𝑘) → 1 ∈ ℝ)
159148zred 12607 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...𝑘) → 𝑖 ∈ ℝ)
16038a1i 11 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...𝑘) → 2 ∈ ℝ)
161 0le2 12255 . . . . . . . . . . . . . . . . . 18 0 ≤ 2
162161a1i 11 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...𝑘) → 0 ≤ 2)
163 elfzle1 13444 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...𝑘) → 1 ≤ 𝑖)
164158, 159, 160, 162, 163lemul2ad 12095 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...𝑘) → (2 · 1) ≤ (2 · 𝑖))
165156, 157, 158, 164lesub1dd 11771 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1...𝑘) → ((2 · 1) − 1) ≤ ((2 · 𝑖) − 1))
166153, 165eqbrtrid 5140 . . . . . . . . . . . . . 14 (𝑖 ∈ (1...𝑘) → 1 ≤ ((2 · 𝑖) − 1))
167166adantl 482 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 1 ≤ ((2 · 𝑖) − 1))
168157adantl 482 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → (2 · 𝑖) ∈ ℝ)
16941adantr 481 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → (2 · 𝑘) ∈ ℝ)
170 1red 11156 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 1 ∈ ℝ)
171159adantl 482 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 𝑖 ∈ ℝ)
17240adantr 481 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 𝑘 ∈ ℝ)
17338a1i 11 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 2 ∈ ℝ)
174161a1i 11 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 0 ≤ 2)
175 elfzle2 13445 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...𝑘) → 𝑖𝑘)
176175adantl 482 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 𝑖𝑘)
177171, 172, 173, 174, 176lemul2ad 12095 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → (2 · 𝑖) ≤ (2 · 𝑘))
178168, 169, 170, 177lesub1dd 11771 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → ((2 · 𝑖) − 1) ≤ ((2 · 𝑘) − 1))
179145, 146, 152, 167, 178elfzd 13432 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → ((2 · 𝑖) − 1) ∈ (1...((2 · 𝑘) − 1)))
180149zcnd 12608 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑘) → (2 · 𝑖) ∈ ℂ)
181 1cnd 11150 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑘) → 1 ∈ ℂ)
182 2cnd 12231 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑘) → 2 ∈ ℂ)
183 2ne0 12257 . . . . . . . . . . . . . . . . . . 19 2 ≠ 0
184183a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑘) → 2 ≠ 0)
185180, 181, 182, 184divsubdird 11970 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...𝑘) → (((2 · 𝑖) − 1) / 2) = (((2 · 𝑖) / 2) − (1 / 2)))
186148zcnd 12608 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (1...𝑘) → 𝑖 ∈ ℂ)
187186, 182, 184divcan3d 11936 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑘) → ((2 · 𝑖) / 2) = 𝑖)
188187oveq1d 7372 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...𝑘) → (((2 · 𝑖) / 2) − (1 / 2)) = (𝑖 − (1 / 2)))
189185, 188eqtrd 2776 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...𝑘) → (((2 · 𝑖) − 1) / 2) = (𝑖 − (1 / 2)))
190148, 150zsubcld 12612 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑘) → (𝑖 − 1) ∈ ℤ)
191160, 184rereccld 11982 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (1...𝑘) → (1 / 2) ∈ ℝ)
192 halflt1 12371 . . . . . . . . . . . . . . . . . . . 20 (1 / 2) < 1
193192a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (1...𝑘) → (1 / 2) < 1)
194191, 158, 159, 193ltsub2dd 11768 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑘) → (𝑖 − 1) < (𝑖 − (1 / 2)))
195 2rp 12920 . . . . . . . . . . . . . . . . . . . . 21 2 ∈ ℝ+
196 rpreccl 12941 . . . . . . . . . . . . . . . . . . . . 21 (2 ∈ ℝ+ → (1 / 2) ∈ ℝ+)
197195, 196mp1i 13 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (1...𝑘) → (1 / 2) ∈ ℝ+)
198159, 197ltsubrpd 12989 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (1...𝑘) → (𝑖 − (1 / 2)) < 𝑖)
199186, 181npcand 11516 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (1...𝑘) → ((𝑖 − 1) + 1) = 𝑖)
200198, 199breqtrrd 5133 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑘) → (𝑖 − (1 / 2)) < ((𝑖 − 1) + 1))
201 btwnnz 12579 . . . . . . . . . . . . . . . . . 18 (((𝑖 − 1) ∈ ℤ ∧ (𝑖 − 1) < (𝑖 − (1 / 2)) ∧ (𝑖 − (1 / 2)) < ((𝑖 − 1) + 1)) → ¬ (𝑖 − (1 / 2)) ∈ ℤ)
202190, 194, 200, 201syl3anc 1371 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...𝑘) → ¬ (𝑖 − (1 / 2)) ∈ ℤ)
203 nnz 12520 . . . . . . . . . . . . . . . . 17 ((𝑖 − (1 / 2)) ∈ ℕ → (𝑖 − (1 / 2)) ∈ ℤ)
204202, 203nsyl 140 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...𝑘) → ¬ (𝑖 − (1 / 2)) ∈ ℕ)
205189, 204eqneltrd 2857 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1...𝑘) → ¬ (((2 · 𝑖) − 1) / 2) ∈ ℕ)
206205intnand 489 . . . . . . . . . . . . . 14 (𝑖 ∈ (1...𝑘) → ¬ (((2 · 𝑖) − 1) ∈ ℕ ∧ (((2 · 𝑖) − 1) / 2) ∈ ℕ))
207 oveq1 7364 . . . . . . . . . . . . . . . 16 (𝑛 = ((2 · 𝑖) − 1) → (𝑛 / 2) = (((2 · 𝑖) − 1) / 2))
208207eleq1d 2822 . . . . . . . . . . . . . . 15 (𝑛 = ((2 · 𝑖) − 1) → ((𝑛 / 2) ∈ ℕ ↔ (((2 · 𝑖) − 1) / 2) ∈ ℕ))
209208elrab 3645 . . . . . . . . . . . . . 14 (((2 · 𝑖) − 1) ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} ↔ (((2 · 𝑖) − 1) ∈ ℕ ∧ (((2 · 𝑖) − 1) / 2) ∈ ℕ))
210206, 209sylnibr 328 . . . . . . . . . . . . 13 (𝑖 ∈ (1...𝑘) → ¬ ((2 · 𝑖) − 1) ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})
211210adantl 482 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → ¬ ((2 · 𝑖) − 1) ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})
212179, 211eldifd 3921 . . . . . . . . . . 11 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → ((2 · 𝑖) − 1) ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
213212fmpttd 7063 . . . . . . . . . 10 (𝑘 ∈ ℕ → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)⟶((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
214 eqidd 2737 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (1...𝑘) → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)) = (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)))
215 oveq2 7365 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑥 → (2 · 𝑖) = (2 · 𝑥))
216215oveq1d 7372 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑥 → ((2 · 𝑖) − 1) = ((2 · 𝑥) − 1))
217216adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1...𝑘) ∧ 𝑖 = 𝑥) → ((2 · 𝑖) − 1) = ((2 · 𝑥) − 1))
218 id 22 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (1...𝑘) → 𝑥 ∈ (1...𝑘))
219 ovexd 7392 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (1...𝑘) → ((2 · 𝑥) − 1) ∈ V)
220214, 217, 218, 219fvmptd 6955 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (1...𝑘) → ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((2 · 𝑥) − 1))
221220eqcomd 2742 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1...𝑘) → ((2 · 𝑥) − 1) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥))
222221ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦)) → ((2 · 𝑥) − 1) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥))
223 simpr 485 . . . . . . . . . . . . . . 15 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦)) → ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦))
224 eqidd 2737 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (1...𝑘) → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)) = (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)))
225 oveq2 7365 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑦 → (2 · 𝑖) = (2 · 𝑦))
226225oveq1d 7372 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑦 → ((2 · 𝑖) − 1) = ((2 · 𝑦) − 1))
227226adantl 482 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ (1...𝑘) ∧ 𝑖 = 𝑦) → ((2 · 𝑖) − 1) = ((2 · 𝑦) − 1))
228 id 22 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (1...𝑘) → 𝑦 ∈ (1...𝑘))
229 ovexd 7392 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (1...𝑘) → ((2 · 𝑦) − 1) ∈ V)
230224, 227, 228, 229fvmptd 6955 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (1...𝑘) → ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦) = ((2 · 𝑦) − 1))
231230ad2antlr 725 . . . . . . . . . . . . . . 15 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦)) → ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦) = ((2 · 𝑦) − 1))
232222, 223, 2313eqtrd 2780 . . . . . . . . . . . . . 14 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦)) → ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1))
233 2cnd 12231 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (1...𝑘) → 2 ∈ ℂ)
234 elfzelz 13441 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (1...𝑘) → 𝑥 ∈ ℤ)
235234zcnd 12608 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (1...𝑘) → 𝑥 ∈ ℂ)
236233, 235mulcld 11175 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (1...𝑘) → (2 · 𝑥) ∈ ℂ)
237236ad2antrr 724 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1)) → (2 · 𝑥) ∈ ℂ)
238 2cnd 12231 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (1...𝑘) → 2 ∈ ℂ)
239 elfzelz 13441 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (1...𝑘) → 𝑦 ∈ ℤ)
240239zcnd 12608 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (1...𝑘) → 𝑦 ∈ ℂ)
241238, 240mulcld 11175 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (1...𝑘) → (2 · 𝑦) ∈ ℂ)
242241ad2antlr 725 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1)) → (2 · 𝑦) ∈ ℂ)
243 1cnd 11150 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1)) → 1 ∈ ℂ)
244 simpr 485 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1)) → ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1))
245237, 242, 243, 244subcan2d 11554 . . . . . . . . . . . . . . 15 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1)) → (2 · 𝑥) = (2 · 𝑦))
246235ad2antrr 724 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ (2 · 𝑥) = (2 · 𝑦)) → 𝑥 ∈ ℂ)
247240ad2antlr 725 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ (2 · 𝑥) = (2 · 𝑦)) → 𝑦 ∈ ℂ)
248 2cnd 12231 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ (2 · 𝑥) = (2 · 𝑦)) → 2 ∈ ℂ)
249183a1i 11 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ (2 · 𝑥) = (2 · 𝑦)) → 2 ≠ 0)
250 simpr 485 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ (2 · 𝑥) = (2 · 𝑦)) → (2 · 𝑥) = (2 · 𝑦))
251246, 247, 248, 249, 250mulcanad 11790 . . . . . . . . . . . . . . 15 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ (2 · 𝑥) = (2 · 𝑦)) → 𝑥 = 𝑦)
252245, 251syldan 591 . . . . . . . . . . . . . 14 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1)) → 𝑥 = 𝑦)
253232, 252syldan 591 . . . . . . . . . . . . 13 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦)) → 𝑥 = 𝑦)
254253adantll 712 . . . . . . . . . . . 12 (((𝑘 ∈ ℕ ∧ (𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘))) ∧ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦)) → 𝑥 = 𝑦)
255254ex 413 . . . . . . . . . . 11 ((𝑘 ∈ ℕ ∧ (𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘))) → (((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦) → 𝑥 = 𝑦))
256255ralrimivva 3197 . . . . . . . . . 10 (𝑘 ∈ ℕ → ∀𝑥 ∈ (1...𝑘)∀𝑦 ∈ (1...𝑘)(((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦) → 𝑥 = 𝑦))
257 dff13 7202 . . . . . . . . . 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))‘𝑦) → 𝑥 = 𝑦)))
258213, 256, 257sylanbrc 583 . . . . . . . . 9 (𝑘 ∈ ℕ → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)–1-1→((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
259 1zzd 12534 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → 1 ∈ ℤ)
26032adantr 481 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → 𝑘 ∈ ℤ)
261134elfzelzd 13442 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → 𝑗 ∈ ℤ)
262 zeo 12589 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℤ → ((𝑗 / 2) ∈ ℤ ∨ ((𝑗 + 1) / 2) ∈ ℤ))
263261, 262syl 17 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → ((𝑗 / 2) ∈ ℤ ∨ ((𝑗 + 1) / 2) ∈ ℤ))
264263adantl 482 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → ((𝑗 / 2) ∈ ℤ ∨ ((𝑗 + 1) / 2) ∈ ℤ))
265 eldifn 4087 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → ¬ 𝑗 ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})
266134, 91syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → 𝑗 ∈ ℕ)
267266adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → 𝑗 ∈ ℕ)
268 simpr 485 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → (𝑗 / 2) ∈ ℤ)
269267nnred 12168 . . . . . . . . . . . . . . . . . . . 20 ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → 𝑗 ∈ ℝ)
27038a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → 2 ∈ ℝ)
271267nngt0d 12202 . . . . . . . . . . . . . . . . . . . 20 ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → 0 < 𝑗)
272 2pos 12256 . . . . . . . . . . . . . . . . . . . . 21 0 < 2
273272a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → 0 < 2)
274269, 270, 271, 273divgt0d 12090 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → 0 < (𝑗 / 2))
275 elnnz 12509 . . . . . . . . . . . . . . . . . . 19 ((𝑗 / 2) ∈ ℕ ↔ ((𝑗 / 2) ∈ ℤ ∧ 0 < (𝑗 / 2)))
276268, 274, 275sylanbrc 583 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → (𝑗 / 2) ∈ ℕ)
277 oveq1 7364 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑗 → (𝑛 / 2) = (𝑗 / 2))
278277eleq1d 2822 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑗 → ((𝑛 / 2) ∈ ℕ ↔ (𝑗 / 2) ∈ ℕ))
279278elrab 3645 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} ↔ (𝑗 ∈ ℕ ∧ (𝑗 / 2) ∈ ℕ))
280267, 276, 279sylanbrc 583 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → 𝑗 ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})
281265, 280mtand 814 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → ¬ (𝑗 / 2) ∈ ℤ)
282281adantl 482 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → ¬ (𝑗 / 2) ∈ ℤ)
283 pm2.53 849 . . . . . . . . . . . . . . 15 (((𝑗 / 2) ∈ ℤ ∨ ((𝑗 + 1) / 2) ∈ ℤ) → (¬ (𝑗 / 2) ∈ ℤ → ((𝑗 + 1) / 2) ∈ ℤ))
284264, 282, 283sylc 65 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → ((𝑗 + 1) / 2) ∈ ℤ)
285 1p1e2 12278 . . . . . . . . . . . . . . . . . . 19 (1 + 1) = 2
286285oveq1i 7367 . . . . . . . . . . . . . . . . . 18 ((1 + 1) / 2) = (2 / 2)
287 2div2e1 12294 . . . . . . . . . . . . . . . . . 18 (2 / 2) = 1
288286, 287eqtr2i 2765 . . . . . . . . . . . . . . . . 17 1 = ((1 + 1) / 2)
289 1red 11156 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → 1 ∈ ℝ)
290289, 289readdcld 11184 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → (1 + 1) ∈ ℝ)
29191nnred 12168 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → 𝑗 ∈ ℝ)
292291, 289readdcld 11184 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → (𝑗 + 1) ∈ ℝ)
293195a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → 2 ∈ ℝ+)
294 elfzle1 13444 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → 1 ≤ 𝑗)
295289, 291, 289, 294leadd1dd 11769 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → (1 + 1) ≤ (𝑗 + 1))
296290, 292, 293, 295lediv1dd 13015 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → ((1 + 1) / 2) ≤ ((𝑗 + 1) / 2))
297288, 296eqbrtrid 5140 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → 1 ≤ ((𝑗 + 1) / 2))
298134, 297syl 17 . . . . . . . . . . . . . . 15 (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → 1 ≤ ((𝑗 + 1) / 2))
299298adantl 482 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → 1 ≤ ((𝑗 + 1) / 2))
300 elfzel2 13439 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → ((2 · 𝑘) − 1) ∈ ℤ)
301300zred 12607 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → ((2 · 𝑘) − 1) ∈ ℝ)
302301, 289readdcld 11184 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → (((2 · 𝑘) − 1) + 1) ∈ ℝ)
303 elfzle2 13445 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → 𝑗 ≤ ((2 · 𝑘) − 1))
304291, 301, 289, 303leadd1dd 11769 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → (𝑗 + 1) ≤ (((2 · 𝑘) − 1) + 1))
305292, 302, 293, 304lediv1dd 13015 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → ((𝑗 + 1) / 2) ≤ ((((2 · 𝑘) − 1) + 1) / 2))
306305adantl 482 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → ((𝑗 + 1) / 2) ≤ ((((2 · 𝑘) − 1) + 1) / 2))
30750adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → (2 · 𝑘) ∈ ℂ)
308 1cnd 11150 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → 1 ∈ ℂ)
309307, 308npcand 11516 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → (((2 · 𝑘) − 1) + 1) = (2 · 𝑘))
310309oveq1d 7372 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → ((((2 · 𝑘) − 1) + 1) / 2) = ((2 · 𝑘) / 2))
311183a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ ℕ → 2 ≠ 0)
31244, 43, 311divcan3d 11936 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℕ → ((2 · 𝑘) / 2) = 𝑘)
313312adantr 481 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → ((2 · 𝑘) / 2) = 𝑘)
314310, 313eqtrd 2776 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → ((((2 · 𝑘) − 1) + 1) / 2) = 𝑘)
315306, 314breqtrd 5131 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → ((𝑗 + 1) / 2) ≤ 𝑘)
316134, 315sylan2 593 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → ((𝑗 + 1) / 2) ≤ 𝑘)
317259, 260, 284, 299, 316elfzd 13432 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → ((𝑗 + 1) / 2) ∈ (1...𝑘))
318266nncnd 12169 . . . . . . . . . . . . . . 15 (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → 𝑗 ∈ ℂ)
319 peano2cn 11327 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℂ → (𝑗 + 1) ∈ ℂ)
320 2cnd 12231 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℂ → 2 ∈ ℂ)
321183a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℂ → 2 ≠ 0)
322319, 320, 321divcan2d 11933 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℂ → (2 · ((𝑗 + 1) / 2)) = (𝑗 + 1))
323322oveq1d 7372 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℂ → ((2 · ((𝑗 + 1) / 2)) − 1) = ((𝑗 + 1) − 1))
324 pncan1 11579 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℂ → ((𝑗 + 1) − 1) = 𝑗)
325323, 324eqtr2d 2777 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℂ → 𝑗 = ((2 · ((𝑗 + 1) / 2)) − 1))
326318, 325syl 17 . . . . . . . . . . . . . 14 (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → 𝑗 = ((2 · ((𝑗 + 1) / 2)) − 1))
327326adantl 482 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → 𝑗 = ((2 · ((𝑗 + 1) / 2)) − 1))
328 oveq2 7365 . . . . . . . . . . . . . . 15 (𝑚 = ((𝑗 + 1) / 2) → (2 · 𝑚) = (2 · ((𝑗 + 1) / 2)))
329328oveq1d 7372 . . . . . . . . . . . . . 14 (𝑚 = ((𝑗 + 1) / 2) → ((2 · 𝑚) − 1) = ((2 · ((𝑗 + 1) / 2)) − 1))
330329rspceeqv 3595 . . . . . . . . . . . . 13 ((((𝑗 + 1) / 2) ∈ (1...𝑘) ∧ 𝑗 = ((2 · ((𝑗 + 1) / 2)) − 1)) → ∃𝑚 ∈ (1...𝑘)𝑗 = ((2 · 𝑚) − 1))
331317, 327, 330syl2anc 584 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → ∃𝑚 ∈ (1...𝑘)𝑗 = ((2 · 𝑚) − 1))
332 eqidd 2737 . . . . . . . . . . . . . . . . 17 ((𝑚 ∈ (1...𝑘) ∧ 𝑗 = ((2 · 𝑚) − 1)) → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)) = (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)))
333 oveq2 7365 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑚 → (2 · 𝑖) = (2 · 𝑚))
334333oveq1d 7372 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑚 → ((2 · 𝑖) − 1) = ((2 · 𝑚) − 1))
335334adantl 482 . . . . . . . . . . . . . . . . 17 (((𝑚 ∈ (1...𝑘) ∧ 𝑗 = ((2 · 𝑚) − 1)) ∧ 𝑖 = 𝑚) → ((2 · 𝑖) − 1) = ((2 · 𝑚) − 1))
336 simpl 483 . . . . . . . . . . . . . . . . 17 ((𝑚 ∈ (1...𝑘) ∧ 𝑗 = ((2 · 𝑚) − 1)) → 𝑚 ∈ (1...𝑘))
337 ovexd 7392 . . . . . . . . . . . . . . . . 17 ((𝑚 ∈ (1...𝑘) ∧ 𝑗 = ((2 · 𝑚) − 1)) → ((2 · 𝑚) − 1) ∈ V)
338332, 335, 336, 337fvmptd 6955 . . . . . . . . . . . . . . . 16 ((𝑚 ∈ (1...𝑘) ∧ 𝑗 = ((2 · 𝑚) − 1)) → ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚) = ((2 · 𝑚) − 1))
339 id 22 . . . . . . . . . . . . . . . . . 18 (𝑗 = ((2 · 𝑚) − 1) → 𝑗 = ((2 · 𝑚) − 1))
340339eqcomd 2742 . . . . . . . . . . . . . . . . 17 (𝑗 = ((2 · 𝑚) − 1) → ((2 · 𝑚) − 1) = 𝑗)
341340adantl 482 . . . . . . . . . . . . . . . 16 ((𝑚 ∈ (1...𝑘) ∧ 𝑗 = ((2 · 𝑚) − 1)) → ((2 · 𝑚) − 1) = 𝑗)
342338, 341eqtr2d 2777 . . . . . . . . . . . . . . 15 ((𝑚 ∈ (1...𝑘) ∧ 𝑗 = ((2 · 𝑚) − 1)) → 𝑗 = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚))
343342ex 413 . . . . . . . . . . . . . 14 (𝑚 ∈ (1...𝑘) → (𝑗 = ((2 · 𝑚) − 1) → 𝑗 = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚)))
344343adantl 482 . . . . . . . . . . . . 13 (((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) ∧ 𝑚 ∈ (1...𝑘)) → (𝑗 = ((2 · 𝑚) − 1) → 𝑗 = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚)))
345344reximdva 3165 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (∃𝑚 ∈ (1...𝑘)𝑗 = ((2 · 𝑚) − 1) → ∃𝑚 ∈ (1...𝑘)𝑗 = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚)))
346331, 345mpd 15 . . . . . . . . . . 11 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → ∃𝑚 ∈ (1...𝑘)𝑗 = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚))
347346ralrimiva 3143 . . . . . . . . . 10 (𝑘 ∈ ℕ → ∀𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})∃𝑚 ∈ (1...𝑘)𝑗 = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚))
348 dffo3 7052 . . . . . . . . . 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))‘𝑚)))
349213, 347, 348sylanbrc 583 . . . . . . . . 9 (𝑘 ∈ ℕ → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)–onto→((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
350 df-f1o 6503 . . . . . . . . 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) ∈ ℕ})))
351258, 349, 350sylanbrc 583 . . . . . . . 8 (𝑘 ∈ ℕ → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)–1-1-onto→((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
352351adantl 482 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)–1-1-onto→((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
353 eqidd 2737 . . . . . . . . 9 (𝑗 ∈ (1...𝑘) → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)) = (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)))
354 oveq2 7365 . . . . . . . . . . 11 (𝑖 = 𝑗 → (2 · 𝑖) = (2 · 𝑗))
355354oveq1d 7372 . . . . . . . . . 10 (𝑖 = 𝑗 → ((2 · 𝑖) − 1) = ((2 · 𝑗) − 1))
356355adantl 482 . . . . . . . . 9 ((𝑗 ∈ (1...𝑘) ∧ 𝑖 = 𝑗) → ((2 · 𝑖) − 1) = ((2 · 𝑗) − 1))
357 id 22 . . . . . . . . 9 (𝑗 ∈ (1...𝑘) → 𝑗 ∈ (1...𝑘))
358 ovexd 7392 . . . . . . . . 9 (𝑗 ∈ (1...𝑘) → ((2 · 𝑗) − 1) ∈ V)
359353, 356, 357, 358fvmptd 6955 . . . . . . . 8 (𝑗 ∈ (1...𝑘) → ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑗) = ((2 · 𝑗) − 1))
360359adantl 482 . . . . . . 7 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑘)) → ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑗) = ((2 · 𝑗) − 1))
361 eleq1w 2820 . . . . . . . . . 10 (𝑗 = 𝑖 → (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ↔ 𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})))
362361anbi2d 629 . . . . . . . . 9 (𝑗 = 𝑖 → (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) ↔ ((𝜑𝑘 ∈ ℕ) ∧ 𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))))
363139eleq1d 2822 . . . . . . . . 9 (𝑗 = 𝑖 → ((𝐹𝑗) ∈ ℂ ↔ (𝐹𝑖) ∈ ℂ))
364362, 363imbi12d 344 . . . . . . . 8 (𝑗 = 𝑖 → ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (𝐹𝑗) ∈ ℂ) ↔ (((𝜑𝑘 ∈ ℕ) ∧ 𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (𝐹𝑖) ∈ ℂ)))
365364, 136chvarvv 2002 . . . . . . 7 (((𝜑𝑘 ∈ ℕ) ∧ 𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (𝐹𝑖) ∈ ℂ)
366143, 144, 352, 360, 365fsumf1o 15608 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → Σ𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑖) = Σ𝑗 ∈ (1...𝑘)(𝐹‘((2 · 𝑗) − 1)))
36795, 142, 3663eqtrrd 2781 . . . . 5 ((𝜑𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...𝑘)(𝐹‘((2 · 𝑗) − 1)) = Σ𝑗 ∈ (1...((2 · 𝑘) − 1))(𝐹𝑗))
368 ovex 7390 . . . . . . . . . 10 ((2 · 𝑘) − 1) ∈ V
36920fvmpt2 6959 . . . . . . . . . 10 ((𝑘 ∈ ℕ ∧ ((2 · 𝑘) − 1) ∈ V) → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) = ((2 · 𝑘) − 1))
370368, 369mpan2 689 . . . . . . . . 9 (𝑘 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) = ((2 · 𝑘) − 1))
371370oveq2d 7373 . . . . . . . 8 (𝑘 ∈ ℕ → (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘)) = (1...((2 · 𝑘) − 1)))
372371eqcomd 2742 . . . . . . 7 (𝑘 ∈ ℕ → (1...((2 · 𝑘) − 1)) = (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘)))
373372sumeq1d 15586 . . . . . 6 (𝑘 ∈ ℕ → Σ𝑗 ∈ (1...((2 · 𝑘) − 1))(𝐹𝑗) = Σ𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))(𝐹𝑗))
374373adantl 482 . . . . 5 ((𝜑𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...((2 · 𝑘) − 1))(𝐹𝑗) = Σ𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))(𝐹𝑗))
375367, 374eqtrd 2776 . . . 4 ((𝜑𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...𝑘)(𝐹‘((2 · 𝑗) − 1)) = Σ𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))(𝐹𝑗))
376 elfznn 13470 . . . . . . 7 (𝑗 ∈ (1...𝑘) → 𝑗 ∈ ℕ)
377376adantl 482 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑘)) → 𝑗 ∈ ℕ)
37812adantr 481 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑘)) → 𝐹:ℕ⟶ℂ)
37930a1i 11 . . . . . . . . . . . 12 (𝑗 ∈ (1...𝑘) → 2 ∈ ℤ)
380 elfzelz 13441 . . . . . . . . . . . 12 (𝑗 ∈ (1...𝑘) → 𝑗 ∈ ℤ)
381379, 380zmulcld 12613 . . . . . . . . . . 11 (𝑗 ∈ (1...𝑘) → (2 · 𝑗) ∈ ℤ)
382 1zzd 12534 . . . . . . . . . . 11 (𝑗 ∈ (1...𝑘) → 1 ∈ ℤ)
383381, 382zsubcld 12612 . . . . . . . . . 10 (𝑗 ∈ (1...𝑘) → ((2 · 𝑗) − 1) ∈ ℤ)
384 0red 11158 . . . . . . . . . . 11 (𝑗 ∈ (1...𝑘) → 0 ∈ ℝ)
38538a1i 11 . . . . . . . . . . . . 13 (𝑗 ∈ (1...𝑘) → 2 ∈ ℝ)
38624, 385eqeltrid 2842 . . . . . . . . . . . 12 (𝑗 ∈ (1...𝑘) → (2 · 1) ∈ ℝ)
387 1red 11156 . . . . . . . . . . . 12 (𝑗 ∈ (1...𝑘) → 1 ∈ ℝ)
388386, 387resubcld 11583 . . . . . . . . . . 11 (𝑗 ∈ (1...𝑘) → ((2 · 1) − 1) ∈ ℝ)
389383zred 12607 . . . . . . . . . . 11 (𝑗 ∈ (1...𝑘) → ((2 · 𝑗) − 1) ∈ ℝ)
390 0lt1 11677 . . . . . . . . . . . 12 0 < 1
391153a1i 11 . . . . . . . . . . . 12 (𝑗 ∈ (1...𝑘) → 1 = ((2 · 1) − 1))
392390, 391breqtrid 5142 . . . . . . . . . . 11 (𝑗 ∈ (1...𝑘) → 0 < ((2 · 1) − 1))
393381zred 12607 . . . . . . . . . . . 12 (𝑗 ∈ (1...𝑘) → (2 · 𝑗) ∈ ℝ)
394376nnred 12168 . . . . . . . . . . . . 13 (𝑗 ∈ (1...𝑘) → 𝑗 ∈ ℝ)
395161a1i 11 . . . . . . . . . . . . 13 (𝑗 ∈ (1...𝑘) → 0 ≤ 2)
396 elfzle1 13444 . . . . . . . . . . . . 13 (𝑗 ∈ (1...𝑘) → 1 ≤ 𝑗)
397387, 394, 385, 395, 396lemul2ad 12095 . . . . . . . . . . . 12 (𝑗 ∈ (1...𝑘) → (2 · 1) ≤ (2 · 𝑗))
398386, 393, 387, 397lesub1dd 11771 . . . . . . . . . . 11 (𝑗 ∈ (1...𝑘) → ((2 · 1) − 1) ≤ ((2 · 𝑗) − 1))
399384, 388, 389, 392, 398ltletrd 11315 . . . . . . . . . 10 (𝑗 ∈ (1...𝑘) → 0 < ((2 · 𝑗) − 1))
400 elnnz 12509 . . . . . . . . . 10 (((2 · 𝑗) − 1) ∈ ℕ ↔ (((2 · 𝑗) − 1) ∈ ℤ ∧ 0 < ((2 · 𝑗) − 1)))
401383, 399, 400sylanbrc 583 . . . . . . . . 9 (𝑗 ∈ (1...𝑘) → ((2 · 𝑗) − 1) ∈ ℕ)
402401adantl 482 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑘)) → ((2 · 𝑗) − 1) ∈ ℕ)
403378, 402ffvelcdmd 7036 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑘)) → (𝐹‘((2 · 𝑗) − 1)) ∈ ℂ)
404403adantlr 713 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑘)) → (𝐹‘((2 · 𝑗) − 1)) ∈ ℂ)
40559fveq2d 6846 . . . . . . . 8 (𝑘 = 𝑗 → (𝐹‘((2 · 𝑘) − 1)) = (𝐹‘((2 · 𝑗) − 1)))
406405cbvmptv 5218 . . . . . . 7 (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))) = (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1)))
407406fvmpt2 6959 . . . . . 6 ((𝑗 ∈ ℕ ∧ (𝐹‘((2 · 𝑗) − 1)) ∈ ℂ) → ((𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))‘𝑗) = (𝐹‘((2 · 𝑗) − 1)))
408377, 404, 407syl2anc 584 . . . . 5 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑘)) → ((𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))‘𝑗) = (𝐹‘((2 · 𝑗) − 1)))
409 simpr 485 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
410409, 8eleqtrdi 2848 . . . . 5 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ (ℤ‘1))
411408, 410, 404fsumser 15615 . . . 4 ((𝜑𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...𝑘)(𝐹‘((2 · 𝑗) − 1)) = (seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))))‘𝑘))
412 eqidd 2737 . . . . 5 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))) → (𝐹𝑗) = (𝐹𝑗))
413155a1i 11 . . . . . . . . . 10 (𝑘 ∈ ℕ → (2 · 1) ∈ ℝ)
414 1red 11156 . . . . . . . . . 10 (𝑘 ∈ ℕ → 1 ∈ ℝ)
415161a1i 11 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 0 ≤ 2)
416 nnge1 12181 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 1 ≤ 𝑘)
417414, 40, 39, 415, 416lemul2ad 12095 . . . . . . . . . 10 (𝑘 ∈ ℕ → (2 · 1) ≤ (2 · 𝑘))
418413, 41, 414, 417lesub1dd 11771 . . . . . . . . 9 (𝑘 ∈ ℕ → ((2 · 1) − 1) ≤ ((2 · 𝑘) − 1))
419153, 418eqbrtrid 5140 . . . . . . . 8 (𝑘 ∈ ℕ → 1 ≤ ((2 · 𝑘) − 1))
420 eluz2 12769 . . . . . . . 8 (((2 · 𝑘) − 1) ∈ (ℤ‘1) ↔ (1 ∈ ℤ ∧ ((2 · 𝑘) − 1) ∈ ℤ ∧ 1 ≤ ((2 · 𝑘) − 1)))
42136, 65, 419, 420syl3anbrc 1343 . . . . . . 7 (𝑘 ∈ ℕ → ((2 · 𝑘) − 1) ∈ (ℤ‘1))
42267, 421eqeltrd 2838 . . . . . 6 (𝑘 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) ∈ (ℤ‘1))
423422adantl 482 . . . . 5 ((𝜑𝑘 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) ∈ (ℤ‘1))
424 simpll 765 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))) → 𝜑)
425 simpr 485 . . . . . . . 8 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))) → 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘)))
426371adantr 481 . . . . . . . 8 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))) → (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘)) = (1...((2 · 𝑘) − 1)))
427425, 426eleqtrd 2840 . . . . . . 7 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))) → 𝑗 ∈ (1...((2 · 𝑘) − 1)))
428427adantll 712 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))) → 𝑗 ∈ (1...((2 · 𝑘) − 1)))
429424, 428, 93syl2anc 584 . . . . 5 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))) → (𝐹𝑗) ∈ ℂ)
430412, 423, 429fsumser 15615 . . . 4 ((𝜑𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))(𝐹𝑗) = (seq1( + , 𝐹)‘((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘)))
431375, 411, 4303eqtr3d 2784 . . 3 ((𝜑𝑘 ∈ ℕ) → (seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))))‘𝑘) = (seq1( + , 𝐹)‘((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘)))
4321, 2, 6, 7, 8, 9, 11, 15, 16, 29, 73, 75, 431climsuse 43839 . 2 (𝜑 → seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ 𝐵)
433 eqidd 2737 . . . 4 ((𝜑𝑘 ∈ ℕ) → (𝐹𝑘) = (𝐹𝑘))
4348, 9, 433, 13isum 15604 . . 3 (𝜑 → Σ𝑘 ∈ ℕ (𝐹𝑘) = ( ⇝ ‘seq1( + , 𝐹)))
435 climrel 15374 . . . . . . 7 Rel ⇝
436435releldmi 5903 . . . . . 6 (seq1( + , 𝐹) ⇝ 𝐵 → seq1( + , 𝐹) ∈ dom ⇝ )
43716, 436syl 17 . . . . 5 (𝜑 → seq1( + , 𝐹) ∈ dom ⇝ )
438 climdm 15436 . . . . 5 (seq1( + , 𝐹) ∈ dom ⇝ ↔ seq1( + , 𝐹) ⇝ ( ⇝ ‘seq1( + , 𝐹)))
439437, 438sylib 217 . . . 4 (𝜑 → seq1( + , 𝐹) ⇝ ( ⇝ ‘seq1( + , 𝐹)))
440 climuni 15434 . . . 4 ((seq1( + , 𝐹) ⇝ ( ⇝ ‘seq1( + , 𝐹)) ∧ seq1( + , 𝐹) ⇝ 𝐵) → ( ⇝ ‘seq1( + , 𝐹)) = 𝐵)
441439, 16, 440syl2anc 584 . . 3 (𝜑 → ( ⇝ ‘seq1( + , 𝐹)) = 𝐵)
442435a1i 11 . . . . . . . 8 (𝜑 → Rel ⇝ )
443 releldm 5899 . . . . . . . 8 ((Rel ⇝ ∧ seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ 𝐵) → seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ∈ dom ⇝ )
444442, 432, 443syl2anc 584 . . . . . . 7 (𝜑 → seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ∈ dom ⇝ )
445 climdm 15436 . . . . . . 7 (seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ∈ dom ⇝ ↔ seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ ( ⇝ ‘seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))))))
446444, 445sylib 217 . . . . . 6 (𝜑 → seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ ( ⇝ ‘seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))))))
447406a1i 11 . . . . . . . 8 (𝜑 → (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))) = (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1))))
448447seqeq3d 13914 . . . . . . 7 (𝜑 → seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) = seq1( + , (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1)))))
449448fveq2d 6846 . . . . . 6 (𝜑 → ( ⇝ ‘seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))))) = ( ⇝ ‘seq1( + , (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1))))))
450446, 449breqtrd 5131 . . . . 5 (𝜑 → seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ ( ⇝ ‘seq1( + , (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1))))))
451 climuni 15434 . . . . 5 ((seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ 𝐵 ∧ seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ ( ⇝ ‘seq1( + , (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1)))))) → 𝐵 = ( ⇝ ‘seq1( + , (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1))))))
452432, 450, 451syl2anc 584 . . . 4 (𝜑𝐵 = ( ⇝ ‘seq1( + , (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1))))))
453 eqidd 2737 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1))) = (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1))))
454 eqcom 2743 . . . . . . . 8 (𝑘 = 𝑗𝑗 = 𝑘)
455 eqcom 2743 . . . . . . . 8 ((𝐹‘((2 · 𝑘) − 1)) = (𝐹‘((2 · 𝑗) − 1)) ↔ (𝐹‘((2 · 𝑗) − 1)) = (𝐹‘((2 · 𝑘) − 1)))
456405, 454, 4553imtr3i 290 . . . . . . 7 (𝑗 = 𝑘 → (𝐹‘((2 · 𝑗) − 1)) = (𝐹‘((2 · 𝑘) − 1)))
457456adantl 482 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 = 𝑘) → (𝐹‘((2 · 𝑗) − 1)) = (𝐹‘((2 · 𝑘) − 1)))
45812adantr 481 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → 𝐹:ℕ⟶ℂ)
459421, 8eleqtrrdi 2849 . . . . . . . 8 (𝑘 ∈ ℕ → ((2 · 𝑘) − 1) ∈ ℕ)
460459adantl 482 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → ((2 · 𝑘) − 1) ∈ ℕ)
461458, 460ffvelcdmd 7036 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → (𝐹‘((2 · 𝑘) − 1)) ∈ ℂ)
462453, 457, 409, 461fvmptd 6955 . . . . 5 ((𝜑𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1)))‘𝑘) = (𝐹‘((2 · 𝑘) − 1)))
4638, 9, 462, 461isum 15604 . . . 4 (𝜑 → Σ𝑘 ∈ ℕ (𝐹‘((2 · 𝑘) − 1)) = ( ⇝ ‘seq1( + , (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1))))))
464452, 463eqtr4d 2779 . . 3 (𝜑𝐵 = Σ𝑘 ∈ ℕ (𝐹‘((2 · 𝑘) − 1)))
465434, 441, 4643eqtrd 2780 . 2 (𝜑 → Σ𝑘 ∈ ℕ (𝐹𝑘) = Σ𝑘 ∈ ℕ (𝐹‘((2 · 𝑘) − 1)))
466432, 465jca 512 1 (𝜑 → (seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ 𝐵 ∧ Σ𝑘 ∈ ℕ (𝐹𝑘) = Σ𝑘 ∈ ℕ (𝐹‘((2 · 𝑘) − 1))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  wo 845  w3a 1087   = wceq 1541  wcel 2106  wne 2943  wral 3064  wrex 3073  {crab 3407  Vcvv 3445  cdif 3907  cun 3908  cin 3909  wss 3910  c0 4282   class class class wbr 5105  cmpt 5188  dom cdm 5633  Rel wrel 5638  wf 6492  1-1wf1 6493  ontowfo 6494  1-1-ontowf1o 6495  cfv 6496  (class class class)co 7357  Fincfn 8883  cc 11049  cr 11050  0cc0 11051  1c1 11052   + caddc 11054   · cmul 11056   < clt 11189  cle 11190  cmin 11385   / cdiv 11812  cn 12153  2c2 12208  cz 12499  cuz 12763  +crp 12915  ...cfz 13424  seqcseq 13906  cli 15366  Σcsu 15570
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-inf2 9577  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-sup 9378  df-oi 9446  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-n0 12414  df-z 12500  df-uz 12764  df-rp 12916  df-fz 13425  df-fzo 13568  df-seq 13907  df-exp 13968  df-hash 14231  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-clim 15370  df-sum 15571
This theorem is referenced by:  fouriersw  44462
  Copyright terms: Public domain W3C validator