Step | Hyp | Ref
| Expression |
1 | | isumsplit.1 |
. 2
⊢ 𝑍 =
(ℤ≥‘𝑀) |
2 | | isumsplit.3 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ 𝑍) |
3 | 2, 1 | eleqtrdi 2270 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
4 | | eluzel2 9522 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
5 | 3, 4 | syl 14 |
. 2
⊢ (𝜑 → 𝑀 ∈ ℤ) |
6 | | isumsplit.4 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴) |
7 | | isumsplit.5 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) |
8 | | isumsplit.2 |
. . 3
⊢ 𝑊 =
(ℤ≥‘𝑁) |
9 | | eluzelz 9526 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
10 | 3, 9 | syl 14 |
. . 3
⊢ (𝜑 → 𝑁 ∈ ℤ) |
11 | | uzss 9537 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (ℤ≥‘𝑁) ⊆
(ℤ≥‘𝑀)) |
12 | 3, 11 | syl 14 |
. . . . . . 7
⊢ (𝜑 →
(ℤ≥‘𝑁) ⊆
(ℤ≥‘𝑀)) |
13 | 12, 8, 1 | 3sstr4g 3198 |
. . . . . 6
⊢ (𝜑 → 𝑊 ⊆ 𝑍) |
14 | 13 | sselda 3155 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → 𝑘 ∈ 𝑍) |
15 | 14, 6 | syldan 282 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘𝑘) = 𝐴) |
16 | 14, 7 | syldan 282 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → 𝐴 ∈ ℂ) |
17 | | isumsplit.6 |
. . . . 5
⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) |
18 | 6, 7 | eqeltrd 2254 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) |
19 | 1, 2, 18 | iserex 11331 |
. . . . 5
⊢ (𝜑 → (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ seq𝑁( + , 𝐹) ∈ dom ⇝ )) |
20 | 17, 19 | mpbid 147 |
. . . 4
⊢ (𝜑 → seq𝑁( + , 𝐹) ∈ dom ⇝ ) |
21 | 8, 10, 15, 16, 20 | isumclim2 11414 |
. . 3
⊢ (𝜑 → seq𝑁( + , 𝐹) ⇝ Σ𝑘 ∈ 𝑊 𝐴) |
22 | | peano2zm 9280 |
. . . . . 6
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
23 | 10, 22 | syl 14 |
. . . . 5
⊢ (𝜑 → (𝑁 − 1) ∈ ℤ) |
24 | 5, 23 | fzfigd 10417 |
. . . 4
⊢ (𝜑 → (𝑀...(𝑁 − 1)) ∈ Fin) |
25 | | elfzuz 10007 |
. . . . . 6
⊢ (𝑘 ∈ (𝑀...(𝑁 − 1)) → 𝑘 ∈ (ℤ≥‘𝑀)) |
26 | 25, 1 | eleqtrrdi 2271 |
. . . . 5
⊢ (𝑘 ∈ (𝑀...(𝑁 − 1)) → 𝑘 ∈ 𝑍) |
27 | 26, 7 | sylan2 286 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → 𝐴 ∈ ℂ) |
28 | 24, 27 | fsumcl 11392 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 ∈ ℂ) |
29 | 14, 18 | syldan 282 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘𝑘) ∈ ℂ) |
30 | 8, 10, 29 | serf 10460 |
. . . 4
⊢ (𝜑 → seq𝑁( + , 𝐹):𝑊⟶ℂ) |
31 | 30 | ffvelcdmda 5647 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (seq𝑁( + , 𝐹)‘𝑗) ∈ ℂ) |
32 | 5 | zred 9364 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ ℝ) |
33 | 32 | ltm1d 8878 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑀 − 1) < 𝑀) |
34 | | peano2zm 9280 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℤ → (𝑀 − 1) ∈
ℤ) |
35 | 5, 34 | syl 14 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑀 − 1) ∈ ℤ) |
36 | | fzn 10028 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ (𝑀 − 1) ∈ ℤ)
→ ((𝑀 − 1) <
𝑀 ↔ (𝑀...(𝑀 − 1)) = ∅)) |
37 | 5, 35, 36 | syl2anc 411 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑀 − 1) < 𝑀 ↔ (𝑀...(𝑀 − 1)) = ∅)) |
38 | 33, 37 | mpbid 147 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀...(𝑀 − 1)) = ∅) |
39 | 38 | sumeq1d 11358 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(𝑀 − 1))𝐴 = Σ𝑘 ∈ ∅ 𝐴) |
40 | 39 | adantr 276 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → Σ𝑘 ∈ (𝑀...(𝑀 − 1))𝐴 = Σ𝑘 ∈ ∅ 𝐴) |
41 | | sum0 11380 |
. . . . . . . 8
⊢
Σ𝑘 ∈
∅ 𝐴 =
0 |
42 | 40, 41 | eqtrdi 2226 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → Σ𝑘 ∈ (𝑀...(𝑀 − 1))𝐴 = 0) |
43 | 42 | oveq1d 5884 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (Σ𝑘 ∈ (𝑀...(𝑀 − 1))𝐴 + (seq𝑀( + , 𝐹)‘𝑗)) = (0 + (seq𝑀( + , 𝐹)‘𝑗))) |
44 | 13 | sselda 3155 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → 𝑗 ∈ 𝑍) |
45 | 1, 5, 18 | serf 10460 |
. . . . . . . . 9
⊢ (𝜑 → seq𝑀( + , 𝐹):𝑍⟶ℂ) |
46 | 45 | ffvelcdmda 5647 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (seq𝑀( + , 𝐹)‘𝑗) ∈ ℂ) |
47 | 44, 46 | syldan 282 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (seq𝑀( + , 𝐹)‘𝑗) ∈ ℂ) |
48 | 47 | addid2d 8097 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (0 + (seq𝑀( + , 𝐹)‘𝑗)) = (seq𝑀( + , 𝐹)‘𝑗)) |
49 | 43, 48 | eqtr2d 2211 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (seq𝑀( + , 𝐹)‘𝑗) = (Σ𝑘 ∈ (𝑀...(𝑀 − 1))𝐴 + (seq𝑀( + , 𝐹)‘𝑗))) |
50 | | oveq1 5876 |
. . . . . . . . 9
⊢ (𝑁 = 𝑀 → (𝑁 − 1) = (𝑀 − 1)) |
51 | 50 | oveq2d 5885 |
. . . . . . . 8
⊢ (𝑁 = 𝑀 → (𝑀...(𝑁 − 1)) = (𝑀...(𝑀 − 1))) |
52 | 51 | sumeq1d 11358 |
. . . . . . 7
⊢ (𝑁 = 𝑀 → Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 = Σ𝑘 ∈ (𝑀...(𝑀 − 1))𝐴) |
53 | | seqeq1 10434 |
. . . . . . . 8
⊢ (𝑁 = 𝑀 → seq𝑁( + , 𝐹) = seq𝑀( + , 𝐹)) |
54 | 53 | fveq1d 5513 |
. . . . . . 7
⊢ (𝑁 = 𝑀 → (seq𝑁( + , 𝐹)‘𝑗) = (seq𝑀( + , 𝐹)‘𝑗)) |
55 | 52, 54 | oveq12d 5887 |
. . . . . 6
⊢ (𝑁 = 𝑀 → (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + (seq𝑁( + , 𝐹)‘𝑗)) = (Σ𝑘 ∈ (𝑀...(𝑀 − 1))𝐴 + (seq𝑀( + , 𝐹)‘𝑗))) |
56 | 55 | eqeq2d 2189 |
. . . . 5
⊢ (𝑁 = 𝑀 → ((seq𝑀( + , 𝐹)‘𝑗) = (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + (seq𝑁( + , 𝐹)‘𝑗)) ↔ (seq𝑀( + , 𝐹)‘𝑗) = (Σ𝑘 ∈ (𝑀...(𝑀 − 1))𝐴 + (seq𝑀( + , 𝐹)‘𝑗)))) |
57 | 49, 56 | syl5ibrcom 157 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (𝑁 = 𝑀 → (seq𝑀( + , 𝐹)‘𝑗) = (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + (seq𝑁( + , 𝐹)‘𝑗)))) |
58 | | addcl 7927 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (𝑘 + 𝑚) ∈ ℂ) |
59 | 58 | adantl 277 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) ∧ (𝑘 ∈ ℂ ∧ 𝑚 ∈ ℂ)) → (𝑘 + 𝑚) ∈ ℂ) |
60 | | addass 7932 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ) → ((𝑘 + 𝑚) + 𝑥) = (𝑘 + (𝑚 + 𝑥))) |
61 | 60 | adantl 277 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) ∧ (𝑘 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → ((𝑘 + 𝑚) + 𝑥) = (𝑘 + (𝑚 + 𝑥))) |
62 | | simplr 528 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑗 ∈ 𝑊) |
63 | | simpll 527 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝜑) |
64 | 10 | zcnd 9365 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℂ) |
65 | | ax-1cn 7895 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
66 | | npcan 8156 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 −
1) + 1) = 𝑁) |
67 | 64, 65, 66 | sylancl 413 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) |
68 | 67 | eqcomd 2183 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 = ((𝑁 − 1) + 1)) |
69 | 63, 68 | syl 14 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑁 = ((𝑁 − 1) + 1)) |
70 | 69 | fveq2d 5515 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) →
(ℤ≥‘𝑁) = (ℤ≥‘((𝑁 − 1) +
1))) |
71 | 8, 70 | eqtrid 2222 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑊 = (ℤ≥‘((𝑁 − 1) +
1))) |
72 | 62, 71 | eleqtrd 2256 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑗 ∈
(ℤ≥‘((𝑁 − 1) + 1))) |
73 | 5 | adantr 276 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → 𝑀 ∈ ℤ) |
74 | | eluzp1m1 9540 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → (𝑁 − 1) ∈
(ℤ≥‘𝑀)) |
75 | 73, 74 | sylan 283 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑁 − 1) ∈
(ℤ≥‘𝑀)) |
76 | 1 | eleq2i 2244 |
. . . . . . . . . 10
⊢ (𝑘 ∈ 𝑍 ↔ 𝑘 ∈ (ℤ≥‘𝑀)) |
77 | 76, 6 | sylan2br 288 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) = 𝐴) |
78 | 63, 77 | sylan 283 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) = 𝐴) |
79 | 76, 7 | sylan2br 288 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → 𝐴 ∈ ℂ) |
80 | 63, 79 | sylan 283 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → 𝐴 ∈ ℂ) |
81 | 78, 80 | eqeltrd 2254 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℂ) |
82 | 59, 61, 72, 75, 81 | seq3split 10465 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (seq𝑀( + , 𝐹)‘𝑗) = ((seq𝑀( + , 𝐹)‘(𝑁 − 1)) + (seq((𝑁 − 1) + 1)( + , 𝐹)‘𝑗))) |
83 | 78, 75, 80 | fsum3ser 11389 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 = (seq𝑀( + , 𝐹)‘(𝑁 − 1))) |
84 | 69 | seqeq1d 10437 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → seq𝑁( + , 𝐹) = seq((𝑁 − 1) + 1)( + , 𝐹)) |
85 | 84 | fveq1d 5513 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (seq𝑁( + , 𝐹)‘𝑗) = (seq((𝑁 − 1) + 1)( + , 𝐹)‘𝑗)) |
86 | 83, 85 | oveq12d 5887 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + (seq𝑁( + , 𝐹)‘𝑗)) = ((seq𝑀( + , 𝐹)‘(𝑁 − 1)) + (seq((𝑁 − 1) + 1)( + , 𝐹)‘𝑗))) |
87 | 82, 86 | eqtr4d 2213 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (seq𝑀( + , 𝐹)‘𝑗) = (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + (seq𝑁( + , 𝐹)‘𝑗))) |
88 | 87 | ex 115 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (𝑁 ∈ (ℤ≥‘(𝑀 + 1)) → (seq𝑀( + , 𝐹)‘𝑗) = (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + (seq𝑁( + , 𝐹)‘𝑗)))) |
89 | | uzp1 9550 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑁 = 𝑀 ∨ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) |
90 | 3, 89 | syl 14 |
. . . . 5
⊢ (𝜑 → (𝑁 = 𝑀 ∨ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) |
91 | 90 | adantr 276 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (𝑁 = 𝑀 ∨ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) |
92 | 57, 88, 91 | mpjaod 718 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (seq𝑀( + , 𝐹)‘𝑗) = (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + (seq𝑁( + , 𝐹)‘𝑗))) |
93 | 8, 10, 21, 28, 17, 31, 92 | climaddc2 11322 |
. 2
⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + Σ𝑘 ∈ 𝑊 𝐴)) |
94 | 1, 5, 6, 7, 93 | isumclim 11413 |
1
⊢ (𝜑 → Σ𝑘 ∈ 𝑍 𝐴 = (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + Σ𝑘 ∈ 𝑊 𝐴)) |