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

Theorem sumnnodd 38697
 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 1830 . . 3 𝑘𝜑
2 nfcv 2751 . . 3 𝑘seq1( + , 𝐹)
3 nfcv 2751 . . . 4 𝑘1
4 nfcv 2751 . . . 4 𝑘 +
5 nfmpt1 4675 . . . 4 𝑘(𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))
63, 4, 5nfseq 12673 . . 3 𝑘seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))))
7 nfmpt1 4675 . . 3 𝑘(𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))
8 nnuz 11599 . . 3 ℕ = (ℤ‘1)
9 1zzd 11285 . . 3 (𝜑 → 1 ∈ ℤ)
10 seqex 12665 . . . 4 seq1( + , 𝐹) ∈ V
1110a1i 11 . . 3 (𝜑 → seq1( + , 𝐹) ∈ V)
12 sumnnodd.1 . . . . . 6 (𝜑𝐹:ℕ⟶ℂ)
1312ffvelrnda 6267 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ℂ)
148, 9, 13serf 12691 . . . 4 (𝜑 → seq1( + , 𝐹):ℕ⟶ℂ)
1514ffvelrnda 6267 . . 3 ((𝜑𝑘 ∈ ℕ) → (seq1( + , 𝐹)‘𝑘) ∈ ℂ)
16 sumnnodd.sc . . 3 (𝜑 → seq1( + , 𝐹) ⇝ 𝐵)
17 1nn 10908 . . . . . . 7 1 ∈ ℕ
18 oveq2 6557 . . . . . . . . 9 (𝑘 = 1 → (2 · 𝑘) = (2 · 1))
1918oveq1d 6564 . . . . . . . 8 (𝑘 = 1 → ((2 · 𝑘) − 1) = ((2 · 1) − 1))
20 eqid 2610 . . . . . . . 8 (𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1)) = (𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))
21 ovex 6577 . . . . . . . 8 ((2 · 1) − 1) ∈ V
2219, 20, 21fvmpt 6191 . . . . . . 7 (1 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘1) = ((2 · 1) − 1))
2317, 22ax-mp 5 . . . . . 6 ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘1) = ((2 · 1) − 1)
24 2t1e2 11053 . . . . . . 7 (2 · 1) = 2
2524oveq1i 6559 . . . . . 6 ((2 · 1) − 1) = (2 − 1)
26 2m1e1 11012 . . . . . 6 (2 − 1) = 1
2723, 25, 263eqtri 2636 . . . . 5 ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘1) = 1
2827, 17eqeltri 2684 . . . 4 ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘1) ∈ ℕ
2928a1i 11 . . 3 (𝜑 → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘1) ∈ ℕ)
30 2z 11286 . . . . . . . 8 2 ∈ ℤ
3130a1i 11 . . . . . . 7 (𝑘 ∈ ℕ → 2 ∈ ℤ)
32 nnz 11276 . . . . . . 7 (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
3331, 32zmulcld 11364 . . . . . 6 (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℤ)
3432peano2zd 11361 . . . . . . . 8 (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℤ)
3531, 34zmulcld 11364 . . . . . . 7 (𝑘 ∈ ℕ → (2 · (𝑘 + 1)) ∈ ℤ)
36 1zzd 11285 . . . . . . 7 (𝑘 ∈ ℕ → 1 ∈ ℤ)
3735, 36zsubcld 11363 . . . . . 6 (𝑘 ∈ ℕ → ((2 · (𝑘 + 1)) − 1) ∈ ℤ)
38 2re 10967 . . . . . . . . . 10 2 ∈ ℝ
3938a1i 11 . . . . . . . . 9 (𝑘 ∈ ℕ → 2 ∈ ℝ)
40 nnre 10904 . . . . . . . . 9 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
4139, 40remulcld 9949 . . . . . . . 8 (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℝ)
4241lep1d 10834 . . . . . . 7 (𝑘 ∈ ℕ → (2 · 𝑘) ≤ ((2 · 𝑘) + 1))
43 2cnd 10970 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 2 ∈ ℂ)
44 nncn 10905 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
45 1cnd 9935 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 1 ∈ ℂ)
4643, 44, 45adddid 9943 . . . . . . . . . 10 (𝑘 ∈ ℕ → (2 · (𝑘 + 1)) = ((2 · 𝑘) + (2 · 1)))
4724oveq2i 6560 . . . . . . . . . 10 ((2 · 𝑘) + (2 · 1)) = ((2 · 𝑘) + 2)
4846, 47syl6eq 2660 . . . . . . . . 9 (𝑘 ∈ ℕ → (2 · (𝑘 + 1)) = ((2 · 𝑘) + 2))
4948oveq1d 6564 . . . . . . . 8 (𝑘 ∈ ℕ → ((2 · (𝑘 + 1)) − 1) = (((2 · 𝑘) + 2) − 1))
5043, 44mulcld 9939 . . . . . . . . 9 (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℂ)
5150, 43, 45addsubassd 10291 . . . . . . . 8 (𝑘 ∈ ℕ → (((2 · 𝑘) + 2) − 1) = ((2 · 𝑘) + (2 − 1)))
5226oveq2i 6560 . . . . . . . . 9 ((2 · 𝑘) + (2 − 1)) = ((2 · 𝑘) + 1)
5352a1i 11 . . . . . . . 8 (𝑘 ∈ ℕ → ((2 · 𝑘) + (2 − 1)) = ((2 · 𝑘) + 1))
5449, 51, 533eqtrrd 2649 . . . . . . 7 (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) = ((2 · (𝑘 + 1)) − 1))
5542, 54breqtrd 4609 . . . . . 6 (𝑘 ∈ ℕ → (2 · 𝑘) ≤ ((2 · (𝑘 + 1)) − 1))
56 eluz2 11569 . . . . . 6 (((2 · (𝑘 + 1)) − 1) ∈ (ℤ‘(2 · 𝑘)) ↔ ((2 · 𝑘) ∈ ℤ ∧ ((2 · (𝑘 + 1)) − 1) ∈ ℤ ∧ (2 · 𝑘) ≤ ((2 · (𝑘 + 1)) − 1)))
5733, 37, 55, 56syl3anbrc 1239 . . . . 5 (𝑘 ∈ ℕ → ((2 · (𝑘 + 1)) − 1) ∈ (ℤ‘(2 · 𝑘)))
58 oveq2 6557 . . . . . . . . 9 (𝑘 = 𝑗 → (2 · 𝑘) = (2 · 𝑗))
5958oveq1d 6564 . . . . . . . 8 (𝑘 = 𝑗 → ((2 · 𝑘) − 1) = ((2 · 𝑗) − 1))
6059cbvmptv 4678 . . . . . . 7 (𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1)) = (𝑗 ∈ ℕ ↦ ((2 · 𝑗) − 1))
6160a1i 11 . . . . . 6 (𝑘 ∈ ℕ → (𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1)) = (𝑗 ∈ ℕ ↦ ((2 · 𝑗) − 1)))
62 oveq2 6557 . . . . . . . 8 (𝑗 = (𝑘 + 1) → (2 · 𝑗) = (2 · (𝑘 + 1)))
6362oveq1d 6564 . . . . . . 7 (𝑗 = (𝑘 + 1) → ((2 · 𝑗) − 1) = ((2 · (𝑘 + 1)) − 1))
6463adantl 481 . . . . . 6 ((𝑘 ∈ ℕ ∧ 𝑗 = (𝑘 + 1)) → ((2 · 𝑗) − 1) = ((2 · (𝑘 + 1)) − 1))
65 peano2nn 10909 . . . . . 6 (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
6661, 64, 65, 37fvmptd 6197 . . . . 5 (𝑘 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘(𝑘 + 1)) = ((2 · (𝑘 + 1)) − 1))
6733, 36zsubcld 11363 . . . . . . . . 9 (𝑘 ∈ ℕ → ((2 · 𝑘) − 1) ∈ ℤ)
6820fvmpt2 6200 . . . . . . . . 9 ((𝑘 ∈ ℕ ∧ ((2 · 𝑘) − 1) ∈ ℤ) → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) = ((2 · 𝑘) − 1))
6967, 68mpdan 699 . . . . . . . 8 (𝑘 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) = ((2 · 𝑘) − 1))
7069oveq1d 6564 . . . . . . 7 (𝑘 ∈ ℕ → (((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) + 1) = (((2 · 𝑘) − 1) + 1))
7150, 45npcand 10275 . . . . . . 7 (𝑘 ∈ ℕ → (((2 · 𝑘) − 1) + 1) = (2 · 𝑘))
7270, 71eqtrd 2644 . . . . . 6 (𝑘 ∈ ℕ → (((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) + 1) = (2 · 𝑘))
7372fveq2d 6107 . . . . 5 (𝑘 ∈ ℕ → (ℤ‘(((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) + 1)) = (ℤ‘(2 · 𝑘)))
7457, 66, 733eltr4d 2703 . . . 4 (𝑘 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘(𝑘 + 1)) ∈ (ℤ‘(((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) + 1)))
7574adantl 481 . . 3 ((𝜑𝑘 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘(𝑘 + 1)) ∈ (ℤ‘(((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) + 1)))
76 seqex 12665 . . . 4 seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ∈ V
7776a1i 11 . . 3 (𝜑 → seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ∈ V)
78 incom 3767 . . . . . . . . . 10 (((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) = (((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
79 inss2 3796 . . . . . . . . . . 11 ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}
80 ssrin 3800 . . . . . . . . . . 11 (((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} → (((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) ⊆ ({𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} ∩ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})))
8179, 80ax-mp 5 . . . . . . . . . 10 (((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) ⊆ ({𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} ∩ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
8278, 81eqsstri 3598 . . . . . . . . 9 (((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) ⊆ ({𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} ∩ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
83 disjdif 3992 . . . . . . . . 9 ({𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} ∩ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) = ∅
8482, 83sseqtri 3600 . . . . . . . 8 (((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) ⊆ ∅
85 ss0 3926 . . . . . . . 8 ((((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) ⊆ ∅ → (((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) = ∅)
8684, 85mp1i 13 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) = ∅)
87 uncom 3719 . . . . . . . . 9 (((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∪ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) = (((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∪ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
88 inundif 3998 . . . . . . . . 9 (((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∪ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) = (1...((2 · 𝑘) − 1))
8987, 88eqtr2i 2633 . . . . . . . 8 (1...((2 · 𝑘) − 1)) = (((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∪ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
9089a1i 11 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (1...((2 · 𝑘) − 1)) = (((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∪ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})))
91 fzfid 12634 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (1...((2 · 𝑘) − 1)) ∈ Fin)
9212adantr 480 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...((2 · 𝑘) − 1))) → 𝐹:ℕ⟶ℂ)
93 elfznn 12241 . . . . . . . . . 10 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → 𝑗 ∈ ℕ)
9493adantl 481 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...((2 · 𝑘) − 1))) → 𝑗 ∈ ℕ)
9592, 94ffvelrnd 6268 . . . . . . . 8 ((𝜑𝑗 ∈ (1...((2 · 𝑘) − 1))) → (𝐹𝑗) ∈ ℂ)
9695adantlr 747 . . . . . . 7 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → (𝐹𝑗) ∈ ℂ)
9786, 90, 91, 96fsumsplit 14318 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...((2 · 𝑘) − 1))(𝐹𝑗) = (Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗) + Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗)))
98 simpl 472 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → 𝜑)
99 ssrab2 3650 . . . . . . . . . . . . . 14 {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} ⊆ ℕ
10079sseli 3564 . . . . . . . . . . . . . 14 (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → 𝑗 ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})
10199, 100sseldi 3566 . . . . . . . . . . . . 13 (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → 𝑗 ∈ ℕ)
102101adantl 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → 𝑗 ∈ ℕ)
103 oveq1 6556 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑗 → (𝑘 / 2) = (𝑗 / 2))
104103eleq1d 2672 . . . . . . . . . . . . . . 15 (𝑘 = 𝑗 → ((𝑘 / 2) ∈ ℕ ↔ (𝑗 / 2) ∈ ℕ))
105 oveq1 6556 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑘 → (𝑛 / 2) = (𝑘 / 2))
106105eleq1d 2672 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑘 → ((𝑛 / 2) ∈ ℕ ↔ (𝑘 / 2) ∈ ℕ))
107106elrab 3331 . . . . . . . . . . . . . . . 16 (𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} ↔ (𝑘 ∈ ℕ ∧ (𝑘 / 2) ∈ ℕ))
108107simprbi 479 . . . . . . . . . . . . . . 15 (𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} → (𝑘 / 2) ∈ ℕ)
109104, 108vtoclga 3245 . . . . . . . . . . . . . 14 (𝑗 ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} → (𝑗 / 2) ∈ ℕ)
110100, 109syl 17 . . . . . . . . . . . . 13 (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → (𝑗 / 2) ∈ ℕ)
111110adantl 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (𝑗 / 2) ∈ ℕ)
112 eleq1 2676 . . . . . . . . . . . . . . 15 (𝑘 = 𝑗 → (𝑘 ∈ ℕ ↔ 𝑗 ∈ ℕ))
113112, 1043anbi23d 1394 . . . . . . . . . . . . . 14 (𝑘 = 𝑗 → ((𝜑𝑘 ∈ ℕ ∧ (𝑘 / 2) ∈ ℕ) ↔ (𝜑𝑗 ∈ ℕ ∧ (𝑗 / 2) ∈ ℕ)))
114 fveq2 6103 . . . . . . . . . . . . . . 15 (𝑘 = 𝑗 → (𝐹𝑘) = (𝐹𝑗))
115114eqeq1d 2612 . . . . . . . . . . . . . 14 (𝑘 = 𝑗 → ((𝐹𝑘) = 0 ↔ (𝐹𝑗) = 0))
116113, 115imbi12d 333 . . . . . . . . . . . . 13 (𝑘 = 𝑗 → (((𝜑𝑘 ∈ ℕ ∧ (𝑘 / 2) ∈ ℕ) → (𝐹𝑘) = 0) ↔ ((𝜑𝑗 ∈ ℕ ∧ (𝑗 / 2) ∈ ℕ) → (𝐹𝑗) = 0)))
117 sumnnodd.even0 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ ∧ (𝑘 / 2) ∈ ℕ) → (𝐹𝑘) = 0)
118116, 117chvarv 2251 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ ∧ (𝑗 / 2) ∈ ℕ) → (𝐹𝑗) = 0)
11998, 102, 111, 118syl3anc 1318 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (𝐹𝑗) = 0)
120119sumeq2dv 14281 . . . . . . . . . 10 (𝜑 → Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗) = Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})0)
121 fzfid 12634 . . . . . . . . . . . . 13 (𝜑 → (1...((2 · 𝑘) − 1)) ∈ Fin)
122 inss1 3795 . . . . . . . . . . . . . 14 ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ (1...((2 · 𝑘) − 1))
123122a1i 11 . . . . . . . . . . . . 13 (𝜑 → ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ (1...((2 · 𝑘) − 1)))
124 ssfi 8065 . . . . . . . . . . . . 13 (((1...((2 · 𝑘) − 1)) ∈ Fin ∧ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ (1...((2 · 𝑘) − 1))) → ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∈ Fin)
125121, 123, 124syl2anc 691 . . . . . . . . . . . 12 (𝜑 → ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∈ Fin)
126125olcd 407 . . . . . . . . . . 11 (𝜑 → (((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ (ℤ𝐶) ∨ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∈ Fin))
127 sumz 14300 . . . . . . . . . . 11 ((((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ (ℤ𝐶) ∨ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∈ Fin) → Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})0 = 0)
128126, 127syl 17 . . . . . . . . . 10 (𝜑 → Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})0 = 0)
129120, 128eqtrd 2644 . . . . . . . . 9 (𝜑 → Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗) = 0)
130129adantr 480 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗) = 0)
131130oveq2d 6565 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗) + Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗)) = (Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗) + 0))
132 fzfi 12633 . . . . . . . . . . . 12 (1...((2 · 𝑘) − 1)) ∈ Fin
133 difss 3699 . . . . . . . . . . . 12 ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ (1...((2 · 𝑘) − 1))
134 ssfi 8065 . . . . . . . . . . . 12 (((1...((2 · 𝑘) − 1)) ∈ Fin ∧ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ (1...((2 · 𝑘) − 1))) → ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∈ Fin)
135132, 133, 134mp2an 704 . . . . . . . . . . 11 ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∈ Fin
136135a1i 11 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∈ Fin)
137133sseli 3564 . . . . . . . . . . . 12 (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → 𝑗 ∈ (1...((2 · 𝑘) − 1)))
138137, 95sylan2 490 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (𝐹𝑗) ∈ ℂ)
139138adantlr 747 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (𝐹𝑗) ∈ ℂ)
140136, 139fsumcl 14311 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗) ∈ ℂ)
141140addid1d 10115 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗) + 0) = Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗))
142 fveq2 6103 . . . . . . . . 9 (𝑗 = 𝑖 → (𝐹𝑗) = (𝐹𝑖))
143142cbvsumv 14274 . . . . . . . 8 Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗) = Σ𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑖)
144141, 143syl6eq 2660 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗) + 0) = Σ𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑖))
145131, 144eqtrd 2644 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → (Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗) + Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗)) = Σ𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑖))
146 fveq2 6103 . . . . . . 7 (𝑖 = ((2 · 𝑗) − 1) → (𝐹𝑖) = (𝐹‘((2 · 𝑗) − 1)))
147 fzfid 12634 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (1...𝑘) ∈ Fin)
148 1zzd 11285 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 1 ∈ ℤ)
14967adantr 480 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → ((2 · 𝑘) − 1) ∈ ℤ)
15030a1i 11 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...𝑘) → 2 ∈ ℤ)
151 elfzelz 12213 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...𝑘) → 𝑖 ∈ ℤ)
152150, 151zmulcld 11364 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...𝑘) → (2 · 𝑖) ∈ ℤ)
153 1zzd 11285 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...𝑘) → 1 ∈ ℤ)
154152, 153zsubcld 11363 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1...𝑘) → ((2 · 𝑖) − 1) ∈ ℤ)
155154adantl 481 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → ((2 · 𝑖) − 1) ∈ ℤ)
156148, 149, 1553jca 1235 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → (1 ∈ ℤ ∧ ((2 · 𝑘) − 1) ∈ ℤ ∧ ((2 · 𝑖) − 1) ∈ ℤ))
15725, 26eqtr2i 2633 . . . . . . . . . . . . . . . 16 1 = ((2 · 1) − 1)
158 1re 9918 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℝ
15938, 158remulcli 9933 . . . . . . . . . . . . . . . . . 18 (2 · 1) ∈ ℝ
160159a1i 11 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...𝑘) → (2 · 1) ∈ ℝ)
161152zred 11358 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...𝑘) → (2 · 𝑖) ∈ ℝ)
162 1red 9934 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...𝑘) → 1 ∈ ℝ)
163151zred 11358 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑘) → 𝑖 ∈ ℝ)
16438a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑘) → 2 ∈ ℝ)
165 0le2 10988 . . . . . . . . . . . . . . . . . . 19 0 ≤ 2
166165a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑘) → 0 ≤ 2)
167 elfzle1 12215 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑘) → 1 ≤ 𝑖)
168162, 163, 164, 166, 167lemul2ad 10843 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...𝑘) → (2 · 1) ≤ (2 · 𝑖))
169160, 161, 162, 168lesub1dd 10522 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...𝑘) → ((2 · 1) − 1) ≤ ((2 · 𝑖) − 1))
170157, 169syl5eqbr 4618 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1...𝑘) → 1 ≤ ((2 · 𝑖) − 1))
171170adantl 481 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 1 ≤ ((2 · 𝑖) − 1))
172161adantl 481 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → (2 · 𝑖) ∈ ℝ)
17341adantr 480 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → (2 · 𝑘) ∈ ℝ)
174 1red 9934 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 1 ∈ ℝ)
175163adantl 481 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 𝑖 ∈ ℝ)
17640adantr 480 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 𝑘 ∈ ℝ)
17738a1i 11 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 2 ∈ ℝ)
178165a1i 11 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 0 ≤ 2)
179 elfzle2 12216 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...𝑘) → 𝑖𝑘)
180179adantl 481 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 𝑖𝑘)
181175, 176, 177, 178, 180lemul2ad 10843 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → (2 · 𝑖) ≤ (2 · 𝑘))
182172, 173, 174, 181lesub1dd 10522 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → ((2 · 𝑖) − 1) ≤ ((2 · 𝑘) − 1))
183171, 182jca 553 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → (1 ≤ ((2 · 𝑖) − 1) ∧ ((2 · 𝑖) − 1) ≤ ((2 · 𝑘) − 1)))
184 elfz2 12204 . . . . . . . . . . . . 13 (((2 · 𝑖) − 1) ∈ (1...((2 · 𝑘) − 1)) ↔ ((1 ∈ ℤ ∧ ((2 · 𝑘) − 1) ∈ ℤ ∧ ((2 · 𝑖) − 1) ∈ ℤ) ∧ (1 ≤ ((2 · 𝑖) − 1) ∧ ((2 · 𝑖) − 1) ≤ ((2 · 𝑘) − 1))))
185156, 183, 184sylanbrc 695 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → ((2 · 𝑖) − 1) ∈ (1...((2 · 𝑘) − 1)))
186152zcnd 11359 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑘) → (2 · 𝑖) ∈ ℂ)
187 1cnd 9935 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑘) → 1 ∈ ℂ)
188 2cnd 10970 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑘) → 2 ∈ ℂ)
189 2ne0 10990 . . . . . . . . . . . . . . . . . . 19 2 ≠ 0
190189a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑘) → 2 ≠ 0)
191186, 187, 188, 190divsubdird 10719 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...𝑘) → (((2 · 𝑖) − 1) / 2) = (((2 · 𝑖) / 2) − (1 / 2)))
192151zcnd 11359 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (1...𝑘) → 𝑖 ∈ ℂ)
193192, 188, 190divcan3d 10685 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑘) → ((2 · 𝑖) / 2) = 𝑖)
194193oveq1d 6564 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...𝑘) → (((2 · 𝑖) / 2) − (1 / 2)) = (𝑖 − (1 / 2)))
195191, 194eqtrd 2644 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...𝑘) → (((2 · 𝑖) − 1) / 2) = (𝑖 − (1 / 2)))
196151, 153zsubcld 11363 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑘) → (𝑖 − 1) ∈ ℤ)
197164, 190rereccld 10731 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (1...𝑘) → (1 / 2) ∈ ℝ)
198 halflt1 11127 . . . . . . . . . . . . . . . . . . . 20 (1 / 2) < 1
199198a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (1...𝑘) → (1 / 2) < 1)
200197, 162, 163, 199ltsub2dd 10519 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑘) → (𝑖 − 1) < (𝑖 − (1 / 2)))
201 2rp 11713 . . . . . . . . . . . . . . . . . . . . 21 2 ∈ ℝ+
202 rpreccl 11733 . . . . . . . . . . . . . . . . . . . . 21 (2 ∈ ℝ+ → (1 / 2) ∈ ℝ+)
203201, 202mp1i 13 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (1...𝑘) → (1 / 2) ∈ ℝ+)
204163, 203ltsubrpd 11780 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (1...𝑘) → (𝑖 − (1 / 2)) < 𝑖)
205192, 187npcand 10275 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (1...𝑘) → ((𝑖 − 1) + 1) = 𝑖)
206204, 205breqtrrd 4611 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑘) → (𝑖 − (1 / 2)) < ((𝑖 − 1) + 1))
207 btwnnz 11329 . . . . . . . . . . . . . . . . . 18 (((𝑖 − 1) ∈ ℤ ∧ (𝑖 − 1) < (𝑖 − (1 / 2)) ∧ (𝑖 − (1 / 2)) < ((𝑖 − 1) + 1)) → ¬ (𝑖 − (1 / 2)) ∈ ℤ)
208196, 200, 206, 207syl3anc 1318 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...𝑘) → ¬ (𝑖 − (1 / 2)) ∈ ℤ)
209 nnz 11276 . . . . . . . . . . . . . . . . 17 ((𝑖 − (1 / 2)) ∈ ℕ → (𝑖 − (1 / 2)) ∈ ℤ)
210208, 209nsyl 134 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...𝑘) → ¬ (𝑖 − (1 / 2)) ∈ ℕ)
211195, 210eqneltrd 2707 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1...𝑘) → ¬ (((2 · 𝑖) − 1) / 2) ∈ ℕ)
212211intnand 953 . . . . . . . . . . . . . 14 (𝑖 ∈ (1...𝑘) → ¬ (((2 · 𝑖) − 1) ∈ ℕ ∧ (((2 · 𝑖) − 1) / 2) ∈ ℕ))
213 oveq1 6556 . . . . . . . . . . . . . . . 16 (𝑛 = ((2 · 𝑖) − 1) → (𝑛 / 2) = (((2 · 𝑖) − 1) / 2))
214213eleq1d 2672 . . . . . . . . . . . . . . 15 (𝑛 = ((2 · 𝑖) − 1) → ((𝑛 / 2) ∈ ℕ ↔ (((2 · 𝑖) − 1) / 2) ∈ ℕ))
215214elrab 3331 . . . . . . . . . . . . . 14 (((2 · 𝑖) − 1) ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} ↔ (((2 · 𝑖) − 1) ∈ ℕ ∧ (((2 · 𝑖) − 1) / 2) ∈ ℕ))
216212, 215sylnibr 318 . . . . . . . . . . . . 13 (𝑖 ∈ (1...𝑘) → ¬ ((2 · 𝑖) − 1) ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})
217216adantl 481 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → ¬ ((2 · 𝑖) − 1) ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})
218185, 217eldifd 3551 . . . . . . . . . . 11 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → ((2 · 𝑖) − 1) ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
219 eqid 2610 . . . . . . . . . . 11 (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)) = (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))
220218, 219fmptd 6292 . . . . . . . . . 10 (𝑘 ∈ ℕ → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)⟶((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
221 eqidd 2611 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (1...𝑘) → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)) = (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)))
222 oveq2 6557 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑥 → (2 · 𝑖) = (2 · 𝑥))
223222oveq1d 6564 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑥 → ((2 · 𝑖) − 1) = ((2 · 𝑥) − 1))
224223adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1...𝑘) ∧ 𝑖 = 𝑥) → ((2 · 𝑖) − 1) = ((2 · 𝑥) − 1))
225 id 22 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (1...𝑘) → 𝑥 ∈ (1...𝑘))
226 ovex 6577 . . . . . . . . . . . . . . . . . . 19 ((2 · 𝑥) − 1) ∈ V
227226a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (1...𝑘) → ((2 · 𝑥) − 1) ∈ V)
228221, 224, 225, 227fvmptd 6197 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (1...𝑘) → ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((2 · 𝑥) − 1))
229228eqcomd 2616 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1...𝑘) → ((2 · 𝑥) − 1) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥))
230229ad2antrr 758 . . . . . . . . . . . . . . 15 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦)) → ((2 · 𝑥) − 1) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥))
231 simpr 476 . . . . . . . . . . . . . . 15 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦)) → ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦))
232 eqidd 2611 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (1...𝑘) → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)) = (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)))
233 oveq2 6557 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑦 → (2 · 𝑖) = (2 · 𝑦))
234233oveq1d 6564 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑦 → ((2 · 𝑖) − 1) = ((2 · 𝑦) − 1))
235234adantl 481 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ (1...𝑘) ∧ 𝑖 = 𝑦) → ((2 · 𝑖) − 1) = ((2 · 𝑦) − 1))
236 id 22 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (1...𝑘) → 𝑦 ∈ (1...𝑘))
237 ovex 6577 . . . . . . . . . . . . . . . . . 18 ((2 · 𝑦) − 1) ∈ V
238237a1i 11 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (1...𝑘) → ((2 · 𝑦) − 1) ∈ V)
239232, 235, 236, 238fvmptd 6197 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (1...𝑘) → ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦) = ((2 · 𝑦) − 1))
240239ad2antlr 759 . . . . . . . . . . . . . . 15 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦)) → ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦) = ((2 · 𝑦) − 1))
241230, 231, 2403eqtrd 2648 . . . . . . . . . . . . . 14 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦)) → ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1))
242 2cnd 10970 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (1...𝑘) → 2 ∈ ℂ)
243 elfzelz 12213 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (1...𝑘) → 𝑥 ∈ ℤ)
244243zcnd 11359 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (1...𝑘) → 𝑥 ∈ ℂ)
245242, 244mulcld 9939 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (1...𝑘) → (2 · 𝑥) ∈ ℂ)
246245ad2antrr 758 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1)) → (2 · 𝑥) ∈ ℂ)
247 2cnd 10970 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (1...𝑘) → 2 ∈ ℂ)
248 elfzelz 12213 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (1...𝑘) → 𝑦 ∈ ℤ)
249248zcnd 11359 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (1...𝑘) → 𝑦 ∈ ℂ)
250247, 249mulcld 9939 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (1...𝑘) → (2 · 𝑦) ∈ ℂ)
251250ad2antlr 759 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1)) → (2 · 𝑦) ∈ ℂ)
252 1cnd 9935 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1)) → 1 ∈ ℂ)
253 simpr 476 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1)) → ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1))
254246, 251, 252, 253subcan2d 10313 . . . . . . . . . . . . . . 15 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1)) → (2 · 𝑥) = (2 · 𝑦))
255244ad2antrr 758 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ (2 · 𝑥) = (2 · 𝑦)) → 𝑥 ∈ ℂ)
256249ad2antlr 759 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ (2 · 𝑥) = (2 · 𝑦)) → 𝑦 ∈ ℂ)
257 2cnd 10970 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ (2 · 𝑥) = (2 · 𝑦)) → 2 ∈ ℂ)
258189a1i 11 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ (2 · 𝑥) = (2 · 𝑦)) → 2 ≠ 0)
259 simpr 476 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ (2 · 𝑥) = (2 · 𝑦)) → (2 · 𝑥) = (2 · 𝑦))
260255, 256, 257, 258, 259mulcanad 10541 . . . . . . . . . . . . . . 15 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ (2 · 𝑥) = (2 · 𝑦)) → 𝑥 = 𝑦)
261254, 260syldan 486 . . . . . . . . . . . . . 14 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1)) → 𝑥 = 𝑦)
262241, 261syldan 486 . . . . . . . . . . . . 13 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦)) → 𝑥 = 𝑦)
263262adantll 746 . . . . . . . . . . . 12 (((𝑘 ∈ ℕ ∧ (𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘))) ∧ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦)) → 𝑥 = 𝑦)
264263ex 449 . . . . . . . . . . 11 ((𝑘 ∈ ℕ ∧ (𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘))) → (((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦) → 𝑥 = 𝑦))
265264ralrimivva 2954 . . . . . . . . . 10 (𝑘 ∈ ℕ → ∀𝑥 ∈ (1...𝑘)∀𝑦 ∈ (1...𝑘)(((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦) → 𝑥 = 𝑦))
266 dff13 6416 . . . . . . . . . 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))‘𝑦) → 𝑥 = 𝑦)))
267220, 265, 266sylanbrc 695 . . . . . . . . 9 (𝑘 ∈ ℕ → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)–1-1→((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
268 1zzd 11285 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → 1 ∈ ℤ)
26932adantr 480 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → 𝑘 ∈ ℤ)
270 fzssz 12214 . . . . . . . . . . . . . . . . . . . 20 (1...((2 · 𝑘) − 1)) ⊆ ℤ
271270, 137sseldi 3566 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → 𝑗 ∈ ℤ)
272 zeo 11339 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℤ → ((𝑗 / 2) ∈ ℤ ∨ ((𝑗 + 1) / 2) ∈ ℤ))
273271, 272syl 17 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → ((𝑗 / 2) ∈ ℤ ∨ ((𝑗 + 1) / 2) ∈ ℤ))
274273adantl 481 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → ((𝑗 / 2) ∈ ℤ ∨ ((𝑗 + 1) / 2) ∈ ℤ))
275 eldifn 3695 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → ¬ 𝑗 ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})
276137, 93syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → 𝑗 ∈ ℕ)
277276adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → 𝑗 ∈ ℕ)
278 simpr 476 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → (𝑗 / 2) ∈ ℤ)
279277nnred 10912 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → 𝑗 ∈ ℝ)
28038a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → 2 ∈ ℝ)
281277nngt0d 10941 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → 0 < 𝑗)
282 2pos 10989 . . . . . . . . . . . . . . . . . . . . . . 23 0 < 2
283282a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → 0 < 2)
284279, 280, 281, 283divgt0d 10838 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → 0 < (𝑗 / 2))
285 elnnz 11264 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗 / 2) ∈ ℕ ↔ ((𝑗 / 2) ∈ ℤ ∧ 0 < (𝑗 / 2)))
286278, 284, 285sylanbrc 695 . . . . . . . . . . . . . . . . . . . 20 ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → (𝑗 / 2) ∈ ℕ)
287 oveq1 6556 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑗 → (𝑛 / 2) = (𝑗 / 2))
288287eleq1d 2672 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑗 → ((𝑛 / 2) ∈ ℕ ↔ (𝑗 / 2) ∈ ℕ))
289288elrab 3331 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} ↔ (𝑗 ∈ ℕ ∧ (𝑗 / 2) ∈ ℕ))
290277, 286, 289sylanbrc 695 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → 𝑗 ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})
291275, 290mtand 689 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → ¬ (𝑗 / 2) ∈ ℤ)
292291adantl 481 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → ¬ (𝑗 / 2) ∈ ℤ)
293 pm2.53 387 . . . . . . . . . . . . . . . . 17 (((𝑗 / 2) ∈ ℤ ∨ ((𝑗 + 1) / 2) ∈ ℤ) → (¬ (𝑗 / 2) ∈ ℤ → ((𝑗 + 1) / 2) ∈ ℤ))
294274, 292, 293sylc 63 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → ((𝑗 + 1) / 2) ∈ ℤ)
295268, 269, 2943jca 1235 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (1 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ ((𝑗 + 1) / 2) ∈ ℤ))
296 1p1e2 11011 . . . . . . . . . . . . . . . . . . . 20 (1 + 1) = 2
297296oveq1i 6559 . . . . . . . . . . . . . . . . . . 19 ((1 + 1) / 2) = (2 / 2)
298 2div2e1 11027 . . . . . . . . . . . . . . . . . . 19 (2 / 2) = 1
299297, 298eqtr2i 2633 . . . . . . . . . . . . . . . . . 18 1 = ((1 + 1) / 2)
300 1red 9934 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → 1 ∈ ℝ)
301300, 300readdcld 9948 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → (1 + 1) ∈ ℝ)
30293nnred 10912 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → 𝑗 ∈ ℝ)
303302, 300readdcld 9948 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → (𝑗 + 1) ∈ ℝ)
304201a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → 2 ∈ ℝ+)
305 elfzle1 12215 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → 1 ≤ 𝑗)
306300, 302, 300, 305leadd1dd 10520 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → (1 + 1) ≤ (𝑗 + 1))
307301, 303, 304, 306lediv1dd 11806 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → ((1 + 1) / 2) ≤ ((𝑗 + 1) / 2))
308299, 307syl5eqbr 4618 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → 1 ≤ ((𝑗 + 1) / 2))
309137, 308syl 17 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → 1 ≤ ((𝑗 + 1) / 2))
310309adantl 481 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → 1 ≤ ((𝑗 + 1) / 2))
311 elfzel2 12211 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → ((2 · 𝑘) − 1) ∈ ℤ)
312311zred 11358 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → ((2 · 𝑘) − 1) ∈ ℝ)
313312, 300readdcld 9948 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → (((2 · 𝑘) − 1) + 1) ∈ ℝ)
314 elfzle2 12216 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → 𝑗 ≤ ((2 · 𝑘) − 1))
315302, 312, 300, 314leadd1dd 10520 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → (𝑗 + 1) ≤ (((2 · 𝑘) − 1) + 1))
316303, 313, 304, 315lediv1dd 11806 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → ((𝑗 + 1) / 2) ≤ ((((2 · 𝑘) − 1) + 1) / 2))
317316adantl 481 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → ((𝑗 + 1) / 2) ≤ ((((2 · 𝑘) − 1) + 1) / 2))
31850adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → (2 · 𝑘) ∈ ℂ)
319 1cnd 9935 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → 1 ∈ ℂ)
320318, 319npcand 10275 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → (((2 · 𝑘) − 1) + 1) = (2 · 𝑘))
321320oveq1d 6564 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → ((((2 · 𝑘) − 1) + 1) / 2) = ((2 · 𝑘) / 2))
322189a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ℕ → 2 ≠ 0)
32344, 43, 322divcan3d 10685 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ ℕ → ((2 · 𝑘) / 2) = 𝑘)
324323adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → ((2 · 𝑘) / 2) = 𝑘)
325321, 324eqtrd 2644 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → ((((2 · 𝑘) − 1) + 1) / 2) = 𝑘)
326317, 325breqtrd 4609 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → ((𝑗 + 1) / 2) ≤ 𝑘)
327137, 326sylan2 490 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → ((𝑗 + 1) / 2) ≤ 𝑘)
328295, 310, 327jca32 556 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → ((1 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ ((𝑗 + 1) / 2) ∈ ℤ) ∧ (1 ≤ ((𝑗 + 1) / 2) ∧ ((𝑗 + 1) / 2) ≤ 𝑘)))
329 elfz2 12204 . . . . . . . . . . . . . 14 (((𝑗 + 1) / 2) ∈ (1...𝑘) ↔ ((1 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ ((𝑗 + 1) / 2) ∈ ℤ) ∧ (1 ≤ ((𝑗 + 1) / 2) ∧ ((𝑗 + 1) / 2) ≤ 𝑘)))
330328, 329sylibr 223 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → ((𝑗 + 1) / 2) ∈ (1...𝑘))
331276nncnd 10913 . . . . . . . . . . . . . . 15 (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → 𝑗 ∈ ℂ)
332 peano2cn 10087 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℂ → (𝑗 + 1) ∈ ℂ)
333 2cnd 10970 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℂ → 2 ∈ ℂ)
334189a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℂ → 2 ≠ 0)
335332, 333, 334divcan2d 10682 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℂ → (2 · ((𝑗 + 1) / 2)) = (𝑗 + 1))
336335oveq1d 6564 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℂ → ((2 · ((𝑗 + 1) / 2)) − 1) = ((𝑗 + 1) − 1))
337 pncan1 10333 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℂ → ((𝑗 + 1) − 1) = 𝑗)
338336, 337eqtr2d 2645 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℂ → 𝑗 = ((2 · ((𝑗 + 1) / 2)) − 1))
339331, 338syl 17 . . . . . . . . . . . . . 14 (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → 𝑗 = ((2 · ((𝑗 + 1) / 2)) − 1))
340339adantl 481 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → 𝑗 = ((2 · ((𝑗 + 1) / 2)) − 1))
341 oveq2 6557 . . . . . . . . . . . . . . . 16 (𝑚 = ((𝑗 + 1) / 2) → (2 · 𝑚) = (2 · ((𝑗 + 1) / 2)))
342341oveq1d 6564 . . . . . . . . . . . . . . 15 (𝑚 = ((𝑗 + 1) / 2) → ((2 · 𝑚) − 1) = ((2 · ((𝑗 + 1) / 2)) − 1))
343342eqeq2d 2620 . . . . . . . . . . . . . 14 (𝑚 = ((𝑗 + 1) / 2) → (𝑗 = ((2 · 𝑚) − 1) ↔ 𝑗 = ((2 · ((𝑗 + 1) / 2)) − 1)))
344343rspcev 3282 . . . . . . . . . . . . 13 ((((𝑗 + 1) / 2) ∈ (1...𝑘) ∧ 𝑗 = ((2 · ((𝑗 + 1) / 2)) − 1)) → ∃𝑚 ∈ (1...𝑘)𝑗 = ((2 · 𝑚) − 1))
345330, 340, 344syl2anc 691 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → ∃𝑚 ∈ (1...𝑘)𝑗 = ((2 · 𝑚) − 1))
346 eqidd 2611 . . . . . . . . . . . . . . . . 17 ((𝑚 ∈ (1...𝑘) ∧ 𝑗 = ((2 · 𝑚) − 1)) → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)) = (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)))
347 oveq2 6557 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑚 → (2 · 𝑖) = (2 · 𝑚))
348347oveq1d 6564 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑚 → ((2 · 𝑖) − 1) = ((2 · 𝑚) − 1))
349348adantl 481 . . . . . . . . . . . . . . . . 17 (((𝑚 ∈ (1...𝑘) ∧ 𝑗 = ((2 · 𝑚) − 1)) ∧ 𝑖 = 𝑚) → ((2 · 𝑖) − 1) = ((2 · 𝑚) − 1))
350 simpl 472 . . . . . . . . . . . . . . . . 17 ((𝑚 ∈ (1...𝑘) ∧ 𝑗 = ((2 · 𝑚) − 1)) → 𝑚 ∈ (1...𝑘))
351 ovex 6577 . . . . . . . . . . . . . . . . . 18 ((2 · 𝑚) − 1) ∈ V
352351a1i 11 . . . . . . . . . . . . . . . . 17 ((𝑚 ∈ (1...𝑘) ∧ 𝑗 = ((2 · 𝑚) − 1)) → ((2 · 𝑚) − 1) ∈ V)
353346, 349, 350, 352fvmptd 6197 . . . . . . . . . . . . . . . 16 ((𝑚 ∈ (1...𝑘) ∧ 𝑗 = ((2 · 𝑚) − 1)) → ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚) = ((2 · 𝑚) − 1))
354 id 22 . . . . . . . . . . . . . . . . . 18 (𝑗 = ((2 · 𝑚) − 1) → 𝑗 = ((2 · 𝑚) − 1))
355354eqcomd 2616 . . . . . . . . . . . . . . . . 17 (𝑗 = ((2 · 𝑚) − 1) → ((2 · 𝑚) − 1) = 𝑗)
356355adantl 481 . . . . . . . . . . . . . . . 16 ((𝑚 ∈ (1...𝑘) ∧ 𝑗 = ((2 · 𝑚) − 1)) → ((2 · 𝑚) − 1) = 𝑗)
357353, 356eqtr2d 2645 . . . . . . . . . . . . . . 15 ((𝑚 ∈ (1...𝑘) ∧ 𝑗 = ((2 · 𝑚) − 1)) → 𝑗 = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚))
358357ex 449 . . . . . . . . . . . . . 14 (𝑚 ∈ (1...𝑘) → (𝑗 = ((2 · 𝑚) − 1) → 𝑗 = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚)))
359358adantl 481 . . . . . . . . . . . . 13 (((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) ∧ 𝑚 ∈ (1...𝑘)) → (𝑗 = ((2 · 𝑚) − 1) → 𝑗 = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚)))
360359reximdva 3000 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (∃𝑚 ∈ (1...𝑘)𝑗 = ((2 · 𝑚) − 1) → ∃𝑚 ∈ (1...𝑘)𝑗 = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚)))
361345, 360mpd 15 . . . . . . . . . . 11 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → ∃𝑚 ∈ (1...𝑘)𝑗 = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚))
362361ralrimiva 2949 . . . . . . . . . 10 (𝑘 ∈ ℕ → ∀𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})∃𝑚 ∈ (1...𝑘)𝑗 = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚))
363 dffo3 6282 . . . . . . . . . 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))‘𝑚)))
364220, 362, 363sylanbrc 695 . . . . . . . . 9 (𝑘 ∈ ℕ → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)–onto→((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
365 df-f1o 5811 . . . . . . . . 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) ∈ ℕ})))
366267, 364, 365sylanbrc 695 . . . . . . . 8 (𝑘 ∈ ℕ → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)–1-1-onto→((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
367366adantl 481 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)–1-1-onto→((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
368 eqidd 2611 . . . . . . . . 9 (𝑗 ∈ (1...𝑘) → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)) = (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)))
369 oveq2 6557 . . . . . . . . . . 11 (𝑖 = 𝑗 → (2 · 𝑖) = (2 · 𝑗))
370369oveq1d 6564 . . . . . . . . . 10 (𝑖 = 𝑗 → ((2 · 𝑖) − 1) = ((2 · 𝑗) − 1))
371370adantl 481 . . . . . . . . 9 ((𝑗 ∈ (1...𝑘) ∧ 𝑖 = 𝑗) → ((2 · 𝑖) − 1) = ((2 · 𝑗) − 1))
372 id 22 . . . . . . . . 9 (𝑗 ∈ (1...𝑘) → 𝑗 ∈ (1...𝑘))
373 ovex 6577 . . . . . . . . . 10 ((2 · 𝑗) − 1) ∈ V
374373a1i 11 . . . . . . . . 9 (𝑗 ∈ (1...𝑘) → ((2 · 𝑗) − 1) ∈ V)
375368, 371, 372, 374fvmptd 6197 . . . . . . . 8 (𝑗 ∈ (1...𝑘) → ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑗) = ((2 · 𝑗) − 1))
376375adantl 481 . . . . . . 7 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑘)) → ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑗) = ((2 · 𝑗) − 1))
377 eleq1 2676 . . . . . . . . . 10 (𝑗 = 𝑖 → (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ↔ 𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})))
378377anbi2d 736 . . . . . . . . 9 (𝑗 = 𝑖 → (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) ↔ ((𝜑𝑘 ∈ ℕ) ∧ 𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))))
379142eleq1d 2672 . . . . . . . . 9 (𝑗 = 𝑖 → ((𝐹𝑗) ∈ ℂ ↔ (𝐹𝑖) ∈ ℂ))
380378, 379imbi12d 333 . . . . . . . 8 (𝑗 = 𝑖 → ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (𝐹𝑗) ∈ ℂ) ↔ (((𝜑𝑘 ∈ ℕ) ∧ 𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (𝐹𝑖) ∈ ℂ)))
381380, 139chvarv 2251 . . . . . . 7 (((𝜑𝑘 ∈ ℕ) ∧ 𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (𝐹𝑖) ∈ ℂ)
382146, 147, 367, 376, 381fsumf1o 14301 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → Σ𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑖) = Σ𝑗 ∈ (1...𝑘)(𝐹‘((2 · 𝑗) − 1)))
38397, 145, 3823eqtrrd 2649 . . . . 5 ((𝜑𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...𝑘)(𝐹‘((2 · 𝑗) − 1)) = Σ𝑗 ∈ (1...((2 · 𝑘) − 1))(𝐹𝑗))
384 ovex 6577 . . . . . . . . . 10 ((2 · 𝑘) − 1) ∈ V
38520fvmpt2 6200 . . . . . . . . . 10 ((𝑘 ∈ ℕ ∧ ((2 · 𝑘) − 1) ∈ V) → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) = ((2 · 𝑘) − 1))
386384, 385mpan2 703 . . . . . . . . 9 (𝑘 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) = ((2 · 𝑘) − 1))
387386oveq2d 6565 . . . . . . . 8 (𝑘 ∈ ℕ → (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘)) = (1...((2 · 𝑘) − 1)))
388387eqcomd 2616 . . . . . . 7 (𝑘 ∈ ℕ → (1...((2 · 𝑘) − 1)) = (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘)))
389388sumeq1d 14279 . . . . . 6 (𝑘 ∈ ℕ → Σ𝑗 ∈ (1...((2 · 𝑘) − 1))(𝐹𝑗) = Σ𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))(𝐹𝑗))
390389adantl 481 . . . . 5 ((𝜑𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...((2 · 𝑘) − 1))(𝐹𝑗) = Σ𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))(𝐹𝑗))
391383, 390eqtrd 2644 . . . 4 ((𝜑𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...𝑘)(𝐹‘((2 · 𝑗) − 1)) = Σ𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))(𝐹𝑗))
392 elfznn 12241 . . . . . . 7 (𝑗 ∈ (1...𝑘) → 𝑗 ∈ ℕ)
393392adantl 481 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑘)) → 𝑗 ∈ ℕ)
39412adantr 480 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑘)) → 𝐹:ℕ⟶ℂ)
39530a1i 11 . . . . . . . . . . . 12 (𝑗 ∈ (1...𝑘) → 2 ∈ ℤ)
396 elfzelz 12213 . . . . . . . . . . . 12 (𝑗 ∈ (1...𝑘) → 𝑗 ∈ ℤ)
397395, 396zmulcld 11364 . . . . . . . . . . 11 (𝑗 ∈ (1...𝑘) → (2 · 𝑗) ∈ ℤ)
398 1zzd 11285 . . . . . . . . . . 11 (𝑗 ∈ (1...𝑘) → 1 ∈ ℤ)
399397, 398zsubcld 11363 . . . . . . . . . 10 (𝑗 ∈ (1...𝑘) → ((2 · 𝑗) − 1) ∈ ℤ)
400 0red 9920 . . . . . . . . . . 11 (𝑗 ∈ (1...𝑘) → 0 ∈ ℝ)
40138a1i 11 . . . . . . . . . . . . 13 (𝑗 ∈ (1...𝑘) → 2 ∈ ℝ)
40224, 401syl5eqel 2692 . . . . . . . . . . . 12 (𝑗 ∈ (1...𝑘) → (2 · 1) ∈ ℝ)
403 1red 9934 . . . . . . . . . . . 12 (𝑗 ∈ (1...𝑘) → 1 ∈ ℝ)
404402, 403resubcld 10337 . . . . . . . . . . 11 (𝑗 ∈ (1...𝑘) → ((2 · 1) − 1) ∈ ℝ)
405399zred 11358 . . . . . . . . . . 11 (𝑗 ∈ (1...𝑘) → ((2 · 𝑗) − 1) ∈ ℝ)
406 0lt1 10429 . . . . . . . . . . . 12 0 < 1
407157a1i 11 . . . . . . . . . . . 12 (𝑗 ∈ (1...𝑘) → 1 = ((2 · 1) − 1))
408406, 407syl5breq 4620 . . . . . . . . . . 11 (𝑗 ∈ (1...𝑘) → 0 < ((2 · 1) − 1))
409397zred 11358 . . . . . . . . . . . 12 (𝑗 ∈ (1...𝑘) → (2 · 𝑗) ∈ ℝ)
410392nnred 10912 . . . . . . . . . . . . 13 (𝑗 ∈ (1...𝑘) → 𝑗 ∈ ℝ)
411165a1i 11 . . . . . . . . . . . . 13 (𝑗 ∈ (1...𝑘) → 0 ≤ 2)
412 elfzle1 12215 . . . . . . . . . . . . 13 (𝑗 ∈ (1...𝑘) → 1 ≤ 𝑗)
413403, 410, 401, 411, 412lemul2ad 10843 . . . . . . . . . . . 12 (𝑗 ∈ (1...𝑘) → (2 · 1) ≤ (2 · 𝑗))
414402, 409, 403, 413lesub1dd 10522 . . . . . . . . . . 11 (𝑗 ∈ (1...𝑘) → ((2 · 1) − 1) ≤ ((2 · 𝑗) − 1))
415400, 404, 405, 408, 414ltletrd 10076 . . . . . . . . . 10 (𝑗 ∈ (1...𝑘) → 0 < ((2 · 𝑗) − 1))
416 elnnz 11264 . . . . . . . . . 10 (((2 · 𝑗) − 1) ∈ ℕ ↔ (((2 · 𝑗) − 1) ∈ ℤ ∧ 0 < ((2 · 𝑗) − 1)))
417399, 415, 416sylanbrc 695 . . . . . . . . 9 (𝑗 ∈ (1...𝑘) → ((2 · 𝑗) − 1) ∈ ℕ)
418417adantl 481 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑘)) → ((2 · 𝑗) − 1) ∈ ℕ)
419394, 418ffvelrnd 6268 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑘)) → (𝐹‘((2 · 𝑗) − 1)) ∈ ℂ)
420419adantlr 747 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑘)) → (𝐹‘((2 · 𝑗) − 1)) ∈ ℂ)
42159fveq2d 6107 . . . . . . . 8 (𝑘 = 𝑗 → (𝐹‘((2 · 𝑘) − 1)) = (𝐹‘((2 · 𝑗) − 1)))
422421cbvmptv 4678 . . . . . . 7 (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))) = (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1)))
423422fvmpt2 6200 . . . . . 6 ((𝑗 ∈ ℕ ∧ (𝐹‘((2 · 𝑗) − 1)) ∈ ℂ) → ((𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))‘𝑗) = (𝐹‘((2 · 𝑗) − 1)))
424393, 420, 423syl2anc 691 . . . . 5 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑘)) → ((𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))‘𝑗) = (𝐹‘((2 · 𝑗) − 1)))
425 simpr 476 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
426425, 8syl6eleq 2698 . . . . 5 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ (ℤ‘1))
427424, 426, 420fsumser 14308 . . . 4 ((𝜑𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...𝑘)(𝐹‘((2 · 𝑗) − 1)) = (seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))))‘𝑘))
428 eqidd 2611 . . . . 5 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))) → (𝐹𝑗) = (𝐹𝑗))
429159a1i 11 . . . . . . . . . 10 (𝑘 ∈ ℕ → (2 · 1) ∈ ℝ)
430 1red 9934 . . . . . . . . . 10 (𝑘 ∈ ℕ → 1 ∈ ℝ)
431165a1i 11 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 0 ≤ 2)
432 nnge1 10923 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 1 ≤ 𝑘)
433430, 40, 39, 431, 432lemul2ad 10843 . . . . . . . . . 10 (𝑘 ∈ ℕ → (2 · 1) ≤ (2 · 𝑘))
434429, 41, 430, 433lesub1dd 10522 . . . . . . . . 9 (𝑘 ∈ ℕ → ((2 · 1) − 1) ≤ ((2 · 𝑘) − 1))
435157, 434syl5eqbr 4618 . . . . . . . 8 (𝑘 ∈ ℕ → 1 ≤ ((2 · 𝑘) − 1))
436 eluz2 11569 . . . . . . . 8 (((2 · 𝑘) − 1) ∈ (ℤ‘1) ↔ (1 ∈ ℤ ∧ ((2 · 𝑘) − 1) ∈ ℤ ∧ 1 ≤ ((2 · 𝑘) − 1)))
43736, 67, 435, 436syl3anbrc 1239 . . . . . . 7 (𝑘 ∈ ℕ → ((2 · 𝑘) − 1) ∈ (ℤ‘1))
43869, 437eqeltrd 2688 . . . . . 6 (𝑘 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) ∈ (ℤ‘1))
439438adantl 481 . . . . 5 ((𝜑𝑘 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) ∈ (ℤ‘1))
440 simpll 786 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))) → 𝜑)
441 simpr 476 . . . . . . . 8 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))) → 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘)))
442387adantr 480 . . . . . . . 8 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))) → (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘)) = (1...((2 · 𝑘) − 1)))
443441, 442eleqtrd 2690 . . . . . . 7 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))) → 𝑗 ∈ (1...((2 · 𝑘) − 1)))
444443adantll 746 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))) → 𝑗 ∈ (1...((2 · 𝑘) − 1)))
445440, 444, 95syl2anc 691 . . . . 5 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))) → (𝐹𝑗) ∈ ℂ)
446428, 439, 445fsumser 14308 . . . 4 ((𝜑𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))(𝐹𝑗) = (seq1( + , 𝐹)‘((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘)))
447391, 427, 4463eqtr3d 2652 . . 3 ((𝜑𝑘 ∈ ℕ) → (seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))))‘𝑘) = (seq1( + , 𝐹)‘((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘)))
4481, 2, 6, 7, 8, 9, 11, 15, 16, 29, 75, 77, 447climsuse 38675 . 2 (𝜑 → seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ 𝐵)
449 eqidd 2611 . . . 4 ((𝜑𝑘 ∈ ℕ) → (𝐹𝑘) = (𝐹𝑘))
4508, 9, 449, 13isum 14297 . . 3 (𝜑 → Σ𝑘 ∈ ℕ (𝐹𝑘) = ( ⇝ ‘seq1( + , 𝐹)))
451 climrel 14071 . . . . . . 7 Rel ⇝
452451releldmi 5283 . . . . . 6 (seq1( + , 𝐹) ⇝ 𝐵 → seq1( + , 𝐹) ∈ dom ⇝ )
45316, 452syl 17 . . . . 5 (𝜑 → seq1( + , 𝐹) ∈ dom ⇝ )
454 climdm 14133 . . . . 5 (seq1( + , 𝐹) ∈ dom ⇝ ↔ seq1( + , 𝐹) ⇝ ( ⇝ ‘seq1( + , 𝐹)))
455453, 454sylib 207 . . . 4 (𝜑 → seq1( + , 𝐹) ⇝ ( ⇝ ‘seq1( + , 𝐹)))
456 climuni 14131 . . . 4 ((seq1( + , 𝐹) ⇝ ( ⇝ ‘seq1( + , 𝐹)) ∧ seq1( + , 𝐹) ⇝ 𝐵) → ( ⇝ ‘seq1( + , 𝐹)) = 𝐵)
457455, 16, 456syl2anc 691 . . 3 (𝜑 → ( ⇝ ‘seq1( + , 𝐹)) = 𝐵)
458451a1i 11 . . . . . . . 8 (𝜑 → Rel ⇝ )
459 releldm 5279 . . . . . . . 8 ((Rel ⇝ ∧ seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ 𝐵) → seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ∈ dom ⇝ )
460458, 448, 459syl2anc 691 . . . . . . 7 (𝜑 → seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ∈ dom ⇝ )
461 climdm 14133 . . . . . . 7 (seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ∈ dom ⇝ ↔ seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ ( ⇝ ‘seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))))))
462460, 461sylib 207 . . . . . 6 (𝜑 → seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ ( ⇝ ‘seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))))))
463422a1i 11 . . . . . . . 8 (𝜑 → (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))) = (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1))))
464463seqeq3d 12671 . . . . . . 7 (𝜑 → seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) = seq1( + , (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1)))))
465464fveq2d 6107 . . . . . 6 (𝜑 → ( ⇝ ‘seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))))) = ( ⇝ ‘seq1( + , (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1))))))
466462, 465breqtrd 4609 . . . . 5 (𝜑 → seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ ( ⇝ ‘seq1( + , (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1))))))
467 climuni 14131 . . . . 5 ((seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ 𝐵 ∧ seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ ( ⇝ ‘seq1( + , (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1)))))) → 𝐵 = ( ⇝ ‘seq1( + , (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1))))))
468448, 466, 467syl2anc 691 . . . 4 (𝜑𝐵 = ( ⇝ ‘seq1( + , (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1))))))
469 eqidd 2611 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1))) = (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1))))
470 eqcom 2617 . . . . . . . 8 (𝑘 = 𝑗𝑗 = 𝑘)
471 eqcom 2617 . . . . . . . 8 ((𝐹‘((2 · 𝑘) − 1)) = (𝐹‘((2 · 𝑗) − 1)) ↔ (𝐹‘((2 · 𝑗) − 1)) = (𝐹‘((2 · 𝑘) − 1)))
472421, 470, 4713imtr3i 279 . . . . . . 7 (𝑗 = 𝑘 → (𝐹‘((2 · 𝑗) − 1)) = (𝐹‘((2 · 𝑘) − 1)))
473472adantl 481 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 = 𝑘) → (𝐹‘((2 · 𝑗) − 1)) = (𝐹‘((2 · 𝑘) − 1)))
47412adantr 480 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → 𝐹:ℕ⟶ℂ)
475437, 8syl6eleqr 2699 . . . . . . . 8 (𝑘 ∈ ℕ → ((2 · 𝑘) − 1) ∈ ℕ)
476475adantl 481 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → ((2 · 𝑘) − 1) ∈ ℕ)
477474, 476ffvelrnd 6268 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → (𝐹‘((2 · 𝑘) − 1)) ∈ ℂ)
478469, 473, 425, 477fvmptd 6197 . . . . 5 ((𝜑𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1)))‘𝑘) = (𝐹‘((2 · 𝑘) − 1)))
4798, 9, 478, 477isum 14297 . . . 4 (𝜑 → Σ𝑘 ∈ ℕ (𝐹‘((2 · 𝑘) − 1)) = ( ⇝ ‘seq1( + , (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1))))))
480468, 479eqtr4d 2647 . . 3 (𝜑𝐵 = Σ𝑘 ∈ ℕ (𝐹‘((2 · 𝑘) − 1)))
481450, 457, 4803eqtrd 2648 . 2 (𝜑 → Σ𝑘 ∈ ℕ (𝐹𝑘) = Σ𝑘 ∈ ℕ (𝐹‘((2 · 𝑘) − 1)))
482448, 481jca 553 1 (𝜑 → (seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ 𝐵 ∧ Σ𝑘 ∈ ℕ (𝐹𝑘) = Σ𝑘 ∈ ℕ (𝐹‘((2 · 𝑘) − 1))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 382   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  {crab 2900  Vcvv 3173   ∖ cdif 3537   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874   class class class wbr 4583   ↦ cmpt 4643  dom cdm 5038  Rel wrel 5043  ⟶wf 5800  –1-1→wf1 5801  –onto→wfo 5802  –1-1-onto→wf1o 5803  ‘cfv 5804  (class class class)co 6549  Fincfn 7841  ℂcc 9813  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818   · cmul 9820   < clt 9953   ≤ cle 9954   − cmin 10145   / cdiv 10563  ℕcn 10897  2c2 10947  ℤcz 11254  ℤ≥cuz 11563  ℝ+crp 11708  ...cfz 12197  seqcseq 12663   ⇝ cli 14063  Σcsu 14264 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-sup 8231  df-oi 8298  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-z 11255  df-uz 11564  df-rp 11709  df-fz 12198  df-fzo 12335  df-seq 12664  df-exp 12723  df-hash 12980  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-clim 14067  df-sum 14265 This theorem is referenced by:  fouriersw  39124
 Copyright terms: Public domain W3C validator