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 sseldi ⊢ ( 𝑗 ∈ ( ( 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 145 146 152 3jca ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑘 ) ) → ( 1 ∈ ℤ ∧ ( ( 2 · 𝑘 ) − 1 ) ∈ ℤ ∧ ( ( 2 · 𝑖 ) − 1 ) ∈ ℤ ) )
154 26 27 eqtr2i ⊢ 1 = ( ( 2 · 1 ) − 1 )
155 1re ⊢ 1 ∈ ℝ
156 39 155 remulcli ⊢ ( 2 · 1 ) ∈ ℝ
157 156 a1i ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ( 2 · 1 ) ∈ ℝ )
158 149 zred ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ( 2 · 𝑖 ) ∈ ℝ )
159 1red ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → 1 ∈ ℝ )
160 148 zred ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → 𝑖 ∈ ℝ )
161 39 a1i ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → 2 ∈ ℝ )
162 0le2 ⊢ 0 ≤ 2
163 162 a1i ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → 0 ≤ 2 )
164 elfzle1 ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → 1 ≤ 𝑖 )
165 159 160 161 163 164 lemul2ad ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ( 2 · 1 ) ≤ ( 2 · 𝑖 ) )
166 157 158 159 165 lesub1dd ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ( ( 2 · 1 ) − 1 ) ≤ ( ( 2 · 𝑖 ) − 1 ) )
167 154 166 eqbrtrid ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → 1 ≤ ( ( 2 · 𝑖 ) − 1 ) )
168 167 adantl ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑘 ) ) → 1 ≤ ( ( 2 · 𝑖 ) − 1 ) )
169 158 adantl ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑘 ) ) → ( 2 · 𝑖 ) ∈ ℝ )
170 42 adantr ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑘 ) ) → ( 2 · 𝑘 ) ∈ ℝ )
171 1red ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑘 ) ) → 1 ∈ ℝ )
172 160 adantl ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑘 ) ) → 𝑖 ∈ ℝ )
173 41 adantr ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑘 ) ) → 𝑘 ∈ ℝ )
174 39 a1i ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑘 ) ) → 2 ∈ ℝ )
175 162 a1i ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑘 ) ) → 0 ≤ 2 )
176 elfzle2 ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → 𝑖 ≤ 𝑘 )
177 176 adantl ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑘 ) ) → 𝑖 ≤ 𝑘 )
178 172 173 174 175 177 lemul2ad ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑘 ) ) → ( 2 · 𝑖 ) ≤ ( 2 · 𝑘 ) )
179 169 170 171 178 lesub1dd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑘 ) ) → ( ( 2 · 𝑖 ) − 1 ) ≤ ( ( 2 · 𝑘 ) − 1 ) )
180 168 179 jca ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑘 ) ) → ( 1 ≤ ( ( 2 · 𝑖 ) − 1 ) ∧ ( ( 2 · 𝑖 ) − 1 ) ≤ ( ( 2 · 𝑘 ) − 1 ) ) )
181 elfz2 ⊢ ( ( ( 2 · 𝑖 ) − 1 ) ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ↔ ( ( 1 ∈ ℤ ∧ ( ( 2 · 𝑘 ) − 1 ) ∈ ℤ ∧ ( ( 2 · 𝑖 ) − 1 ) ∈ ℤ ) ∧ ( 1 ≤ ( ( 2 · 𝑖 ) − 1 ) ∧ ( ( 2 · 𝑖 ) − 1 ) ≤ ( ( 2 · 𝑘 ) − 1 ) ) ) )
182 153 180 181 sylanbrc ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑘 ) ) → ( ( 2 · 𝑖 ) − 1 ) ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) )
183 149 zcnd ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ( 2 · 𝑖 ) ∈ ℂ )
184 1cnd ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → 1 ∈ ℂ )
185 2cnd ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → 2 ∈ ℂ )
186 2ne0 ⊢ 2 ≠ 0
187 186 a1i ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → 2 ≠ 0 )
188 183 184 185 187 divsubdird ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ( ( ( 2 · 𝑖 ) − 1 ) / 2 ) = ( ( ( 2 · 𝑖 ) / 2 ) − ( 1 / 2 ) ) )
189 148 zcnd ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → 𝑖 ∈ ℂ )
190 189 185 187 divcan3d ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ( ( 2 · 𝑖 ) / 2 ) = 𝑖 )
191 190 oveq1d ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ( ( ( 2 · 𝑖 ) / 2 ) − ( 1 / 2 ) ) = ( 𝑖 − ( 1 / 2 ) ) )
192 188 191 eqtrd ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ( ( ( 2 · 𝑖 ) − 1 ) / 2 ) = ( 𝑖 − ( 1 / 2 ) ) )
193 148 150 zsubcld ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ( 𝑖 − 1 ) ∈ ℤ )
194 161 187 rereccld ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ( 1 / 2 ) ∈ ℝ )
195 halflt1 ⊢ ( 1 / 2 ) < 1
196 195 a1i ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ( 1 / 2 ) < 1 )
197 194 159 160 196 ltsub2dd ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ( 𝑖 − 1 ) < ( 𝑖 − ( 1 / 2 ) ) )
198 2rp ⊢ 2 ∈ ℝ+
199 rpreccl ⊢ ( 2 ∈ ℝ+ → ( 1 / 2 ) ∈ ℝ+ )
200 198 199 mp1i ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ( 1 / 2 ) ∈ ℝ+ )
201 160 200 ltsubrpd ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ( 𝑖 − ( 1 / 2 ) ) < 𝑖 )
202 189 184 npcand ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ( ( 𝑖 − 1 ) + 1 ) = 𝑖 )
203 201 202 breqtrrd ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ( 𝑖 − ( 1 / 2 ) ) < ( ( 𝑖 − 1 ) + 1 ) )
204 btwnnz ⊢ ( ( ( 𝑖 − 1 ) ∈ ℤ ∧ ( 𝑖 − 1 ) < ( 𝑖 − ( 1 / 2 ) ) ∧ ( 𝑖 − ( 1 / 2 ) ) < ( ( 𝑖 − 1 ) + 1 ) ) → ¬ ( 𝑖 − ( 1 / 2 ) ) ∈ ℤ )
205 193 197 203 204 syl3anc ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ¬ ( 𝑖 − ( 1 / 2 ) ) ∈ ℤ )
206 nnz ⊢ ( ( 𝑖 − ( 1 / 2 ) ) ∈ ℕ → ( 𝑖 − ( 1 / 2 ) ) ∈ ℤ )
207 205 206 nsyl ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ¬ ( 𝑖 − ( 1 / 2 ) ) ∈ ℕ )
208 192 207 eqneltrd ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ¬ ( ( ( 2 · 𝑖 ) − 1 ) / 2 ) ∈ ℕ )
209 208 intnand ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ¬ ( ( ( 2 · 𝑖 ) − 1 ) ∈ ℕ ∧ ( ( ( 2 · 𝑖 ) − 1 ) / 2 ) ∈ ℕ ) )
210 oveq1 ⊢ ( 𝑛 = ( ( 2 · 𝑖 ) − 1 ) → ( 𝑛 / 2 ) = ( ( ( 2 · 𝑖 ) − 1 ) / 2 ) )
211 210 eleq1d ⊢ ( 𝑛 = ( ( 2 · 𝑖 ) − 1 ) → ( ( 𝑛 / 2 ) ∈ ℕ ↔ ( ( ( 2 · 𝑖 ) − 1 ) / 2 ) ∈ ℕ ) )
212 211 elrab ⊢ ( ( ( 2 · 𝑖 ) − 1 ) ∈ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ↔ ( ( ( 2 · 𝑖 ) − 1 ) ∈ ℕ ∧ ( ( ( 2 · 𝑖 ) − 1 ) / 2 ) ∈ ℕ ) )
213 209 212 sylnibr ⊢ ( 𝑖 ∈ ( 1 ... 𝑘 ) → ¬ ( ( 2 · 𝑖 ) − 1 ) ∈ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } )
214 213 adantl ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑘 ) ) → ¬ ( ( 2 · 𝑖 ) − 1 ) ∈ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } )
215 182 214 eldifd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑘 ) ) → ( ( 2 · 𝑖 ) − 1 ) ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) )
216 215 fmpttd ⊢ ( 𝑘 ∈ ℕ → ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) : ( 1 ... 𝑘 ) ⟶ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) )
217 eqidd ⊢ ( 𝑥 ∈ ( 1 ... 𝑘 ) → ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) = ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) )
218 oveq2 ⊢ ( 𝑖 = 𝑥 → ( 2 · 𝑖 ) = ( 2 · 𝑥 ) )
219 218 oveq1d ⊢ ( 𝑖 = 𝑥 → ( ( 2 · 𝑖 ) − 1 ) = ( ( 2 · 𝑥 ) − 1 ) )
220 219 adantl ⊢ ( ( 𝑥 ∈ ( 1 ... 𝑘 ) ∧ 𝑖 = 𝑥 ) → ( ( 2 · 𝑖 ) − 1 ) = ( ( 2 · 𝑥 ) − 1 ) )
221 id ⊢ ( 𝑥 ∈ ( 1 ... 𝑘 ) → 𝑥 ∈ ( 1 ... 𝑘 ) )
222 ovexd ⊢ ( 𝑥 ∈ ( 1 ... 𝑘 ) → ( ( 2 · 𝑥 ) − 1 ) ∈ V )
223 217 220 221 222 fvmptd ⊢ ( 𝑥 ∈ ( 1 ... 𝑘 ) → ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑥 ) = ( ( 2 · 𝑥 ) − 1 ) )
224 223 eqcomd ⊢ ( 𝑥 ∈ ( 1 ... 𝑘 ) → ( ( 2 · 𝑥 ) − 1 ) = ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑥 ) )
225 224 ad2antrr ⊢ ( ( ( 𝑥 ∈ ( 1 ... 𝑘 ) ∧ 𝑦 ∈ ( 1 ... 𝑘 ) ) ∧ ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑥 ) = ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑦 ) ) → ( ( 2 · 𝑥 ) − 1 ) = ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑥 ) )
226 simpr ⊢ ( ( ( 𝑥 ∈ ( 1 ... 𝑘 ) ∧ 𝑦 ∈ ( 1 ... 𝑘 ) ) ∧ ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑥 ) = ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑦 ) ) → ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑥 ) = ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑦 ) )
227 eqidd ⊢ ( 𝑦 ∈ ( 1 ... 𝑘 ) → ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) = ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) )
228 oveq2 ⊢ ( 𝑖 = 𝑦 → ( 2 · 𝑖 ) = ( 2 · 𝑦 ) )
229 228 oveq1d ⊢ ( 𝑖 = 𝑦 → ( ( 2 · 𝑖 ) − 1 ) = ( ( 2 · 𝑦 ) − 1 ) )
230 229 adantl ⊢ ( ( 𝑦 ∈ ( 1 ... 𝑘 ) ∧ 𝑖 = 𝑦 ) → ( ( 2 · 𝑖 ) − 1 ) = ( ( 2 · 𝑦 ) − 1 ) )
231 id ⊢ ( 𝑦 ∈ ( 1 ... 𝑘 ) → 𝑦 ∈ ( 1 ... 𝑘 ) )
232 ovexd ⊢ ( 𝑦 ∈ ( 1 ... 𝑘 ) → ( ( 2 · 𝑦 ) − 1 ) ∈ V )
233 227 230 231 232 fvmptd ⊢ ( 𝑦 ∈ ( 1 ... 𝑘 ) → ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑦 ) = ( ( 2 · 𝑦 ) − 1 ) )
234 233 ad2antlr ⊢ ( ( ( 𝑥 ∈ ( 1 ... 𝑘 ) ∧ 𝑦 ∈ ( 1 ... 𝑘 ) ) ∧ ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑥 ) = ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑦 ) ) → ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑦 ) = ( ( 2 · 𝑦 ) − 1 ) )
235 225 226 234 3eqtrd ⊢ ( ( ( 𝑥 ∈ ( 1 ... 𝑘 ) ∧ 𝑦 ∈ ( 1 ... 𝑘 ) ) ∧ ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑥 ) = ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑦 ) ) → ( ( 2 · 𝑥 ) − 1 ) = ( ( 2 · 𝑦 ) − 1 ) )
236 2cnd ⊢ ( 𝑥 ∈ ( 1 ... 𝑘 ) → 2 ∈ ℂ )
237 elfzelz ⊢ ( 𝑥 ∈ ( 1 ... 𝑘 ) → 𝑥 ∈ ℤ )
238 237 zcnd ⊢ ( 𝑥 ∈ ( 1 ... 𝑘 ) → 𝑥 ∈ ℂ )
239 236 238 mulcld ⊢ ( 𝑥 ∈ ( 1 ... 𝑘 ) → ( 2 · 𝑥 ) ∈ ℂ )
240 239 ad2antrr ⊢ ( ( ( 𝑥 ∈ ( 1 ... 𝑘 ) ∧ 𝑦 ∈ ( 1 ... 𝑘 ) ) ∧ ( ( 2 · 𝑥 ) − 1 ) = ( ( 2 · 𝑦 ) − 1 ) ) → ( 2 · 𝑥 ) ∈ ℂ )
241 2cnd ⊢ ( 𝑦 ∈ ( 1 ... 𝑘 ) → 2 ∈ ℂ )
242 elfzelz ⊢ ( 𝑦 ∈ ( 1 ... 𝑘 ) → 𝑦 ∈ ℤ )
243 242 zcnd ⊢ ( 𝑦 ∈ ( 1 ... 𝑘 ) → 𝑦 ∈ ℂ )
244 241 243 mulcld ⊢ ( 𝑦 ∈ ( 1 ... 𝑘 ) → ( 2 · 𝑦 ) ∈ ℂ )
245 244 ad2antlr ⊢ ( ( ( 𝑥 ∈ ( 1 ... 𝑘 ) ∧ 𝑦 ∈ ( 1 ... 𝑘 ) ) ∧ ( ( 2 · 𝑥 ) − 1 ) = ( ( 2 · 𝑦 ) − 1 ) ) → ( 2 · 𝑦 ) ∈ ℂ )
246 1cnd ⊢ ( ( ( 𝑥 ∈ ( 1 ... 𝑘 ) ∧ 𝑦 ∈ ( 1 ... 𝑘 ) ) ∧ ( ( 2 · 𝑥 ) − 1 ) = ( ( 2 · 𝑦 ) − 1 ) ) → 1 ∈ ℂ )
247 simpr ⊢ ( ( ( 𝑥 ∈ ( 1 ... 𝑘 ) ∧ 𝑦 ∈ ( 1 ... 𝑘 ) ) ∧ ( ( 2 · 𝑥 ) − 1 ) = ( ( 2 · 𝑦 ) − 1 ) ) → ( ( 2 · 𝑥 ) − 1 ) = ( ( 2 · 𝑦 ) − 1 ) )
248 240 245 246 247 subcan2d ⊢ ( ( ( 𝑥 ∈ ( 1 ... 𝑘 ) ∧ 𝑦 ∈ ( 1 ... 𝑘 ) ) ∧ ( ( 2 · 𝑥 ) − 1 ) = ( ( 2 · 𝑦 ) − 1 ) ) → ( 2 · 𝑥 ) = ( 2 · 𝑦 ) )
249 238 ad2antrr ⊢ ( ( ( 𝑥 ∈ ( 1 ... 𝑘 ) ∧ 𝑦 ∈ ( 1 ... 𝑘 ) ) ∧ ( 2 · 𝑥 ) = ( 2 · 𝑦 ) ) → 𝑥 ∈ ℂ )
250 243 ad2antlr ⊢ ( ( ( 𝑥 ∈ ( 1 ... 𝑘 ) ∧ 𝑦 ∈ ( 1 ... 𝑘 ) ) ∧ ( 2 · 𝑥 ) = ( 2 · 𝑦 ) ) → 𝑦 ∈ ℂ )
251 2cnd ⊢ ( ( ( 𝑥 ∈ ( 1 ... 𝑘 ) ∧ 𝑦 ∈ ( 1 ... 𝑘 ) ) ∧ ( 2 · 𝑥 ) = ( 2 · 𝑦 ) ) → 2 ∈ ℂ )
252 186 a1i ⊢ ( ( ( 𝑥 ∈ ( 1 ... 𝑘 ) ∧ 𝑦 ∈ ( 1 ... 𝑘 ) ) ∧ ( 2 · 𝑥 ) = ( 2 · 𝑦 ) ) → 2 ≠ 0 )
253 simpr ⊢ ( ( ( 𝑥 ∈ ( 1 ... 𝑘 ) ∧ 𝑦 ∈ ( 1 ... 𝑘 ) ) ∧ ( 2 · 𝑥 ) = ( 2 · 𝑦 ) ) → ( 2 · 𝑥 ) = ( 2 · 𝑦 ) )
254 249 250 251 252 253 mulcanad ⊢ ( ( ( 𝑥 ∈ ( 1 ... 𝑘 ) ∧ 𝑦 ∈ ( 1 ... 𝑘 ) ) ∧ ( 2 · 𝑥 ) = ( 2 · 𝑦 ) ) → 𝑥 = 𝑦 )
255 248 254 syldan ⊢ ( ( ( 𝑥 ∈ ( 1 ... 𝑘 ) ∧ 𝑦 ∈ ( 1 ... 𝑘 ) ) ∧ ( ( 2 · 𝑥 ) − 1 ) = ( ( 2 · 𝑦 ) − 1 ) ) → 𝑥 = 𝑦 )
256 235 255 syldan ⊢ ( ( ( 𝑥 ∈ ( 1 ... 𝑘 ) ∧ 𝑦 ∈ ( 1 ... 𝑘 ) ) ∧ ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑥 ) = ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑦 ) ) → 𝑥 = 𝑦 )
257 256 adantll ⊢ ( ( ( 𝑘 ∈ ℕ ∧ ( 𝑥 ∈ ( 1 ... 𝑘 ) ∧ 𝑦 ∈ ( 1 ... 𝑘 ) ) ) ∧ ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑥 ) = ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑦 ) ) → 𝑥 = 𝑦 )
258 257 ex ⊢ ( ( 𝑘 ∈ ℕ ∧ ( 𝑥 ∈ ( 1 ... 𝑘 ) ∧ 𝑦 ∈ ( 1 ... 𝑘 ) ) ) → ( ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑥 ) = ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
259 258 ralrimivva ⊢ ( 𝑘 ∈ ℕ → ∀ 𝑥 ∈ ( 1 ... 𝑘 ) ∀ 𝑦 ∈ ( 1 ... 𝑘 ) ( ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑥 ) = ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
260 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 ) ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
261 216 259 260 sylanbrc ⊢ ( 𝑘 ∈ ℕ → ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) : ( 1 ... 𝑘 ) –1-1→ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) )
262 1zzd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) → 1 ∈ ℤ )
263 33 adantr ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) → 𝑘 ∈ ℤ )
264 fzssz ⊢ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ⊆ ℤ
265 264 134 sseldi ⊢ ( 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) → 𝑗 ∈ ℤ )
266 zeo ⊢ ( 𝑗 ∈ ℤ → ( ( 𝑗 / 2 ) ∈ ℤ ∨ ( ( 𝑗 + 1 ) / 2 ) ∈ ℤ ) )
267 265 266 syl ⊢ ( 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) → ( ( 𝑗 / 2 ) ∈ ℤ ∨ ( ( 𝑗 + 1 ) / 2 ) ∈ ℤ ) )
268 267 adantl ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) → ( ( 𝑗 / 2 ) ∈ ℤ ∨ ( ( 𝑗 + 1 ) / 2 ) ∈ ℤ ) )
269 eldifn ⊢ ( 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) → ¬ 𝑗 ∈ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } )
270 134 92 syl ⊢ ( 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) → 𝑗 ∈ ℕ )
271 270 adantr ⊢ ( ( 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∧ ( 𝑗 / 2 ) ∈ ℤ ) → 𝑗 ∈ ℕ )
272 simpr ⊢ ( ( 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∧ ( 𝑗 / 2 ) ∈ ℤ ) → ( 𝑗 / 2 ) ∈ ℤ )
273 271 nnred ⊢ ( ( 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∧ ( 𝑗 / 2 ) ∈ ℤ ) → 𝑗 ∈ ℝ )
274 39 a1i ⊢ ( ( 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∧ ( 𝑗 / 2 ) ∈ ℤ ) → 2 ∈ ℝ )
275 271 nngt0d ⊢ ( ( 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∧ ( 𝑗 / 2 ) ∈ ℤ ) → 0 < 𝑗 )
276 2pos ⊢ 0 < 2
277 276 a1i ⊢ ( ( 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∧ ( 𝑗 / 2 ) ∈ ℤ ) → 0 < 2 )
278 273 274 275 277 divgt0d ⊢ ( ( 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∧ ( 𝑗 / 2 ) ∈ ℤ ) → 0 < ( 𝑗 / 2 ) )
279 elnnz ⊢ ( ( 𝑗 / 2 ) ∈ ℕ ↔ ( ( 𝑗 / 2 ) ∈ ℤ ∧ 0 < ( 𝑗 / 2 ) ) )
280 272 278 279 sylanbrc ⊢ ( ( 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∧ ( 𝑗 / 2 ) ∈ ℤ ) → ( 𝑗 / 2 ) ∈ ℕ )
281 oveq1 ⊢ ( 𝑛 = 𝑗 → ( 𝑛 / 2 ) = ( 𝑗 / 2 ) )
282 281 eleq1d ⊢ ( 𝑛 = 𝑗 → ( ( 𝑛 / 2 ) ∈ ℕ ↔ ( 𝑗 / 2 ) ∈ ℕ ) )
283 282 elrab ⊢ ( 𝑗 ∈ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ↔ ( 𝑗 ∈ ℕ ∧ ( 𝑗 / 2 ) ∈ ℕ ) )
284 271 280 283 sylanbrc ⊢ ( ( 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∧ ( 𝑗 / 2 ) ∈ ℤ ) → 𝑗 ∈ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } )
285 269 284 mtand ⊢ ( 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) → ¬ ( 𝑗 / 2 ) ∈ ℤ )
286 285 adantl ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) → ¬ ( 𝑗 / 2 ) ∈ ℤ )
287 pm2.53 ⊢ ( ( ( 𝑗 / 2 ) ∈ ℤ ∨ ( ( 𝑗 + 1 ) / 2 ) ∈ ℤ ) → ( ¬ ( 𝑗 / 2 ) ∈ ℤ → ( ( 𝑗 + 1 ) / 2 ) ∈ ℤ ) )
288 268 286 287 sylc ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) → ( ( 𝑗 + 1 ) / 2 ) ∈ ℤ )
289 262 263 288 3jca ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) → ( 1 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ ( ( 𝑗 + 1 ) / 2 ) ∈ ℤ ) )
290 1p1e2 ⊢ ( 1 + 1 ) = 2
291 290 oveq1i ⊢ ( ( 1 + 1 ) / 2 ) = ( 2 / 2 )
292 2div2e1 ⊢ ( 2 / 2 ) = 1
293 291 292 eqtr2i ⊢ 1 = ( ( 1 + 1 ) / 2 )
294 1red ⊢ ( 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) → 1 ∈ ℝ )
295 294 294 readdcld ⊢ ( 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) → ( 1 + 1 ) ∈ ℝ )
296 92 nnred ⊢ ( 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) → 𝑗 ∈ ℝ )
297 296 294 readdcld ⊢ ( 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) → ( 𝑗 + 1 ) ∈ ℝ )
298 198 a1i ⊢ ( 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) → 2 ∈ ℝ+ )
299 elfzle1 ⊢ ( 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) → 1 ≤ 𝑗 )
300 294 296 294 299 leadd1dd ⊢ ( 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) → ( 1 + 1 ) ≤ ( 𝑗 + 1 ) )
301 295 297 298 300 lediv1dd ⊢ ( 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) → ( ( 1 + 1 ) / 2 ) ≤ ( ( 𝑗 + 1 ) / 2 ) )
302 293 301 eqbrtrid ⊢ ( 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) → 1 ≤ ( ( 𝑗 + 1 ) / 2 ) )
303 134 302 syl ⊢ ( 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) → 1 ≤ ( ( 𝑗 + 1 ) / 2 ) )
304 303 adantl ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) → 1 ≤ ( ( 𝑗 + 1 ) / 2 ) )
305 elfzel2 ⊢ ( 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) → ( ( 2 · 𝑘 ) − 1 ) ∈ ℤ )
306 305 zred ⊢ ( 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) → ( ( 2 · 𝑘 ) − 1 ) ∈ ℝ )
307 306 294 readdcld ⊢ ( 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) → ( ( ( 2 · 𝑘 ) − 1 ) + 1 ) ∈ ℝ )
308 elfzle2 ⊢ ( 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) → 𝑗 ≤ ( ( 2 · 𝑘 ) − 1 ) )
309 296 306 294 308 leadd1dd ⊢ ( 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) → ( 𝑗 + 1 ) ≤ ( ( ( 2 · 𝑘 ) − 1 ) + 1 ) )
310 297 307 298 309 lediv1dd ⊢ ( 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) → ( ( 𝑗 + 1 ) / 2 ) ≤ ( ( ( ( 2 · 𝑘 ) − 1 ) + 1 ) / 2 ) )
311 310 adantl ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ) → ( ( 𝑗 + 1 ) / 2 ) ≤ ( ( ( ( 2 · 𝑘 ) − 1 ) + 1 ) / 2 ) )
312 51 adantr ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ) → ( 2 · 𝑘 ) ∈ ℂ )
313 1cnd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ) → 1 ∈ ℂ )
314 312 313 npcand ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ) → ( ( ( 2 · 𝑘 ) − 1 ) + 1 ) = ( 2 · 𝑘 ) )
315 314 oveq1d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ) → ( ( ( ( 2 · 𝑘 ) − 1 ) + 1 ) / 2 ) = ( ( 2 · 𝑘 ) / 2 ) )
316 186 a1i ⊢ ( 𝑘 ∈ ℕ → 2 ≠ 0 )
317 45 44 316 divcan3d ⊢ ( 𝑘 ∈ ℕ → ( ( 2 · 𝑘 ) / 2 ) = 𝑘 )
318 317 adantr ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ) → ( ( 2 · 𝑘 ) / 2 ) = 𝑘 )
319 315 318 eqtrd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ) → ( ( ( ( 2 · 𝑘 ) − 1 ) + 1 ) / 2 ) = 𝑘 )
320 311 319 breqtrd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ) → ( ( 𝑗 + 1 ) / 2 ) ≤ 𝑘 )
321 134 320 sylan2 ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) → ( ( 𝑗 + 1 ) / 2 ) ≤ 𝑘 )
322 289 304 321 jca32 ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) → ( ( 1 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ ( ( 𝑗 + 1 ) / 2 ) ∈ ℤ ) ∧ ( 1 ≤ ( ( 𝑗 + 1 ) / 2 ) ∧ ( ( 𝑗 + 1 ) / 2 ) ≤ 𝑘 ) ) )
323 elfz2 ⊢ ( ( ( 𝑗 + 1 ) / 2 ) ∈ ( 1 ... 𝑘 ) ↔ ( ( 1 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ ( ( 𝑗 + 1 ) / 2 ) ∈ ℤ ) ∧ ( 1 ≤ ( ( 𝑗 + 1 ) / 2 ) ∧ ( ( 𝑗 + 1 ) / 2 ) ≤ 𝑘 ) ) )
324 322 323 sylibr ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) → ( ( 𝑗 + 1 ) / 2 ) ∈ ( 1 ... 𝑘 ) )
325 270 nncnd ⊢ ( 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) → 𝑗 ∈ ℂ )
326 peano2cn ⊢ ( 𝑗 ∈ ℂ → ( 𝑗 + 1 ) ∈ ℂ )
327 2cnd ⊢ ( 𝑗 ∈ ℂ → 2 ∈ ℂ )
328 186 a1i ⊢ ( 𝑗 ∈ ℂ → 2 ≠ 0 )
329 326 327 328 divcan2d ⊢ ( 𝑗 ∈ ℂ → ( 2 · ( ( 𝑗 + 1 ) / 2 ) ) = ( 𝑗 + 1 ) )
330 329 oveq1d ⊢ ( 𝑗 ∈ ℂ → ( ( 2 · ( ( 𝑗 + 1 ) / 2 ) ) − 1 ) = ( ( 𝑗 + 1 ) − 1 ) )
331 pncan1 ⊢ ( 𝑗 ∈ ℂ → ( ( 𝑗 + 1 ) − 1 ) = 𝑗 )
332 330 331 eqtr2d ⊢ ( 𝑗 ∈ ℂ → 𝑗 = ( ( 2 · ( ( 𝑗 + 1 ) / 2 ) ) − 1 ) )
333 325 332 syl ⊢ ( 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) → 𝑗 = ( ( 2 · ( ( 𝑗 + 1 ) / 2 ) ) − 1 ) )
334 333 adantl ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) → 𝑗 = ( ( 2 · ( ( 𝑗 + 1 ) / 2 ) ) − 1 ) )
335 oveq2 ⊢ ( 𝑚 = ( ( 𝑗 + 1 ) / 2 ) → ( 2 · 𝑚 ) = ( 2 · ( ( 𝑗 + 1 ) / 2 ) ) )
336 335 oveq1d ⊢ ( 𝑚 = ( ( 𝑗 + 1 ) / 2 ) → ( ( 2 · 𝑚 ) − 1 ) = ( ( 2 · ( ( 𝑗 + 1 ) / 2 ) ) − 1 ) )
337 336 rspceeqv ⊢ ( ( ( ( 𝑗 + 1 ) / 2 ) ∈ ( 1 ... 𝑘 ) ∧ 𝑗 = ( ( 2 · ( ( 𝑗 + 1 ) / 2 ) ) − 1 ) ) → ∃ 𝑚 ∈ ( 1 ... 𝑘 ) 𝑗 = ( ( 2 · 𝑚 ) − 1 ) )
338 324 334 337 syl2anc ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) → ∃ 𝑚 ∈ ( 1 ... 𝑘 ) 𝑗 = ( ( 2 · 𝑚 ) − 1 ) )
339 eqidd ⊢ ( ( 𝑚 ∈ ( 1 ... 𝑘 ) ∧ 𝑗 = ( ( 2 · 𝑚 ) − 1 ) ) → ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) = ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) )
340 oveq2 ⊢ ( 𝑖 = 𝑚 → ( 2 · 𝑖 ) = ( 2 · 𝑚 ) )
341 340 oveq1d ⊢ ( 𝑖 = 𝑚 → ( ( 2 · 𝑖 ) − 1 ) = ( ( 2 · 𝑚 ) − 1 ) )
342 341 adantl ⊢ ( ( ( 𝑚 ∈ ( 1 ... 𝑘 ) ∧ 𝑗 = ( ( 2 · 𝑚 ) − 1 ) ) ∧ 𝑖 = 𝑚 ) → ( ( 2 · 𝑖 ) − 1 ) = ( ( 2 · 𝑚 ) − 1 ) )
343 simpl ⊢ ( ( 𝑚 ∈ ( 1 ... 𝑘 ) ∧ 𝑗 = ( ( 2 · 𝑚 ) − 1 ) ) → 𝑚 ∈ ( 1 ... 𝑘 ) )
344 ovexd ⊢ ( ( 𝑚 ∈ ( 1 ... 𝑘 ) ∧ 𝑗 = ( ( 2 · 𝑚 ) − 1 ) ) → ( ( 2 · 𝑚 ) − 1 ) ∈ V )
345 339 342 343 344 fvmptd ⊢ ( ( 𝑚 ∈ ( 1 ... 𝑘 ) ∧ 𝑗 = ( ( 2 · 𝑚 ) − 1 ) ) → ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑚 ) = ( ( 2 · 𝑚 ) − 1 ) )
346 id ⊢ ( 𝑗 = ( ( 2 · 𝑚 ) − 1 ) → 𝑗 = ( ( 2 · 𝑚 ) − 1 ) )
347 346 eqcomd ⊢ ( 𝑗 = ( ( 2 · 𝑚 ) − 1 ) → ( ( 2 · 𝑚 ) − 1 ) = 𝑗 )
348 347 adantl ⊢ ( ( 𝑚 ∈ ( 1 ... 𝑘 ) ∧ 𝑗 = ( ( 2 · 𝑚 ) − 1 ) ) → ( ( 2 · 𝑚 ) − 1 ) = 𝑗 )
349 345 348 eqtr2d ⊢ ( ( 𝑚 ∈ ( 1 ... 𝑘 ) ∧ 𝑗 = ( ( 2 · 𝑚 ) − 1 ) ) → 𝑗 = ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑚 ) )
350 349 ex ⊢ ( 𝑚 ∈ ( 1 ... 𝑘 ) → ( 𝑗 = ( ( 2 · 𝑚 ) − 1 ) → 𝑗 = ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑚 ) ) )
351 350 adantl ⊢ ( ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) ∧ 𝑚 ∈ ( 1 ... 𝑘 ) ) → ( 𝑗 = ( ( 2 · 𝑚 ) − 1 ) → 𝑗 = ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑚 ) ) )
352 351 reximdva ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) → ( ∃ 𝑚 ∈ ( 1 ... 𝑘 ) 𝑗 = ( ( 2 · 𝑚 ) − 1 ) → ∃ 𝑚 ∈ ( 1 ... 𝑘 ) 𝑗 = ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑚 ) ) )
353 338 352 mpd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) → ∃ 𝑚 ∈ ( 1 ... 𝑘 ) 𝑗 = ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑚 ) )
354 353 ralrimiva ⊢ ( 𝑘 ∈ ℕ → ∀ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ∃ 𝑚 ∈ ( 1 ... 𝑘 ) 𝑗 = ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑚 ) )
355 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 ) ) ‘ 𝑚 ) ) )
356 216 354 355 sylanbrc ⊢ ( 𝑘 ∈ ℕ → ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) : ( 1 ... 𝑘 ) –onto→ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) )
357 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 ) ∈ ℕ } ) ) )
358 261 356 357 sylanbrc ⊢ ( 𝑘 ∈ ℕ → ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) : ( 1 ... 𝑘 ) –1-1-onto→ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) )
359 358 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) : ( 1 ... 𝑘 ) –1-1-onto→ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) )
360 eqidd ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) = ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) )
361 oveq2 ⊢ ( 𝑖 = 𝑗 → ( 2 · 𝑖 ) = ( 2 · 𝑗 ) )
362 361 oveq1d ⊢ ( 𝑖 = 𝑗 → ( ( 2 · 𝑖 ) − 1 ) = ( ( 2 · 𝑗 ) − 1 ) )
363 362 adantl ⊢ ( ( 𝑗 ∈ ( 1 ... 𝑘 ) ∧ 𝑖 = 𝑗 ) → ( ( 2 · 𝑖 ) − 1 ) = ( ( 2 · 𝑗 ) − 1 ) )
364 id ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → 𝑗 ∈ ( 1 ... 𝑘 ) )
365 ovexd ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → ( ( 2 · 𝑗 ) − 1 ) ∈ V )
366 360 363 364 365 fvmptd ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑗 ) = ( ( 2 · 𝑗 ) − 1 ) )
367 366 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → ( ( 𝑖 ∈ ( 1 ... 𝑘 ) ↦ ( ( 2 · 𝑖 ) − 1 ) ) ‘ 𝑗 ) = ( ( 2 · 𝑗 ) − 1 ) )
368 eleq1w ⊢ ( 𝑗 = 𝑖 → ( 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ↔ 𝑖 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) )
369 368 anbi2d ⊢ ( 𝑗 = 𝑖 → ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) ↔ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) ) )
370 139 eleq1d ⊢ ( 𝑗 = 𝑖 → ( ( 𝐹 ‘ 𝑗 ) ∈ ℂ ↔ ( 𝐹 ‘ 𝑖 ) ∈ ℂ ) )
371 369 370 imbi12d ⊢ ( 𝑗 = 𝑖 → ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℂ ) ↔ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) → ( 𝐹 ‘ 𝑖 ) ∈ ℂ ) ) )
372 371 136 chvarvv ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ) → ( 𝐹 ‘ 𝑖 ) ∈ ℂ )
373 143 144 359 367 372 fsumf1o ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → Σ 𝑖 ∈ ( ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ∖ { 𝑛 ∈ ℕ ∣ ( 𝑛 / 2 ) ∈ ℕ } ) ( 𝐹 ‘ 𝑖 ) = Σ 𝑗 ∈ ( 1 ... 𝑘 ) ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) )
374 96 142 373 3eqtrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → Σ 𝑗 ∈ ( 1 ... 𝑘 ) ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) = Σ 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) )
375 ovex ⊢ ( ( 2 · 𝑘 ) − 1 ) ∈ V
376 21 fvmpt2 ⊢ ( ( 𝑘 ∈ ℕ ∧ ( ( 2 · 𝑘 ) − 1 ) ∈ V ) → ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) = ( ( 2 · 𝑘 ) − 1 ) )
377 375 376 mpan2 ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) = ( ( 2 · 𝑘 ) − 1 ) )
378 377 oveq2d ⊢ ( 𝑘 ∈ ℕ → ( 1 ... ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) ) = ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) )
379 378 eqcomd ⊢ ( 𝑘 ∈ ℕ → ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) = ( 1 ... ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) ) )
380 379 sumeq1d ⊢ ( 𝑘 ∈ ℕ → Σ 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) = Σ 𝑗 ∈ ( 1 ... ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) ) ( 𝐹 ‘ 𝑗 ) )
381 380 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → Σ 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) = Σ 𝑗 ∈ ( 1 ... ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) ) ( 𝐹 ‘ 𝑗 ) )
382 374 381 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → Σ 𝑗 ∈ ( 1 ... 𝑘 ) ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) = Σ 𝑗 ∈ ( 1 ... ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) ) ( 𝐹 ‘ 𝑗 ) )
383 elfznn ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → 𝑗 ∈ ℕ )
384 383 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → 𝑗 ∈ ℕ )
385 1 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → 𝐹 : ℕ ⟶ ℂ )
386 31 a1i ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → 2 ∈ ℤ )
387 elfzelz ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → 𝑗 ∈ ℤ )
388 386 387 zmulcld ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → ( 2 · 𝑗 ) ∈ ℤ )
389 1zzd ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → 1 ∈ ℤ )
390 388 389 zsubcld ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → ( ( 2 · 𝑗 ) − 1 ) ∈ ℤ )
391 0red ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → 0 ∈ ℝ )
392 39 a1i ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → 2 ∈ ℝ )
393 25 392 eqeltrid ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → ( 2 · 1 ) ∈ ℝ )
394 1red ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → 1 ∈ ℝ )
395 393 394 resubcld ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → ( ( 2 · 1 ) − 1 ) ∈ ℝ )
396 390 zred ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → ( ( 2 · 𝑗 ) − 1 ) ∈ ℝ )
397 0lt1 ⊢ 0 < 1
398 154 a1i ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → 1 = ( ( 2 · 1 ) − 1 ) )
399 397 398 breqtrid ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → 0 < ( ( 2 · 1 ) − 1 ) )
400 388 zred ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → ( 2 · 𝑗 ) ∈ ℝ )
401 383 nnred ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → 𝑗 ∈ ℝ )
402 162 a1i ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → 0 ≤ 2 )
403 elfzle1 ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → 1 ≤ 𝑗 )
404 394 401 392 402 403 lemul2ad ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → ( 2 · 1 ) ≤ ( 2 · 𝑗 ) )
405 393 400 394 404 lesub1dd ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → ( ( 2 · 1 ) − 1 ) ≤ ( ( 2 · 𝑗 ) − 1 ) )
406 391 395 396 399 405 ltletrd ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → 0 < ( ( 2 · 𝑗 ) − 1 ) )
407 elnnz ⊢ ( ( ( 2 · 𝑗 ) − 1 ) ∈ ℕ ↔ ( ( ( 2 · 𝑗 ) − 1 ) ∈ ℤ ∧ 0 < ( ( 2 · 𝑗 ) − 1 ) ) )
408 390 406 407 sylanbrc ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → ( ( 2 · 𝑗 ) − 1 ) ∈ ℕ )
409 408 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → ( ( 2 · 𝑗 ) − 1 ) ∈ ℕ )
410 385 409 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) ∈ ℂ )
411 410 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) ∈ ℂ )
412 60 fveq2d ⊢ ( 𝑘 = 𝑗 → ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) = ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) )
413 412 cbvmptv ⊢ ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) = ( 𝑗 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) )
414 413 fvmpt2 ⊢ ( ( 𝑗 ∈ ℕ ∧ ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) ∈ ℂ ) → ( ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ‘ 𝑗 ) = ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) )
415 384 411 414 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → ( ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ‘ 𝑗 ) = ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) )
416 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ )
417 416 11 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ( ℤ≥ ‘ 1 ) )
418 415 417 411 fsumser ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → Σ 𝑗 ∈ ( 1 ... 𝑘 ) ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) = ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ) ‘ 𝑘 ) )
419 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) ) ) → ( 𝐹 ‘ 𝑗 ) = ( 𝐹 ‘ 𝑗 ) )
420 156 a1i ⊢ ( 𝑘 ∈ ℕ → ( 2 · 1 ) ∈ ℝ )
421 1red ⊢ ( 𝑘 ∈ ℕ → 1 ∈ ℝ )
422 162 a1i ⊢ ( 𝑘 ∈ ℕ → 0 ≤ 2 )
423 nnge1 ⊢ ( 𝑘 ∈ ℕ → 1 ≤ 𝑘 )
424 421 41 40 422 423 lemul2ad ⊢ ( 𝑘 ∈ ℕ → ( 2 · 1 ) ≤ ( 2 · 𝑘 ) )
425 420 42 421 424 lesub1dd ⊢ ( 𝑘 ∈ ℕ → ( ( 2 · 1 ) − 1 ) ≤ ( ( 2 · 𝑘 ) − 1 ) )
426 154 425 eqbrtrid ⊢ ( 𝑘 ∈ ℕ → 1 ≤ ( ( 2 · 𝑘 ) − 1 ) )
427 eluz2 ⊢ ( ( ( 2 · 𝑘 ) − 1 ) ∈ ( ℤ≥ ‘ 1 ) ↔ ( 1 ∈ ℤ ∧ ( ( 2 · 𝑘 ) − 1 ) ∈ ℤ ∧ 1 ≤ ( ( 2 · 𝑘 ) − 1 ) ) )
428 37 66 426 427 syl3anbrc ⊢ ( 𝑘 ∈ ℕ → ( ( 2 · 𝑘 ) − 1 ) ∈ ( ℤ≥ ‘ 1 ) )
429 68 428 eqeltrd ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 1 ) )
430 429 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 1 ) )
431 simpll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) ) ) → 𝜑 )
432 simpr ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( 1 ... ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) ) ) → 𝑗 ∈ ( 1 ... ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) ) )
433 378 adantr ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( 1 ... ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) ) ) → ( 1 ... ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) ) = ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) )
434 432 433 eleqtrd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑗 ∈ ( 1 ... ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) ) ) → 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) )
435 434 adantll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) ) ) → 𝑗 ∈ ( 1 ... ( ( 2 · 𝑘 ) − 1 ) ) )
436 431 435 94 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℂ )
437 419 430 436 fsumser ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → Σ 𝑗 ∈ ( 1 ... ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) ) ( 𝐹 ‘ 𝑗 ) = ( seq 1 ( + , 𝐹 ) ‘ ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) ) )
438 382 418 437 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ) ‘ 𝑘 ) = ( seq 1 ( + , 𝐹 ) ‘ ( ( 𝑘 ∈ ℕ ↦ ( ( 2 · 𝑘 ) − 1 ) ) ‘ 𝑘 ) ) )
439 4 5 9 10 11 12 14 17 3 30 74 76 438 climsuse ⊢ ( 𝜑 → seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ) ⇝ 𝐵 )
440 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
441 11 12 440 15 isum ⊢ ( 𝜑 → Σ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) = ( ⇝ ‘ seq 1 ( + , 𝐹 ) ) )
442 climrel ⊢ Rel ⇝
443 442 releldmi ⊢ ( seq 1 ( + , 𝐹 ) ⇝ 𝐵 → seq 1 ( + , 𝐹 ) ∈ dom ⇝ )
444 3 443 syl ⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) ∈ dom ⇝ )
445 climdm ⊢ ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ↔ seq 1 ( + , 𝐹 ) ⇝ ( ⇝ ‘ seq 1 ( + , 𝐹 ) ) )
446 444 445 sylib ⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) ⇝ ( ⇝ ‘ seq 1 ( + , 𝐹 ) ) )
447 climuni ⊢ ( ( seq 1 ( + , 𝐹 ) ⇝ ( ⇝ ‘ seq 1 ( + , 𝐹 ) ) ∧ seq 1 ( + , 𝐹 ) ⇝ 𝐵 ) → ( ⇝ ‘ seq 1 ( + , 𝐹 ) ) = 𝐵 )
448 446 3 447 syl2anc ⊢ ( 𝜑 → ( ⇝ ‘ seq 1 ( + , 𝐹 ) ) = 𝐵 )
449 442 a1i ⊢ ( 𝜑 → Rel ⇝ )
450 releldm ⊢ ( ( Rel ⇝ ∧ seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ) ⇝ 𝐵 ) → seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ) ∈ dom ⇝ )
451 449 439 450 syl2anc ⊢ ( 𝜑 → seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ) ∈ dom ⇝ )
452 climdm ⊢ ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ) ∈ dom ⇝ ↔ seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ) ⇝ ( ⇝ ‘ seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ) ) )
453 451 452 sylib ⊢ ( 𝜑 → seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ) ⇝ ( ⇝ ‘ seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ) ) )
454 413 a1i ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) = ( 𝑗 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) ) )
455 454 seqeq3d ⊢ ( 𝜑 → seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ) = seq 1 ( + , ( 𝑗 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) ) ) )
456 455 fveq2d ⊢ ( 𝜑 → ( ⇝ ‘ seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ) ) = ( ⇝ ‘ seq 1 ( + , ( 𝑗 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) ) ) ) )
457 453 456 breqtrd ⊢ ( 𝜑 → seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ) ⇝ ( ⇝ ‘ seq 1 ( + , ( 𝑗 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) ) ) ) )
458 climuni ⊢ ( ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ) ⇝ 𝐵 ∧ seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ) ⇝ ( ⇝ ‘ seq 1 ( + , ( 𝑗 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) ) ) ) ) → 𝐵 = ( ⇝ ‘ seq 1 ( + , ( 𝑗 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) ) ) ) )
459 439 457 458 syl2anc ⊢ ( 𝜑 → 𝐵 = ( ⇝ ‘ seq 1 ( + , ( 𝑗 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) ) ) ) )
460 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑗 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) ) = ( 𝑗 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) ) )
461 eqcom ⊢ ( 𝑘 = 𝑗 ↔ 𝑗 = 𝑘 )
462 eqcom ⊢ ( ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) = ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) ↔ ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) = ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) )
463 412 461 462 3imtr3i ⊢ ( 𝑗 = 𝑘 → ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) = ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) )
464 463 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 = 𝑘 ) → ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) = ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) )
465 1 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐹 : ℕ ⟶ ℂ )
466 428 11 eleqtrrdi ⊢ ( 𝑘 ∈ ℕ → ( ( 2 · 𝑘 ) − 1 ) ∈ ℕ )
467 466 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 2 · 𝑘 ) − 1 ) ∈ ℕ )
468 465 467 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ∈ ℂ )
469 460 464 416 468 fvmptd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑗 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) ) ‘ 𝑘 ) = ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) )
470 11 12 469 468 isum ⊢ ( 𝜑 → Σ 𝑘 ∈ ℕ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) = ( ⇝ ‘ seq 1 ( + , ( 𝑗 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑗 ) − 1 ) ) ) ) ) )
471 459 470 eqtr4d ⊢ ( 𝜑 → 𝐵 = Σ 𝑘 ∈ ℕ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) )
472 441 448 471 3eqtrd ⊢ ( 𝜑 → Σ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) = Σ 𝑘 ∈ ℕ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) )
473 439 472 jca ⊢ ( 𝜑 → ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ) ⇝ 𝐵 ∧ Σ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) = Σ 𝑘 ∈ ℕ ( 𝐹 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) )