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