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 ) ) ) ) |