Metamath Proof Explorer

Theorem sumnnodd

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

Ref Expression
Hypotheses sumnnodd.1 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ℂ )
sumnnodd.even0 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ ( 𝑘 / 2 ) ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) = 0 )
sumnnodd.sc ⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) ⇝ 𝐵 )
Assertion sumnnodd ( 𝜑 → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ) ⇝ 𝐵 ∧ Σ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) = Σ 𝑘 ∈ ℕ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 sumnnodd.1 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ℂ )
2 sumnnodd.even0 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ ( 𝑘 / 2 ) ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) = 0 )
3 sumnnodd.sc ⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) ⇝ 𝐵 )
4 nfv ⊢ Ⅎ 𝑘 𝜑
5 nfcv ⊢ Ⅎ 𝑘 seq 1 ( + , 𝐹 )
6 nfcv ⊢ Ⅎ 𝑘 1
7 nfcv ⊢ Ⅎ 𝑘 +
8 nfmpt1 ⊢ Ⅎ 𝑘 ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) )
9 6 7 8 nfseq ⊢ Ⅎ 𝑘 seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) )
10 nfmpt1 ⊢ Ⅎ 𝑘 ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) )
11 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
12 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
13 seqex ⊢ seq 1 ( + , 𝐹 ) ∈ V
14 13 a1i ⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) ∈ V )
15 1 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
16 11 12 15 serf ⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) : ℕ ⟶ ℂ )
17 16 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ∈ ℂ )
18 1nn ⊢ 1 ∈ ℕ
19 oveq2 ⊢ ( 𝑘 = 1 → ( 2 · 𝑘 ) = ( 2 · 1 ) )
20 19 oveq1d ⊢ ( 𝑘 = 1 → ( ( 2 · 𝑘 ) − 1 ) = ( ( 2 · 1 ) − 1 ) )
21 eqid ⊢ ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) = ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) )
22 ovex ⊢ ( ( 2 · 1 ) − 1 ) ∈ V
23 20 21 22 fvmpt ⊢ ( 1 ∈ ℕ → ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 1 ) = ( ( 2 · 1 ) − 1 ) )
24 18 23 ax-mp ⊢ ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 1 ) = ( ( 2 · 1 ) − 1 )
25 2t1e2 ⊢ ( 2 · 1 ) = 2
26 25 oveq1i ⊢ ( ( 2 · 1 ) − 1 ) = ( 2 − 1 )
27 2m1e1 ⊢ ( 2 − 1 ) = 1
28 24 26 27 3eqtri ⊢ ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 1 ) = 1
29 28 18 eqeltri ⊢ ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 1 ) ∈ ℕ
30 29 a1i ⊢ ( 𝜑 → ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 1 ) ∈ ℕ )
31 2z ⊢ 2 ∈ ℤ
32 31 a1i ⊢ ( 𝑘 ∈ ℕ → 2 ∈ ℤ )
33 nnz ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℤ )
34 32 33 zmulcld ⊢ ( 𝑘 ∈ ℕ → ( 2 · 𝑘 ) ∈ ℤ )
35 33 peano2zd ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 + 1 ) ∈ ℤ )
36 32 35 zmulcld ⊢ ( 𝑘 ∈ ℕ → ( 2 · ( 𝑘 + 1 ) ) ∈ ℤ )
37 1zzd ⊢ ( 𝑘 ∈ ℕ → 1 ∈ ℤ )
38 36 37 zsubcld ⊢ ( 𝑘 ∈ ℕ → ( ( 2 · ( 𝑘 + 1 ) ) − 1 ) ∈ ℤ )
39 2re ⊢ 2 ∈ ℝ
40 39 a1i ⊢ ( 𝑘 ∈ ℕ → 2 ∈ ℝ )
41 nnre ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ )
42 40 41 remulcld ⊢ ( 𝑘 ∈ ℕ → ( 2 · 𝑘 ) ∈ ℝ )
43 42 lep1d ⊢ ( 𝑘 ∈ ℕ → ( 2 · 𝑘 ) ≤ ( ( 2 · 𝑘 ) + 1 ) )
44 2cnd ⊢ ( 𝑘 ∈ ℕ → 2 ∈ ℂ )
45 nncn ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℂ )
46 1cnd ⊢ ( 𝑘 ∈ ℕ → 1 ∈ ℂ )
47 44 45 46 adddid ⊢ ( 𝑘 ∈ ℕ → ( 2 · ( 𝑘 + 1 ) ) = ( ( 2 · 𝑘 ) + ( 2 · 1 ) ) )
48 25 oveq2i ⊢ ( ( 2 · 𝑘 ) + ( 2 · 1 ) ) = ( ( 2 · 𝑘 ) + 2 )
49 47 48 eqtrdi ⊢ ( 𝑘 ∈ ℕ → ( 2 · ( 𝑘 + 1 ) ) = ( ( 2 · 𝑘 ) + 2 ) )
50 49 oveq1d ⊢ ( 𝑘 ∈ ℕ → ( ( 2 · ( 𝑘 + 1 ) ) − 1 ) = ( ( ( 2 · 𝑘 ) + 2 ) − 1 ) )
51 44 45 mulcld ⊢ ( 𝑘 ∈ ℕ → ( 2 · 𝑘 ) ∈ ℂ )
52 51 44 46 addsubassd ⊢ ( 𝑘 ∈ ℕ → ( ( ( 2 · 𝑘 ) + 2 ) − 1 ) = ( ( 2 · 𝑘 ) + ( 2 − 1 ) ) )
53 27 oveq2i ⊢ ( ( 2 · 𝑘 ) + ( 2 − 1 ) ) = ( ( 2 · 𝑘 ) + 1 )
54 53 a1i ⊢ ( 𝑘 ∈ ℕ → ( ( 2 · 𝑘 ) + ( 2 − 1 ) ) = ( ( 2 · 𝑘 ) + 1 ) )
55 50 52 54 3eqtrrd ⊢ ( 𝑘 ∈ ℕ → ( ( 2 · 𝑘 ) + 1 ) = ( ( 2 · ( 𝑘 + 1 ) ) − 1 ) )
56 43 55 breqtrd ⊢ ( 𝑘 ∈ ℕ → ( 2 · 𝑘 ) ≤ ( ( 2 · ( 𝑘 + 1 ) ) − 1 ) )
57 eluz2 ⊢ ( ( ( 2 · ( 𝑘 + 1 ) ) − 1 ) ∈ ( ℤ≥ ‘ ( 2 · 𝑘 ) ) ↔ ( ( 2 · 𝑘 ) ∈ ℤ ∧ ( ( 2 · ( 𝑘 + 1 ) ) − 1 ) ∈ ℤ ∧ ( 2 · 𝑘 ) ≤ ( ( 2 · ( 𝑘 + 1 ) ) − 1 ) ) )
58 34 38 56 57 syl3anbrc ⊢ ( 𝑘 ∈ ℕ → ( ( 2 · ( 𝑘 + 1 ) ) − 1 ) ∈ ( ℤ≥ ‘ ( 2 · 𝑘 ) ) )
59 oveq2 ⊢ ( 𝑘 = 𝑗 → ( 2 · 𝑘 ) = ( 2 · 𝑗 ) )
60 59 oveq1d ⊢ ( 𝑘 = 𝑗 → ( ( 2 · 𝑘 ) − 1 ) = ( ( 2 · 𝑗 ) − 1 ) )
61 60 cbvmptv ⊢ ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) = ( 𝑗 ∈ ℕ ↦ ( ( 2 · 𝑗 ) − 1 ) )
62 oveq2 ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 2 · 𝑗 ) = ( 2 · ( 𝑘 + 1 ) ) )
63 62 oveq1d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 2 · 𝑗 ) − 1 ) = ( ( 2 · ( 𝑘 + 1 ) ) − 1 ) )
64 peano2nn ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 + 1 ) ∈ ℕ )
65 61 63 64 38 fvmptd3 ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ ( 𝑘 + 1 ) ) = ( ( 2 · ( 𝑘 + 1 ) ) − 1 ) )
66 34 37 zsubcld ⊢ ( 𝑘 ∈ ℕ → ( ( 2 · 𝑘 ) − 1 ) ∈ ℤ )
67 21 fvmpt2 ⊢ ( ( 𝑘 ∈ ℕ ∧ ( ( 2 · 𝑘 ) − 1 ) ∈ ℤ ) → ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) = ( ( 2 · 𝑘 ) − 1 ) )
68 66 67 mpdan ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) = ( ( 2 · 𝑘 ) − 1 ) )
69 68 oveq1d ⊢ ( 𝑘 ∈ ℕ → ( ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) + 1 ) = ( ( ( 2 · 𝑘 ) − 1 ) + 1 ) )
70 51 46 npcand ⊢ ( 𝑘 ∈ ℕ → ( ( ( 2 · 𝑘 ) − 1 ) + 1 ) = ( 2 · 𝑘 ) )
71 69 70 eqtrd ⊢ ( 𝑘 ∈ ℕ → ( ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) + 1 ) = ( 2 · 𝑘 ) )
72 71 fveq2d ⊢ ( 𝑘 ∈ ℕ → ( ℤ≥ ‘ ( ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) + 1 ) ) = ( ℤ≥ ‘ ( 2 · 𝑘 ) ) )
73 58 65 72 3eltr4d ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ ( 𝑘 + 1 ) ) ∈ ( ℤ≥ ‘ ( ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) + 1 ) ) )
74 73 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ ( 𝑘 + 1 ) ) ∈ ( ℤ≥ ‘ ( ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) + 1 ) ) )
75 seqex ⊢ seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ) ∈ V
76 75 a1i ⊢ ( 𝜑 → seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ) ∈ V )
77 incom ⊢ ( ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∩ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∩ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) = ( ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∩ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∩ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) )
78 inss2 ⊢ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∩ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ⊆ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ }
79 ssrin ⊢ ( ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∩ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ⊆ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } → ( ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∩ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∩ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) ⊆ ( { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ∩ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) )
80 78 79 ax-mp ⊢ ( ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∩ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∩ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) ⊆ ( { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ∩ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) )
81 77 80 eqsstri ⊢ ( ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∩ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∩ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) ⊆ ( { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ∩ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) )
82 disjdif ⊢ ( { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ∩ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) = ∅
83 81 82 sseqtri ⊢ ( ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∩ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∩ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) ⊆ ∅
84 ss0 ⊢ ( ( ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∩ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∩ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) ⊆ ∅ → ( ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∩ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∩ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) = ∅ )
85 83 84 mp1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∩ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∩ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) = ∅ )
86 uncom ⊢ ( ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∪ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∩ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) = ( ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∩ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∪ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) )
87 inundif ⊢ ( ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∩ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∪ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) = ( 1 ... ( ( 2 · 𝑘 ) − 1 ) )
88 86 87 eqtr2i ⊢ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) = ( ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∪ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∩ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) )
89 88 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) = ( ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∪ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∩ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) )
90 fzfid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∈ Fin )
91 1 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ) → 𝐹 : ℕ ⟶ ℂ )
92 elfznn ⊢ ( 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) → 𝑗 ∈ ℕ )
93 92 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ) → 𝑗 ∈ ℕ )
94 91 93 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℂ )
95 94 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℂ )
96 85 89 90 95 fsumsplit ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → Σ 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) = ( Σ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ( 𝐹 ‘ 𝑗 ) + Σ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∩ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ( 𝐹 ‘ 𝑗 ) ) )
97 simpl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∩ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) → 𝜑 )
98 ssrab2 ⊢ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ⊆ ℕ
99 78 sseli ⊢ ( 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∩ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) → 𝑗 ∈ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } )
100 98 99 sselid ⊢ ( 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∩ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) → 𝑗 ∈ ℕ )
101 100 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∩ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) → 𝑗 ∈ ℕ )
102 oveq1 ⊢ ( 𝑘 = 𝑗 → ( 𝑘 / 2 ) = ( 𝑗 / 2 ) )
103 102 eleq1d ⊢ ( 𝑘 = 𝑗 → ( ( 𝑘 / 2 ) ∈ ℕ ↔ ( 𝑗 / 2 ) ∈ ℕ ) )
104 oveq1 ⊢ ( 𝑛 = 𝑘 → ( 𝑛 / 2 ) = ( 𝑘 / 2 ) )
105 104 eleq1d ⊢ ( 𝑛 = 𝑘 → ( ( 𝑛 / 2 ) ∈ ℕ ↔ ( 𝑘 / 2 ) ∈ ℕ ) )
106 105 elrab ⊢ ( 𝑘 ∈ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ↔ ( 𝑘 ∈ ℕ ∧ ( 𝑘 / 2 ) ∈ ℕ ) )
107 106 simprbi ⊢ ( 𝑘 ∈ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } → ( 𝑘 / 2 ) ∈ ℕ )
108 103 107 vtoclga ⊢ ( 𝑗 ∈ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } → ( 𝑗 / 2 ) ∈ ℕ )
109 99 108 syl ⊢ ( 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∩ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) → ( 𝑗 / 2 ) ∈ ℕ )
110 109 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∩ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) → ( 𝑗 / 2 ) ∈ ℕ )
111 eleq1w ⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ ℕ ↔ 𝑗 ∈ ℕ ) )
112 111 103 3anbi23d ⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ ( 𝑘 / 2 ) ∈ ℕ ) ↔ ( 𝜑 ∧ 𝑗 ∈ ℕ ∧ ( 𝑗 / 2 ) ∈ ℕ ) ) )
113 fveqeq2 ⊢ ( 𝑘 = 𝑗 → ( ( 𝐹 ‘ 𝑘 ) = 0 ↔ ( 𝐹 ‘ 𝑗 ) = 0 ) )
114 112 113 imbi12d ⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ ( 𝑘 / 2 ) ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) = 0 ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ∧ ( 𝑗 / 2 ) ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) = 0 ) ) )
115 114 2 chvarvv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ∧ ( 𝑗 / 2 ) ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) = 0 )
116 97 101 110 115 syl3anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∩ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) → ( 𝐹 ‘ 𝑗 ) = 0 )
117 116 sumeq2dv ⊢ ( 𝜑 → Σ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∩ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ( 𝐹 ‘ 𝑗 ) = Σ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∩ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) 0 )
118 fzfid ⊢ ( 𝜑 → ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∈ Fin )
119 inss1 ⊢ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∩ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ⊆ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) )
120 119 a1i ⊢ ( 𝜑 → ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∩ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ⊆ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) )
121 ssfi ⊢ ( ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∈ Fin ∧ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∩ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ⊆ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ) → ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∩ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∈ Fin )
122 118 120 121 syl2anc ⊢ ( 𝜑 → ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∩ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∈ Fin )
123 122 olcd ⊢ ( 𝜑 → ( ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∩ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ⊆ ( ℤ≥ ‘ 𝐶 ) ∨ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∩ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∈ Fin ) )
124 sumz ⊢ ( ( ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∩ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ⊆ ( ℤ≥ ‘ 𝐶 ) ∨ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∩ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∈ Fin ) → Σ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∩ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) 0 = 0 )
125 123 124 syl ⊢ ( 𝜑 → Σ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∩ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) 0 = 0 )
126 117 125 eqtrd ⊢ ( 𝜑 → Σ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∩ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ( 𝐹 ‘ 𝑗 ) = 0 )
127 126 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → Σ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∩ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ( 𝐹 ‘ 𝑗 ) = 0 )
128 127 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( Σ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ( 𝐹 ‘ 𝑗 ) + Σ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∩ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ( 𝐹 ‘ 𝑗 ) ) = ( Σ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ( 𝐹 ‘ 𝑗 ) + 0 ) )
129 fzfi ⊢ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∈ Fin
130 difss ⊢ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ⊆ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) )
131 ssfi ⊢ ( ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∈ Fin ∧ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ⊆ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ) → ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∈ Fin )
132 129 130 131 mp2an ⊢ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∈ Fin
133 132 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∈ Fin )
134 130 sseli ⊢ ( 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) → 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) )
135 134 94 sylan2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℂ )
136 135 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℂ )
137 133 136 fsumcl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → Σ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ( 𝐹 ‘ 𝑗 ) ∈ ℂ )
138 137 addid1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( Σ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ( 𝐹 ‘ 𝑗 ) + 0 ) = Σ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ( 𝐹 ‘ 𝑗 ) )
139 fveq2 ⊢ ( 𝑗 = 𝑖 → ( 𝐹 ‘ 𝑗 ) = ( 𝐹 ‘ 𝑖 ) )
140 139 cbvsumv ⊢ Σ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ( 𝐹 ‘ 𝑗 ) = Σ 𝑖 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ( 𝐹 ‘ 𝑖 )
141 138 140 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( Σ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ( 𝐹 ‘ 𝑗 ) + 0 ) = Σ 𝑖 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ( 𝐹 ‘ 𝑖 ) )
142 128 141 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( Σ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ( 𝐹 ‘ 𝑗 ) + Σ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∩ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ( 𝐹 ‘ 𝑗 ) ) = Σ 𝑖 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ( 𝐹 ‘ 𝑖 ) )
143 fveq2 ⊢ ( 𝑖 = ( ( 2 · 𝑗 ) − 1 ) → ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) )
144 fzfid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 1 ... 𝑘 ) ∈ Fin )
145 1zzd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑘 ) ) → 1 ∈ ℤ )
146 66 adantr ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑘 ) ) → ( ( 2 · 𝑘 ) − 1 ) ∈ ℤ )
147 31 a1i ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → 2 ∈ ℤ )
148 elfzelz ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → 𝑖 ∈ ℤ )
149 147 148 zmulcld ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ( 2 · 𝑖 ) ∈ ℤ )
150 1zzd ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → 1 ∈ ℤ )
151 149 150 zsubcld ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ( ( 2 · 𝑖 ) − 1 ) ∈ ℤ )
152 151 adantl ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑘 ) ) → ( ( 2 · 𝑖 ) − 1 ) ∈ ℤ )
153 26 27 eqtr2i ⊢ 1 = ( ( 2 · 1 ) − 1 )
154 1re ⊢ 1 ∈ ℝ
155 39 154 remulcli ⊢ ( 2 · 1 ) ∈ ℝ
156 155 a1i ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ( 2 · 1 ) ∈ ℝ )
157 149 zred ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ( 2 · 𝑖 ) ∈ ℝ )
158 1red ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → 1 ∈ ℝ )
159 148 zred ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → 𝑖 ∈ ℝ )
160 39 a1i ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → 2 ∈ ℝ )
161 0le2 ⊢ 0 ≤ 2
162 161 a1i ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → 0 ≤ 2 )
163 elfzle1 ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → 1 ≤ 𝑖 )
164 158 159 160 162 163 lemul2ad ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ( 2 · 1 ) ≤ ( 2 · 𝑖 ) )
165 156 157 158 164 lesub1dd ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ( ( 2 · 1 ) − 1 ) ≤ ( ( 2 · 𝑖 ) − 1 ) )
166 153 165 eqbrtrid ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → 1 ≤ ( ( 2 · 𝑖 ) − 1 ) )
167 166 adantl ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑘 ) ) → 1 ≤ ( ( 2 · 𝑖 ) − 1 ) )
168 157 adantl ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑘 ) ) → ( 2 · 𝑖 ) ∈ ℝ )
169 42 adantr ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑘 ) ) → ( 2 · 𝑘 ) ∈ ℝ )
170 1red ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑘 ) ) → 1 ∈ ℝ )
171 159 adantl ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑘 ) ) → 𝑖 ∈ ℝ )
172 41 adantr ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑘 ) ) → 𝑘 ∈ ℝ )
173 39 a1i ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑘 ) ) → 2 ∈ ℝ )
174 161 a1i ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑘 ) ) → 0 ≤ 2 )
175 elfzle2 ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → 𝑖 ≤ 𝑘 )
176 175 adantl ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑘 ) ) → 𝑖 ≤ 𝑘 )
177 171 172 173 174 176 lemul2ad ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑘 ) ) → ( 2 · 𝑖 ) ≤ ( 2 · 𝑘 ) )
178 168 169 170 177 lesub1dd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑘 ) ) → ( ( 2 · 𝑖 ) − 1 ) ≤ ( ( 2 · 𝑘 ) − 1 ) )
179 145 146 152 167 178 elfzd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑘 ) ) → ( ( 2 · 𝑖 ) − 1 ) ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) )
180 149 zcnd ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ( 2 · 𝑖 ) ∈ ℂ )
181 1cnd ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → 1 ∈ ℂ )
182 2cnd ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → 2 ∈ ℂ )
183 2ne0 ⊢ 2 ≠ 0
184 183 a1i ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → 2 ≠ 0 )
185 180 181 182 184 divsubdird ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ( ( ( 2 · 𝑖 ) − 1 ) / 2 ) = ( ( ( 2 · 𝑖 ) / 2 ) − ( 1 / 2 ) ) )
186 148 zcnd ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → 𝑖 ∈ ℂ )
187 186 182 184 divcan3d ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ( ( 2 · 𝑖 ) / 2 ) = 𝑖 )
188 187 oveq1d ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ( ( ( 2 · 𝑖 ) / 2 ) − ( 1 / 2 ) ) = ( 𝑖 − ( 1 / 2 ) ) )
189 185 188 eqtrd ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ( ( ( 2 · 𝑖 ) − 1 ) / 2 ) = ( 𝑖 − ( 1 / 2 ) ) )
190 148 150 zsubcld ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ( 𝑖 − 1 ) ∈ ℤ )
191 160 184 rereccld ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ( 1 / 2 ) ∈ ℝ )
192 halflt1 ⊢ ( 1 / 2 ) < 1
193 192 a1i ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ( 1 / 2 ) < 1 )
194 191 158 159 193 ltsub2dd ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ( 𝑖 − 1 ) < ( 𝑖 − ( 1 / 2 ) ) )
195 2rp ⊢ 2 ∈ ℝ+
196 rpreccl ⊢ ( 2 ∈ ℝ+ → ( 1 / 2 ) ∈ ℝ+ )
197 195 196 mp1i ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ( 1 / 2 ) ∈ ℝ+ )
198 159 197 ltsubrpd ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ( 𝑖 − ( 1 / 2 ) ) < 𝑖 )
199 186 181 npcand ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ( ( 𝑖 − 1 ) + 1 ) = 𝑖 )
200 198 199 breqtrrd ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ( 𝑖 − ( 1 / 2 ) ) < ( ( 𝑖 − 1 ) + 1 ) )
201 btwnnz ⊢ ( ( ( 𝑖 − 1 ) ∈ ℤ ∧ ( 𝑖 − 1 ) < ( 𝑖 − ( 1 / 2 ) ) ∧ ( 𝑖 − ( 1 / 2 ) ) < ( ( 𝑖 − 1 ) + 1 ) ) → ¬ ( 𝑖 − ( 1 / 2 ) ) ∈ ℤ )
202 190 194 200 201 syl3anc ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ¬ ( 𝑖 − ( 1 / 2 ) ) ∈ ℤ )
203 nnz ⊢ ( ( 𝑖 − ( 1 / 2 ) ) ∈ ℕ → ( 𝑖 − ( 1 / 2 ) ) ∈ ℤ )
204 202 203 nsyl ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ¬ ( 𝑖 − ( 1 / 2 ) ) ∈ ℕ )
205 189 204 eqneltrd ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ¬ ( ( ( 2 · 𝑖 ) − 1 ) / 2 ) ∈ ℕ )
206 205 intnand ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ¬ ( ( ( 2 · 𝑖 ) − 1 ) ∈ ℕ ∧ ( ( ( 2 · 𝑖 ) − 1 ) / 2 ) ∈ ℕ ) )
207 oveq1 ⊢ ( 𝑛 = ( ( 2 · 𝑖 ) − 1 ) → ( 𝑛 / 2 ) = ( ( ( 2 · 𝑖 ) − 1 ) / 2 ) )
208 207 eleq1d ⊢ ( 𝑛 = ( ( 2 · 𝑖 ) − 1 ) → ( ( 𝑛 / 2 ) ∈ ℕ ↔ ( ( ( 2 · 𝑖 ) − 1 ) / 2 ) ∈ ℕ ) )
209 208 elrab ⊢ ( ( ( 2 · 𝑖 ) − 1 ) ∈ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ↔ ( ( ( 2 · 𝑖 ) − 1 ) ∈ ℕ ∧ ( ( ( 2 · 𝑖 ) − 1 ) / 2 ) ∈ ℕ ) )
210 206 209 sylnibr ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ¬ ( ( 2 · 𝑖 ) − 1 ) ∈ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } )
211 210 adantl ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑘 ) ) → ¬ ( ( 2 · 𝑖 ) − 1 ) ∈ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } )
212 179 211 eldifd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑘 ) ) → ( ( 2 · 𝑖 ) − 1 ) ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) )
213 212 fmpttd ⊢ ( 𝑘 ∈ ℕ → ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) : ( 1 ... 𝑘 ) ⟶ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) )
214 eqidd ⊢ ( 𝑥 ∈ ( 1 ... 𝑘 ) → ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) = ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) )
215 oveq2 ⊢ ( 𝑖 = 𝑥 → ( 2 · 𝑖 ) = ( 2 · 𝑥 ) )
216 215 oveq1d ⊢ ( 𝑖 = 𝑥 → ( ( 2 · 𝑖 ) − 1 ) = ( ( 2 · 𝑥 ) − 1 ) )
217 216 adantl ⊢ ( ( 𝑥 ∈ ( 1 ... 𝑘 ) ∧ 𝑖 = 𝑥 ) → ( ( 2 · 𝑖 ) − 1 ) = ( ( 2 · 𝑥 ) − 1 ) )
218 id ⊢ ( 𝑥 ∈ ( 1 ... 𝑘 ) → 𝑥 ∈ ( 1 ... 𝑘 ) )
219 ovexd ⊢ ( 𝑥 ∈ ( 1 ... 𝑘 ) → ( ( 2 · 𝑥 ) − 1 ) ∈ V )
220 214 217 218 219 fvmptd ⊢ ( 𝑥 ∈ ( 1 ... 𝑘 ) → ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑥 ) = ( ( 2 · 𝑥 ) − 1 ) )
221 220 eqcomd ⊢ ( 𝑥 ∈ ( 1 ... 𝑘 ) → ( ( 2 · 𝑥 ) − 1 ) = ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑥 ) )
222 221 ad2antrr ⊢ ( ( ( 𝑥 ∈ ( 1 ... 𝑘 ) ∧ 𝑦 ∈ ( 1 ... 𝑘 ) ) ∧ ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑥 ) = ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑦 ) ) → ( ( 2 · 𝑥 ) − 1 ) = ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑥 ) )
223 simpr ⊢ ( ( ( 𝑥 ∈ ( 1 ... 𝑘 ) ∧ 𝑦 ∈ ( 1 ... 𝑘 ) ) ∧ ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑥 ) = ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑦 ) ) → ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑥 ) = ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑦 ) )
224 eqidd ⊢ ( 𝑦 ∈ ( 1 ... 𝑘 ) → ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) = ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) )
225 oveq2 ⊢ ( 𝑖 = 𝑦 → ( 2 · 𝑖 ) = ( 2 · 𝑦 ) )
226 225 oveq1d ⊢ ( 𝑖 = 𝑦 → ( ( 2 · 𝑖 ) − 1 ) = ( ( 2 · 𝑦 ) − 1 ) )
227 226 adantl ⊢ ( ( 𝑦 ∈ ( 1 ... 𝑘 ) ∧ 𝑖 = 𝑦 ) → ( ( 2 · 𝑖 ) − 1 ) = ( ( 2 · 𝑦 ) − 1 ) )
228 id ⊢ ( 𝑦 ∈ ( 1 ... 𝑘 ) → 𝑦 ∈ ( 1 ... 𝑘 ) )
229 ovexd ⊢ ( 𝑦 ∈ ( 1 ... 𝑘 ) → ( ( 2 · 𝑦 ) − 1 ) ∈ V )
230 224 227 228 229 fvmptd ⊢ ( 𝑦 ∈ ( 1 ... 𝑘 ) → ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑦 ) = ( ( 2 · 𝑦 ) − 1 ) )
231 230 ad2antlr ⊢ ( ( ( 𝑥 ∈ ( 1 ... 𝑘 ) ∧ 𝑦 ∈ ( 1 ... 𝑘 ) ) ∧ ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑥 ) = ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑦 ) ) → ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑦 ) = ( ( 2 · 𝑦 ) − 1 ) )
232 222 223 231 3eqtrd ⊢ ( ( ( 𝑥 ∈ ( 1 ... 𝑘 ) ∧ 𝑦 ∈ ( 1 ... 𝑘 ) ) ∧ ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑥 ) = ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑦 ) ) → ( ( 2 · 𝑥 ) − 1 ) = ( ( 2 · 𝑦 ) − 1 ) )
233 2cnd ⊢ ( 𝑥 ∈ ( 1 ... 𝑘 ) → 2 ∈ ℂ )
234 elfzelz ⊢ ( 𝑥 ∈ ( 1 ... 𝑘 ) → 𝑥 ∈ ℤ )
235 234 zcnd ⊢ ( 𝑥 ∈ ( 1 ... 𝑘 ) → 𝑥 ∈ ℂ )
236 233 235 mulcld ⊢ ( 𝑥 ∈ ( 1 ... 𝑘 ) → ( 2 · 𝑥 ) ∈ ℂ )
237 236 ad2antrr ⊢ ( ( ( 𝑥 ∈ ( 1 ... 𝑘 ) ∧ 𝑦 ∈ ( 1 ... 𝑘 ) ) ∧ ( ( 2 · 𝑥 ) − 1 ) = ( ( 2 · 𝑦 ) − 1 ) ) → ( 2 · 𝑥 ) ∈ ℂ )
238 2cnd ⊢ ( 𝑦 ∈ ( 1 ... 𝑘 ) → 2 ∈ ℂ )
239 elfzelz ⊢ ( 𝑦 ∈ ( 1 ... 𝑘 ) → 𝑦 ∈ ℤ )
240 239 zcnd ⊢ ( 𝑦 ∈ ( 1 ... 𝑘 ) → 𝑦 ∈ ℂ )
241 238 240 mulcld ⊢ ( 𝑦 ∈ ( 1 ... 𝑘 ) → ( 2 · 𝑦 ) ∈ ℂ )
242 241 ad2antlr ⊢ ( ( ( 𝑥 ∈ ( 1 ... 𝑘 ) ∧ 𝑦 ∈ ( 1 ... 𝑘 ) ) ∧ ( ( 2 · 𝑥 ) − 1 ) = ( ( 2 · 𝑦 ) − 1 ) ) → ( 2 · 𝑦 ) ∈ ℂ )
243 1cnd ⊢ ( ( ( 𝑥 ∈ ( 1 ... 𝑘 ) ∧ 𝑦 ∈ ( 1 ... 𝑘 ) ) ∧ ( ( 2 · 𝑥 ) − 1 ) = ( ( 2 · 𝑦 ) − 1 ) ) → 1 ∈ ℂ )
244 simpr ⊢ ( ( ( 𝑥 ∈ ( 1 ... 𝑘 ) ∧ 𝑦 ∈ ( 1 ... 𝑘 ) ) ∧ ( ( 2 · 𝑥 ) − 1 ) = ( ( 2 · 𝑦 ) − 1 ) ) → ( ( 2 · 𝑥 ) − 1 ) = ( ( 2 · 𝑦 ) − 1 ) )
245 237 242 243 244 subcan2d ⊢ ( ( ( 𝑥 ∈ ( 1 ... 𝑘 ) ∧ 𝑦 ∈ ( 1 ... 𝑘 ) ) ∧ ( ( 2 · 𝑥 ) − 1 ) = ( ( 2 · 𝑦 ) − 1 ) ) → ( 2 · 𝑥 ) = ( 2 · 𝑦 ) )
246 235 ad2antrr ⊢ ( ( ( 𝑥 ∈ ( 1 ... 𝑘 ) ∧ 𝑦 ∈ ( 1 ... 𝑘 ) ) ∧ ( 2 · 𝑥 ) = ( 2 · 𝑦 ) ) → 𝑥 ∈ ℂ )
247 240 ad2antlr ⊢ ( ( ( 𝑥 ∈ ( 1 ... 𝑘 ) ∧ 𝑦 ∈ ( 1 ... 𝑘 ) ) ∧ ( 2 · 𝑥 ) = ( 2 · 𝑦 ) ) → 𝑦 ∈ ℂ )
248 2cnd ⊢ ( ( ( 𝑥 ∈ ( 1 ... 𝑘 ) ∧ 𝑦 ∈ ( 1 ... 𝑘 ) ) ∧ ( 2 · 𝑥 ) = ( 2 · 𝑦 ) ) → 2 ∈ ℂ )
249 183 a1i ⊢ ( ( ( 𝑥 ∈ ( 1 ... 𝑘 ) ∧ 𝑦 ∈ ( 1 ... 𝑘 ) ) ∧ ( 2 · 𝑥 ) = ( 2 · 𝑦 ) ) → 2 ≠ 0 )
250 simpr ⊢ ( ( ( 𝑥 ∈ ( 1 ... 𝑘 ) ∧ 𝑦 ∈ ( 1 ... 𝑘 ) ) ∧ ( 2 · 𝑥 ) = ( 2 · 𝑦 ) ) → ( 2 · 𝑥 ) = ( 2 · 𝑦 ) )
251 246 247 248 249 250 mulcanad ⊢ ( ( ( 𝑥 ∈ ( 1 ... 𝑘 ) ∧ 𝑦 ∈ ( 1 ... 𝑘 ) ) ∧ ( 2 · 𝑥 ) = ( 2 · 𝑦 ) ) → 𝑥 = 𝑦 )
252 245 251 syldan ⊢ ( ( ( 𝑥 ∈ ( 1 ... 𝑘 ) ∧ 𝑦 ∈ ( 1 ... 𝑘 ) ) ∧ ( ( 2 · 𝑥 ) − 1 ) = ( ( 2 · 𝑦 ) − 1 ) ) → 𝑥 = 𝑦 )
253 232 252 syldan ⊢ ( ( ( 𝑥 ∈ ( 1 ... 𝑘 ) ∧ 𝑦 ∈ ( 1 ... 𝑘 ) ) ∧ ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑥 ) = ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑦 ) ) → 𝑥 = 𝑦 )
254 253 adantll ⊢ ( ( ( 𝑘 ∈ ℕ ∧ ( 𝑥 ∈ ( 1 ... 𝑘 ) ∧ 𝑦 ∈ ( 1 ... 𝑘 ) ) ) ∧ ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑥 ) = ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑦 ) ) → 𝑥 = 𝑦 )
255 254 ex ⊢ ( ( 𝑘 ∈ ℕ ∧ ( 𝑥 ∈ ( 1 ... 𝑘 ) ∧ 𝑦 ∈ ( 1 ... 𝑘 ) ) ) → ( ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑥 ) = ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
256 255 ralrimivva ⊢ ( 𝑘 ∈ ℕ → ∀ 𝑥 ∈ ( 1 ... 𝑘 ) ∀ 𝑦 ∈ ( 1 ... 𝑘 ) ( ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑥 ) = ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
257 dff13 ⊢ ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) : ( 1 ... 𝑘 ) –1-1→ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ↔ ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) : ( 1 ... 𝑘 ) ⟶ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝑘 ) ∀ 𝑦 ∈ ( 1 ... 𝑘 ) ( ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑥 ) = ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
258 213 256 257 sylanbrc ⊢ ( 𝑘 ∈ ℕ → ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) : ( 1 ... 𝑘 ) –1-1→ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) )
259 1zzd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) → 1 ∈ ℤ )
260 33 adantr ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) → 𝑘 ∈ ℤ )
261 134 elfzelzd ⊢ ( 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) → 𝑗 ∈ ℤ )
262 zeo ⊢ ( 𝑗 ∈ ℤ → ( ( 𝑗 / 2 ) ∈ ℤ ∨ ( ( 𝑗 + 1 ) / 2 ) ∈ ℤ ) )
263 261 262 syl ⊢ ( 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) → ( ( 𝑗 / 2 ) ∈ ℤ ∨ ( ( 𝑗 + 1 ) / 2 ) ∈ ℤ ) )
264 263 adantl ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) → ( ( 𝑗 / 2 ) ∈ ℤ ∨ ( ( 𝑗 + 1 ) / 2 ) ∈ ℤ ) )
265 eldifn ⊢ ( 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) → ¬ 𝑗 ∈ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } )
266 134 92 syl ⊢ ( 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) → 𝑗 ∈ ℕ )
267 266 adantr ⊢ ( ( 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∧ ( 𝑗 / 2 ) ∈ ℤ ) → 𝑗 ∈ ℕ )
268 simpr ⊢ ( ( 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∧ ( 𝑗 / 2 ) ∈ ℤ ) → ( 𝑗 / 2 ) ∈ ℤ )
269 267 nnred ⊢ ( ( 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∧ ( 𝑗 / 2 ) ∈ ℤ ) → 𝑗 ∈ ℝ )
270 39 a1i ⊢ ( ( 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∧ ( 𝑗 / 2 ) ∈ ℤ ) → 2 ∈ ℝ )
271 267 nngt0d ⊢ ( ( 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∧ ( 𝑗 / 2 ) ∈ ℤ ) → 0 < 𝑗 )
272 2pos ⊢ 0 < 2
273 272 a1i ⊢ ( ( 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∧ ( 𝑗 / 2 ) ∈ ℤ ) → 0 < 2 )
274 269 270 271 273 divgt0d ⊢ ( ( 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∧ ( 𝑗 / 2 ) ∈ ℤ ) → 0 < ( 𝑗 / 2 ) )
275 elnnz ⊢ ( ( 𝑗 / 2 ) ∈ ℕ ↔ ( ( 𝑗 / 2 ) ∈ ℤ ∧ 0 < ( 𝑗 / 2 ) ) )
276 268 274 275 sylanbrc ⊢ ( ( 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∧ ( 𝑗 / 2 ) ∈ ℤ ) → ( 𝑗 / 2 ) ∈ ℕ )
277 oveq1 ⊢ ( 𝑛 = 𝑗 → ( 𝑛 / 2 ) = ( 𝑗 / 2 ) )
278 277 eleq1d ⊢ ( 𝑛 = 𝑗 → ( ( 𝑛 / 2 ) ∈ ℕ ↔ ( 𝑗 / 2 ) ∈ ℕ ) )
279 278 elrab ⊢ ( 𝑗 ∈ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ↔ ( 𝑗 ∈ ℕ ∧ ( 𝑗 / 2 ) ∈ ℕ ) )
280 267 276 279 sylanbrc ⊢ ( ( 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∧ ( 𝑗 / 2 ) ∈ ℤ ) → 𝑗 ∈ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } )
281 265 280 mtand ⊢ ( 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) → ¬ ( 𝑗 / 2 ) ∈ ℤ )
282 281 adantl ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) → ¬ ( 𝑗 / 2 ) ∈ ℤ )
283 pm2.53 ⊢ ( ( ( 𝑗 / 2 ) ∈ ℤ ∨ ( ( 𝑗 + 1 ) / 2 ) ∈ ℤ ) → ( ¬ ( 𝑗 / 2 ) ∈ ℤ → ( ( 𝑗 + 1 ) / 2 ) ∈ ℤ ) )
284 264 282 283 sylc ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) → ( ( 𝑗 + 1 ) / 2 ) ∈ ℤ )
285 1p1e2 ⊢ ( 1 + 1 ) = 2
286 285 oveq1i ⊢ ( ( 1 + 1 ) / 2 ) = ( 2 / 2 )
287 2div2e1 ⊢ ( 2 / 2 ) = 1
288 286 287 eqtr2i ⊢ 1 = ( ( 1 + 1 ) / 2 )
289 1red ⊢ ( 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) → 1 ∈ ℝ )
290 289 289 readdcld ⊢ ( 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) → ( 1 + 1 ) ∈ ℝ )
291 92 nnred ⊢ ( 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) → 𝑗 ∈ ℝ )
292 291 289 readdcld ⊢ ( 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) → ( 𝑗 + 1 ) ∈ ℝ )
293 195 a1i ⊢ ( 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) → 2 ∈ ℝ+ )
294 elfzle1 ⊢ ( 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) → 1 ≤ 𝑗 )
295 289 291 289 294 leadd1dd ⊢ ( 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) → ( 1 + 1 ) ≤ ( 𝑗 + 1 ) )
296 290 292 293 295 lediv1dd ⊢ ( 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) → ( ( 1 + 1 ) / 2 ) ≤ ( ( 𝑗 + 1 ) / 2 ) )
297 288 296 eqbrtrid ⊢ ( 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) → 1 ≤ ( ( 𝑗 + 1 ) / 2 ) )
298 134 297 syl ⊢ ( 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) → 1 ≤ ( ( 𝑗 + 1 ) / 2 ) )
299 298 adantl ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) → 1 ≤ ( ( 𝑗 + 1 ) / 2 ) )
300 elfzel2 ⊢ ( 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) → ( ( 2 · 𝑘 ) − 1 ) ∈ ℤ )
301 300 zred ⊢ ( 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) → ( ( 2 · 𝑘 ) − 1 ) ∈ ℝ )
302 301 289 readdcld ⊢ ( 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) → ( ( ( 2 · 𝑘 ) − 1 ) + 1 ) ∈ ℝ )
303 elfzle2 ⊢ ( 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) → 𝑗 ≤ ( ( 2 · 𝑘 ) − 1 ) )
304 291 301 289 303 leadd1dd ⊢ ( 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) → ( 𝑗 + 1 ) ≤ ( ( ( 2 · 𝑘 ) − 1 ) + 1 ) )
305 292 302 293 304 lediv1dd ⊢ ( 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) → ( ( 𝑗 + 1 ) / 2 ) ≤ ( ( ( ( 2 · 𝑘 ) − 1 ) + 1 ) / 2 ) )
306 305 adantl ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ) → ( ( 𝑗 + 1 ) / 2 ) ≤ ( ( ( ( 2 · 𝑘 ) − 1 ) + 1 ) / 2 ) )
307 51 adantr ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ) → ( 2 · 𝑘 ) ∈ ℂ )
308 1cnd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ) → 1 ∈ ℂ )
309 307 308 npcand ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ) → ( ( ( 2 · 𝑘 ) − 1 ) + 1 ) = ( 2 · 𝑘 ) )
310 309 oveq1d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ) → ( ( ( ( 2 · 𝑘 ) − 1 ) + 1 ) / 2 ) = ( ( 2 · 𝑘 ) / 2 ) )
311 183 a1i ⊢ ( 𝑘 ∈ ℕ → 2 ≠ 0 )
312 45 44 311 divcan3d ⊢ ( 𝑘 ∈ ℕ → ( ( 2 · 𝑘 ) / 2 ) = 𝑘 )
313 312 adantr ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ) → ( ( 2 · 𝑘 ) / 2 ) = 𝑘 )
314 310 313 eqtrd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ) → ( ( ( ( 2 · 𝑘 ) − 1 ) + 1 ) / 2 ) = 𝑘 )
315 306 314 breqtrd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ) → ( ( 𝑗 + 1 ) / 2 ) ≤ 𝑘 )
316 134 315 sylan2 ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) → ( ( 𝑗 + 1 ) / 2 ) ≤ 𝑘 )
317 259 260 284 299 316 elfzd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) → ( ( 𝑗 + 1 ) / 2 ) ∈ ( 1 ... 𝑘 ) )
318 266 nncnd ⊢ ( 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) → 𝑗 ∈ ℂ )
319 peano2cn ⊢ ( 𝑗 ∈ ℂ → ( 𝑗 + 1 ) ∈ ℂ )
320 2cnd ⊢ ( 𝑗 ∈ ℂ → 2 ∈ ℂ )
321 183 a1i ⊢ ( 𝑗 ∈ ℂ → 2 ≠ 0 )
322 319 320 321 divcan2d ⊢ ( 𝑗 ∈ ℂ → ( 2 · ( ( 𝑗 + 1 ) / 2 ) ) = ( 𝑗 + 1 ) )
323 322 oveq1d ⊢ ( 𝑗 ∈ ℂ → ( ( 2 · ( ( 𝑗 + 1 ) / 2 ) ) − 1 ) = ( ( 𝑗 + 1 ) − 1 ) )
324 pncan1 ⊢ ( 𝑗 ∈ ℂ → ( ( 𝑗 + 1 ) − 1 ) = 𝑗 )
325 323 324 eqtr2d ⊢ ( 𝑗 ∈ ℂ → 𝑗 = ( ( 2 · ( ( 𝑗 + 1 ) / 2 ) ) − 1 ) )
326 318 325 syl ⊢ ( 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) → 𝑗 = ( ( 2 · ( ( 𝑗 + 1 ) / 2 ) ) − 1 ) )
327 326 adantl ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) → 𝑗 = ( ( 2 · ( ( 𝑗 + 1 ) / 2 ) ) − 1 ) )
328 oveq2 ⊢ ( 𝑚 = ( ( 𝑗 + 1 ) / 2 ) → ( 2 · 𝑚 ) = ( 2 · ( ( 𝑗 + 1 ) / 2 ) ) )
329 328 oveq1d ⊢ ( 𝑚 = ( ( 𝑗 + 1 ) / 2 ) → ( ( 2 · 𝑚 ) − 1 ) = ( ( 2 · ( ( 𝑗 + 1 ) / 2 ) ) − 1 ) )
330 329 rspceeqv ⊢ ( ( ( ( 𝑗 + 1 ) / 2 ) ∈ ( 1 ... 𝑘 ) ∧ 𝑗 = ( ( 2 · ( ( 𝑗 + 1 ) / 2 ) ) − 1 ) ) → ∃ 𝑚 ∈ ( 1 ... 𝑘 ) 𝑗 = ( ( 2 · 𝑚 ) − 1 ) )
331 317 327 330 syl2anc ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) → ∃ 𝑚 ∈ ( 1 ... 𝑘 ) 𝑗 = ( ( 2 · 𝑚 ) − 1 ) )
332 eqidd ⊢ ( ( 𝑚 ∈ ( 1 ... 𝑘 ) ∧ 𝑗 = ( ( 2 · 𝑚 ) − 1 ) ) → ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) = ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) )
333 oveq2 ⊢ ( 𝑖 = 𝑚 → ( 2 · 𝑖 ) = ( 2 · 𝑚 ) )
334 333 oveq1d ⊢ ( 𝑖 = 𝑚 → ( ( 2 · 𝑖 ) − 1 ) = ( ( 2 · 𝑚 ) − 1 ) )
335 334 adantl ⊢ ( ( ( 𝑚 ∈ ( 1 ... 𝑘 ) ∧ 𝑗 = ( ( 2 · 𝑚 ) − 1 ) ) ∧ 𝑖 = 𝑚 ) → ( ( 2 · 𝑖 ) − 1 ) = ( ( 2 · 𝑚 ) − 1 ) )
336 simpl ⊢ ( ( 𝑚 ∈ ( 1 ... 𝑘 ) ∧ 𝑗 = ( ( 2 · 𝑚 ) − 1 ) ) → 𝑚 ∈ ( 1 ... 𝑘 ) )
337 ovexd ⊢ ( ( 𝑚 ∈ ( 1 ... 𝑘 ) ∧ 𝑗 = ( ( 2 · 𝑚 ) − 1 ) ) → ( ( 2 · 𝑚 ) − 1 ) ∈ V )
338 332 335 336 337 fvmptd ⊢ ( ( 𝑚 ∈ ( 1 ... 𝑘 ) ∧ 𝑗 = ( ( 2 · 𝑚 ) − 1 ) ) → ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑚 ) = ( ( 2 · 𝑚 ) − 1 ) )
339 id ⊢ ( 𝑗 = ( ( 2 · 𝑚 ) − 1 ) → 𝑗 = ( ( 2 · 𝑚 ) − 1 ) )
340 339 eqcomd ⊢ ( 𝑗 = ( ( 2 · 𝑚 ) − 1 ) → ( ( 2 · 𝑚 ) − 1 ) = 𝑗 )
341 340 adantl ⊢ ( ( 𝑚 ∈ ( 1 ... 𝑘 ) ∧ 𝑗 = ( ( 2 · 𝑚 ) − 1 ) ) → ( ( 2 · 𝑚 ) − 1 ) = 𝑗 )
342 338 341 eqtr2d ⊢ ( ( 𝑚 ∈ ( 1 ... 𝑘 ) ∧ 𝑗 = ( ( 2 · 𝑚 ) − 1 ) ) → 𝑗 = ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑚 ) )
343 342 ex ⊢ ( 𝑚 ∈ ( 1 ... 𝑘 ) → ( 𝑗 = ( ( 2 · 𝑚 ) − 1 ) → 𝑗 = ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑚 ) ) )
344 343 adantl ⊢ ( ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) ∧ 𝑚 ∈ ( 1 ... 𝑘 ) ) → ( 𝑗 = ( ( 2 · 𝑚 ) − 1 ) → 𝑗 = ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑚 ) ) )
345 344 reximdva ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) → ( ∃ 𝑚 ∈ ( 1 ... 𝑘 ) 𝑗 = ( ( 2 · 𝑚 ) − 1 ) → ∃ 𝑚 ∈ ( 1 ... 𝑘 ) 𝑗 = ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑚 ) ) )
346 331 345 mpd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) → ∃ 𝑚 ∈ ( 1 ... 𝑘 ) 𝑗 = ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑚 ) )
347 346 ralrimiva ⊢ ( 𝑘 ∈ ℕ → ∀ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∃ 𝑚 ∈ ( 1 ... 𝑘 ) 𝑗 = ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑚 ) )
348 dffo3 ⊢ ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) : ( 1 ... 𝑘 ) –onto→ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ↔ ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) : ( 1 ... 𝑘 ) ⟶ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∧ ∀ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∃ 𝑚 ∈ ( 1 ... 𝑘 ) 𝑗 = ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑚 ) ) )
349 213 347 348 sylanbrc ⊢ ( 𝑘 ∈ ℕ → ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) : ( 1 ... 𝑘 ) –onto→ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) )
350 df-f1o ⊢ ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) : ( 1 ... 𝑘 ) –1-1-onto→ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ↔ ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) : ( 1 ... 𝑘 ) –1-1→ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∧ ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) : ( 1 ... 𝑘 ) –onto→ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) )
351 258 349 350 sylanbrc ⊢ ( 𝑘 ∈ ℕ → ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) : ( 1 ... 𝑘 ) –1-1-onto→ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) )
352 351 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) : ( 1 ... 𝑘 ) –1-1-onto→ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) )
353 eqidd ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) = ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) )
354 oveq2 ⊢ ( 𝑖 = 𝑗 → ( 2 · 𝑖 ) = ( 2 · 𝑗 ) )
355 354 oveq1d ⊢ ( 𝑖 = 𝑗 → ( ( 2 · 𝑖 ) − 1 ) = ( ( 2 · 𝑗 ) − 1 ) )
356 355 adantl ⊢ ( ( 𝑗 ∈ ( 1 ... 𝑘 ) ∧ 𝑖 = 𝑗 ) → ( ( 2 · 𝑖 ) − 1 ) = ( ( 2 · 𝑗 ) − 1 ) )
357 id ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → 𝑗 ∈ ( 1 ... 𝑘 ) )
358 ovexd ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → ( ( 2 · 𝑗 ) − 1 ) ∈ V )
359 353 356 357 358 fvmptd ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑗 ) = ( ( 2 · 𝑗 ) − 1 ) )
360 359 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑗 ) = ( ( 2 · 𝑗 ) − 1 ) )
361 eleq1w ⊢ ( 𝑗 = 𝑖 → ( 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ↔ 𝑖 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) )
362 361 anbi2d ⊢ ( 𝑗 = 𝑖 → ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) ↔ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) ) )
363 139 eleq1d ⊢ ( 𝑗 = 𝑖 → ( ( 𝐹 ‘ 𝑗 ) ∈ ℂ ↔ ( 𝐹 ‘ 𝑖 ) ∈ ℂ ) )
364 362 363 imbi12d ⊢ ( 𝑗 = 𝑖 → ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℂ ) ↔ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) → ( 𝐹 ‘ 𝑖 ) ∈ ℂ ) ) )
365 364 136 chvarvv ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) → ( 𝐹 ‘ 𝑖 ) ∈ ℂ )
366 143 144 352 360 365 fsumf1o ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → Σ 𝑖 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ( 𝐹 ‘ 𝑖 ) = Σ 𝑗 ∈ ( 1 ... 𝑘 ) ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) )
367 96 142 366 3eqtrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → Σ 𝑗 ∈ ( 1 ... 𝑘 ) ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) = Σ 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) )
368 ovex ⊢ ( ( 2 · 𝑘 ) − 1 ) ∈ V
369 21 fvmpt2 ⊢ ( ( 𝑘 ∈ ℕ ∧ ( ( 2 · 𝑘 ) − 1 ) ∈ V ) → ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) = ( ( 2 · 𝑘 ) − 1 ) )
370 368 369 mpan2 ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) = ( ( 2 · 𝑘 ) − 1 ) )
371 370 oveq2d ⊢ ( 𝑘 ∈ ℕ → ( 1 ... ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) ) = ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) )
372 371 eqcomd ⊢ ( 𝑘 ∈ ℕ → ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) = ( 1 ... ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) ) )
373 372 sumeq1d ⊢ ( 𝑘 ∈ ℕ → Σ 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) = Σ 𝑗 ∈ ( 1 ... ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) ) ( 𝐹 ‘ 𝑗 ) )
374 373 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → Σ 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) = Σ 𝑗 ∈ ( 1 ... ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) ) ( 𝐹 ‘ 𝑗 ) )
375 367 374 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → Σ 𝑗 ∈ ( 1 ... 𝑘 ) ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) = Σ 𝑗 ∈ ( 1 ... ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) ) ( 𝐹 ‘ 𝑗 ) )
376 elfznn ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → 𝑗 ∈ ℕ )
377 376 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → 𝑗 ∈ ℕ )
378 1 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → 𝐹 : ℕ ⟶ ℂ )
379 31 a1i ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → 2 ∈ ℤ )
380 elfzelz ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → 𝑗 ∈ ℤ )
381 379 380 zmulcld ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → ( 2 · 𝑗 ) ∈ ℤ )
382 1zzd ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → 1 ∈ ℤ )
383 381 382 zsubcld ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → ( ( 2 · 𝑗 ) − 1 ) ∈ ℤ )
384 0red ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → 0 ∈ ℝ )
385 39 a1i ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → 2 ∈ ℝ )
386 25 385 eqeltrid ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → ( 2 · 1 ) ∈ ℝ )
387 1red ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → 1 ∈ ℝ )
388 386 387 resubcld ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → ( ( 2 · 1 ) − 1 ) ∈ ℝ )
389 383 zred ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → ( ( 2 · 𝑗 ) − 1 ) ∈ ℝ )
390 0lt1 ⊢ 0 < 1
391 153 a1i ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → 1 = ( ( 2 · 1 ) − 1 ) )
392 390 391 breqtrid ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → 0 < ( ( 2 · 1 ) − 1 ) )
393 381 zred ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → ( 2 · 𝑗 ) ∈ ℝ )
394 376 nnred ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → 𝑗 ∈ ℝ )
395 161 a1i ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → 0 ≤ 2 )
396 elfzle1 ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → 1 ≤ 𝑗 )
397 387 394 385 395 396 lemul2ad ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → ( 2 · 1 ) ≤ ( 2 · 𝑗 ) )
398 386 393 387 397 lesub1dd ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → ( ( 2 · 1 ) − 1 ) ≤ ( ( 2 · 𝑗 ) − 1 ) )
399 384 388 389 392 398 ltletrd ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → 0 < ( ( 2 · 𝑗 ) − 1 ) )
400 elnnz ⊢ ( ( ( 2 · 𝑗 ) − 1 ) ∈ ℕ ↔ ( ( ( 2 · 𝑗 ) − 1 ) ∈ ℤ ∧ 0 < ( ( 2 · 𝑗 ) − 1 ) ) )
401 383 399 400 sylanbrc ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → ( ( 2 · 𝑗 ) − 1 ) ∈ ℕ )
402 401 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → ( ( 2 · 𝑗 ) − 1 ) ∈ ℕ )
403 378 402 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) ∈ ℂ )
404 403 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) ∈ ℂ )
405 60 fveq2d ⊢ ( 𝑘 = 𝑗 → ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) = ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) )
406 405 cbvmptv ⊢ ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) = ( 𝑗 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) )
407 406 fvmpt2 ⊢ ( ( 𝑗 ∈ ℕ ∧ ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) ∈ ℂ ) → ( ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ‘ 𝑗 ) = ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) )
408 377 404 407 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → ( ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ‘ 𝑗 ) = ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) )
409 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ )
410 409 11 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ( ℤ≥ ‘ 1 ) )
411 408 410 404 fsumser ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → Σ 𝑗 ∈ ( 1 ... 𝑘 ) ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) = ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ) ‘ 𝑘 ) )
412 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) ) ) → ( 𝐹 ‘ 𝑗 ) = ( 𝐹 ‘ 𝑗 ) )
413 155 a1i ⊢ ( 𝑘 ∈ ℕ → ( 2 · 1 ) ∈ ℝ )
414 1red ⊢ ( 𝑘 ∈ ℕ → 1 ∈ ℝ )
415 161 a1i ⊢ ( 𝑘 ∈ ℕ → 0 ≤ 2 )
416 nnge1 ⊢ ( 𝑘 ∈ ℕ → 1 ≤ 𝑘 )
417 414 41 40 415 416 lemul2ad ⊢ ( 𝑘 ∈ ℕ → ( 2 · 1 ) ≤ ( 2 · 𝑘 ) )
418 413 42 414 417 lesub1dd ⊢ ( 𝑘 ∈ ℕ → ( ( 2 · 1 ) − 1 ) ≤ ( ( 2 · 𝑘 ) − 1 ) )
419 153 418 eqbrtrid ⊢ ( 𝑘 ∈ ℕ → 1 ≤ ( ( 2 · 𝑘 ) − 1 ) )
420 eluz2 ⊢ ( ( ( 2 · 𝑘 ) − 1 ) ∈ ( ℤ≥ ‘ 1 ) ↔ ( 1 ∈ ℤ ∧ ( ( 2 · 𝑘 ) − 1 ) ∈ ℤ ∧ 1 ≤ ( ( 2 · 𝑘 ) − 1 ) ) )
421 37 66 419 420 syl3anbrc ⊢ ( 𝑘 ∈ ℕ → ( ( 2 · 𝑘 ) − 1 ) ∈ ( ℤ≥ ‘ 1 ) )
422 68 421 eqeltrd ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 1 ) )
423 422 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 1 ) )
424 simpll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) ) ) → 𝜑 )
425 simpr ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( 1 ... ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) ) ) → 𝑗 ∈ ( 1 ... ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) ) )
426 371 adantr ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( 1 ... ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) ) ) → ( 1 ... ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) ) = ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) )
427 425 426 eleqtrd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( 1 ... ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) ) ) → 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) )
428 427 adantll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) ) ) → 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) )
429 424 428 94 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℂ )
430 412 423 429 fsumser ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → Σ 𝑗 ∈ ( 1 ... ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) ) ( 𝐹 ‘ 𝑗 ) = ( seq 1 ( + , 𝐹 ) ‘ ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) ) )
431 375 411 430 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ) ‘ 𝑘 ) = ( seq 1 ( + , 𝐹 ) ‘ ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) ) )
432 4 5 9 10 11 12 14 17 3 30 74 76 431 climsuse ⊢ ( 𝜑 → seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ) ⇝ 𝐵 )
433 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
434 11 12 433 15 isum ⊢ ( 𝜑 → Σ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) = ( ⇝ ‘ seq 1 ( + , 𝐹 ) ) )
435 climrel ⊢ Rel ⇝
436 435 releldmi ⊢ ( seq 1 ( + , 𝐹 ) ⇝ 𝐵 → seq 1 ( + , 𝐹 ) ∈ dom ⇝ )
437 3 436 syl ⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) ∈ dom ⇝ )
438 climdm ⊢ ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ↔ seq 1 ( + , 𝐹 ) ⇝ ( ⇝ ‘ seq 1 ( + , 𝐹 ) ) )
439 437 438 sylib ⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) ⇝ ( ⇝ ‘ seq 1 ( + , 𝐹 ) ) )
440 climuni ⊢ ( ( seq 1 ( + , 𝐹 ) ⇝ ( ⇝ ‘ seq 1 ( + , 𝐹 ) ) ∧ seq 1 ( + , 𝐹 ) ⇝ 𝐵 ) → ( ⇝ ‘ seq 1 ( + , 𝐹 ) ) = 𝐵 )
441 439 3 440 syl2anc ⊢ ( 𝜑 → ( ⇝ ‘ seq 1 ( + , 𝐹 ) ) = 𝐵 )
442 435 a1i ⊢ ( 𝜑 → Rel ⇝ )
443 releldm ⊢ ( ( Rel ⇝ ∧ seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ) ⇝ 𝐵 ) → seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ) ∈ dom ⇝ )
444 442 432 443 syl2anc ⊢ ( 𝜑 → seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ) ∈ dom ⇝ )
445 climdm ⊢ ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ) ∈ dom ⇝ ↔ seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ) ⇝ ( ⇝ ‘ seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ) ) )
446 444 445 sylib ⊢ ( 𝜑 → seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ) ⇝ ( ⇝ ‘ seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ) ) )
447 406 a1i ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) = ( 𝑗 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) ) )
448 447 seqeq3d ⊢ ( 𝜑 → seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ) = seq 1 ( + , ( 𝑗 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) ) ) )
449 448 fveq2d ⊢ ( 𝜑 → ( ⇝ ‘ seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ) ) = ( ⇝ ‘ seq 1 ( + , ( 𝑗 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) ) ) ) )
450 446 449 breqtrd ⊢ ( 𝜑 → seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ) ⇝ ( ⇝ ‘ seq 1 ( + , ( 𝑗 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) ) ) ) )
451 climuni ⊢ ( ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ) ⇝ 𝐵 ∧ seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ) ⇝ ( ⇝ ‘ seq 1 ( + , ( 𝑗 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) ) ) ) ) → 𝐵 = ( ⇝ ‘ seq 1 ( + , ( 𝑗 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) ) ) ) )
452 432 450 451 syl2anc ⊢ ( 𝜑 → 𝐵 = ( ⇝ ‘ seq 1 ( + , ( 𝑗 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) ) ) ) )
453 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑗 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) ) = ( 𝑗 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) ) )
454 eqcom ⊢ ( 𝑘 = 𝑗 ↔ 𝑗 = 𝑘 )
455 eqcom ⊢ ( ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) = ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) ↔ ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) = ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) )
456 405 454 455 3imtr3i ⊢ ( 𝑗 = 𝑘 → ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) = ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) )
457 456 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 = 𝑘 ) → ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) = ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) )
458 1 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐹 : ℕ ⟶ ℂ )
459 421 11 eleqtrrdi ⊢ ( 𝑘 ∈ ℕ → ( ( 2 · 𝑘 ) − 1 ) ∈ ℕ )
460 459 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 2 · 𝑘 ) − 1 ) ∈ ℕ )
461 458 460 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ∈ ℂ )
462 453 457 409 461 fvmptd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑗 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) ) ‘ 𝑘 ) = ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) )
463 11 12 462 461 isum ⊢ ( 𝜑 → Σ 𝑘 ∈ ℕ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) = ( ⇝ ‘ seq 1 ( + , ( 𝑗 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) ) ) ) )
464 452 463 eqtr4d ⊢ ( 𝜑 → 𝐵 = Σ 𝑘 ∈ ℕ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) )
465 434 441 464 3eqtrd ⊢ ( 𝜑 → Σ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) = Σ 𝑘 ∈ ℕ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) )
466 432 465 jca ⊢ ( 𝜑 → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ) ⇝ 𝐵 ∧ Σ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) = Σ 𝑘 ∈ ℕ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) )