Step | Hyp | Ref
| Expression |
1 | | nfv 1830 |
. . 3
⊢
Ⅎ𝑘𝜑 |
2 | | nfcv 2751 |
. . 3
⊢
Ⅎ𝑘seq1(
+ , 𝐹) |
3 | | nfcv 2751 |
. . . 4
⊢
Ⅎ𝑘1 |
4 | | nfcv 2751 |
. . . 4
⊢
Ⅎ𝑘
+ |
5 | | nfmpt1 4675 |
. . . 4
⊢
Ⅎ𝑘(𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))) |
6 | 3, 4, 5 | nfseq 12673 |
. . 3
⊢
Ⅎ𝑘seq1(
+ , (𝑘 ∈ ℕ
↦ (𝐹‘((2
· 𝑘) −
1)))) |
7 | | nfmpt1 4675 |
. . 3
⊢
Ⅎ𝑘(𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1)) |
8 | | nnuz 11599 |
. . 3
⊢ ℕ =
(ℤ≥‘1) |
9 | | 1zzd 11285 |
. . 3
⊢ (𝜑 → 1 ∈
ℤ) |
10 | | seqex 12665 |
. . . 4
⊢ seq1( + ,
𝐹) ∈
V |
11 | 10 | a1i 11 |
. . 3
⊢ (𝜑 → seq1( + , 𝐹) ∈ V) |
12 | | sumnnodd.1 |
. . . . . 6
⊢ (𝜑 → 𝐹:ℕ⟶ℂ) |
13 | 12 | ffvelrnda 6267 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ) |
14 | 8, 9, 13 | serf 12691 |
. . . 4
⊢ (𝜑 → seq1( + , 𝐹):ℕ⟶ℂ) |
15 | 14 | ffvelrnda 6267 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , 𝐹)‘𝑘) ∈ ℂ) |
16 | | sumnnodd.sc |
. . 3
⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝐵) |
17 | | 1nn 10908 |
. . . . . . 7
⊢ 1 ∈
ℕ |
18 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑘 = 1 → (2 · 𝑘) = (2 ·
1)) |
19 | 18 | oveq1d 6564 |
. . . . . . . 8
⊢ (𝑘 = 1 → ((2 · 𝑘) − 1) = ((2 · 1)
− 1)) |
20 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ ↦ ((2
· 𝑘) − 1)) =
(𝑘 ∈ ℕ ↦
((2 · 𝑘) −
1)) |
21 | | ovex 6577 |
. . . . . . . 8
⊢ ((2
· 1) − 1) ∈ V |
22 | 19, 20, 21 | fvmpt 6191 |
. . . . . . 7
⊢ (1 ∈
ℕ → ((𝑘 ∈
ℕ ↦ ((2 · 𝑘) − 1))‘1) = ((2 · 1)
− 1)) |
23 | 17, 22 | ax-mp 5 |
. . . . . 6
⊢ ((𝑘 ∈ ℕ ↦ ((2
· 𝑘) −
1))‘1) = ((2 · 1) − 1) |
24 | | 2t1e2 11053 |
. . . . . . 7
⊢ (2
· 1) = 2 |
25 | 24 | oveq1i 6559 |
. . . . . 6
⊢ ((2
· 1) − 1) = (2 − 1) |
26 | | 2m1e1 11012 |
. . . . . 6
⊢ (2
− 1) = 1 |
27 | 23, 25, 26 | 3eqtri 2636 |
. . . . 5
⊢ ((𝑘 ∈ ℕ ↦ ((2
· 𝑘) −
1))‘1) = 1 |
28 | 27, 17 | eqeltri 2684 |
. . . 4
⊢ ((𝑘 ∈ ℕ ↦ ((2
· 𝑘) −
1))‘1) ∈ ℕ |
29 | 28 | a1i 11 |
. . 3
⊢ (𝜑 → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘1) ∈
ℕ) |
30 | | 2z 11286 |
. . . . . . . 8
⊢ 2 ∈
ℤ |
31 | 30 | a1i 11 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → 2 ∈
ℤ) |
32 | | nnz 11276 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℤ) |
33 | 31, 32 | zmulcld 11364 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → (2
· 𝑘) ∈
ℤ) |
34 | 32 | peano2zd 11361 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈
ℤ) |
35 | 31, 34 | zmulcld 11364 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → (2
· (𝑘 + 1)) ∈
ℤ) |
36 | | 1zzd 11285 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → 1 ∈
ℤ) |
37 | 35, 36 | zsubcld 11363 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → ((2
· (𝑘 + 1)) −
1) ∈ ℤ) |
38 | | 2re 10967 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ |
39 | 38 | a1i 11 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → 2 ∈
ℝ) |
40 | | nnre 10904 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ) |
41 | 39, 40 | remulcld 9949 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → (2
· 𝑘) ∈
ℝ) |
42 | 41 | lep1d 10834 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → (2
· 𝑘) ≤ ((2
· 𝑘) +
1)) |
43 | | 2cnd 10970 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → 2 ∈
ℂ) |
44 | | nncn 10905 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℂ) |
45 | | 1cnd 9935 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → 1 ∈
ℂ) |
46 | 43, 44, 45 | adddid 9943 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → (2
· (𝑘 + 1)) = ((2
· 𝑘) + (2 ·
1))) |
47 | 24 | oveq2i 6560 |
. . . . . . . . . 10
⊢ ((2
· 𝑘) + (2 ·
1)) = ((2 · 𝑘) +
2) |
48 | 46, 47 | syl6eq 2660 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → (2
· (𝑘 + 1)) = ((2
· 𝑘) +
2)) |
49 | 48 | oveq1d 6564 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → ((2
· (𝑘 + 1)) −
1) = (((2 · 𝑘) + 2)
− 1)) |
50 | 43, 44 | mulcld 9939 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → (2
· 𝑘) ∈
ℂ) |
51 | 50, 43, 45 | addsubassd 10291 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → (((2
· 𝑘) + 2) − 1)
= ((2 · 𝑘) + (2
− 1))) |
52 | 26 | oveq2i 6560 |
. . . . . . . . 9
⊢ ((2
· 𝑘) + (2 −
1)) = ((2 · 𝑘) +
1) |
53 | 52 | a1i 11 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → ((2
· 𝑘) + (2 −
1)) = ((2 · 𝑘) +
1)) |
54 | 49, 51, 53 | 3eqtrrd 2649 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → ((2
· 𝑘) + 1) = ((2
· (𝑘 + 1)) −
1)) |
55 | 42, 54 | breqtrd 4609 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → (2
· 𝑘) ≤ ((2
· (𝑘 + 1)) −
1)) |
56 | | eluz2 11569 |
. . . . . 6
⊢ (((2
· (𝑘 + 1)) −
1) ∈ (ℤ≥‘(2 · 𝑘)) ↔ ((2 · 𝑘) ∈ ℤ ∧ ((2 · (𝑘 + 1)) − 1) ∈ ℤ
∧ (2 · 𝑘) ≤
((2 · (𝑘 + 1))
− 1))) |
57 | 33, 37, 55, 56 | syl3anbrc 1239 |
. . . . 5
⊢ (𝑘 ∈ ℕ → ((2
· (𝑘 + 1)) −
1) ∈ (ℤ≥‘(2 · 𝑘))) |
58 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑘 = 𝑗 → (2 · 𝑘) = (2 · 𝑗)) |
59 | 58 | oveq1d 6564 |
. . . . . . . 8
⊢ (𝑘 = 𝑗 → ((2 · 𝑘) − 1) = ((2 · 𝑗) − 1)) |
60 | 59 | cbvmptv 4678 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ ↦ ((2
· 𝑘) − 1)) =
(𝑗 ∈ ℕ ↦
((2 · 𝑗) −
1)) |
61 | 60 | a1i 11 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → (𝑘 ∈ ℕ ↦ ((2
· 𝑘) − 1)) =
(𝑗 ∈ ℕ ↦
((2 · 𝑗) −
1))) |
62 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑗 = (𝑘 + 1) → (2 · 𝑗) = (2 · (𝑘 + 1))) |
63 | 62 | oveq1d 6564 |
. . . . . . 7
⊢ (𝑗 = (𝑘 + 1) → ((2 · 𝑗) − 1) = ((2 · (𝑘 + 1)) −
1)) |
64 | 63 | adantl 481 |
. . . . . 6
⊢ ((𝑘 ∈ ℕ ∧ 𝑗 = (𝑘 + 1)) → ((2 · 𝑗) − 1) = ((2 · (𝑘 + 1)) −
1)) |
65 | | peano2nn 10909 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈
ℕ) |
66 | 61, 64, 65, 37 | fvmptd 6197 |
. . . . 5
⊢ (𝑘 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((2
· 𝑘) −
1))‘(𝑘 + 1)) = ((2
· (𝑘 + 1)) −
1)) |
67 | 33, 36 | zsubcld 11363 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → ((2
· 𝑘) − 1)
∈ ℤ) |
68 | 20 | fvmpt2 6200 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ ∧ ((2
· 𝑘) − 1)
∈ ℤ) → ((𝑘
∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) = ((2 · 𝑘) − 1)) |
69 | 67, 68 | mpdan 699 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((2
· 𝑘) −
1))‘𝑘) = ((2 ·
𝑘) −
1)) |
70 | 69 | oveq1d 6564 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → (((𝑘 ∈ ℕ ↦ ((2
· 𝑘) −
1))‘𝑘) + 1) = (((2
· 𝑘) − 1) +
1)) |
71 | 50, 45 | npcand 10275 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → (((2
· 𝑘) − 1) + 1)
= (2 · 𝑘)) |
72 | 70, 71 | eqtrd 2644 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → (((𝑘 ∈ ℕ ↦ ((2
· 𝑘) −
1))‘𝑘) + 1) = (2
· 𝑘)) |
73 | 72 | fveq2d 6107 |
. . . . 5
⊢ (𝑘 ∈ ℕ →
(ℤ≥‘(((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) + 1)) =
(ℤ≥‘(2 · 𝑘))) |
74 | 57, 66, 73 | 3eltr4d 2703 |
. . . 4
⊢ (𝑘 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((2
· 𝑘) −
1))‘(𝑘 + 1)) ∈
(ℤ≥‘(((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) + 1))) |
75 | 74 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘(𝑘 + 1)) ∈
(ℤ≥‘(((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) + 1))) |
76 | | seqex 12665 |
. . . 4
⊢ seq1( + ,
(𝑘 ∈ ℕ ↦
(𝐹‘((2 · 𝑘) − 1)))) ∈
V |
77 | 76 | a1i 11 |
. . 3
⊢ (𝜑 → seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ∈
V) |
78 | | incom 3767 |
. . . . . . . . . 10
⊢
(((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2
· 𝑘) − 1))
∩ {𝑛 ∈ ℕ
∣ (𝑛 / 2) ∈
ℕ})) = (((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2
· 𝑘) − 1))
∖ {𝑛 ∈ ℕ
∣ (𝑛 / 2) ∈
ℕ})) |
79 | | inss2 3796 |
. . . . . . . . . . 11
⊢ ((1...((2
· 𝑘) − 1))
∩ {𝑛 ∈ ℕ
∣ (𝑛 / 2) ∈
ℕ}) ⊆ {𝑛 ∈
ℕ ∣ (𝑛 / 2)
∈ ℕ} |
80 | | ssrin 3800 |
. . . . . . . . . . 11
⊢
(((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} →
(((1...((2 · 𝑘)
− 1)) ∩ {𝑛 ∈
ℕ ∣ (𝑛 / 2)
∈ ℕ}) ∩ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) ⊆ ({𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} ∩
((1...((2 · 𝑘)
− 1)) ∖ {𝑛
∈ ℕ ∣ (𝑛 /
2) ∈ ℕ}))) |
81 | 79, 80 | ax-mp 5 |
. . . . . . . . . 10
⊢
(((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2
· 𝑘) − 1))
∖ {𝑛 ∈ ℕ
∣ (𝑛 / 2) ∈
ℕ})) ⊆ ({𝑛
∈ ℕ ∣ (𝑛 /
2) ∈ ℕ} ∩ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) |
82 | 78, 81 | eqsstri 3598 |
. . . . . . . . 9
⊢
(((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2
· 𝑘) − 1))
∩ {𝑛 ∈ ℕ
∣ (𝑛 / 2) ∈
ℕ})) ⊆ ({𝑛
∈ ℕ ∣ (𝑛 /
2) ∈ ℕ} ∩ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) |
83 | | disjdif 3992 |
. . . . . . . . 9
⊢ ({𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} ∩
((1...((2 · 𝑘)
− 1)) ∖ {𝑛
∈ ℕ ∣ (𝑛 /
2) ∈ ℕ})) = ∅ |
84 | 82, 83 | sseqtri 3600 |
. . . . . . . 8
⊢
(((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2
· 𝑘) − 1))
∩ {𝑛 ∈ ℕ
∣ (𝑛 / 2) ∈
ℕ})) ⊆ ∅ |
85 | | ss0 3926 |
. . . . . . . 8
⊢
((((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2
· 𝑘) − 1))
∩ {𝑛 ∈ ℕ
∣ (𝑛 / 2) ∈
ℕ})) ⊆ ∅ → (((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∩ ((1...((2
· 𝑘) − 1))
∩ {𝑛 ∈ ℕ
∣ (𝑛 / 2) ∈
ℕ})) = ∅) |
86 | 84, 85 | mp1i 13 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((1...((2 ·
𝑘) − 1)) ∖
{𝑛 ∈ ℕ ∣
(𝑛 / 2) ∈ ℕ})
∩ ((1...((2 · 𝑘)
− 1)) ∩ {𝑛 ∈
ℕ ∣ (𝑛 / 2)
∈ ℕ})) = ∅) |
87 | | uncom 3719 |
. . . . . . . . 9
⊢
(((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∪ ((1...((2
· 𝑘) − 1))
∩ {𝑛 ∈ ℕ
∣ (𝑛 / 2) ∈
ℕ})) = (((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∪ ((1...((2
· 𝑘) − 1))
∖ {𝑛 ∈ ℕ
∣ (𝑛 / 2) ∈
ℕ})) |
88 | | inundif 3998 |
. . . . . . . . 9
⊢
(((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∪ ((1...((2
· 𝑘) − 1))
∖ {𝑛 ∈ ℕ
∣ (𝑛 / 2) ∈
ℕ})) = (1...((2 · 𝑘) − 1)) |
89 | 87, 88 | eqtr2i 2633 |
. . . . . . . 8
⊢ (1...((2
· 𝑘) − 1)) =
(((1...((2 · 𝑘)
− 1)) ∖ {𝑛
∈ ℕ ∣ (𝑛 /
2) ∈ ℕ}) ∪ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) |
90 | 89 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1...((2 ·
𝑘) − 1)) = (((1...((2
· 𝑘) − 1))
∖ {𝑛 ∈ ℕ
∣ (𝑛 / 2) ∈
ℕ}) ∪ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))) |
91 | | fzfid 12634 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1...((2 ·
𝑘) − 1)) ∈
Fin) |
92 | 12 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → 𝐹:ℕ⟶ℂ) |
93 | | elfznn 12241 |
. . . . . . . . . 10
⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → 𝑗 ∈
ℕ) |
94 | 93 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → 𝑗 ∈ ℕ) |
95 | 92, 94 | ffvelrnd 6268 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → (𝐹‘𝑗) ∈ ℂ) |
96 | 95 | adantlr 747 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → (𝐹‘𝑗) ∈ ℂ) |
97 | 86, 90, 91, 96 | fsumsplit 14318 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...((2 · 𝑘) − 1))(𝐹‘𝑗) = (Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗) + Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗))) |
98 | | simpl 472 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → 𝜑) |
99 | | ssrab2 3650 |
. . . . . . . . . . . . . 14
⊢ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} ⊆
ℕ |
100 | 79 | sseli 3564 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) →
𝑗 ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈
ℕ}) |
101 | 99, 100 | sseldi 3566 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) →
𝑗 ∈
ℕ) |
102 | 101 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → 𝑗 ∈
ℕ) |
103 | | oveq1 6556 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑗 → (𝑘 / 2) = (𝑗 / 2)) |
104 | 103 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑗 → ((𝑘 / 2) ∈ ℕ ↔ (𝑗 / 2) ∈
ℕ)) |
105 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑘 → (𝑛 / 2) = (𝑘 / 2)) |
106 | 105 | eleq1d 2672 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑘 → ((𝑛 / 2) ∈ ℕ ↔ (𝑘 / 2) ∈
ℕ)) |
107 | 106 | elrab 3331 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} ↔ (𝑘 ∈ ℕ ∧ (𝑘 / 2) ∈
ℕ)) |
108 | 107 | simprbi 479 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} → (𝑘 / 2) ∈
ℕ) |
109 | 104, 108 | vtoclga 3245 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} → (𝑗 / 2) ∈
ℕ) |
110 | 100, 109 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) →
(𝑗 / 2) ∈
ℕ) |
111 | 110 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (𝑗 / 2) ∈
ℕ) |
112 | | eleq1 2676 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑗 → (𝑘 ∈ ℕ ↔ 𝑗 ∈ ℕ)) |
113 | 112, 104 | 3anbi23d 1394 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑗 → ((𝜑 ∧ 𝑘 ∈ ℕ ∧ (𝑘 / 2) ∈ ℕ) ↔ (𝜑 ∧ 𝑗 ∈ ℕ ∧ (𝑗 / 2) ∈ ℕ))) |
114 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑗 → (𝐹‘𝑘) = (𝐹‘𝑗)) |
115 | 114 | eqeq1d 2612 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑗 → ((𝐹‘𝑘) = 0 ↔ (𝐹‘𝑗) = 0)) |
116 | 113, 115 | imbi12d 333 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑗 → (((𝜑 ∧ 𝑘 ∈ ℕ ∧ (𝑘 / 2) ∈ ℕ) → (𝐹‘𝑘) = 0) ↔ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ (𝑗 / 2) ∈ ℕ) → (𝐹‘𝑗) = 0))) |
117 | | sumnnodd.even0 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ (𝑘 / 2) ∈ ℕ) → (𝐹‘𝑘) = 0) |
118 | 116, 117 | chvarv 2251 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ (𝑗 / 2) ∈ ℕ) → (𝐹‘𝑗) = 0) |
119 | 98, 102, 111, 118 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (𝐹‘𝑗) = 0) |
120 | 119 | sumeq2dv 14281 |
. . . . . . . . . 10
⊢ (𝜑 → Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗) = Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})0) |
121 | | fzfid 12634 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1...((2 · 𝑘) − 1)) ∈
Fin) |
122 | | inss1 3795 |
. . . . . . . . . . . . . 14
⊢ ((1...((2
· 𝑘) − 1))
∩ {𝑛 ∈ ℕ
∣ (𝑛 / 2) ∈
ℕ}) ⊆ (1...((2 · 𝑘) − 1)) |
123 | 122 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆
(1...((2 · 𝑘)
− 1))) |
124 | | ssfi 8065 |
. . . . . . . . . . . . 13
⊢
(((1...((2 · 𝑘) − 1)) ∈ Fin ∧ ((1...((2
· 𝑘) − 1))
∩ {𝑛 ∈ ℕ
∣ (𝑛 / 2) ∈
ℕ}) ⊆ (1...((2 · 𝑘) − 1))) → ((1...((2 ·
𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∈
Fin) |
125 | 121, 123,
124 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∈
Fin) |
126 | 125 | olcd 407 |
. . . . . . . . . . 11
⊢ (𝜑 → (((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆
(ℤ≥‘𝐶) ∨ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∈
Fin)) |
127 | | sumz 14300 |
. . . . . . . . . . 11
⊢
((((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ⊆
(ℤ≥‘𝐶) ∨ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∈ Fin) →
Σ𝑗 ∈ ((1...((2
· 𝑘) − 1))
∩ {𝑛 ∈ ℕ
∣ (𝑛 / 2) ∈
ℕ})0 = 0) |
128 | 126, 127 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})0 = 0) |
129 | 120, 128 | eqtrd 2644 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗) = 0) |
130 | 129 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗) = 0) |
131 | 130 | oveq2d 6565 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗) + Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗)) = (Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗) + 0)) |
132 | | fzfi 12633 |
. . . . . . . . . . . 12
⊢ (1...((2
· 𝑘) − 1))
∈ Fin |
133 | | difss 3699 |
. . . . . . . . . . . 12
⊢ ((1...((2
· 𝑘) − 1))
∖ {𝑛 ∈ ℕ
∣ (𝑛 / 2) ∈
ℕ}) ⊆ (1...((2 · 𝑘) − 1)) |
134 | | ssfi 8065 |
. . . . . . . . . . . 12
⊢
(((1...((2 · 𝑘) − 1)) ∈ Fin ∧ ((1...((2
· 𝑘) − 1))
∖ {𝑛 ∈ ℕ
∣ (𝑛 / 2) ∈
ℕ}) ⊆ (1...((2 · 𝑘) − 1))) → ((1...((2 ·
𝑘) − 1)) ∖
{𝑛 ∈ ℕ ∣
(𝑛 / 2) ∈ ℕ})
∈ Fin) |
135 | 132, 133,
134 | mp2an 704 |
. . . . . . . . . . 11
⊢ ((1...((2
· 𝑘) − 1))
∖ {𝑛 ∈ ℕ
∣ (𝑛 / 2) ∈
ℕ}) ∈ Fin |
136 | 135 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((1...((2 ·
𝑘) − 1)) ∖
{𝑛 ∈ ℕ ∣
(𝑛 / 2) ∈ ℕ})
∈ Fin) |
137 | 133 | sseli 3564 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) →
𝑗 ∈ (1...((2 ·
𝑘) −
1))) |
138 | 137, 95 | sylan2 490 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (𝐹‘𝑗) ∈ ℂ) |
139 | 138 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (𝐹‘𝑗) ∈ ℂ) |
140 | 136, 139 | fsumcl 14311 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗) ∈ ℂ) |
141 | 140 | addid1d 10115 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗) + 0) = Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗)) |
142 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑗 = 𝑖 → (𝐹‘𝑗) = (𝐹‘𝑖)) |
143 | 142 | cbvsumv 14274 |
. . . . . . . 8
⊢
Σ𝑗 ∈
((1...((2 · 𝑘)
− 1)) ∖ {𝑛
∈ ℕ ∣ (𝑛 /
2) ∈ ℕ})(𝐹‘𝑗) = Σ𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑖) |
144 | 141, 143 | syl6eq 2660 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗) + 0) = Σ𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑖)) |
145 | 131, 144 | eqtrd 2644 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗) + Σ𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∩ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑗)) = Σ𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑖)) |
146 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑖 = ((2 · 𝑗) − 1) → (𝐹‘𝑖) = (𝐹‘((2 · 𝑗) − 1))) |
147 | | fzfid 12634 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1...𝑘) ∈ Fin) |
148 | | 1zzd 11285 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 1 ∈ ℤ) |
149 | 67 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → ((2 · 𝑘) − 1) ∈ ℤ) |
150 | 30 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ (1...𝑘) → 2 ∈ ℤ) |
151 | | elfzelz 12213 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ (1...𝑘) → 𝑖 ∈ ℤ) |
152 | 150, 151 | zmulcld 11364 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (1...𝑘) → (2 · 𝑖) ∈ ℤ) |
153 | | 1zzd 11285 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (1...𝑘) → 1 ∈ ℤ) |
154 | 152, 153 | zsubcld 11363 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (1...𝑘) → ((2 · 𝑖) − 1) ∈ ℤ) |
155 | 154 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → ((2 · 𝑖) − 1) ∈ ℤ) |
156 | 148, 149,
155 | 3jca 1235 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → (1 ∈ ℤ ∧ ((2
· 𝑘) − 1)
∈ ℤ ∧ ((2 · 𝑖) − 1) ∈
ℤ)) |
157 | 25, 26 | eqtr2i 2633 |
. . . . . . . . . . . . . . . 16
⊢ 1 = ((2
· 1) − 1) |
158 | | 1re 9918 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℝ |
159 | 38, 158 | remulcli 9933 |
. . . . . . . . . . . . . . . . . 18
⊢ (2
· 1) ∈ ℝ |
160 | 159 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ (1...𝑘) → (2 · 1) ∈
ℝ) |
161 | 152 | zred 11358 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ (1...𝑘) → (2 · 𝑖) ∈ ℝ) |
162 | | 1red 9934 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ (1...𝑘) → 1 ∈ ℝ) |
163 | 151 | zred 11358 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ (1...𝑘) → 𝑖 ∈ ℝ) |
164 | 38 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ (1...𝑘) → 2 ∈ ℝ) |
165 | | 0le2 10988 |
. . . . . . . . . . . . . . . . . . 19
⊢ 0 ≤
2 |
166 | 165 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ (1...𝑘) → 0 ≤ 2) |
167 | | elfzle1 12215 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ (1...𝑘) → 1 ≤ 𝑖) |
168 | 162, 163,
164, 166, 167 | lemul2ad 10843 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ (1...𝑘) → (2 · 1) ≤ (2 ·
𝑖)) |
169 | 160, 161,
162, 168 | lesub1dd 10522 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (1...𝑘) → ((2 · 1) − 1) ≤ ((2
· 𝑖) −
1)) |
170 | 157, 169 | syl5eqbr 4618 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (1...𝑘) → 1 ≤ ((2 · 𝑖) − 1)) |
171 | 170 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 1 ≤ ((2 · 𝑖) − 1)) |
172 | 161 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → (2 · 𝑖) ∈ ℝ) |
173 | 41 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → (2 · 𝑘) ∈ ℝ) |
174 | | 1red 9934 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 1 ∈ ℝ) |
175 | 163 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 𝑖 ∈ ℝ) |
176 | 40 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 𝑘 ∈ ℝ) |
177 | 38 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 2 ∈ ℝ) |
178 | 165 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 0 ≤ 2) |
179 | | elfzle2 12216 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ (1...𝑘) → 𝑖 ≤ 𝑘) |
180 | 179 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → 𝑖 ≤ 𝑘) |
181 | 175, 176,
177, 178, 180 | lemul2ad 10843 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → (2 · 𝑖) ≤ (2 · 𝑘)) |
182 | 172, 173,
174, 181 | lesub1dd 10522 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → ((2 · 𝑖) − 1) ≤ ((2 · 𝑘) − 1)) |
183 | 171, 182 | jca 553 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → (1 ≤ ((2 · 𝑖) − 1) ∧ ((2 ·
𝑖) − 1) ≤ ((2
· 𝑘) −
1))) |
184 | | elfz2 12204 |
. . . . . . . . . . . . 13
⊢ (((2
· 𝑖) − 1)
∈ (1...((2 · 𝑘)
− 1)) ↔ ((1 ∈ ℤ ∧ ((2 · 𝑘) − 1) ∈ ℤ ∧ ((2
· 𝑖) − 1)
∈ ℤ) ∧ (1 ≤ ((2 · 𝑖) − 1) ∧ ((2 · 𝑖) − 1) ≤ ((2 ·
𝑘) −
1)))) |
185 | 156, 183,
184 | sylanbrc 695 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → ((2 · 𝑖) − 1) ∈ (1...((2 · 𝑘) − 1))) |
186 | 152 | zcnd 11359 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ (1...𝑘) → (2 · 𝑖) ∈ ℂ) |
187 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ (1...𝑘) → 1 ∈ ℂ) |
188 | | 2cnd 10970 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ (1...𝑘) → 2 ∈ ℂ) |
189 | | 2ne0 10990 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ≠
0 |
190 | 189 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ (1...𝑘) → 2 ≠ 0) |
191 | 186, 187,
188, 190 | divsubdird 10719 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ (1...𝑘) → (((2 · 𝑖) − 1) / 2) = (((2 · 𝑖) / 2) − (1 /
2))) |
192 | 151 | zcnd 11359 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ (1...𝑘) → 𝑖 ∈ ℂ) |
193 | 192, 188,
190 | divcan3d 10685 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ (1...𝑘) → ((2 · 𝑖) / 2) = 𝑖) |
194 | 193 | oveq1d 6564 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ (1...𝑘) → (((2 · 𝑖) / 2) − (1 / 2)) = (𝑖 − (1 / 2))) |
195 | 191, 194 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (1...𝑘) → (((2 · 𝑖) − 1) / 2) = (𝑖 − (1 / 2))) |
196 | 151, 153 | zsubcld 11363 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ (1...𝑘) → (𝑖 − 1) ∈ ℤ) |
197 | 164, 190 | rereccld 10731 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ (1...𝑘) → (1 / 2) ∈
ℝ) |
198 | | halflt1 11127 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1 / 2)
< 1 |
199 | 198 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ (1...𝑘) → (1 / 2) < 1) |
200 | 197, 162,
163, 199 | ltsub2dd 10519 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ (1...𝑘) → (𝑖 − 1) < (𝑖 − (1 / 2))) |
201 | | 2rp 11713 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 2 ∈
ℝ+ |
202 | | rpreccl 11733 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (2 ∈
ℝ+ → (1 / 2) ∈ ℝ+) |
203 | 201, 202 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈ (1...𝑘) → (1 / 2) ∈
ℝ+) |
204 | 163, 203 | ltsubrpd 11780 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ (1...𝑘) → (𝑖 − (1 / 2)) < 𝑖) |
205 | 192, 187 | npcand 10275 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ (1...𝑘) → ((𝑖 − 1) + 1) = 𝑖) |
206 | 204, 205 | breqtrrd 4611 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ (1...𝑘) → (𝑖 − (1 / 2)) < ((𝑖 − 1) + 1)) |
207 | | btwnnz 11329 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑖 − 1) ∈ ℤ ∧
(𝑖 − 1) < (𝑖 − (1 / 2)) ∧ (𝑖 − (1 / 2)) < ((𝑖 − 1) + 1)) → ¬
(𝑖 − (1 / 2)) ∈
ℤ) |
208 | 196, 200,
206, 207 | syl3anc 1318 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ (1...𝑘) → ¬ (𝑖 − (1 / 2)) ∈
ℤ) |
209 | | nnz 11276 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 − (1 / 2)) ∈ ℕ
→ (𝑖 − (1 / 2))
∈ ℤ) |
210 | 208, 209 | nsyl 134 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (1...𝑘) → ¬ (𝑖 − (1 / 2)) ∈
ℕ) |
211 | 195, 210 | eqneltrd 2707 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (1...𝑘) → ¬ (((2 · 𝑖) − 1) / 2) ∈
ℕ) |
212 | 211 | intnand 953 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (1...𝑘) → ¬ (((2 · 𝑖) − 1) ∈ ℕ
∧ (((2 · 𝑖)
− 1) / 2) ∈ ℕ)) |
213 | | oveq1 6556 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = ((2 · 𝑖) − 1) → (𝑛 / 2) = (((2 · 𝑖) − 1) /
2)) |
214 | 213 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = ((2 · 𝑖) − 1) → ((𝑛 / 2) ∈ ℕ ↔ (((2
· 𝑖) − 1) / 2)
∈ ℕ)) |
215 | 214 | elrab 3331 |
. . . . . . . . . . . . . 14
⊢ (((2
· 𝑖) − 1)
∈ {𝑛 ∈ ℕ
∣ (𝑛 / 2) ∈
ℕ} ↔ (((2 · 𝑖) − 1) ∈ ℕ ∧ (((2
· 𝑖) − 1) / 2)
∈ ℕ)) |
216 | 212, 215 | sylnibr 318 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (1...𝑘) → ¬ ((2 · 𝑖) − 1) ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈
ℕ}) |
217 | 216 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → ¬ ((2 · 𝑖) − 1) ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈
ℕ}) |
218 | 185, 217 | eldifd 3551 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (1...𝑘)) → ((2 · 𝑖) − 1) ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈
ℕ})) |
219 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)) = (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)) |
220 | 218, 219 | fmptd 6292 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)⟶((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈
ℕ})) |
221 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (1...𝑘) → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)) = (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))) |
222 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = 𝑥 → (2 · 𝑖) = (2 · 𝑥)) |
223 | 222 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 = 𝑥 → ((2 · 𝑖) − 1) = ((2 · 𝑥) − 1)) |
224 | 223 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (1...𝑘) ∧ 𝑖 = 𝑥) → ((2 · 𝑖) − 1) = ((2 · 𝑥) − 1)) |
225 | | id 22 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (1...𝑘) → 𝑥 ∈ (1...𝑘)) |
226 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((2
· 𝑥) − 1)
∈ V |
227 | 226 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (1...𝑘) → ((2 · 𝑥) − 1) ∈ V) |
228 | 221, 224,
225, 227 | fvmptd 6197 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (1...𝑘) → ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((2 · 𝑥) − 1)) |
229 | 228 | eqcomd 2616 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (1...𝑘) → ((2 · 𝑥) − 1) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥)) |
230 | 229 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦)) → ((2 · 𝑥) − 1) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥)) |
231 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦)) → ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦)) |
232 | | eqidd 2611 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (1...𝑘) → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)) = (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))) |
233 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 = 𝑦 → (2 · 𝑖) = (2 · 𝑦)) |
234 | 233 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 = 𝑦 → ((2 · 𝑖) − 1) = ((2 · 𝑦) − 1)) |
235 | 234 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ (1...𝑘) ∧ 𝑖 = 𝑦) → ((2 · 𝑖) − 1) = ((2 · 𝑦) − 1)) |
236 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (1...𝑘) → 𝑦 ∈ (1...𝑘)) |
237 | | ovex 6577 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2
· 𝑦) − 1)
∈ V |
238 | 237 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (1...𝑘) → ((2 · 𝑦) − 1) ∈ V) |
239 | 232, 235,
236, 238 | fvmptd 6197 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (1...𝑘) → ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦) = ((2 · 𝑦) − 1)) |
240 | 239 | ad2antlr 759 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦)) → ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦) = ((2 · 𝑦) − 1)) |
241 | 230, 231,
240 | 3eqtrd 2648 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦)) → ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1)) |
242 | | 2cnd 10970 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (1...𝑘) → 2 ∈ ℂ) |
243 | | elfzelz 12213 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (1...𝑘) → 𝑥 ∈ ℤ) |
244 | 243 | zcnd 11359 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (1...𝑘) → 𝑥 ∈ ℂ) |
245 | 242, 244 | mulcld 9939 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (1...𝑘) → (2 · 𝑥) ∈ ℂ) |
246 | 245 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1)) → (2 ·
𝑥) ∈
ℂ) |
247 | | 2cnd 10970 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ (1...𝑘) → 2 ∈ ℂ) |
248 | | elfzelz 12213 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (1...𝑘) → 𝑦 ∈ ℤ) |
249 | 248 | zcnd 11359 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ (1...𝑘) → 𝑦 ∈ ℂ) |
250 | 247, 249 | mulcld 9939 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (1...𝑘) → (2 · 𝑦) ∈ ℂ) |
251 | 250 | ad2antlr 759 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1)) → (2 ·
𝑦) ∈
ℂ) |
252 | | 1cnd 9935 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1)) → 1 ∈
ℂ) |
253 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1)) → ((2
· 𝑥) − 1) =
((2 · 𝑦) −
1)) |
254 | 246, 251,
252, 253 | subcan2d 10313 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1)) → (2 ·
𝑥) = (2 · 𝑦)) |
255 | 244 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ (2 · 𝑥) = (2 · 𝑦)) → 𝑥 ∈ ℂ) |
256 | 249 | ad2antlr 759 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ (2 · 𝑥) = (2 · 𝑦)) → 𝑦 ∈ ℂ) |
257 | | 2cnd 10970 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ (2 · 𝑥) = (2 · 𝑦)) → 2 ∈ ℂ) |
258 | 189 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ (2 · 𝑥) = (2 · 𝑦)) → 2 ≠ 0) |
259 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ (2 · 𝑥) = (2 · 𝑦)) → (2 · 𝑥) = (2 · 𝑦)) |
260 | 255, 256,
257, 258, 259 | mulcanad 10541 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ (2 · 𝑥) = (2 · 𝑦)) → 𝑥 = 𝑦) |
261 | 254, 260 | syldan 486 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1)) → 𝑥 = 𝑦) |
262 | 241, 261 | syldan 486 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘)) ∧ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦)) → 𝑥 = 𝑦) |
263 | 262 | adantll 746 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ℕ ∧ (𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘))) ∧ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦)) → 𝑥 = 𝑦) |
264 | 263 | ex 449 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧ (𝑥 ∈ (1...𝑘) ∧ 𝑦 ∈ (1...𝑘))) → (((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦) → 𝑥 = 𝑦)) |
265 | 264 | ralrimivva 2954 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ →
∀𝑥 ∈ (1...𝑘)∀𝑦 ∈ (1...𝑘)(((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦) → 𝑥 = 𝑦)) |
266 | | dff13 6416 |
. . . . . . . . . 10
⊢ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)–1-1→((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ↔ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)⟶((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧
∀𝑥 ∈ (1...𝑘)∀𝑦 ∈ (1...𝑘)(((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑥) = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑦) → 𝑥 = 𝑦))) |
267 | 220, 265,
266 | sylanbrc 695 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)–1-1→((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) |
268 | | 1zzd 11285 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → 1
∈ ℤ) |
269 | 32 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) →
𝑘 ∈
ℤ) |
270 | | fzssz 12214 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1...((2
· 𝑘) − 1))
⊆ ℤ |
271 | 270, 137 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) →
𝑗 ∈
ℤ) |
272 | | zeo 11339 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ℤ → ((𝑗 / 2) ∈ ℤ ∨
((𝑗 + 1) / 2) ∈
ℤ)) |
273 | 271, 272 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) →
((𝑗 / 2) ∈ ℤ
∨ ((𝑗 + 1) / 2) ∈
ℤ)) |
274 | 273 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) →
((𝑗 / 2) ∈ ℤ
∨ ((𝑗 + 1) / 2) ∈
ℤ)) |
275 | | eldifn 3695 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) →
¬ 𝑗 ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈
ℕ}) |
276 | 137, 93 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) →
𝑗 ∈
ℕ) |
277 | 276 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧
(𝑗 / 2) ∈ ℤ)
→ 𝑗 ∈
ℕ) |
278 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧
(𝑗 / 2) ∈ ℤ)
→ (𝑗 / 2) ∈
ℤ) |
279 | 277 | nnred 10912 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧
(𝑗 / 2) ∈ ℤ)
→ 𝑗 ∈
ℝ) |
280 | 38 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧
(𝑗 / 2) ∈ ℤ)
→ 2 ∈ ℝ) |
281 | 277 | nngt0d 10941 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧
(𝑗 / 2) ∈ ℤ)
→ 0 < 𝑗) |
282 | | 2pos 10989 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 <
2 |
283 | 282 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧
(𝑗 / 2) ∈ ℤ)
→ 0 < 2) |
284 | 279, 280,
281, 283 | divgt0d 10838 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧
(𝑗 / 2) ∈ ℤ)
→ 0 < (𝑗 /
2)) |
285 | | elnnz 11264 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑗 / 2) ∈ ℕ ↔
((𝑗 / 2) ∈ ℤ
∧ 0 < (𝑗 /
2))) |
286 | 278, 284,
285 | sylanbrc 695 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧
(𝑗 / 2) ∈ ℤ)
→ (𝑗 / 2) ∈
ℕ) |
287 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = 𝑗 → (𝑛 / 2) = (𝑗 / 2)) |
288 | 287 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 𝑗 → ((𝑛 / 2) ∈ ℕ ↔ (𝑗 / 2) ∈
ℕ)) |
289 | 288 | elrab 3331 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ} ↔ (𝑗 ∈ ℕ ∧ (𝑗 / 2) ∈
ℕ)) |
290 | 277, 286,
289 | sylanbrc 695 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧
(𝑗 / 2) ∈ ℤ)
→ 𝑗 ∈ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈
ℕ}) |
291 | 275, 290 | mtand 689 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) →
¬ (𝑗 / 2) ∈
ℤ) |
292 | 291 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) →
¬ (𝑗 / 2) ∈
ℤ) |
293 | | pm2.53 387 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑗 / 2) ∈ ℤ ∨
((𝑗 + 1) / 2) ∈
ℤ) → (¬ (𝑗 /
2) ∈ ℤ → ((𝑗 + 1) / 2) ∈ ℤ)) |
294 | 274, 292,
293 | sylc 63 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) →
((𝑗 + 1) / 2) ∈
ℤ) |
295 | 268, 269,
294 | 3jca 1235 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) →
(1 ∈ ℤ ∧ 𝑘
∈ ℤ ∧ ((𝑗 +
1) / 2) ∈ ℤ)) |
296 | | 1p1e2 11011 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1 + 1) =
2 |
297 | 296 | oveq1i 6559 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((1 + 1)
/ 2) = (2 / 2) |
298 | | 2div2e1 11027 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2 / 2) =
1 |
299 | 297, 298 | eqtr2i 2633 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 = ((1 +
1) / 2) |
300 | | 1red 9934 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → 1 ∈
ℝ) |
301 | 300, 300 | readdcld 9948 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → (1 + 1)
∈ ℝ) |
302 | 93 | nnred 10912 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → 𝑗 ∈
ℝ) |
303 | 302, 300 | readdcld 9948 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → (𝑗 + 1) ∈
ℝ) |
304 | 201 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → 2 ∈
ℝ+) |
305 | | elfzle1 12215 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → 1 ≤
𝑗) |
306 | 300, 302,
300, 305 | leadd1dd 10520 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → (1 + 1)
≤ (𝑗 +
1)) |
307 | 301, 303,
304, 306 | lediv1dd 11806 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → ((1 + 1) /
2) ≤ ((𝑗 + 1) /
2)) |
308 | 299, 307 | syl5eqbr 4618 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → 1 ≤
((𝑗 + 1) /
2)) |
309 | 137, 308 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) → 1
≤ ((𝑗 + 1) /
2)) |
310 | 309 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → 1
≤ ((𝑗 + 1) /
2)) |
311 | | elfzel2 12211 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → ((2
· 𝑘) − 1)
∈ ℤ) |
312 | 311 | zred 11358 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → ((2
· 𝑘) − 1)
∈ ℝ) |
313 | 312, 300 | readdcld 9948 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → (((2
· 𝑘) − 1) + 1)
∈ ℝ) |
314 | | elfzle2 12216 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → 𝑗 ≤ ((2 · 𝑘) − 1)) |
315 | 302, 312,
300, 314 | leadd1dd 10520 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → (𝑗 + 1) ≤ (((2 · 𝑘) − 1) +
1)) |
316 | 303, 313,
304, 315 | lediv1dd 11806 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (1...((2 · 𝑘) − 1)) → ((𝑗 + 1) / 2) ≤ ((((2 ·
𝑘) − 1) + 1) /
2)) |
317 | 316 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → ((𝑗 + 1) / 2) ≤ ((((2 ·
𝑘) − 1) + 1) /
2)) |
318 | 50 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → (2
· 𝑘) ∈
ℂ) |
319 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → 1 ∈
ℂ) |
320 | 318, 319 | npcand 10275 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → (((2
· 𝑘) − 1) + 1)
= (2 · 𝑘)) |
321 | 320 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → ((((2
· 𝑘) − 1) + 1)
/ 2) = ((2 · 𝑘) /
2)) |
322 | 189 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ ℕ → 2 ≠
0) |
323 | 44, 43, 322 | divcan3d 10685 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ ℕ → ((2
· 𝑘) / 2) = 𝑘) |
324 | 323 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → ((2
· 𝑘) / 2) = 𝑘) |
325 | 321, 324 | eqtrd 2644 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → ((((2
· 𝑘) − 1) + 1)
/ 2) = 𝑘) |
326 | 317, 325 | breqtrd 4609 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((2 · 𝑘) − 1))) → ((𝑗 + 1) / 2) ≤ 𝑘) |
327 | 137, 326 | sylan2 490 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) →
((𝑗 + 1) / 2) ≤ 𝑘) |
328 | 295, 310,
327 | jca32 556 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) →
((1 ∈ ℤ ∧ 𝑘
∈ ℤ ∧ ((𝑗 +
1) / 2) ∈ ℤ) ∧ (1 ≤ ((𝑗 + 1) / 2) ∧ ((𝑗 + 1) / 2) ≤ 𝑘))) |
329 | | elfz2 12204 |
. . . . . . . . . . . . . 14
⊢ (((𝑗 + 1) / 2) ∈ (1...𝑘) ↔ ((1 ∈ ℤ
∧ 𝑘 ∈ ℤ
∧ ((𝑗 + 1) / 2) ∈
ℤ) ∧ (1 ≤ ((𝑗
+ 1) / 2) ∧ ((𝑗 + 1) /
2) ≤ 𝑘))) |
330 | 328, 329 | sylibr 223 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) →
((𝑗 + 1) / 2) ∈
(1...𝑘)) |
331 | 276 | nncnd 10913 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) →
𝑗 ∈
ℂ) |
332 | | peano2cn 10087 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ ℂ → (𝑗 + 1) ∈
ℂ) |
333 | | 2cnd 10970 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ ℂ → 2 ∈
ℂ) |
334 | 189 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ ℂ → 2 ≠
0) |
335 | 332, 333,
334 | divcan2d 10682 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ ℂ → (2
· ((𝑗 + 1) / 2)) =
(𝑗 + 1)) |
336 | 335 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ ℂ → ((2
· ((𝑗 + 1) / 2))
− 1) = ((𝑗 + 1)
− 1)) |
337 | | pncan1 10333 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ ℂ → ((𝑗 + 1) − 1) = 𝑗) |
338 | 336, 337 | eqtr2d 2645 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ℂ → 𝑗 = ((2 · ((𝑗 + 1) / 2)) −
1)) |
339 | 331, 338 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) →
𝑗 = ((2 · ((𝑗 + 1) / 2)) −
1)) |
340 | 339 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) →
𝑗 = ((2 · ((𝑗 + 1) / 2)) −
1)) |
341 | | oveq2 6557 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = ((𝑗 + 1) / 2) → (2 · 𝑚) = (2 · ((𝑗 + 1) / 2))) |
342 | 341 | oveq1d 6564 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = ((𝑗 + 1) / 2) → ((2 · 𝑚) − 1) = ((2 ·
((𝑗 + 1) / 2)) −
1)) |
343 | 342 | eqeq2d 2620 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = ((𝑗 + 1) / 2) → (𝑗 = ((2 · 𝑚) − 1) ↔ 𝑗 = ((2 · ((𝑗 + 1) / 2)) − 1))) |
344 | 343 | rspcev 3282 |
. . . . . . . . . . . . 13
⊢ ((((𝑗 + 1) / 2) ∈ (1...𝑘) ∧ 𝑗 = ((2 · ((𝑗 + 1) / 2)) − 1)) → ∃𝑚 ∈ (1...𝑘)𝑗 = ((2 · 𝑚) − 1)) |
345 | 330, 340,
344 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) →
∃𝑚 ∈ (1...𝑘)𝑗 = ((2 · 𝑚) − 1)) |
346 | | eqidd 2611 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑚 ∈ (1...𝑘) ∧ 𝑗 = ((2 · 𝑚) − 1)) → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)) = (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))) |
347 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 = 𝑚 → (2 · 𝑖) = (2 · 𝑚)) |
348 | 347 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 = 𝑚 → ((2 · 𝑖) − 1) = ((2 · 𝑚) − 1)) |
349 | 348 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑚 ∈ (1...𝑘) ∧ 𝑗 = ((2 · 𝑚) − 1)) ∧ 𝑖 = 𝑚) → ((2 · 𝑖) − 1) = ((2 · 𝑚) − 1)) |
350 | | simpl 472 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑚 ∈ (1...𝑘) ∧ 𝑗 = ((2 · 𝑚) − 1)) → 𝑚 ∈ (1...𝑘)) |
351 | | ovex 6577 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2
· 𝑚) − 1)
∈ V |
352 | 351 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑚 ∈ (1...𝑘) ∧ 𝑗 = ((2 · 𝑚) − 1)) → ((2 · 𝑚) − 1) ∈
V) |
353 | 346, 349,
350, 352 | fvmptd 6197 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑚 ∈ (1...𝑘) ∧ 𝑗 = ((2 · 𝑚) − 1)) → ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚) = ((2 · 𝑚) − 1)) |
354 | | id 22 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = ((2 · 𝑚) − 1) → 𝑗 = ((2 · 𝑚) − 1)) |
355 | 354 | eqcomd 2616 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = ((2 · 𝑚) − 1) → ((2 ·
𝑚) − 1) = 𝑗) |
356 | 355 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑚 ∈ (1...𝑘) ∧ 𝑗 = ((2 · 𝑚) − 1)) → ((2 · 𝑚) − 1) = 𝑗) |
357 | 353, 356 | eqtr2d 2645 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 ∈ (1...𝑘) ∧ 𝑗 = ((2 · 𝑚) − 1)) → 𝑗 = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚)) |
358 | 357 | ex 449 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ (1...𝑘) → (𝑗 = ((2 · 𝑚) − 1) → 𝑗 = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚))) |
359 | 358 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) ∧
𝑚 ∈ (1...𝑘)) → (𝑗 = ((2 · 𝑚) − 1) → 𝑗 = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚))) |
360 | 359 | reximdva 3000 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) →
(∃𝑚 ∈ (1...𝑘)𝑗 = ((2 · 𝑚) − 1) → ∃𝑚 ∈ (1...𝑘)𝑗 = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚))) |
361 | 345, 360 | mpd 15 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) →
∃𝑚 ∈ (1...𝑘)𝑗 = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚)) |
362 | 361 | ralrimiva 2949 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ →
∀𝑗 ∈ ((1...((2
· 𝑘) − 1))
∖ {𝑛 ∈ ℕ
∣ (𝑛 / 2) ∈
ℕ})∃𝑚 ∈
(1...𝑘)𝑗 = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚)) |
363 | | dffo3 6282 |
. . . . . . . . . 10
⊢ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)–onto→((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ↔ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)⟶((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧
∀𝑗 ∈ ((1...((2
· 𝑘) − 1))
∖ {𝑛 ∈ ℕ
∣ (𝑛 / 2) ∈
ℕ})∃𝑚 ∈
(1...𝑘)𝑗 = ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑚))) |
364 | 220, 362,
363 | sylanbrc 695 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)–onto→((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) |
365 | | df-f1o 5811 |
. . . . . . . . 9
⊢ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)–1-1-onto→((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ↔ ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)–1-1→((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ∧ (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)–onto→((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}))) |
366 | 267, 364,
365 | sylanbrc 695 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)–1-1-onto→((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) |
367 | 366 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)):(1...𝑘)–1-1-onto→((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) |
368 | | eqidd 2611 |
. . . . . . . . 9
⊢ (𝑗 ∈ (1...𝑘) → (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1)) = (𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))) |
369 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑗 → (2 · 𝑖) = (2 · 𝑗)) |
370 | 369 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑗 → ((2 · 𝑖) − 1) = ((2 · 𝑗) − 1)) |
371 | 370 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑗 ∈ (1...𝑘) ∧ 𝑖 = 𝑗) → ((2 · 𝑖) − 1) = ((2 · 𝑗) − 1)) |
372 | | id 22 |
. . . . . . . . 9
⊢ (𝑗 ∈ (1...𝑘) → 𝑗 ∈ (1...𝑘)) |
373 | | ovex 6577 |
. . . . . . . . . 10
⊢ ((2
· 𝑗) − 1)
∈ V |
374 | 373 | a1i 11 |
. . . . . . . . 9
⊢ (𝑗 ∈ (1...𝑘) → ((2 · 𝑗) − 1) ∈ V) |
375 | 368, 371,
372, 374 | fvmptd 6197 |
. . . . . . . 8
⊢ (𝑗 ∈ (1...𝑘) → ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑗) = ((2 · 𝑗) − 1)) |
376 | 375 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑘)) → ((𝑖 ∈ (1...𝑘) ↦ ((2 · 𝑖) − 1))‘𝑗) = ((2 · 𝑗) − 1)) |
377 | | eleq1 2676 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑖 → (𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ}) ↔ 𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈
ℕ}))) |
378 | 377 | anbi2d 736 |
. . . . . . . . 9
⊢ (𝑗 = 𝑖 → (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) ↔ ((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})))) |
379 | 142 | eleq1d 2672 |
. . . . . . . . 9
⊢ (𝑗 = 𝑖 → ((𝐹‘𝑗) ∈ ℂ ↔ (𝐹‘𝑖) ∈ ℂ)) |
380 | 378, 379 | imbi12d 333 |
. . . . . . . 8
⊢ (𝑗 = 𝑖 → ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (𝐹‘𝑗) ∈ ℂ) ↔ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (𝐹‘𝑖) ∈ ℂ))) |
381 | 380, 139 | chvarv 2251 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})) → (𝐹‘𝑖) ∈ ℂ) |
382 | 146, 147,
367, 376, 381 | fsumf1o 14301 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑖 ∈ ((1...((2 · 𝑘) − 1)) ∖ {𝑛 ∈ ℕ ∣ (𝑛 / 2) ∈ ℕ})(𝐹‘𝑖) = Σ𝑗 ∈ (1...𝑘)(𝐹‘((2 · 𝑗) − 1))) |
383 | 97, 145, 382 | 3eqtrrd 2649 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...𝑘)(𝐹‘((2 · 𝑗) − 1)) = Σ𝑗 ∈ (1...((2 · 𝑘) − 1))(𝐹‘𝑗)) |
384 | | ovex 6577 |
. . . . . . . . . 10
⊢ ((2
· 𝑘) − 1)
∈ V |
385 | 20 | fvmpt2 6200 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ∧ ((2
· 𝑘) − 1)
∈ V) → ((𝑘 ∈
ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) = ((2 · 𝑘) − 1)) |
386 | 384, 385 | mpan2 703 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((2
· 𝑘) −
1))‘𝑘) = ((2 ·
𝑘) −
1)) |
387 | 386 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ →
(1...((𝑘 ∈ ℕ
↦ ((2 · 𝑘)
− 1))‘𝑘)) =
(1...((2 · 𝑘)
− 1))) |
388 | 387 | eqcomd 2616 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → (1...((2
· 𝑘) − 1)) =
(1...((𝑘 ∈ ℕ
↦ ((2 · 𝑘)
− 1))‘𝑘))) |
389 | 388 | sumeq1d 14279 |
. . . . . 6
⊢ (𝑘 ∈ ℕ →
Σ𝑗 ∈ (1...((2
· 𝑘) −
1))(𝐹‘𝑗) = Σ𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))(𝐹‘𝑗)) |
390 | 389 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...((2 · 𝑘) − 1))(𝐹‘𝑗) = Σ𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))(𝐹‘𝑗)) |
391 | 383, 390 | eqtrd 2644 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...𝑘)(𝐹‘((2 · 𝑗) − 1)) = Σ𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))(𝐹‘𝑗)) |
392 | | elfznn 12241 |
. . . . . . 7
⊢ (𝑗 ∈ (1...𝑘) → 𝑗 ∈ ℕ) |
393 | 392 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑘)) → 𝑗 ∈ ℕ) |
394 | 12 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑘)) → 𝐹:ℕ⟶ℂ) |
395 | 30 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ (1...𝑘) → 2 ∈ ℤ) |
396 | | elfzelz 12213 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ (1...𝑘) → 𝑗 ∈ ℤ) |
397 | 395, 396 | zmulcld 11364 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ (1...𝑘) → (2 · 𝑗) ∈ ℤ) |
398 | | 1zzd 11285 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ (1...𝑘) → 1 ∈ ℤ) |
399 | 397, 398 | zsubcld 11363 |
. . . . . . . . . 10
⊢ (𝑗 ∈ (1...𝑘) → ((2 · 𝑗) − 1) ∈ ℤ) |
400 | | 0red 9920 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ (1...𝑘) → 0 ∈ ℝ) |
401 | 38 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (1...𝑘) → 2 ∈ ℝ) |
402 | 24, 401 | syl5eqel 2692 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ (1...𝑘) → (2 · 1) ∈
ℝ) |
403 | | 1red 9934 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ (1...𝑘) → 1 ∈ ℝ) |
404 | 402, 403 | resubcld 10337 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ (1...𝑘) → ((2 · 1) − 1) ∈
ℝ) |
405 | 399 | zred 11358 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ (1...𝑘) → ((2 · 𝑗) − 1) ∈ ℝ) |
406 | | 0lt1 10429 |
. . . . . . . . . . . 12
⊢ 0 <
1 |
407 | 157 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ (1...𝑘) → 1 = ((2 · 1) −
1)) |
408 | 406, 407 | syl5breq 4620 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ (1...𝑘) → 0 < ((2 · 1) −
1)) |
409 | 397 | zred 11358 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ (1...𝑘) → (2 · 𝑗) ∈ ℝ) |
410 | 392 | nnred 10912 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (1...𝑘) → 𝑗 ∈ ℝ) |
411 | 165 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (1...𝑘) → 0 ≤ 2) |
412 | | elfzle1 12215 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (1...𝑘) → 1 ≤ 𝑗) |
413 | 403, 410,
401, 411, 412 | lemul2ad 10843 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ (1...𝑘) → (2 · 1) ≤ (2 ·
𝑗)) |
414 | 402, 409,
403, 413 | lesub1dd 10522 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ (1...𝑘) → ((2 · 1) − 1) ≤ ((2
· 𝑗) −
1)) |
415 | 400, 404,
405, 408, 414 | ltletrd 10076 |
. . . . . . . . . 10
⊢ (𝑗 ∈ (1...𝑘) → 0 < ((2 · 𝑗) − 1)) |
416 | | elnnz 11264 |
. . . . . . . . . 10
⊢ (((2
· 𝑗) − 1)
∈ ℕ ↔ (((2 · 𝑗) − 1) ∈ ℤ ∧ 0 < ((2
· 𝑗) −
1))) |
417 | 399, 415,
416 | sylanbrc 695 |
. . . . . . . . 9
⊢ (𝑗 ∈ (1...𝑘) → ((2 · 𝑗) − 1) ∈ ℕ) |
418 | 417 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑘)) → ((2 · 𝑗) − 1) ∈ ℕ) |
419 | 394, 418 | ffvelrnd 6268 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑘)) → (𝐹‘((2 · 𝑗) − 1)) ∈
ℂ) |
420 | 419 | adantlr 747 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑘)) → (𝐹‘((2 · 𝑗) − 1)) ∈
ℂ) |
421 | 59 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑘 = 𝑗 → (𝐹‘((2 · 𝑘) − 1)) = (𝐹‘((2 · 𝑗) − 1))) |
422 | 421 | cbvmptv 4678 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))) = (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1))) |
423 | 422 | fvmpt2 6200 |
. . . . . 6
⊢ ((𝑗 ∈ ℕ ∧ (𝐹‘((2 · 𝑗) − 1)) ∈ ℂ)
→ ((𝑘 ∈ ℕ
↦ (𝐹‘((2
· 𝑘) −
1)))‘𝑗) = (𝐹‘((2 · 𝑗) − 1))) |
424 | 393, 420,
423 | syl2anc 691 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑘)) → ((𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))‘𝑗) = (𝐹‘((2 · 𝑗) − 1))) |
425 | | simpr 476 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ) |
426 | 425, 8 | syl6eleq 2698 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈
(ℤ≥‘1)) |
427 | 424, 426,
420 | fsumser 14308 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...𝑘)(𝐹‘((2 · 𝑗) − 1)) = (seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))))‘𝑘)) |
428 | | eqidd 2611 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))) → (𝐹‘𝑗) = (𝐹‘𝑗)) |
429 | 159 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → (2
· 1) ∈ ℝ) |
430 | | 1red 9934 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → 1 ∈
ℝ) |
431 | 165 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → 0 ≤
2) |
432 | | nnge1 10923 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → 1 ≤
𝑘) |
433 | 430, 40, 39, 431, 432 | lemul2ad 10843 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → (2
· 1) ≤ (2 · 𝑘)) |
434 | 429, 41, 430, 433 | lesub1dd 10522 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → ((2
· 1) − 1) ≤ ((2 · 𝑘) − 1)) |
435 | 157, 434 | syl5eqbr 4618 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → 1 ≤
((2 · 𝑘) −
1)) |
436 | | eluz2 11569 |
. . . . . . . 8
⊢ (((2
· 𝑘) − 1)
∈ (ℤ≥‘1) ↔ (1 ∈ ℤ ∧ ((2
· 𝑘) − 1)
∈ ℤ ∧ 1 ≤ ((2 · 𝑘) − 1))) |
437 | 36, 67, 435, 436 | syl3anbrc 1239 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → ((2
· 𝑘) − 1)
∈ (ℤ≥‘1)) |
438 | 69, 437 | eqeltrd 2688 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((2
· 𝑘) −
1))‘𝑘) ∈
(ℤ≥‘1)) |
439 | 438 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘) ∈
(ℤ≥‘1)) |
440 | | simpll 786 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))) → 𝜑) |
441 | | simpr 476 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2
· 𝑘) −
1))‘𝑘))) → 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2
· 𝑘) −
1))‘𝑘))) |
442 | 387 | adantr 480 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2
· 𝑘) −
1))‘𝑘))) →
(1...((𝑘 ∈ ℕ
↦ ((2 · 𝑘)
− 1))‘𝑘)) =
(1...((2 · 𝑘)
− 1))) |
443 | 441, 442 | eleqtrd 2690 |
. . . . . . 7
⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2
· 𝑘) −
1))‘𝑘))) → 𝑗 ∈ (1...((2 · 𝑘) − 1))) |
444 | 443 | adantll 746 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))) → 𝑗 ∈ (1...((2 · 𝑘) − 1))) |
445 | 440, 444,
95 | syl2anc 691 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))) → (𝐹‘𝑗) ∈ ℂ) |
446 | 428, 439,
445 | fsumser 14308 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...((𝑘 ∈ ℕ ↦ ((2
· 𝑘) −
1))‘𝑘))(𝐹‘𝑗) = (seq1( + , 𝐹)‘((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))) |
447 | 391, 427,
446 | 3eqtr3d 2652 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))))‘𝑘) = (seq1( + , 𝐹)‘((𝑘 ∈ ℕ ↦ ((2 · 𝑘) − 1))‘𝑘))) |
448 | 1, 2, 6, 7, 8, 9, 11, 15, 16, 29, 75, 77, 447 | climsuse 38675 |
. 2
⊢ (𝜑 → seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ 𝐵) |
449 | | eqidd 2611 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
450 | 8, 9, 449, 13 | isum 14297 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ ℕ (𝐹‘𝑘) = ( ⇝ ‘seq1( + , 𝐹))) |
451 | | climrel 14071 |
. . . . . . 7
⊢ Rel
⇝ |
452 | 451 | releldmi 5283 |
. . . . . 6
⊢ (seq1( +
, 𝐹) ⇝ 𝐵 → seq1( + , 𝐹) ∈ dom ⇝
) |
453 | 16, 452 | syl 17 |
. . . . 5
⊢ (𝜑 → seq1( + , 𝐹) ∈ dom ⇝
) |
454 | | climdm 14133 |
. . . . 5
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
↔ seq1( + , 𝐹) ⇝
( ⇝ ‘seq1( + , 𝐹))) |
455 | 453, 454 | sylib 207 |
. . . 4
⊢ (𝜑 → seq1( + , 𝐹) ⇝ ( ⇝ ‘seq1(
+ , 𝐹))) |
456 | | climuni 14131 |
. . . 4
⊢ ((seq1( +
, 𝐹) ⇝ ( ⇝
‘seq1( + , 𝐹)) ∧
seq1( + , 𝐹) ⇝ 𝐵) → ( ⇝ ‘seq1(
+ , 𝐹)) = 𝐵) |
457 | 455, 16, 456 | syl2anc 691 |
. . 3
⊢ (𝜑 → ( ⇝ ‘seq1( + ,
𝐹)) = 𝐵) |
458 | 451 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → Rel ⇝
) |
459 | | releldm 5279 |
. . . . . . . 8
⊢ ((Rel
⇝ ∧ seq1( + , (𝑘
∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ 𝐵) → seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ∈ dom ⇝
) |
460 | 458, 448,
459 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ∈ dom
⇝ ) |
461 | | climdm 14133 |
. . . . . . 7
⊢ (seq1( +
, (𝑘 ∈ ℕ ↦
(𝐹‘((2 · 𝑘) − 1)))) ∈ dom
⇝ ↔ seq1( + , (𝑘
∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ ( ⇝
‘seq1( + , (𝑘 ∈
ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))))) |
462 | 460, 461 | sylib 207 |
. . . . . 6
⊢ (𝜑 → seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ (
⇝ ‘seq1( + , (𝑘
∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))))) |
463 | 422 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1))) = (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1)))) |
464 | 463 | seqeq3d 12671 |
. . . . . . 7
⊢ (𝜑 → seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) = seq1( + ,
(𝑗 ∈ ℕ ↦
(𝐹‘((2 · 𝑗) −
1))))) |
465 | 464 | fveq2d 6107 |
. . . . . 6
⊢ (𝜑 → ( ⇝ ‘seq1( + ,
(𝑘 ∈ ℕ ↦
(𝐹‘((2 · 𝑘) − 1))))) = ( ⇝
‘seq1( + , (𝑗 ∈
ℕ ↦ (𝐹‘((2 · 𝑗) − 1)))))) |
466 | 462, 465 | breqtrd 4609 |
. . . . 5
⊢ (𝜑 → seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ (
⇝ ‘seq1( + , (𝑗
∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1)))))) |
467 | | climuni 14131 |
. . . . 5
⊢ ((seq1( +
, (𝑘 ∈ ℕ ↦
(𝐹‘((2 · 𝑘) − 1)))) ⇝ 𝐵 ∧ seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ (
⇝ ‘seq1( + , (𝑗
∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1)))))) → 𝐵 = ( ⇝ ‘seq1( + , (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) −
1)))))) |
468 | 448, 466,
467 | syl2anc 691 |
. . . 4
⊢ (𝜑 → 𝐵 = ( ⇝ ‘seq1( + , (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) −
1)))))) |
469 | | eqidd 2611 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1))) = (𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1)))) |
470 | | eqcom 2617 |
. . . . . . . 8
⊢ (𝑘 = 𝑗 ↔ 𝑗 = 𝑘) |
471 | | eqcom 2617 |
. . . . . . . 8
⊢ ((𝐹‘((2 · 𝑘) − 1)) = (𝐹‘((2 · 𝑗) − 1)) ↔ (𝐹‘((2 · 𝑗) − 1)) = (𝐹‘((2 · 𝑘) − 1))) |
472 | 421, 470,
471 | 3imtr3i 279 |
. . . . . . 7
⊢ (𝑗 = 𝑘 → (𝐹‘((2 · 𝑗) − 1)) = (𝐹‘((2 · 𝑘) − 1))) |
473 | 472 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 = 𝑘) → (𝐹‘((2 · 𝑗) − 1)) = (𝐹‘((2 · 𝑘) − 1))) |
474 | 12 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐹:ℕ⟶ℂ) |
475 | 437, 8 | syl6eleqr 2699 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → ((2
· 𝑘) − 1)
∈ ℕ) |
476 | 475 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) − 1) ∈
ℕ) |
477 | 474, 476 | ffvelrnd 6268 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘((2 · 𝑘) − 1)) ∈
ℂ) |
478 | 469, 473,
425, 477 | fvmptd 6197 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (𝐹‘((2 · 𝑗) − 1)))‘𝑘) = (𝐹‘((2 · 𝑘) − 1))) |
479 | 8, 9, 478, 477 | isum 14297 |
. . . 4
⊢ (𝜑 → Σ𝑘 ∈ ℕ (𝐹‘((2 · 𝑘) − 1)) = ( ⇝ ‘seq1( + ,
(𝑗 ∈ ℕ ↦
(𝐹‘((2 · 𝑗) −
1)))))) |
480 | 468, 479 | eqtr4d 2647 |
. . 3
⊢ (𝜑 → 𝐵 = Σ𝑘 ∈ ℕ (𝐹‘((2 · 𝑘) − 1))) |
481 | 450, 457,
480 | 3eqtrd 2648 |
. 2
⊢ (𝜑 → Σ𝑘 ∈ ℕ (𝐹‘𝑘) = Σ𝑘 ∈ ℕ (𝐹‘((2 · 𝑘) − 1))) |
482 | 448, 481 | jca 553 |
1
⊢ (𝜑 → (seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ 𝐵 ∧ Σ𝑘 ∈ ℕ (𝐹‘𝑘) = Σ𝑘 ∈ ℕ (𝐹‘((2 · 𝑘) − 1)))) |