Step | Hyp | Ref
| Expression |
1 | | isumsplit.1 |
. 2
⊢ 𝑍 =
(ℤ≥‘𝑀) |
2 | | isumsplit.3 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ 𝑍) |
3 | 2, 1 | syl6eleq 2916 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
4 | | eluzel2 11973 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
5 | 3, 4 | syl 17 |
. 2
⊢ (𝜑 → 𝑀 ∈ ℤ) |
6 | | isumsplit.4 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴) |
7 | | isumsplit.5 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) |
8 | | isumsplit.2 |
. . 3
⊢ 𝑊 =
(ℤ≥‘𝑁) |
9 | | eluzelz 11978 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
10 | 3, 9 | syl 17 |
. . 3
⊢ (𝜑 → 𝑁 ∈ ℤ) |
11 | | uzss 11989 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (ℤ≥‘𝑁) ⊆
(ℤ≥‘𝑀)) |
12 | 3, 11 | syl 17 |
. . . . . . 7
⊢ (𝜑 →
(ℤ≥‘𝑁) ⊆
(ℤ≥‘𝑀)) |
13 | 12, 8, 1 | 3sstr4g 3871 |
. . . . . 6
⊢ (𝜑 → 𝑊 ⊆ 𝑍) |
14 | 13 | sselda 3827 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → 𝑘 ∈ 𝑍) |
15 | 14, 6 | syldan 585 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘𝑘) = 𝐴) |
16 | 14, 7 | syldan 585 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → 𝐴 ∈ ℂ) |
17 | | isumsplit.6 |
. . . . 5
⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) |
18 | 6, 7 | eqeltrd 2906 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) |
19 | 1, 2, 18 | iserex 14764 |
. . . . 5
⊢ (𝜑 → (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ seq𝑁( + , 𝐹) ∈ dom ⇝ )) |
20 | 17, 19 | mpbid 224 |
. . . 4
⊢ (𝜑 → seq𝑁( + , 𝐹) ∈ dom ⇝ ) |
21 | 8, 10, 15, 16, 20 | isumclim2 14864 |
. . 3
⊢ (𝜑 → seq𝑁( + , 𝐹) ⇝ Σ𝑘 ∈ 𝑊 𝐴) |
22 | | fzfid 13067 |
. . . 4
⊢ (𝜑 → (𝑀...(𝑁 − 1)) ∈ Fin) |
23 | | elfzuz 12631 |
. . . . . 6
⊢ (𝑘 ∈ (𝑀...(𝑁 − 1)) → 𝑘 ∈ (ℤ≥‘𝑀)) |
24 | 23, 1 | syl6eleqr 2917 |
. . . . 5
⊢ (𝑘 ∈ (𝑀...(𝑁 − 1)) → 𝑘 ∈ 𝑍) |
25 | 24, 7 | sylan2 586 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → 𝐴 ∈ ℂ) |
26 | 22, 25 | fsumcl 14841 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 ∈ ℂ) |
27 | 14, 18 | syldan 585 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘𝑘) ∈ ℂ) |
28 | 8, 10, 27 | serf 13123 |
. . . 4
⊢ (𝜑 → seq𝑁( + , 𝐹):𝑊⟶ℂ) |
29 | 28 | ffvelrnda 6608 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (seq𝑁( + , 𝐹)‘𝑗) ∈ ℂ) |
30 | 5 | zred 11810 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ ℝ) |
31 | 30 | ltm1d 11286 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑀 − 1) < 𝑀) |
32 | | peano2zm 11748 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℤ → (𝑀 − 1) ∈
ℤ) |
33 | 5, 32 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑀 − 1) ∈ ℤ) |
34 | | fzn 12650 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ (𝑀 − 1) ∈ ℤ)
→ ((𝑀 − 1) <
𝑀 ↔ (𝑀...(𝑀 − 1)) = ∅)) |
35 | 5, 33, 34 | syl2anc 579 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑀 − 1) < 𝑀 ↔ (𝑀...(𝑀 − 1)) = ∅)) |
36 | 31, 35 | mpbid 224 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀...(𝑀 − 1)) = ∅) |
37 | 36 | sumeq1d 14808 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(𝑀 − 1))𝐴 = Σ𝑘 ∈ ∅ 𝐴) |
38 | 37 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → Σ𝑘 ∈ (𝑀...(𝑀 − 1))𝐴 = Σ𝑘 ∈ ∅ 𝐴) |
39 | | sum0 14829 |
. . . . . . . 8
⊢
Σ𝑘 ∈
∅ 𝐴 =
0 |
40 | 38, 39 | syl6eq 2877 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → Σ𝑘 ∈ (𝑀...(𝑀 − 1))𝐴 = 0) |
41 | 40 | oveq1d 6920 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (Σ𝑘 ∈ (𝑀...(𝑀 − 1))𝐴 + (seq𝑀( + , 𝐹)‘𝑗)) = (0 + (seq𝑀( + , 𝐹)‘𝑗))) |
42 | 13 | sselda 3827 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → 𝑗 ∈ 𝑍) |
43 | 1, 5, 18 | serf 13123 |
. . . . . . . . 9
⊢ (𝜑 → seq𝑀( + , 𝐹):𝑍⟶ℂ) |
44 | 43 | ffvelrnda 6608 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (seq𝑀( + , 𝐹)‘𝑗) ∈ ℂ) |
45 | 42, 44 | syldan 585 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (seq𝑀( + , 𝐹)‘𝑗) ∈ ℂ) |
46 | 45 | addid2d 10556 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (0 + (seq𝑀( + , 𝐹)‘𝑗)) = (seq𝑀( + , 𝐹)‘𝑗)) |
47 | 41, 46 | eqtr2d 2862 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (seq𝑀( + , 𝐹)‘𝑗) = (Σ𝑘 ∈ (𝑀...(𝑀 − 1))𝐴 + (seq𝑀( + , 𝐹)‘𝑗))) |
48 | | oveq1 6912 |
. . . . . . . . 9
⊢ (𝑁 = 𝑀 → (𝑁 − 1) = (𝑀 − 1)) |
49 | 48 | oveq2d 6921 |
. . . . . . . 8
⊢ (𝑁 = 𝑀 → (𝑀...(𝑁 − 1)) = (𝑀...(𝑀 − 1))) |
50 | 49 | sumeq1d 14808 |
. . . . . . 7
⊢ (𝑁 = 𝑀 → Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 = Σ𝑘 ∈ (𝑀...(𝑀 − 1))𝐴) |
51 | | seqeq1 13098 |
. . . . . . . 8
⊢ (𝑁 = 𝑀 → seq𝑁( + , 𝐹) = seq𝑀( + , 𝐹)) |
52 | 51 | fveq1d 6435 |
. . . . . . 7
⊢ (𝑁 = 𝑀 → (seq𝑁( + , 𝐹)‘𝑗) = (seq𝑀( + , 𝐹)‘𝑗)) |
53 | 50, 52 | oveq12d 6923 |
. . . . . 6
⊢ (𝑁 = 𝑀 → (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + (seq𝑁( + , 𝐹)‘𝑗)) = (Σ𝑘 ∈ (𝑀...(𝑀 − 1))𝐴 + (seq𝑀( + , 𝐹)‘𝑗))) |
54 | 53 | eqeq2d 2835 |
. . . . 5
⊢ (𝑁 = 𝑀 → ((seq𝑀( + , 𝐹)‘𝑗) = (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + (seq𝑁( + , 𝐹)‘𝑗)) ↔ (seq𝑀( + , 𝐹)‘𝑗) = (Σ𝑘 ∈ (𝑀...(𝑀 − 1))𝐴 + (seq𝑀( + , 𝐹)‘𝑗)))) |
55 | 47, 54 | syl5ibrcom 239 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (𝑁 = 𝑀 → (seq𝑀( + , 𝐹)‘𝑗) = (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + (seq𝑁( + , 𝐹)‘𝑗)))) |
56 | | addcl 10334 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (𝑘 + 𝑚) ∈ ℂ) |
57 | 56 | adantl 475 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) ∧ (𝑘 ∈ ℂ ∧ 𝑚 ∈ ℂ)) → (𝑘 + 𝑚) ∈ ℂ) |
58 | | addass 10339 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ) → ((𝑘 + 𝑚) + 𝑥) = (𝑘 + (𝑚 + 𝑥))) |
59 | 58 | adantl 475 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) ∧ (𝑘 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → ((𝑘 + 𝑚) + 𝑥) = (𝑘 + (𝑚 + 𝑥))) |
60 | | simplr 785 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑗 ∈ 𝑊) |
61 | | simpll 783 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝜑) |
62 | 10 | zcnd 11811 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℂ) |
63 | | ax-1cn 10310 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
64 | | npcan 10611 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 −
1) + 1) = 𝑁) |
65 | 62, 63, 64 | sylancl 580 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) |
66 | 65 | eqcomd 2831 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 = ((𝑁 − 1) + 1)) |
67 | 61, 66 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑁 = ((𝑁 − 1) + 1)) |
68 | 67 | fveq2d 6437 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) →
(ℤ≥‘𝑁) = (ℤ≥‘((𝑁 − 1) +
1))) |
69 | 8, 68 | syl5eq 2873 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑊 = (ℤ≥‘((𝑁 − 1) +
1))) |
70 | 60, 69 | eleqtrd 2908 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑗 ∈
(ℤ≥‘((𝑁 − 1) + 1))) |
71 | 5 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → 𝑀 ∈ ℤ) |
72 | | eluzp1m1 11992 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → (𝑁 − 1) ∈
(ℤ≥‘𝑀)) |
73 | 71, 72 | sylan 575 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑁 − 1) ∈
(ℤ≥‘𝑀)) |
74 | | elfzuz 12631 |
. . . . . . . . 9
⊢ (𝑘 ∈ (𝑀...𝑗) → 𝑘 ∈ (ℤ≥‘𝑀)) |
75 | 74, 1 | syl6eleqr 2917 |
. . . . . . . 8
⊢ (𝑘 ∈ (𝑀...𝑗) → 𝑘 ∈ 𝑍) |
76 | 61, 75, 18 | syl2an 589 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) ∧ 𝑘 ∈ (𝑀...𝑗)) → (𝐹‘𝑘) ∈ ℂ) |
77 | 57, 59, 70, 73, 76 | seqsplit 13128 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (seq𝑀( + , 𝐹)‘𝑗) = ((seq𝑀( + , 𝐹)‘(𝑁 − 1)) + (seq((𝑁 − 1) + 1)( + , 𝐹)‘𝑗))) |
78 | 61, 24, 6 | syl2an 589 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘𝑘) = 𝐴) |
79 | 61, 24, 7 | syl2an 589 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → 𝐴 ∈ ℂ) |
80 | 78, 73, 79 | fsumser 14838 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 = (seq𝑀( + , 𝐹)‘(𝑁 − 1))) |
81 | 67 | seqeq1d 13101 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → seq𝑁( + , 𝐹) = seq((𝑁 − 1) + 1)( + , 𝐹)) |
82 | 81 | fveq1d 6435 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (seq𝑁( + , 𝐹)‘𝑗) = (seq((𝑁 − 1) + 1)( + , 𝐹)‘𝑗)) |
83 | 80, 82 | oveq12d 6923 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + (seq𝑁( + , 𝐹)‘𝑗)) = ((seq𝑀( + , 𝐹)‘(𝑁 − 1)) + (seq((𝑁 − 1) + 1)( + , 𝐹)‘𝑗))) |
84 | 77, 83 | eqtr4d 2864 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (seq𝑀( + , 𝐹)‘𝑗) = (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + (seq𝑁( + , 𝐹)‘𝑗))) |
85 | 84 | ex 403 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (𝑁 ∈ (ℤ≥‘(𝑀 + 1)) → (seq𝑀( + , 𝐹)‘𝑗) = (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + (seq𝑁( + , 𝐹)‘𝑗)))) |
86 | | uzp1 12003 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑁 = 𝑀 ∨ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) |
87 | 3, 86 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑁 = 𝑀 ∨ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) |
88 | 87 | adantr 474 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (𝑁 = 𝑀 ∨ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) |
89 | 55, 85, 88 | mpjaod 891 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (seq𝑀( + , 𝐹)‘𝑗) = (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + (seq𝑁( + , 𝐹)‘𝑗))) |
90 | 8, 10, 21, 26, 17, 29, 89 | climaddc2 14743 |
. 2
⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + Σ𝑘 ∈ 𝑊 𝐴)) |
91 | 1, 5, 6, 7, 90 | isumclim 14863 |
1
⊢ (𝜑 → Σ𝑘 ∈ 𝑍 𝐴 = (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + Σ𝑘 ∈ 𝑊 𝐴)) |