| Step | Hyp | Ref
| Expression |
| 1 | | isumsplit.1 |
. 2
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 2 | | isumsplit.3 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ 𝑍) |
| 3 | 2, 1 | eleqtrdi 2851 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
| 4 | | eluzel2 12883 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
| 5 | 3, 4 | syl 17 |
. 2
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 6 | | isumsplit.4 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴) |
| 7 | | isumsplit.5 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) |
| 8 | | isumsplit.2 |
. . 3
⊢ 𝑊 =
(ℤ≥‘𝑁) |
| 9 | | eluzelz 12888 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
| 10 | 3, 9 | syl 17 |
. . 3
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 11 | | uzss 12901 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (ℤ≥‘𝑁) ⊆
(ℤ≥‘𝑀)) |
| 12 | 3, 11 | syl 17 |
. . . . . . 7
⊢ (𝜑 →
(ℤ≥‘𝑁) ⊆
(ℤ≥‘𝑀)) |
| 13 | 12, 8, 1 | 3sstr4g 4037 |
. . . . . 6
⊢ (𝜑 → 𝑊 ⊆ 𝑍) |
| 14 | 13 | sselda 3983 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → 𝑘 ∈ 𝑍) |
| 15 | 14, 6 | syldan 591 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘𝑘) = 𝐴) |
| 16 | 14, 7 | syldan 591 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → 𝐴 ∈ ℂ) |
| 17 | | isumsplit.6 |
. . . . 5
⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) |
| 18 | 6, 7 | eqeltrd 2841 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) |
| 19 | 1, 2, 18 | iserex 15693 |
. . . . 5
⊢ (𝜑 → (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ seq𝑁( + , 𝐹) ∈ dom ⇝ )) |
| 20 | 17, 19 | mpbid 232 |
. . . 4
⊢ (𝜑 → seq𝑁( + , 𝐹) ∈ dom ⇝ ) |
| 21 | 8, 10, 15, 16, 20 | isumclim2 15794 |
. . 3
⊢ (𝜑 → seq𝑁( + , 𝐹) ⇝ Σ𝑘 ∈ 𝑊 𝐴) |
| 22 | | fzfid 14014 |
. . . 4
⊢ (𝜑 → (𝑀...(𝑁 − 1)) ∈ Fin) |
| 23 | | elfzuz 13560 |
. . . . . 6
⊢ (𝑘 ∈ (𝑀...(𝑁 − 1)) → 𝑘 ∈ (ℤ≥‘𝑀)) |
| 24 | 23, 1 | eleqtrrdi 2852 |
. . . . 5
⊢ (𝑘 ∈ (𝑀...(𝑁 − 1)) → 𝑘 ∈ 𝑍) |
| 25 | 24, 7 | sylan2 593 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → 𝐴 ∈ ℂ) |
| 26 | 22, 25 | fsumcl 15769 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 ∈ ℂ) |
| 27 | 14, 18 | syldan 591 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘𝑘) ∈ ℂ) |
| 28 | 8, 10, 27 | serf 14071 |
. . . 4
⊢ (𝜑 → seq𝑁( + , 𝐹):𝑊⟶ℂ) |
| 29 | 28 | ffvelcdmda 7104 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (seq𝑁( + , 𝐹)‘𝑗) ∈ ℂ) |
| 30 | 5 | zred 12722 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ ℝ) |
| 31 | 30 | ltm1d 12200 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑀 − 1) < 𝑀) |
| 32 | | peano2zm 12660 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℤ → (𝑀 − 1) ∈
ℤ) |
| 33 | | fzn 13580 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ (𝑀 − 1) ∈ ℤ)
→ ((𝑀 − 1) <
𝑀 ↔ (𝑀...(𝑀 − 1)) = ∅)) |
| 34 | 5, 32, 33 | syl2anc2 585 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑀 − 1) < 𝑀 ↔ (𝑀...(𝑀 − 1)) = ∅)) |
| 35 | 31, 34 | mpbid 232 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀...(𝑀 − 1)) = ∅) |
| 36 | 35 | sumeq1d 15736 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(𝑀 − 1))𝐴 = Σ𝑘 ∈ ∅ 𝐴) |
| 37 | 36 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → Σ𝑘 ∈ (𝑀...(𝑀 − 1))𝐴 = Σ𝑘 ∈ ∅ 𝐴) |
| 38 | | sum0 15757 |
. . . . . . . 8
⊢
Σ𝑘 ∈
∅ 𝐴 =
0 |
| 39 | 37, 38 | eqtrdi 2793 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → Σ𝑘 ∈ (𝑀...(𝑀 − 1))𝐴 = 0) |
| 40 | 39 | oveq1d 7446 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (Σ𝑘 ∈ (𝑀...(𝑀 − 1))𝐴 + (seq𝑀( + , 𝐹)‘𝑗)) = (0 + (seq𝑀( + , 𝐹)‘𝑗))) |
| 41 | 13 | sselda 3983 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → 𝑗 ∈ 𝑍) |
| 42 | 1, 5, 18 | serf 14071 |
. . . . . . . . 9
⊢ (𝜑 → seq𝑀( + , 𝐹):𝑍⟶ℂ) |
| 43 | 42 | ffvelcdmda 7104 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (seq𝑀( + , 𝐹)‘𝑗) ∈ ℂ) |
| 44 | 41, 43 | syldan 591 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (seq𝑀( + , 𝐹)‘𝑗) ∈ ℂ) |
| 45 | 44 | addlidd 11462 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (0 + (seq𝑀( + , 𝐹)‘𝑗)) = (seq𝑀( + , 𝐹)‘𝑗)) |
| 46 | 40, 45 | eqtr2d 2778 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (seq𝑀( + , 𝐹)‘𝑗) = (Σ𝑘 ∈ (𝑀...(𝑀 − 1))𝐴 + (seq𝑀( + , 𝐹)‘𝑗))) |
| 47 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑁 = 𝑀 → (𝑁 − 1) = (𝑀 − 1)) |
| 48 | 47 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑁 = 𝑀 → (𝑀...(𝑁 − 1)) = (𝑀...(𝑀 − 1))) |
| 49 | 48 | sumeq1d 15736 |
. . . . . . 7
⊢ (𝑁 = 𝑀 → Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 = Σ𝑘 ∈ (𝑀...(𝑀 − 1))𝐴) |
| 50 | | seqeq1 14045 |
. . . . . . . 8
⊢ (𝑁 = 𝑀 → seq𝑁( + , 𝐹) = seq𝑀( + , 𝐹)) |
| 51 | 50 | fveq1d 6908 |
. . . . . . 7
⊢ (𝑁 = 𝑀 → (seq𝑁( + , 𝐹)‘𝑗) = (seq𝑀( + , 𝐹)‘𝑗)) |
| 52 | 49, 51 | oveq12d 7449 |
. . . . . 6
⊢ (𝑁 = 𝑀 → (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + (seq𝑁( + , 𝐹)‘𝑗)) = (Σ𝑘 ∈ (𝑀...(𝑀 − 1))𝐴 + (seq𝑀( + , 𝐹)‘𝑗))) |
| 53 | 52 | eqeq2d 2748 |
. . . . 5
⊢ (𝑁 = 𝑀 → ((seq𝑀( + , 𝐹)‘𝑗) = (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + (seq𝑁( + , 𝐹)‘𝑗)) ↔ (seq𝑀( + , 𝐹)‘𝑗) = (Σ𝑘 ∈ (𝑀...(𝑀 − 1))𝐴 + (seq𝑀( + , 𝐹)‘𝑗)))) |
| 54 | 46, 53 | syl5ibrcom 247 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (𝑁 = 𝑀 → (seq𝑀( + , 𝐹)‘𝑗) = (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + (seq𝑁( + , 𝐹)‘𝑗)))) |
| 55 | | addcl 11237 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (𝑘 + 𝑚) ∈ ℂ) |
| 56 | 55 | adantl 481 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) ∧ (𝑘 ∈ ℂ ∧ 𝑚 ∈ ℂ)) → (𝑘 + 𝑚) ∈ ℂ) |
| 57 | | addass 11242 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ) → ((𝑘 + 𝑚) + 𝑥) = (𝑘 + (𝑚 + 𝑥))) |
| 58 | 57 | adantl 481 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) ∧ (𝑘 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → ((𝑘 + 𝑚) + 𝑥) = (𝑘 + (𝑚 + 𝑥))) |
| 59 | | simplr 769 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑗 ∈ 𝑊) |
| 60 | | simpll 767 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝜑) |
| 61 | 10 | zcnd 12723 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℂ) |
| 62 | | ax-1cn 11213 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
| 63 | | npcan 11517 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 −
1) + 1) = 𝑁) |
| 64 | 61, 62, 63 | sylancl 586 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) |
| 65 | 64 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 = ((𝑁 − 1) + 1)) |
| 66 | 60, 65 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑁 = ((𝑁 − 1) + 1)) |
| 67 | 66 | fveq2d 6910 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) →
(ℤ≥‘𝑁) = (ℤ≥‘((𝑁 − 1) +
1))) |
| 68 | 8, 67 | eqtrid 2789 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑊 = (ℤ≥‘((𝑁 − 1) +
1))) |
| 69 | 59, 68 | eleqtrd 2843 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑗 ∈
(ℤ≥‘((𝑁 − 1) + 1))) |
| 70 | 5 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → 𝑀 ∈ ℤ) |
| 71 | | eluzp1m1 12904 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → (𝑁 − 1) ∈
(ℤ≥‘𝑀)) |
| 72 | 70, 71 | sylan 580 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑁 − 1) ∈
(ℤ≥‘𝑀)) |
| 73 | | elfzuz 13560 |
. . . . . . . . 9
⊢ (𝑘 ∈ (𝑀...𝑗) → 𝑘 ∈ (ℤ≥‘𝑀)) |
| 74 | 73, 1 | eleqtrrdi 2852 |
. . . . . . . 8
⊢ (𝑘 ∈ (𝑀...𝑗) → 𝑘 ∈ 𝑍) |
| 75 | 60, 74, 18 | syl2an 596 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) ∧ 𝑘 ∈ (𝑀...𝑗)) → (𝐹‘𝑘) ∈ ℂ) |
| 76 | 56, 58, 69, 72, 75 | seqsplit 14076 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (seq𝑀( + , 𝐹)‘𝑗) = ((seq𝑀( + , 𝐹)‘(𝑁 − 1)) + (seq((𝑁 − 1) + 1)( + , 𝐹)‘𝑗))) |
| 77 | 60, 24, 6 | syl2an 596 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘𝑘) = 𝐴) |
| 78 | 60, 24, 7 | syl2an 596 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → 𝐴 ∈ ℂ) |
| 79 | 77, 72, 78 | fsumser 15766 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 = (seq𝑀( + , 𝐹)‘(𝑁 − 1))) |
| 80 | 66 | seqeq1d 14048 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → seq𝑁( + , 𝐹) = seq((𝑁 − 1) + 1)( + , 𝐹)) |
| 81 | 80 | fveq1d 6908 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (seq𝑁( + , 𝐹)‘𝑗) = (seq((𝑁 − 1) + 1)( + , 𝐹)‘𝑗)) |
| 82 | 79, 81 | oveq12d 7449 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + (seq𝑁( + , 𝐹)‘𝑗)) = ((seq𝑀( + , 𝐹)‘(𝑁 − 1)) + (seq((𝑁 − 1) + 1)( + , 𝐹)‘𝑗))) |
| 83 | 76, 82 | eqtr4d 2780 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (seq𝑀( + , 𝐹)‘𝑗) = (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + (seq𝑁( + , 𝐹)‘𝑗))) |
| 84 | 83 | ex 412 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (𝑁 ∈ (ℤ≥‘(𝑀 + 1)) → (seq𝑀( + , 𝐹)‘𝑗) = (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + (seq𝑁( + , 𝐹)‘𝑗)))) |
| 85 | | uzp1 12919 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑁 = 𝑀 ∨ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) |
| 86 | 3, 85 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑁 = 𝑀 ∨ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) |
| 87 | 86 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (𝑁 = 𝑀 ∨ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) |
| 88 | 54, 84, 87 | mpjaod 861 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (seq𝑀( + , 𝐹)‘𝑗) = (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + (seq𝑁( + , 𝐹)‘𝑗))) |
| 89 | 8, 10, 21, 26, 17, 29, 88 | climaddc2 15672 |
. 2
⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + Σ𝑘 ∈ 𝑊 𝐴)) |
| 90 | 1, 5, 6, 7, 89 | isumclim 15793 |
1
⊢ (𝜑 → Σ𝑘 ∈ 𝑍 𝐴 = (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + Σ𝑘 ∈ 𝑊 𝐴)) |