Step | Hyp | Ref
| Expression |
1 | | isumsplit.1 |
. 2
⊢ 𝑍 =
(ℤ≥‘𝑀) |
2 | | isumsplit.3 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ 𝑍) |
3 | 2, 1 | eleqtrdi 2257 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
4 | | eluzel2 9465 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
5 | 3, 4 | syl 14 |
. 2
⊢ (𝜑 → 𝑀 ∈ ℤ) |
6 | | isumsplit.4 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴) |
7 | | isumsplit.5 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) |
8 | | isumsplit.2 |
. . 3
⊢ 𝑊 =
(ℤ≥‘𝑁) |
9 | | eluzelz 9469 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
10 | 3, 9 | syl 14 |
. . 3
⊢ (𝜑 → 𝑁 ∈ ℤ) |
11 | | uzss 9480 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (ℤ≥‘𝑁) ⊆
(ℤ≥‘𝑀)) |
12 | 3, 11 | syl 14 |
. . . . . . 7
⊢ (𝜑 →
(ℤ≥‘𝑁) ⊆
(ℤ≥‘𝑀)) |
13 | 12, 8, 1 | 3sstr4g 3183 |
. . . . . 6
⊢ (𝜑 → 𝑊 ⊆ 𝑍) |
14 | 13 | sselda 3140 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → 𝑘 ∈ 𝑍) |
15 | 14, 6 | syldan 280 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘𝑘) = 𝐴) |
16 | 14, 7 | syldan 280 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → 𝐴 ∈ ℂ) |
17 | | isumsplit.6 |
. . . . 5
⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) |
18 | 6, 7 | eqeltrd 2241 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) |
19 | 1, 2, 18 | iserex 11274 |
. . . . 5
⊢ (𝜑 → (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ seq𝑁( + , 𝐹) ∈ dom ⇝ )) |
20 | 17, 19 | mpbid 146 |
. . . 4
⊢ (𝜑 → seq𝑁( + , 𝐹) ∈ dom ⇝ ) |
21 | 8, 10, 15, 16, 20 | isumclim2 11357 |
. . 3
⊢ (𝜑 → seq𝑁( + , 𝐹) ⇝ Σ𝑘 ∈ 𝑊 𝐴) |
22 | | peano2zm 9223 |
. . . . . 6
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
23 | 10, 22 | syl 14 |
. . . . 5
⊢ (𝜑 → (𝑁 − 1) ∈ ℤ) |
24 | 5, 23 | fzfigd 10360 |
. . . 4
⊢ (𝜑 → (𝑀...(𝑁 − 1)) ∈ Fin) |
25 | | elfzuz 9950 |
. . . . . 6
⊢ (𝑘 ∈ (𝑀...(𝑁 − 1)) → 𝑘 ∈ (ℤ≥‘𝑀)) |
26 | 25, 1 | eleqtrrdi 2258 |
. . . . 5
⊢ (𝑘 ∈ (𝑀...(𝑁 − 1)) → 𝑘 ∈ 𝑍) |
27 | 26, 7 | sylan2 284 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → 𝐴 ∈ ℂ) |
28 | 24, 27 | fsumcl 11335 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 ∈ ℂ) |
29 | 14, 18 | syldan 280 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘𝑘) ∈ ℂ) |
30 | 8, 10, 29 | serf 10403 |
. . . 4
⊢ (𝜑 → seq𝑁( + , 𝐹):𝑊⟶ℂ) |
31 | 30 | ffvelrnda 5617 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (seq𝑁( + , 𝐹)‘𝑗) ∈ ℂ) |
32 | 5 | zred 9307 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ ℝ) |
33 | 32 | ltm1d 8821 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑀 − 1) < 𝑀) |
34 | | peano2zm 9223 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℤ → (𝑀 − 1) ∈
ℤ) |
35 | 5, 34 | syl 14 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑀 − 1) ∈ ℤ) |
36 | | fzn 9971 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ (𝑀 − 1) ∈ ℤ)
→ ((𝑀 − 1) <
𝑀 ↔ (𝑀...(𝑀 − 1)) = ∅)) |
37 | 5, 35, 36 | syl2anc 409 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑀 − 1) < 𝑀 ↔ (𝑀...(𝑀 − 1)) = ∅)) |
38 | 33, 37 | mpbid 146 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀...(𝑀 − 1)) = ∅) |
39 | 38 | sumeq1d 11301 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(𝑀 − 1))𝐴 = Σ𝑘 ∈ ∅ 𝐴) |
40 | 39 | adantr 274 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → Σ𝑘 ∈ (𝑀...(𝑀 − 1))𝐴 = Σ𝑘 ∈ ∅ 𝐴) |
41 | | sum0 11323 |
. . . . . . . 8
⊢
Σ𝑘 ∈
∅ 𝐴 =
0 |
42 | 40, 41 | eqtrdi 2213 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → Σ𝑘 ∈ (𝑀...(𝑀 − 1))𝐴 = 0) |
43 | 42 | oveq1d 5854 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (Σ𝑘 ∈ (𝑀...(𝑀 − 1))𝐴 + (seq𝑀( + , 𝐹)‘𝑗)) = (0 + (seq𝑀( + , 𝐹)‘𝑗))) |
44 | 13 | sselda 3140 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → 𝑗 ∈ 𝑍) |
45 | 1, 5, 18 | serf 10403 |
. . . . . . . . 9
⊢ (𝜑 → seq𝑀( + , 𝐹):𝑍⟶ℂ) |
46 | 45 | ffvelrnda 5617 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (seq𝑀( + , 𝐹)‘𝑗) ∈ ℂ) |
47 | 44, 46 | syldan 280 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (seq𝑀( + , 𝐹)‘𝑗) ∈ ℂ) |
48 | 47 | addid2d 8042 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (0 + (seq𝑀( + , 𝐹)‘𝑗)) = (seq𝑀( + , 𝐹)‘𝑗)) |
49 | 43, 48 | eqtr2d 2198 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (seq𝑀( + , 𝐹)‘𝑗) = (Σ𝑘 ∈ (𝑀...(𝑀 − 1))𝐴 + (seq𝑀( + , 𝐹)‘𝑗))) |
50 | | oveq1 5846 |
. . . . . . . . 9
⊢ (𝑁 = 𝑀 → (𝑁 − 1) = (𝑀 − 1)) |
51 | 50 | oveq2d 5855 |
. . . . . . . 8
⊢ (𝑁 = 𝑀 → (𝑀...(𝑁 − 1)) = (𝑀...(𝑀 − 1))) |
52 | 51 | sumeq1d 11301 |
. . . . . . 7
⊢ (𝑁 = 𝑀 → Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 = Σ𝑘 ∈ (𝑀...(𝑀 − 1))𝐴) |
53 | | seqeq1 10377 |
. . . . . . . 8
⊢ (𝑁 = 𝑀 → seq𝑁( + , 𝐹) = seq𝑀( + , 𝐹)) |
54 | 53 | fveq1d 5485 |
. . . . . . 7
⊢ (𝑁 = 𝑀 → (seq𝑁( + , 𝐹)‘𝑗) = (seq𝑀( + , 𝐹)‘𝑗)) |
55 | 52, 54 | oveq12d 5857 |
. . . . . 6
⊢ (𝑁 = 𝑀 → (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + (seq𝑁( + , 𝐹)‘𝑗)) = (Σ𝑘 ∈ (𝑀...(𝑀 − 1))𝐴 + (seq𝑀( + , 𝐹)‘𝑗))) |
56 | 55 | eqeq2d 2176 |
. . . . 5
⊢ (𝑁 = 𝑀 → ((seq𝑀( + , 𝐹)‘𝑗) = (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + (seq𝑁( + , 𝐹)‘𝑗)) ↔ (seq𝑀( + , 𝐹)‘𝑗) = (Σ𝑘 ∈ (𝑀...(𝑀 − 1))𝐴 + (seq𝑀( + , 𝐹)‘𝑗)))) |
57 | 49, 56 | syl5ibrcom 156 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (𝑁 = 𝑀 → (seq𝑀( + , 𝐹)‘𝑗) = (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + (seq𝑁( + , 𝐹)‘𝑗)))) |
58 | | addcl 7872 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (𝑘 + 𝑚) ∈ ℂ) |
59 | 58 | adantl 275 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) ∧ (𝑘 ∈ ℂ ∧ 𝑚 ∈ ℂ)) → (𝑘 + 𝑚) ∈ ℂ) |
60 | | addass 7877 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ) → ((𝑘 + 𝑚) + 𝑥) = (𝑘 + (𝑚 + 𝑥))) |
61 | 60 | adantl 275 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) ∧ (𝑘 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → ((𝑘 + 𝑚) + 𝑥) = (𝑘 + (𝑚 + 𝑥))) |
62 | | simplr 520 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑗 ∈ 𝑊) |
63 | | simpll 519 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝜑) |
64 | 10 | zcnd 9308 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℂ) |
65 | | ax-1cn 7840 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
66 | | npcan 8101 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 −
1) + 1) = 𝑁) |
67 | 64, 65, 66 | sylancl 410 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) |
68 | 67 | eqcomd 2170 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 = ((𝑁 − 1) + 1)) |
69 | 63, 68 | syl 14 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑁 = ((𝑁 − 1) + 1)) |
70 | 69 | fveq2d 5487 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) →
(ℤ≥‘𝑁) = (ℤ≥‘((𝑁 − 1) +
1))) |
71 | 8, 70 | syl5eq 2209 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑊 = (ℤ≥‘((𝑁 − 1) +
1))) |
72 | 62, 71 | eleqtrd 2243 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑗 ∈
(ℤ≥‘((𝑁 − 1) + 1))) |
73 | 5 | adantr 274 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → 𝑀 ∈ ℤ) |
74 | | eluzp1m1 9483 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → (𝑁 − 1) ∈
(ℤ≥‘𝑀)) |
75 | 73, 74 | sylan 281 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑁 − 1) ∈
(ℤ≥‘𝑀)) |
76 | 1 | eleq2i 2231 |
. . . . . . . . . 10
⊢ (𝑘 ∈ 𝑍 ↔ 𝑘 ∈ (ℤ≥‘𝑀)) |
77 | 76, 6 | sylan2br 286 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) = 𝐴) |
78 | 63, 77 | sylan 281 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) = 𝐴) |
79 | 76, 7 | sylan2br 286 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → 𝐴 ∈ ℂ) |
80 | 63, 79 | sylan 281 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → 𝐴 ∈ ℂ) |
81 | 78, 80 | eqeltrd 2241 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℂ) |
82 | 59, 61, 72, 75, 81 | seq3split 10408 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (seq𝑀( + , 𝐹)‘𝑗) = ((seq𝑀( + , 𝐹)‘(𝑁 − 1)) + (seq((𝑁 − 1) + 1)( + , 𝐹)‘𝑗))) |
83 | 78, 75, 80 | fsum3ser 11332 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 = (seq𝑀( + , 𝐹)‘(𝑁 − 1))) |
84 | 69 | seqeq1d 10380 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → seq𝑁( + , 𝐹) = seq((𝑁 − 1) + 1)( + , 𝐹)) |
85 | 84 | fveq1d 5485 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (seq𝑁( + , 𝐹)‘𝑗) = (seq((𝑁 − 1) + 1)( + , 𝐹)‘𝑗)) |
86 | 83, 85 | oveq12d 5857 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + (seq𝑁( + , 𝐹)‘𝑗)) = ((seq𝑀( + , 𝐹)‘(𝑁 − 1)) + (seq((𝑁 − 1) + 1)( + , 𝐹)‘𝑗))) |
87 | 82, 86 | eqtr4d 2200 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (seq𝑀( + , 𝐹)‘𝑗) = (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + (seq𝑁( + , 𝐹)‘𝑗))) |
88 | 87 | ex 114 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (𝑁 ∈ (ℤ≥‘(𝑀 + 1)) → (seq𝑀( + , 𝐹)‘𝑗) = (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + (seq𝑁( + , 𝐹)‘𝑗)))) |
89 | | uzp1 9493 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑁 = 𝑀 ∨ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) |
90 | 3, 89 | syl 14 |
. . . . 5
⊢ (𝜑 → (𝑁 = 𝑀 ∨ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) |
91 | 90 | adantr 274 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (𝑁 = 𝑀 ∨ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) |
92 | 57, 88, 91 | mpjaod 708 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (seq𝑀( + , 𝐹)‘𝑗) = (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + (seq𝑁( + , 𝐹)‘𝑗))) |
93 | 8, 10, 21, 28, 17, 31, 92 | climaddc2 11265 |
. 2
⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + Σ𝑘 ∈ 𝑊 𝐴)) |
94 | 1, 5, 6, 7, 93 | isumclim 11356 |
1
⊢ (𝜑 → Σ𝑘 ∈ 𝑍 𝐴 = (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + Σ𝑘 ∈ 𝑊 𝐴)) |