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

Theorem sumnnodd 40180
 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 1883 . . 3 𝑘𝜑
2 nfcv 2793 . . 3 𝑘seq1( + , 𝐹)
3 nfcv 2793 . . . 4 𝑘1
4 nfcv 2793 . . . 4 𝑘 +
5 nfmpt1 4780 . . . 4 𝑘(𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))
63, 4, 5nfseq 12851 . . 3 𝑘seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))))
7 nfmpt1 4780 . . 3 𝑘(𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))
8 nnuz 11761 . . 3 ℕ = (ℤ‘1)
9 1zzd 11446 . . 3 (𝜑 → 1 ∈ ℤ)
10 seqex 12843 . . . 4 seq1( + , 𝐹) ∈ V
1110a1i 11 . . 3 (𝜑 → seq1( + , 𝐹) ∈ V)
12 sumnnodd.1 . . . . . 6 (𝜑𝐹:ℕ⟶ℂ)
1312ffvelrnda 6399 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ℂ)
148, 9, 13serf 12869 . . . 4 (𝜑 → seq1( + , 𝐹):ℕ⟶ℂ)
1514ffvelrnda 6399 . . 3 ((𝜑𝑘 ∈ ℕ) → (seq1( + , 𝐹)‘𝑘) ∈ ℂ)
16 sumnnodd.sc . . 3 (𝜑 → seq1( + , 𝐹) ⇝ 𝐵)
17 1nn 11069 . . . . . . 7 1 ∈ ℕ
18 oveq2 6698 . . . . . . . . 9 (𝑘 = 1 → (2 · 𝑘) = (2 · 1))
1918oveq1d 6705 . . . . . . . 8 (𝑘 = 1 → ((2 · 𝑘) − 1) = ((2 · 1) − 1))
20 eqid 2651 . . . . . . . 8 (𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1)) = (𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))
21 ovex 6718 . . . . . . . 8 ((2 · 1) − 1) ∈ V
2219, 20, 21fvmpt 6321 . . . . . . 7 (1 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘1) = ((2 · 1) − 1))
2317, 22ax-mp 5 . . . . . 6 ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘1) = ((2 · 1) − 1)
24 2t1e2 11214 . . . . . . 7 (2 · 1) = 2
2524oveq1i 6700 . . . . . 6 ((2 · 1) − 1) = (2 − 1)
26 2m1e1 11173 . . . . . 6 (2 − 1) = 1
2723, 25, 263eqtri 2677 . . . . 5 ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘1) = 1
2827, 17eqeltri 2726 . . . 4 ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘1) ∈ ℕ
2928a1i 11 . . 3 (𝜑 → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘1) ∈ ℕ)
30 2z 11447 . . . . . . . 8 2 ∈ ℤ
3130a1i 11 . . . . . . 7 (𝑘 ∈ ℕ → 2 ∈ ℤ)
32 nnz 11437 . . . . . . 7 (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
3331, 32zmulcld 11526 . . . . . 6 (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℤ)
3432peano2zd 11523 . . . . . . . 8 (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℤ)
3531, 34zmulcld 11526 . . . . . . 7 (𝑘 ∈ ℕ → (2 · (𝑘 + 1)) ∈ ℤ)
36 1zzd 11446 . . . . . . 7 (𝑘 ∈ ℕ → 1 ∈ ℤ)
3735, 36zsubcld 11525 . . . . . 6 (𝑘 ∈ ℕ → ((2 · (𝑘 + 1)) − 1) ∈ ℤ)
38 2re 11128 . . . . . . . . . 10 2 ∈ ℝ
3938a1i 11 . . . . . . . . 9 (𝑘 ∈ ℕ → 2 ∈ ℝ)
40 nnre 11065 . . . . . . . . 9 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
4139, 40remulcld 10108 . . . . . . . 8 (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℝ)
4241lep1d 10993 . . . . . . 7 (𝑘 ∈ ℕ → (2 · 𝑘) ≤ ((2 · 𝑘) + 1))
43 2cnd 11131 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 2 ∈ ℂ)
44 nncn 11066 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
45 1cnd 10094 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 1 ∈ ℂ)
4643, 44, 45adddid 10102 . . . . . . . . . 10 (𝑘 ∈ ℕ → (2 · (𝑘 + 1)) = ((2 · 𝑘) + (2 · 1)))
4724oveq2i 6701 . . . . . . . . . 10 ((2 · 𝑘) + (2 · 1)) = ((2 · 𝑘) + 2)
4846, 47syl6eq 2701 . . . . . . . . 9 (𝑘 ∈ ℕ → (2 · (𝑘 + 1)) = ((2 · 𝑘) + 2))
4948oveq1d 6705 . . . . . . . 8 (𝑘 ∈ ℕ → ((2 · (𝑘 + 1)) − 1) = (((2 · 𝑘) + 2) − 1))
5043, 44mulcld 10098 . . . . . . . . 9 (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℂ)
5150, 43, 45addsubassd 10450 . . . . . . . 8 (𝑘 ∈ ℕ → (((2 · 𝑘) + 2) − 1) = ((2 · 𝑘) + (2 − 1)))
5226oveq2i 6701 . . . . . . . . 9 ((2 · 𝑘) + (2 − 1)) = ((2 · 𝑘) + 1)
5352a1i 11 . . . . . . . 8 (𝑘 ∈ ℕ → ((2 · 𝑘) + (2 − 1)) = ((2 · 𝑘) + 1))
5449, 51, 533eqtrrd 2690 . . . . . . 7 (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) = ((2 · (𝑘 + 1)) − 1))
5542, 54breqtrd 4711 . . . . . 6 (𝑘 ∈ ℕ → (2 · 𝑘) ≤ ((2 · (𝑘 + 1)) − 1))
56 eluz2 11731 . . . . . 6 (((2 · (𝑘 + 1)) − 1) ∈ (ℤ‘(2 · 𝑘)) ↔ ((2 · 𝑘) ∈ ℤ ∧ ((2 · (𝑘 + 1)) − 1) ∈ ℤ ∧ (2 · 𝑘) ≤ ((2 · (𝑘 + 1)) − 1)))
5733, 37, 55, 56syl3anbrc 1265 . . . . 5 (𝑘 ∈ ℕ → ((2 · (𝑘 + 1)) − 1) ∈ (ℤ‘(2 · 𝑘)))
58 oveq2 6698 . . . . . . . . 9 (𝑘 = 𝑗 → (2 · 𝑘) = (2 · 𝑗))
5958oveq1d 6705 . . . . . . . 8 (𝑘 = 𝑗 → ((2 · 𝑘) − 1) = ((2 · 𝑗) − 1))
6059cbvmptv 4783 . . . . . . 7 (𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1)) = (𝑗 ∈ ℕ ↦ ((2 · 𝑗) − 1))
6160a1i 11 . . . . . 6 (𝑘 ∈ ℕ → (𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1)) = (𝑗 ∈ ℕ ↦ ((2 · 𝑗) − 1)))
62 oveq2 6698 . . . . . . . 8 (𝑗 = (𝑘 + 1) → (2 · 𝑗) = (2 · (𝑘 + 1)))
6362oveq1d 6705 . . . . . . 7 (𝑗 = (𝑘 + 1) → ((2 · 𝑗) − 1) = ((2 · (𝑘 + 1)) − 1))
6463adantl 481 . . . . . 6 ((𝑘 ∈ ℕ ∧ 𝑗 = (𝑘 + 1)) → ((2 · 𝑗) − 1) = ((2 · (𝑘 + 1)) − 1))
65 peano2nn 11070 . . . . . 6 (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
6661, 64, 65, 37fvmptd 6327 . . . . 5 (𝑘 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘(𝑘 + 1)) = ((2 · (𝑘 + 1)) − 1))
6733, 36zsubcld 11525 . . . . . . . . 9 (𝑘 ∈ ℕ → ((2 · 𝑘) − 1) ∈ ℤ)
6820fvmpt2 6330 . . . . . . . . 9 ((𝑘 ∈ ℕ ∧ ((2 · 𝑘) − 1) ∈ ℤ) → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) = ((2 · 𝑘) − 1))
6967, 68mpdan 703 . . . . . . . 8 (𝑘 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) = ((2 · 𝑘) − 1))
7069oveq1d 6705 . . . . . . 7 (𝑘 ∈ ℕ → (((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) + 1) = (((2 · 𝑘) − 1) + 1))
7150, 45npcand 10434 . . . . . . 7 (𝑘 ∈ ℕ → (((2 · 𝑘) − 1) + 1) = (2 · 𝑘))
7270, 71eqtrd 2685 . . . . . 6 (𝑘 ∈ ℕ → (((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) + 1) = (2 · 𝑘))
7372fveq2d 6233 . . . . 5 (𝑘 ∈ ℕ → (ℤ‘(((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) + 1)) = (ℤ‘(2 · 𝑘)))
7457, 66, 733eltr4d 2745 . . . 4 (𝑘 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘(𝑘 + 1)) ∈ (ℤ‘(((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) + 1)))
7574adantl 481 . . 3 ((𝜑𝑘 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘(𝑘 + 1)) ∈ (ℤ‘(((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) + 1)))
76 seqex 12843 . . . 4 seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ∈ V
7776a1i 11 . . 3 (𝜑 → seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ∈ V)
78 incom 3838 . . . . . . . . . 10 (((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) = (((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
79 inss2 3867 . . . . . . . . . . 11 ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}
80 ssrin 3871 . . . . . . . . . . 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 3668 . . . . . . . . 9 (((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) ⊆ ({𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} ∩ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
83 disjdif 4073 . . . . . . . . 9 ({𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} ∩ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) = ∅
8482, 83sseqtri 3670 . . . . . . . 8 (((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) ⊆ ∅
85 ss0 4007 . . . . . . . 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 3790 . . . . . . . . 9 (((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∪ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) = (((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∪ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
88 inundif 4079 . . . . . . . . 9 (((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∪ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) = (1...((2 · 𝑘) − 1))
8987, 88eqtr2i 2674 . . . . . . . 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 12812 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (1...((2 · 𝑘) − 1)) ∈ Fin)
9212adantr 480 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...((2 · 𝑘) − 1))) → 𝐹:ℕ⟶ℂ)
93 elfznn 12408 . . . . . . . . . 10 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → 𝑗 ∈ ℕ)
9493adantl 481 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...((2 · 𝑘) − 1))) → 𝑗 ∈ ℕ)
9592, 94ffvelrnd 6400 . . . . . . . 8 ((𝜑𝑗 ∈ (1...((2 · 𝑘) − 1))) → (𝐹𝑗) ∈ ℂ)
9695adantlr 751 . . . . . . 7 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → (𝐹𝑗) ∈ ℂ)
9786, 90, 91, 96fsumsplit 14515 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...((2 · 𝑘) − 1))(𝐹𝑗) = (Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗) + Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗)))
98 simpl 472 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → 𝜑)
99 ssrab2 3720 . . . . . . . . . . . . . 14 {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} ⊆ ℕ
10079sseli 3632 . . . . . . . . . . . . . 14 (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → 𝑗 ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})
10199, 100sseldi 3634 . . . . . . . . . . . . 13 (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → 𝑗 ∈ ℕ)
102101adantl 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → 𝑗 ∈ ℕ)
103 oveq1 6697 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑗 → (𝑘 / 2) = (𝑗 / 2))
104103eleq1d 2715 . . . . . . . . . . . . . . 15 (𝑘 = 𝑗 → ((𝑘 / 2) ∈ ℕ ↔ (𝑗 / 2) ∈ ℕ))
105 oveq1 6697 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑘 → (𝑛 / 2) = (𝑘 / 2))
106105eleq1d 2715 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑘 → ((𝑛 / 2) ∈ ℕ ↔ (𝑘 / 2) ∈ ℕ))
107106elrab 3396 . . . . . . . . . . . . . . . 16 (𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} ↔ (𝑘 ∈ ℕ ∧ (𝑘 / 2) ∈ ℕ))
108107simprbi 479 . . . . . . . . . . . . . . 15 (𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} → (𝑘 / 2) ∈ ℕ)
109104, 108vtoclga 3303 . . . . . . . . . . . . . 14 (𝑗 ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} → (𝑗 / 2) ∈ ℕ)
110100, 109syl 17 . . . . . . . . . . . . 13 (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → (𝑗 / 2) ∈ ℕ)
111110adantl 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (𝑗 / 2) ∈ ℕ)
112 eleq1 2718 . . . . . . . . . . . . . . 15 (𝑘 = 𝑗 → (𝑘 ∈ ℕ ↔ 𝑗 ∈ ℕ))
113112, 1043anbi23d 1442 . . . . . . . . . . . . . 14 (𝑘 = 𝑗 → ((𝜑𝑘 ∈ ℕ ∧ (𝑘 / 2) ∈ ℕ) ↔ (𝜑𝑗 ∈ ℕ ∧ (𝑗 / 2) ∈ ℕ)))
114 fveq2 6229 . . . . . . . . . . . . . . 15 (𝑘 = 𝑗 → (𝐹𝑘) = (𝐹𝑗))
115114eqeq1d 2653 . . . . . . . . . . . . . 14 (𝑘 = 𝑗 → ((𝐹𝑘) = 0 ↔ (𝐹𝑗) = 0))
116113, 115imbi12d 333 . . . . . . . . . . . . 13 (𝑘 = 𝑗 → (((𝜑𝑘 ∈ ℕ ∧ (𝑘 / 2) ∈ ℕ) → (𝐹𝑘) = 0) ↔ ((𝜑𝑗 ∈ ℕ ∧ (𝑗 / 2) ∈ ℕ) → (𝐹𝑗) = 0)))
117 sumnnodd.even0 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ ∧ (𝑘 / 2) ∈ ℕ) → (𝐹𝑘) = 0)
118116, 117chvarv 2299 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ ∧ (𝑗 / 2) ∈ ℕ) → (𝐹𝑗) = 0)
11998, 102, 111, 118syl3anc 1366 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (𝐹𝑗) = 0)
120119sumeq2dv 14477 . . . . . . . . . 10 (𝜑 → Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗) = Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})0)
121 fzfid 12812 . . . . . . . . . . . . 13 (𝜑 → (1...((2 · 𝑘) − 1)) ∈ Fin)
122 inss1 3866 . . . . . . . . . . . . . 14 ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ (1...((2 · 𝑘) − 1))
123122a1i 11 . . . . . . . . . . . . 13 (𝜑 → ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ (1...((2 · 𝑘) − 1)))
124 ssfi 8221 . . . . . . . . . . . . 13 (((1...((2 · 𝑘) − 1)) ∈ Fin ∧ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ (1...((2 · 𝑘) − 1))) → ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∈ Fin)
125121, 123, 124syl2anc 694 . . . . . . . . . . . 12 (𝜑 → ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∈ Fin)
126125olcd 407 . . . . . . . . . . 11 (𝜑 → (((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ (ℤ𝐶) ∨ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∈ Fin))
127 sumz 14497 . . . . . . . . . . 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 2685 . . . . . . . . 9 (𝜑 → Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗) = 0)
130129adantr 480 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗) = 0)
131130oveq2d 6706 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗) + Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗)) = (Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗) + 0))
132 fzfi 12811 . . . . . . . . . . . 12 (1...((2 · 𝑘) − 1)) ∈ Fin
133 difss 3770 . . . . . . . . . . . 12 ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ (1...((2 · 𝑘) − 1))
134 ssfi 8221 . . . . . . . . . . . 12 (((1...((2 · 𝑘) − 1)) ∈ Fin ∧ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ (1...((2 · 𝑘) − 1))) → ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∈ Fin)
135132, 133, 134mp2an 708 . . . . . . . . . . 11 ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∈ Fin
136135a1i 11 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∈ Fin)
137133sseli 3632 . . . . . . . . . . . 12 (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → 𝑗 ∈ (1...((2 · 𝑘) − 1)))
138137, 95sylan2 490 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (𝐹𝑗) ∈ ℂ)
139138adantlr 751 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (𝐹𝑗) ∈ ℂ)
140136, 139fsumcl 14508 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗) ∈ ℂ)
141140addid1d 10274 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗) + 0) = Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗))
142 fveq2 6229 . . . . . . . . 9 (𝑗 = 𝑖 → (𝐹𝑗) = (𝐹𝑖))
143142cbvsumv 14470 . . . . . . . 8 Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗) = Σ𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑖)
144141, 143syl6eq 2701 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗) + 0) = Σ𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑖))
145131, 144eqtrd 2685 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → (Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗) + Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑗)) = Σ𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑖))
146 fveq2 6229 . . . . . . 7 (𝑖 = ((2 · 𝑗) − 1) → (𝐹𝑖) = (𝐹‘((2 · 𝑗) − 1)))
147 fzfid 12812 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (1...𝑘) ∈ Fin)
148 1zzd 11446 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 1 ∈ ℤ)
14967adantr 480 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → ((2 · 𝑘) − 1) ∈ ℤ)
15030a1i 11 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...𝑘) → 2 ∈ ℤ)
151 elfzelz 12380 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...𝑘) → 𝑖 ∈ ℤ)
152150, 151zmulcld 11526 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...𝑘) → (2 · 𝑖) ∈ ℤ)
153 1zzd 11446 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...𝑘) → 1 ∈ ℤ)
154152, 153zsubcld 11525 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1...𝑘) → ((2 · 𝑖) − 1) ∈ ℤ)
155154adantl 481 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → ((2 · 𝑖) − 1) ∈ ℤ)
156148, 149, 1553jca 1261 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → (1 ∈ ℤ ∧ ((2 · 𝑘) − 1) ∈ ℤ ∧ ((2 · 𝑖) − 1) ∈ ℤ))
15725, 26eqtr2i 2674 . . . . . . . . . . . . . . . 16 1 = ((2 · 1) − 1)
158 1re 10077 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℝ
15938, 158remulcli 10092 . . . . . . . . . . . . . . . . . 18 (2 · 1) ∈ ℝ
160159a1i 11 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...𝑘) → (2 · 1) ∈ ℝ)
161152zred 11520 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...𝑘) → (2 · 𝑖) ∈ ℝ)
162 1red 10093 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...𝑘) → 1 ∈ ℝ)
163151zred 11520 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑘) → 𝑖 ∈ ℝ)
16438a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑘) → 2 ∈ ℝ)
165 0le2 11149 . . . . . . . . . . . . . . . . . . 19 0 ≤ 2
166165a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑘) → 0 ≤ 2)
167 elfzle1 12382 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑘) → 1 ≤ 𝑖)
168162, 163, 164, 166, 167lemul2ad 11002 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...𝑘) → (2 · 1) ≤ (2 · 𝑖))
169160, 161, 162, 168lesub1dd 10681 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...𝑘) → ((2 · 1) − 1) ≤ ((2 · 𝑖) − 1))
170157, 169syl5eqbr 4720 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1...𝑘) → 1 ≤ ((2 · 𝑖) − 1))
171170adantl 481 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 1 ≤ ((2 · 𝑖) − 1))
172161adantl 481 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → (2 · 𝑖) ∈ ℝ)
17341adantr 480 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → (2 · 𝑘) ∈ ℝ)
174 1red 10093 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 1 ∈ ℝ)
175163adantl 481 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 𝑖 ∈ ℝ)
17640adantr 480 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 𝑘 ∈ ℝ)
17738a1i 11 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 2 ∈ ℝ)
178165a1i 11 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 0 ≤ 2)
179 elfzle2 12383 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...𝑘) → 𝑖𝑘)
180179adantl 481 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 𝑖𝑘)
181175, 176, 177, 178, 180lemul2ad 11002 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → (2 · 𝑖) ≤ (2 · 𝑘))
182172, 173, 174, 181lesub1dd 10681 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → ((2 · 𝑖) − 1) ≤ ((2 · 𝑘) − 1))
183171, 182jca 553 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → (1 ≤ ((2 · 𝑖) − 1) ∧ ((2 · 𝑖) − 1) ≤ ((2 · 𝑘) − 1)))
184 elfz2 12371 . . . . . . . . . . . . 13 (((2 · 𝑖) − 1) ∈ (1...((2 · 𝑘) − 1)) ↔ ((1 ∈ ℤ ∧ ((2 · 𝑘) − 1) ∈ ℤ ∧ ((2 · 𝑖) − 1) ∈ ℤ) ∧ (1 ≤ ((2 · 𝑖) − 1) ∧ ((2 · 𝑖) − 1) ≤ ((2 · 𝑘) − 1))))
185156, 183, 184sylanbrc 699 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → ((2 · 𝑖) − 1) ∈ (1...((2 · 𝑘) − 1)))
186152zcnd 11521 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑘) → (2 · 𝑖) ∈ ℂ)
187 1cnd 10094 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑘) → 1 ∈ ℂ)
188 2cnd 11131 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑘) → 2 ∈ ℂ)
189 2ne0 11151 . . . . . . . . . . . . . . . . . . 19 2 ≠ 0
190189a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑘) → 2 ≠ 0)
191186, 187, 188, 190divsubdird 10878 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...𝑘) → (((2 · 𝑖) − 1) / 2) = (((2 · 𝑖) / 2) − (1 / 2)))
192151zcnd 11521 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (1...𝑘) → 𝑖 ∈ ℂ)
193192, 188, 190divcan3d 10844 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑘) → ((2 · 𝑖) / 2) = 𝑖)
194193oveq1d 6705 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...𝑘) → (((2 · 𝑖) / 2) − (1 / 2)) = (𝑖 − (1 / 2)))
195191, 194eqtrd 2685 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...𝑘) → (((2 · 𝑖) − 1) / 2) = (𝑖 − (1 / 2)))
196151, 153zsubcld 11525 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑘) → (𝑖 − 1) ∈ ℤ)
197164, 190rereccld 10890 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (1...𝑘) → (1 / 2) ∈ ℝ)
198 halflt1 11288 . . . . . . . . . . . . . . . . . . . 20 (1 / 2) < 1
199198a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (1...𝑘) → (1 / 2) < 1)
200197, 162, 163, 199ltsub2dd 10678 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑘) → (𝑖 − 1) < (𝑖 − (1 / 2)))
201 2rp 11875 . . . . . . . . . . . . . . . . . . . . 21 2 ∈ ℝ+
202 rpreccl 11895 . . . . . . . . . . . . . . . . . . . . 21 (2 ∈ ℝ+ → (1 / 2) ∈ ℝ+)
203201, 202mp1i 13 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (1...𝑘) → (1 / 2) ∈ ℝ+)
204163, 203ltsubrpd 11942 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (1...𝑘) → (𝑖 − (1 / 2)) < 𝑖)
205192, 187npcand 10434 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (1...𝑘) → ((𝑖 − 1) + 1) = 𝑖)
206204, 205breqtrrd 4713 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑘) → (𝑖 − (1 / 2)) < ((𝑖 − 1) + 1))
207 btwnnz 11491 . . . . . . . . . . . . . . . . . 18 (((𝑖 − 1) ∈ ℤ ∧ (𝑖 − 1) < (𝑖 − (1 / 2)) ∧ (𝑖 − (1 / 2)) < ((𝑖 − 1) + 1)) → ¬ (𝑖 − (1 / 2)) ∈ ℤ)
208196, 200, 206, 207syl3anc 1366 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...𝑘) → ¬ (𝑖 − (1 / 2)) ∈ ℤ)
209 nnz 11437 . . . . . . . . . . . . . . . . 17 ((𝑖 − (1 / 2)) ∈ ℕ → (𝑖 − (1 / 2)) ∈ ℤ)
210208, 209nsyl 135 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...𝑘) → ¬ (𝑖 − (1 / 2)) ∈ ℕ)
211195, 210eqneltrd 2749 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1...𝑘) → ¬ (((2 · 𝑖) − 1) / 2) ∈ ℕ)
212211intnand 982 . . . . . . . . . . . . . 14 (𝑖 ∈ (1...𝑘) → ¬ (((2 · 𝑖) − 1) ∈ ℕ ∧ (((2 · 𝑖) − 1) / 2) ∈ ℕ))
213 oveq1 6697 . . . . . . . . . . . . . . . 16 (𝑛 = ((2 · 𝑖) − 1) → (𝑛 / 2) = (((2 · 𝑖) − 1) / 2))
214213eleq1d 2715 . . . . . . . . . . . . . . 15 (𝑛 = ((2 · 𝑖) − 1) → ((𝑛 / 2) ∈ ℕ ↔ (((2 · 𝑖) − 1) / 2) ∈ ℕ))
215214elrab 3396 . . . . . . . . . . . . . 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 3618 . . . . . . . . . . 11 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → ((2 · 𝑖) − 1) ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
219 eqid 2651 . . . . . . . . . . 11 (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)) = (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))
220218, 219fmptd 6425 . . . . . . . . . 10 (𝑘 ∈ ℕ → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)⟶((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
221 eqidd 2652 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (1...𝑘) → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)) = (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)))
222 oveq2 6698 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑥 → (2 · 𝑖) = (2 · 𝑥))
223222oveq1d 6705 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑥 → ((2 · 𝑖) − 1) = ((2 · 𝑥) − 1))
224223adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1...𝑘) ∧ 𝑖 = 𝑥) → ((2 · 𝑖) − 1) = ((2 · 𝑥) − 1))
225 id 22 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (1...𝑘) → 𝑥 ∈ (1...𝑘))
226 ovexd 6720 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (1...𝑘) → ((2 · 𝑥) − 1) ∈ V)
227221, 224, 225, 226fvmptd 6327 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (1...𝑘) → ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((2 · 𝑥) − 1))
228227eqcomd 2657 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1...𝑘) → ((2 · 𝑥) − 1) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥))
229228ad2antrr 762 . . . . . . . . . . . . . . 15 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦)) → ((2 · 𝑥) − 1) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥))
230 simpr 476 . . . . . . . . . . . . . . 15 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦)) → ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦))
231 eqidd 2652 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (1...𝑘) → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)) = (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)))
232 oveq2 6698 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑦 → (2 · 𝑖) = (2 · 𝑦))
233232oveq1d 6705 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑦 → ((2 · 𝑖) − 1) = ((2 · 𝑦) − 1))
234233adantl 481 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ (1...𝑘) ∧ 𝑖 = 𝑦) → ((2 · 𝑖) − 1) = ((2 · 𝑦) − 1))
235 id 22 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (1...𝑘) → 𝑦 ∈ (1...𝑘))
236 ovexd 6720 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (1...𝑘) → ((2 · 𝑦) − 1) ∈ V)
237231, 234, 235, 236fvmptd 6327 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (1...𝑘) → ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦) = ((2 · 𝑦) − 1))
238237ad2antlr 763 . . . . . . . . . . . . . . 15 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦)) → ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦) = ((2 · 𝑦) − 1))
239229, 230, 2383eqtrd 2689 . . . . . . . . . . . . . 14 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦)) → ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1))
240 2cnd 11131 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (1...𝑘) → 2 ∈ ℂ)
241 elfzelz 12380 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (1...𝑘) → 𝑥 ∈ ℤ)
242241zcnd 11521 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (1...𝑘) → 𝑥 ∈ ℂ)
243240, 242mulcld 10098 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (1...𝑘) → (2 · 𝑥) ∈ ℂ)
244243ad2antrr 762 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1)) → (2 · 𝑥) ∈ ℂ)
245 2cnd 11131 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (1...𝑘) → 2 ∈ ℂ)
246 elfzelz 12380 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (1...𝑘) → 𝑦 ∈ ℤ)
247246zcnd 11521 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (1...𝑘) → 𝑦 ∈ ℂ)
248245, 247mulcld 10098 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (1...𝑘) → (2 · 𝑦) ∈ ℂ)
249248ad2antlr 763 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1)) → (2 · 𝑦) ∈ ℂ)
250 1cnd 10094 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1)) → 1 ∈ ℂ)
251 simpr 476 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1)) → ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1))
252244, 249, 250, 251subcan2d 10472 . . . . . . . . . . . . . . 15 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1)) → (2 · 𝑥) = (2 · 𝑦))
253242ad2antrr 762 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ (2 · 𝑥) = (2 · 𝑦)) → 𝑥 ∈ ℂ)
254247ad2antlr 763 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ (2 · 𝑥) = (2 · 𝑦)) → 𝑦 ∈ ℂ)
255 2cnd 11131 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ (2 · 𝑥) = (2 · 𝑦)) → 2 ∈ ℂ)
256189a1i 11 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ (2 · 𝑥) = (2 · 𝑦)) → 2 ≠ 0)
257 simpr 476 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ (2 · 𝑥) = (2 · 𝑦)) → (2 · 𝑥) = (2 · 𝑦))
258253, 254, 255, 256, 257mulcanad 10700 . . . . . . . . . . . . . . 15 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ (2 · 𝑥) = (2 · 𝑦)) → 𝑥 = 𝑦)
259252, 258syldan 486 . . . . . . . . . . . . . 14 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1)) → 𝑥 = 𝑦)
260239, 259syldan 486 . . . . . . . . . . . . 13 (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦)) → 𝑥 = 𝑦)
261260adantll 750 . . . . . . . . . . . 12 (((𝑘 ∈ ℕ ∧ (𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘))) ∧ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦)) → 𝑥 = 𝑦)
262261ex 449 . . . . . . . . . . 11 ((𝑘 ∈ ℕ ∧ (𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘))) → (((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦) → 𝑥 = 𝑦))
263262ralrimivva 3000 . . . . . . . . . 10 (𝑘 ∈ ℕ → ∀𝑥 ∈ (1...𝑘)∀𝑦 ∈ (1...𝑘)(((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦) → 𝑥 = 𝑦))
264 dff13 6552 . . . . . . . . . 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))‘𝑦) → 𝑥 = 𝑦)))
265220, 263, 264sylanbrc 699 . . . . . . . . 9 (𝑘 ∈ ℕ → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)–1-1→((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
266 1zzd 11446 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → 1 ∈ ℤ)
26732adantr 480 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → 𝑘 ∈ ℤ)
268 fzssz 12381 . . . . . . . . . . . . . . . . . . . 20 (1...((2 · 𝑘) − 1)) ⊆ ℤ
269268, 137sseldi 3634 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → 𝑗 ∈ ℤ)
270 zeo 11501 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℤ → ((𝑗 / 2) ∈ ℤ ∨ ((𝑗 + 1) / 2) ∈ ℤ))
271269, 270syl 17 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → ((𝑗 / 2) ∈ ℤ ∨ ((𝑗 + 1) / 2) ∈ ℤ))
272271adantl 481 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → ((𝑗 / 2) ∈ ℤ ∨ ((𝑗 + 1) / 2) ∈ ℤ))
273 eldifn 3766 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → ¬ 𝑗 ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})
274137, 93syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → 𝑗 ∈ ℕ)
275274adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → 𝑗 ∈ ℕ)
276 simpr 476 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → (𝑗 / 2) ∈ ℤ)
277275nnred 11073 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → 𝑗 ∈ ℝ)
27838a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → 2 ∈ ℝ)
279275nngt0d 11102 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → 0 < 𝑗)
280 2pos 11150 . . . . . . . . . . . . . . . . . . . . . . 23 0 < 2
281280a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → 0 < 2)
282277, 278, 279, 281divgt0d 10997 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → 0 < (𝑗 / 2))
283 elnnz 11425 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗 / 2) ∈ ℕ ↔ ((𝑗 / 2) ∈ ℤ ∧ 0 < (𝑗 / 2)))
284276, 282, 283sylanbrc 699 . . . . . . . . . . . . . . . . . . . 20 ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → (𝑗 / 2) ∈ ℕ)
285 oveq1 6697 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑗 → (𝑛 / 2) = (𝑗 / 2))
286285eleq1d 2715 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑗 → ((𝑛 / 2) ∈ ℕ ↔ (𝑗 / 2) ∈ ℕ))
287286elrab 3396 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} ↔ (𝑗 ∈ ℕ ∧ (𝑗 / 2) ∈ ℕ))
288275, 284, 287sylanbrc 699 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑗 / 2) ∈ ℤ) → 𝑗 ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})
289273, 288mtand 692 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → ¬ (𝑗 / 2) ∈ ℤ)
290289adantl 481 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → ¬ (𝑗 / 2) ∈ ℤ)
291 pm2.53 387 . . . . . . . . . . . . . . . . 17 (((𝑗 / 2) ∈ ℤ ∨ ((𝑗 + 1) / 2) ∈ ℤ) → (¬ (𝑗 / 2) ∈ ℤ → ((𝑗 + 1) / 2) ∈ ℤ))
292272, 290, 291sylc 65 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → ((𝑗 + 1) / 2) ∈ ℤ)
293266, 267, 2923jca 1261 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (1 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ ((𝑗 + 1) / 2) ∈ ℤ))
294 1p1e2 11172 . . . . . . . . . . . . . . . . . . . 20 (1 + 1) = 2
295294oveq1i 6700 . . . . . . . . . . . . . . . . . . 19 ((1 + 1) / 2) = (2 / 2)
296 2div2e1 11188 . . . . . . . . . . . . . . . . . . 19 (2 / 2) = 1
297295, 296eqtr2i 2674 . . . . . . . . . . . . . . . . . 18 1 = ((1 + 1) / 2)
298 1red 10093 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → 1 ∈ ℝ)
299298, 298readdcld 10107 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → (1 + 1) ∈ ℝ)
30093nnred 11073 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → 𝑗 ∈ ℝ)
301300, 298readdcld 10107 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → (𝑗 + 1) ∈ ℝ)
302201a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → 2 ∈ ℝ+)
303 elfzle1 12382 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → 1 ≤ 𝑗)
304298, 300, 298, 303leadd1dd 10679 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → (1 + 1) ≤ (𝑗 + 1))
305299, 301, 302, 304lediv1dd 11968 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → ((1 + 1) / 2) ≤ ((𝑗 + 1) / 2))
306297, 305syl5eqbr 4720 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → 1 ≤ ((𝑗 + 1) / 2))
307137, 306syl 17 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → 1 ≤ ((𝑗 + 1) / 2))
308307adantl 481 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → 1 ≤ ((𝑗 + 1) / 2))
309 elfzel2 12378 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → ((2 · 𝑘) − 1) ∈ ℤ)
310309zred 11520 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → ((2 · 𝑘) − 1) ∈ ℝ)
311310, 298readdcld 10107 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → (((2 · 𝑘) − 1) + 1) ∈ ℝ)
312 elfzle2 12383 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → 𝑗 ≤ ((2 · 𝑘) − 1))
313300, 310, 298, 312leadd1dd 10679 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → (𝑗 + 1) ≤ (((2 · 𝑘) − 1) + 1))
314301, 311, 302, 313lediv1dd 11968 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (1...((2 · 𝑘) − 1)) → ((𝑗 + 1) / 2) ≤ ((((2 · 𝑘) − 1) + 1) / 2))
315314adantl 481 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → ((𝑗 + 1) / 2) ≤ ((((2 · 𝑘) − 1) + 1) / 2))
31650adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → (2 · 𝑘) ∈ ℂ)
317 1cnd 10094 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → 1 ∈ ℂ)
318316, 317npcand 10434 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → (((2 · 𝑘) − 1) + 1) = (2 · 𝑘))
319318oveq1d 6705 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → ((((2 · 𝑘) − 1) + 1) / 2) = ((2 · 𝑘) / 2))
320189a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ℕ → 2 ≠ 0)
32144, 43, 320divcan3d 10844 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ ℕ → ((2 · 𝑘) / 2) = 𝑘)
322321adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → ((2 · 𝑘) / 2) = 𝑘)
323319, 322eqtrd 2685 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → ((((2 · 𝑘) − 1) + 1) / 2) = 𝑘)
324315, 323breqtrd 4711 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → ((𝑗 + 1) / 2) ≤ 𝑘)
325137, 324sylan2 490 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → ((𝑗 + 1) / 2) ≤ 𝑘)
326293, 308, 325jca32 557 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → ((1 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ ((𝑗 + 1) / 2) ∈ ℤ) ∧ (1 ≤ ((𝑗 + 1) / 2) ∧ ((𝑗 + 1) / 2) ≤ 𝑘)))
327 elfz2 12371 . . . . . . . . . . . . . 14 (((𝑗 + 1) / 2) ∈ (1...𝑘) ↔ ((1 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ ((𝑗 + 1) / 2) ∈ ℤ) ∧ (1 ≤ ((𝑗 + 1) / 2) ∧ ((𝑗 + 1) / 2) ≤ 𝑘)))
328326, 327sylibr 224 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → ((𝑗 + 1) / 2) ∈ (1...𝑘))
329274nncnd 11074 . . . . . . . . . . . . . . 15 (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → 𝑗 ∈ ℂ)
330 peano2cn 10246 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℂ → (𝑗 + 1) ∈ ℂ)
331 2cnd 11131 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℂ → 2 ∈ ℂ)
332189a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℂ → 2 ≠ 0)
333330, 331, 332divcan2d 10841 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℂ → (2 · ((𝑗 + 1) / 2)) = (𝑗 + 1))
334333oveq1d 6705 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℂ → ((2 · ((𝑗 + 1) / 2)) − 1) = ((𝑗 + 1) − 1))
335 pncan1 10492 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℂ → ((𝑗 + 1) − 1) = 𝑗)
336334, 335eqtr2d 2686 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℂ → 𝑗 = ((2 · ((𝑗 + 1) / 2)) − 1))
337329, 336syl 17 . . . . . . . . . . . . . 14 (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → 𝑗 = ((2 · ((𝑗 + 1) / 2)) − 1))
338337adantl 481 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → 𝑗 = ((2 · ((𝑗 + 1) / 2)) − 1))
339 oveq2 6698 . . . . . . . . . . . . . . . 16 (𝑚 = ((𝑗 + 1) / 2) → (2 · 𝑚) = (2 · ((𝑗 + 1) / 2)))
340339oveq1d 6705 . . . . . . . . . . . . . . 15 (𝑚 = ((𝑗 + 1) / 2) → ((2 · 𝑚) − 1) = ((2 · ((𝑗 + 1) / 2)) − 1))
341340eqeq2d 2661 . . . . . . . . . . . . . 14 (𝑚 = ((𝑗 + 1) / 2) → (𝑗 = ((2 · 𝑚) − 1) ↔ 𝑗 = ((2 · ((𝑗 + 1) / 2)) − 1)))
342341rspcev 3340 . . . . . . . . . . . . 13 ((((𝑗 + 1) / 2) ∈ (1...𝑘) ∧ 𝑗 = ((2 · ((𝑗 + 1) / 2)) − 1)) → ∃𝑚 ∈ (1...𝑘)𝑗 = ((2 · 𝑚) − 1))
343328, 338, 342syl2anc 694 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → ∃𝑚 ∈ (1...𝑘)𝑗 = ((2 · 𝑚) − 1))
344 eqidd 2652 . . . . . . . . . . . . . . . . 17 ((𝑚 ∈ (1...𝑘) ∧ 𝑗 = ((2 · 𝑚) − 1)) → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)) = (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)))
345 oveq2 6698 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑚 → (2 · 𝑖) = (2 · 𝑚))
346345oveq1d 6705 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑚 → ((2 · 𝑖) − 1) = ((2 · 𝑚) − 1))
347346adantl 481 . . . . . . . . . . . . . . . . 17 (((𝑚 ∈ (1...𝑘) ∧ 𝑗 = ((2 · 𝑚) − 1)) ∧ 𝑖 = 𝑚) → ((2 · 𝑖) − 1) = ((2 · 𝑚) − 1))
348 simpl 472 . . . . . . . . . . . . . . . . 17 ((𝑚 ∈ (1...𝑘) ∧ 𝑗 = ((2 · 𝑚) − 1)) → 𝑚 ∈ (1...𝑘))
349 ovexd 6720 . . . . . . . . . . . . . . . . 17 ((𝑚 ∈ (1...𝑘) ∧ 𝑗 = ((2 · 𝑚) − 1)) → ((2 · 𝑚) − 1) ∈ V)
350344, 347, 348, 349fvmptd 6327 . . . . . . . . . . . . . . . 16 ((𝑚 ∈ (1...𝑘) ∧ 𝑗 = ((2 · 𝑚) − 1)) → ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚) = ((2 · 𝑚) − 1))
351 id 22 . . . . . . . . . . . . . . . . . 18 (𝑗 = ((2 · 𝑚) − 1) → 𝑗 = ((2 · 𝑚) − 1))
352351eqcomd 2657 . . . . . . . . . . . . . . . . 17 (𝑗 = ((2 · 𝑚) − 1) → ((2 · 𝑚) − 1) = 𝑗)
353352adantl 481 . . . . . . . . . . . . . . . 16 ((𝑚 ∈ (1...𝑘) ∧ 𝑗 = ((2 · 𝑚) − 1)) → ((2 · 𝑚) − 1) = 𝑗)
354350, 353eqtr2d 2686 . . . . . . . . . . . . . . 15 ((𝑚 ∈ (1...𝑘) ∧ 𝑗 = ((2 · 𝑚) − 1)) → 𝑗 = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚))
355354ex 449 . . . . . . . . . . . . . 14 (𝑚 ∈ (1...𝑘) → (𝑗 = ((2 · 𝑚) − 1) → 𝑗 = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚)))
356355adantl 481 . . . . . . . . . . . . 13 (((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) ∧ 𝑚 ∈ (1...𝑘)) → (𝑗 = ((2 · 𝑚) − 1) → 𝑗 = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚)))
357356reximdva 3046 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (∃𝑚 ∈ (1...𝑘)𝑗 = ((2 · 𝑚) − 1) → ∃𝑚 ∈ (1...𝑘)𝑗 = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚)))
358343, 357mpd 15 . . . . . . . . . . 11 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → ∃𝑚 ∈ (1...𝑘)𝑗 = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚))
359358ralrimiva 2995 . . . . . . . . . 10 (𝑘 ∈ ℕ → ∀𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})∃𝑚 ∈ (1...𝑘)𝑗 = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚))
360 dffo3 6414 . . . . . . . . . 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))‘𝑚)))
361220, 359, 360sylanbrc 699 . . . . . . . . 9 (𝑘 ∈ ℕ → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)–onto→((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
362 df-f1o 5933 . . . . . . . . 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) ∈ ℕ})))
363265, 361, 362sylanbrc 699 . . . . . . . 8 (𝑘 ∈ ℕ → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)–1-1-onto→((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
364363adantl 481 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)–1-1-onto→((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))
365 eqidd 2652 . . . . . . . . 9 (𝑗 ∈ (1...𝑘) → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)) = (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)))
366 oveq2 6698 . . . . . . . . . . 11 (𝑖 = 𝑗 → (2 · 𝑖) = (2 · 𝑗))
367366oveq1d 6705 . . . . . . . . . 10 (𝑖 = 𝑗 → ((2 · 𝑖) − 1) = ((2 · 𝑗) − 1))
368367adantl 481 . . . . . . . . 9 ((𝑗 ∈ (1...𝑘) ∧ 𝑖 = 𝑗) → ((2 · 𝑖) − 1) = ((2 · 𝑗) − 1))
369 id 22 . . . . . . . . 9 (𝑗 ∈ (1...𝑘) → 𝑗 ∈ (1...𝑘))
370 ovexd 6720 . . . . . . . . 9 (𝑗 ∈ (1...𝑘) → ((2 · 𝑗) − 1) ∈ V)
371365, 368, 369, 370fvmptd 6327 . . . . . . . 8 (𝑗 ∈ (1...𝑘) → ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑗) = ((2 · 𝑗) − 1))
372371adantl 481 . . . . . . 7 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑘)) → ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑗) = ((2 · 𝑗) − 1))
373 eleq1 2718 . . . . . . . . . 10 (𝑗 = 𝑖 → (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ↔ 𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})))
374373anbi2d 740 . . . . . . . . 9 (𝑗 = 𝑖 → (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) ↔ ((𝜑𝑘 ∈ ℕ) ∧ 𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))))
375142eleq1d 2715 . . . . . . . . 9 (𝑗 = 𝑖 → ((𝐹𝑗) ∈ ℂ ↔ (𝐹𝑖) ∈ ℂ))
376374, 375imbi12d 333 . . . . . . . 8 (𝑗 = 𝑖 → ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (𝐹𝑗) ∈ ℂ) ↔ (((𝜑𝑘 ∈ ℕ) ∧ 𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (𝐹𝑖) ∈ ℂ)))
377376, 139chvarv 2299 . . . . . . 7 (((𝜑𝑘 ∈ ℕ) ∧ 𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (𝐹𝑖) ∈ ℂ)
378146, 147, 364, 372, 377fsumf1o 14498 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → Σ𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹𝑖) = Σ𝑗 ∈ (1...𝑘)(𝐹‘((2 · 𝑗) − 1)))
37997, 145, 3783eqtrrd 2690 . . . . 5 ((𝜑𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...𝑘)(𝐹‘((2 · 𝑗) − 1)) = Σ𝑗 ∈ (1...((2 · 𝑘) − 1))(𝐹𝑗))
380 ovex 6718 . . . . . . . . . 10 ((2 · 𝑘) − 1) ∈ V
38120fvmpt2 6330 . . . . . . . . . 10 ((𝑘 ∈ ℕ ∧ ((2 · 𝑘) − 1) ∈ V) → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) = ((2 · 𝑘) − 1))
382380, 381mpan2 707 . . . . . . . . 9 (𝑘 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) = ((2 · 𝑘) − 1))
383382oveq2d 6706 . . . . . . . 8 (𝑘 ∈ ℕ → (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘)) = (1...((2 · 𝑘) − 1)))
384383eqcomd 2657 . . . . . . 7 (𝑘 ∈ ℕ → (1...((2 · 𝑘) − 1)) = (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘)))
385384sumeq1d 14475 . . . . . 6 (𝑘 ∈ ℕ → Σ𝑗 ∈ (1...((2 · 𝑘) − 1))(𝐹𝑗) = Σ𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))(𝐹𝑗))
386385adantl 481 . . . . 5 ((𝜑𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...((2 · 𝑘) − 1))(𝐹𝑗) = Σ𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))(𝐹𝑗))
387379, 386eqtrd 2685 . . . 4 ((𝜑𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...𝑘)(𝐹‘((2 · 𝑗) − 1)) = Σ𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))(𝐹𝑗))
388 elfznn 12408 . . . . . . 7 (𝑗 ∈ (1...𝑘) → 𝑗 ∈ ℕ)
389388adantl 481 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑘)) → 𝑗 ∈ ℕ)
39012adantr 480 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑘)) → 𝐹:ℕ⟶ℂ)
39130a1i 11 . . . . . . . . . . . 12 (𝑗 ∈ (1...𝑘) → 2 ∈ ℤ)
392 elfzelz 12380 . . . . . . . . . . . 12 (𝑗 ∈ (1...𝑘) → 𝑗 ∈ ℤ)
393391, 392zmulcld 11526 . . . . . . . . . . 11 (𝑗 ∈ (1...𝑘) → (2 · 𝑗) ∈ ℤ)
394 1zzd 11446 . . . . . . . . . . 11 (𝑗 ∈ (1...𝑘) → 1 ∈ ℤ)
395393, 394zsubcld 11525 . . . . . . . . . 10 (𝑗 ∈ (1...𝑘) → ((2 · 𝑗) − 1) ∈ ℤ)
396 0red 10079 . . . . . . . . . . 11 (𝑗 ∈ (1...𝑘) → 0 ∈ ℝ)
39738a1i 11 . . . . . . . . . . . . 13 (𝑗 ∈ (1...𝑘) → 2 ∈ ℝ)
39824, 397syl5eqel 2734 . . . . . . . . . . . 12 (𝑗 ∈ (1...𝑘) → (2 · 1) ∈ ℝ)
399 1red 10093 . . . . . . . . . . . 12 (𝑗 ∈ (1...𝑘) → 1 ∈ ℝ)
400398, 399resubcld 10496 . . . . . . . . . . 11 (𝑗 ∈ (1...𝑘) → ((2 · 1) − 1) ∈ ℝ)
401395zred 11520 . . . . . . . . . . 11 (𝑗 ∈ (1...𝑘) → ((2 · 𝑗) − 1) ∈ ℝ)
402 0lt1 10588 . . . . . . . . . . . 12 0 < 1
403157a1i 11 . . . . . . . . . . . 12 (𝑗 ∈ (1...𝑘) → 1 = ((2 · 1) − 1))
404402, 403syl5breq 4722 . . . . . . . . . . 11 (𝑗 ∈ (1...𝑘) → 0 < ((2 · 1) − 1))
405393zred 11520 . . . . . . . . . . . 12 (𝑗 ∈ (1...𝑘) → (2 · 𝑗) ∈ ℝ)
406388nnred 11073 . . . . . . . . . . . . 13 (𝑗 ∈ (1...𝑘) → 𝑗 ∈ ℝ)
407165a1i 11 . . . . . . . . . . . . 13 (𝑗 ∈ (1...𝑘) → 0 ≤ 2)
408 elfzle1 12382 . . . . . . . . . . . . 13 (𝑗 ∈ (1...𝑘) → 1 ≤ 𝑗)
409399, 406, 397, 407, 408lemul2ad 11002 . . . . . . . . . . . 12 (𝑗 ∈ (1...𝑘) → (2 · 1) ≤ (2 · 𝑗))
410398, 405, 399, 409lesub1dd 10681 . . . . . . . . . . 11 (𝑗 ∈ (1...𝑘) → ((2 · 1) − 1) ≤ ((2 · 𝑗) − 1))
411396, 400, 401, 404, 410ltletrd 10235 . . . . . . . . . 10 (𝑗 ∈ (1...𝑘) → 0 < ((2 · 𝑗) − 1))
412 elnnz 11425 . . . . . . . . . 10 (((2 · 𝑗) − 1) ∈ ℕ ↔ (((2 · 𝑗) − 1) ∈ ℤ ∧ 0 < ((2 · 𝑗) − 1)))
413395, 411, 412sylanbrc 699 . . . . . . . . 9 (𝑗 ∈ (1...𝑘) → ((2 · 𝑗) − 1) ∈ ℕ)
414413adantl 481 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑘)) → ((2 · 𝑗) − 1) ∈ ℕ)
415390, 414ffvelrnd 6400 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑘)) → (𝐹‘((2 · 𝑗) − 1)) ∈ ℂ)
416415adantlr 751 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑘)) → (𝐹‘((2 · 𝑗) − 1)) ∈ ℂ)
41759fveq2d 6233 . . . . . . . 8 (𝑘 = 𝑗 → (𝐹‘((2 · 𝑘) − 1)) = (𝐹‘((2 · 𝑗) − 1)))
418417cbvmptv 4783 . . . . . . 7 (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))) = (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1)))
419418fvmpt2 6330 . . . . . 6 ((𝑗 ∈ ℕ ∧ (𝐹‘((2 · 𝑗) − 1)) ∈ ℂ) → ((𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))‘𝑗) = (𝐹‘((2 · 𝑗) − 1)))
420389, 416, 419syl2anc 694 . . . . 5 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑘)) → ((𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))‘𝑗) = (𝐹‘((2 · 𝑗) − 1)))
421 simpr 476 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
422421, 8syl6eleq 2740 . . . . 5 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ (ℤ‘1))
423420, 422, 416fsumser 14505 . . . 4 ((𝜑𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...𝑘)(𝐹‘((2 · 𝑗) − 1)) = (seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))))‘𝑘))
424 eqidd 2652 . . . . 5 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))) → (𝐹𝑗) = (𝐹𝑗))
425159a1i 11 . . . . . . . . . 10 (𝑘 ∈ ℕ → (2 · 1) ∈ ℝ)
426 1red 10093 . . . . . . . . . 10 (𝑘 ∈ ℕ → 1 ∈ ℝ)
427165a1i 11 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 0 ≤ 2)
428 nnge1 11084 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 1 ≤ 𝑘)
429426, 40, 39, 427, 428lemul2ad 11002 . . . . . . . . . 10 (𝑘 ∈ ℕ → (2 · 1) ≤ (2 · 𝑘))
430425, 41, 426, 429lesub1dd 10681 . . . . . . . . 9 (𝑘 ∈ ℕ → ((2 · 1) − 1) ≤ ((2 · 𝑘) − 1))
431157, 430syl5eqbr 4720 . . . . . . . 8 (𝑘 ∈ ℕ → 1 ≤ ((2 · 𝑘) − 1))
432 eluz2 11731 . . . . . . . 8 (((2 · 𝑘) − 1) ∈ (ℤ‘1) ↔ (1 ∈ ℤ ∧ ((2 · 𝑘) − 1) ∈ ℤ ∧ 1 ≤ ((2 · 𝑘) − 1)))
43336, 67, 431, 432syl3anbrc 1265 . . . . . . 7 (𝑘 ∈ ℕ → ((2 · 𝑘) − 1) ∈ (ℤ‘1))
43469, 433eqeltrd 2730 . . . . . 6 (𝑘 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) ∈ (ℤ‘1))
435434adantl 481 . . . . 5 ((𝜑𝑘 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) ∈ (ℤ‘1))
436 simpll 805 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))) → 𝜑)
437 simpr 476 . . . . . . . 8 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))) → 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘)))
438383adantr 480 . . . . . . . 8 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))) → (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘)) = (1...((2 · 𝑘) − 1)))
439437, 438eleqtrd 2732 . . . . . . 7 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))) → 𝑗 ∈ (1...((2 · 𝑘) − 1)))
440439adantll 750 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))) → 𝑗 ∈ (1...((2 · 𝑘) − 1)))
441436, 440, 95syl2anc 694 . . . . 5 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))) → (𝐹𝑗) ∈ ℂ)
442424, 435, 441fsumser 14505 . . . 4 ((𝜑𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))(𝐹𝑗) = (seq1( + , 𝐹)‘((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘)))
443387, 423, 4423eqtr3d 2693 . . 3 ((𝜑𝑘 ∈ ℕ) → (seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))))‘𝑘) = (seq1( + , 𝐹)‘((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘)))
4441, 2, 6, 7, 8, 9, 11, 15, 16, 29, 75, 77, 443climsuse 40158 . 2 (𝜑 → seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ 𝐵)
445 eqidd 2652 . . . 4 ((𝜑𝑘 ∈ ℕ) → (𝐹𝑘) = (𝐹𝑘))
4468, 9, 445, 13isum 14494 . . 3 (𝜑 → Σ𝑘 ∈ ℕ (𝐹𝑘) = ( ⇝ ‘seq1( + , 𝐹)))
447 climrel 14267 . . . . . . 7 Rel ⇝
448447releldmi 5394 . . . . . 6 (seq1( + , 𝐹) ⇝ 𝐵 → seq1( + , 𝐹) ∈ dom ⇝ )
44916, 448syl 17 . . . . 5 (𝜑 → seq1( + , 𝐹) ∈ dom ⇝ )
450 climdm 14329 . . . . 5 (seq1( + , 𝐹) ∈ dom ⇝ ↔ seq1( + , 𝐹) ⇝ ( ⇝ ‘seq1( + , 𝐹)))
451449, 450sylib 208 . . . 4 (𝜑 → seq1( + , 𝐹) ⇝ ( ⇝ ‘seq1( + , 𝐹)))
452 climuni 14327 . . . 4 ((seq1( + , 𝐹) ⇝ ( ⇝ ‘seq1( + , 𝐹)) ∧ seq1( + , 𝐹) ⇝ 𝐵) → ( ⇝ ‘seq1( + , 𝐹)) = 𝐵)
453451, 16, 452syl2anc 694 . . 3 (𝜑 → ( ⇝ ‘seq1( + , 𝐹)) = 𝐵)
454447a1i 11 . . . . . . . 8 (𝜑 → Rel ⇝ )
455 releldm 5390 . . . . . . . 8 ((Rel ⇝ ∧ seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ 𝐵) → seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ∈ dom ⇝ )
456454, 444, 455syl2anc 694 . . . . . . 7 (𝜑 → seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ∈ dom ⇝ )
457 climdm 14329 . . . . . . 7 (seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ∈ dom ⇝ ↔ seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ ( ⇝ ‘seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))))))
458456, 457sylib 208 . . . . . 6 (𝜑 → seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ ( ⇝ ‘seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))))))
459418a1i 11 . . . . . . . 8 (𝜑 → (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))) = (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1))))
460459seqeq3d 12849 . . . . . . 7 (𝜑 → seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) = seq1( + , (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1)))))
461460fveq2d 6233 . . . . . 6 (𝜑 → ( ⇝ ‘seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))))) = ( ⇝ ‘seq1( + , (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1))))))
462458, 461breqtrd 4711 . . . . 5 (𝜑 → seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ ( ⇝ ‘seq1( + , (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1))))))
463 climuni 14327 . . . . 5 ((seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ 𝐵 ∧ seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ ( ⇝ ‘seq1( + , (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1)))))) → 𝐵 = ( ⇝ ‘seq1( + , (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1))))))
464444, 462, 463syl2anc 694 . . . 4 (𝜑𝐵 = ( ⇝ ‘seq1( + , (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1))))))
465 eqidd 2652 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1))) = (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1))))
466 eqcom 2658 . . . . . . . 8 (𝑘 = 𝑗𝑗 = 𝑘)
467 eqcom 2658 . . . . . . . 8 ((𝐹‘((2 · 𝑘) − 1)) = (𝐹‘((2 · 𝑗) − 1)) ↔ (𝐹‘((2 · 𝑗) − 1)) = (𝐹‘((2 · 𝑘) − 1)))
468417, 466, 4673imtr3i 280 . . . . . . 7 (𝑗 = 𝑘 → (𝐹‘((2 · 𝑗) − 1)) = (𝐹‘((2 · 𝑘) − 1)))
469468adantl 481 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 = 𝑘) → (𝐹‘((2 · 𝑗) − 1)) = (𝐹‘((2 · 𝑘) − 1)))
47012adantr 480 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → 𝐹:ℕ⟶ℂ)
471433, 8syl6eleqr 2741 . . . . . . . 8 (𝑘 ∈ ℕ → ((2 · 𝑘) − 1) ∈ ℕ)
472471adantl 481 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → ((2 · 𝑘) − 1) ∈ ℕ)
473470, 472ffvelrnd 6400 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → (𝐹‘((2 · 𝑘) − 1)) ∈ ℂ)
474465, 469, 421, 473fvmptd 6327 . . . . 5 ((𝜑𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1)))‘𝑘) = (𝐹‘((2 · 𝑘) − 1)))
4758, 9, 474, 473isum 14494 . . . 4 (𝜑 → Σ𝑘 ∈ ℕ (𝐹‘((2 · 𝑘) − 1)) = ( ⇝ ‘seq1( + , (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1))))))
476464, 475eqtr4d 2688 . . 3 (𝜑𝐵 = Σ𝑘 ∈ ℕ (𝐹‘((2 · 𝑘) − 1)))
477446, 453, 4763eqtrd 2689 . 2 (𝜑 → Σ𝑘 ∈ ℕ (𝐹𝑘) = Σ𝑘 ∈ ℕ (𝐹‘((2 · 𝑘) − 1)))
478444, 477jca 553 1 (𝜑 → (seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ 𝐵 ∧ Σ𝑘 ∈ ℕ (𝐹𝑘) = Σ𝑘 ∈ ℕ (𝐹‘((2 · 𝑘) − 1))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 382   ∧ wa 383   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030   ≠ wne 2823  ∀wral 2941  ∃wrex 2942  {crab 2945  Vcvv 3231   ∖ cdif 3604   ∪ cun 3605   ∩ cin 3606   ⊆ wss 3607  ∅c0 3948   class class class wbr 4685   ↦ cmpt 4762  dom cdm 5143  Rel wrel 5148  ⟶wf 5922  –1-1→wf1 5923  –onto→wfo 5924  –1-1-onto→wf1o 5925  ‘cfv 5926  (class class class)co 6690  Fincfn 7997  ℂcc 9972  ℝcr 9973  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979   < clt 10112   ≤ cle 10113   − cmin 10304   / cdiv 10722  ℕcn 11058  2c2 11108  ℤcz 11415  ℤ≥cuz 11725  ℝ+crp 11870  ...cfz 12364  seqcseq 12841   ⇝ cli 14259  Σcsu 14460 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-oi 8456  df-card 8803  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-z 11416  df-uz 11726  df-rp 11871  df-fz 12365  df-fzo 12505  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-clim 14263  df-sum 14461 This theorem is referenced by:  fouriersw  40766
 Copyright terms: Public domain W3C validator