Proof of Theorem fsumparts
Step | Hyp | Ref
| Expression |
1 | | sum0 14299 |
. . . 4
⊢
Σ𝑗 ∈
∅ (𝐵 · (𝑋 − 𝑊)) = 0 |
2 | | 0m0e0 11007 |
. . . 4
⊢ (0
− 0) = 0 |
3 | 1, 2 | eqtr4i 2635 |
. . 3
⊢
Σ𝑗 ∈
∅ (𝐵 · (𝑋 − 𝑊)) = (0 − 0) |
4 | | simpr 476 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 = 𝑀) → 𝑁 = 𝑀) |
5 | 4 | oveq2d 6565 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 = 𝑀) → (𝑀..^𝑁) = (𝑀..^𝑀)) |
6 | | fzo0 12361 |
. . . . 5
⊢ (𝑀..^𝑀) = ∅ |
7 | 5, 6 | syl6eq 2660 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 = 𝑀) → (𝑀..^𝑁) = ∅) |
8 | 7 | sumeq1d 14279 |
. . 3
⊢ ((𝜑 ∧ 𝑁 = 𝑀) → Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 · (𝑋 − 𝑊)) = Σ𝑗 ∈ ∅ (𝐵 · (𝑋 − 𝑊))) |
9 | | fsumparts.1 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
10 | | eluzfz1 12219 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁)) |
11 | 9, 10 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ (𝑀...𝑁)) |
12 | | eqtr3 2631 |
. . . . . . . . . . . 12
⊢ ((𝑘 = 𝑀 ∧ 𝑁 = 𝑀) → 𝑘 = 𝑁) |
13 | | fsumparts.e |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑁 → (𝐴 = 𝐸 ∧ 𝑉 = 𝑍)) |
14 | | oveq12 6558 |
. . . . . . . . . . . 12
⊢ ((𝐴 = 𝐸 ∧ 𝑉 = 𝑍) → (𝐴 · 𝑉) = (𝐸 · 𝑍)) |
15 | 12, 13, 14 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((𝑘 = 𝑀 ∧ 𝑁 = 𝑀) → (𝐴 · 𝑉) = (𝐸 · 𝑍)) |
16 | | fsumparts.d |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑀 → (𝐴 = 𝐷 ∧ 𝑉 = 𝑌)) |
17 | | oveq12 6558 |
. . . . . . . . . . . . 13
⊢ ((𝐴 = 𝐷 ∧ 𝑉 = 𝑌) → (𝐴 · 𝑉) = (𝐷 · 𝑌)) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑀 → (𝐴 · 𝑉) = (𝐷 · 𝑌)) |
19 | 18 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑘 = 𝑀 ∧ 𝑁 = 𝑀) → (𝐴 · 𝑉) = (𝐷 · 𝑌)) |
20 | 15, 19 | eqeq12d 2625 |
. . . . . . . . . 10
⊢ ((𝑘 = 𝑀 ∧ 𝑁 = 𝑀) → ((𝐴 · 𝑉) = (𝐴 · 𝑉) ↔ (𝐸 · 𝑍) = (𝐷 · 𝑌))) |
21 | 20 | pm5.74da 719 |
. . . . . . . . 9
⊢ (𝑘 = 𝑀 → ((𝑁 = 𝑀 → (𝐴 · 𝑉) = (𝐴 · 𝑉)) ↔ (𝑁 = 𝑀 → (𝐸 · 𝑍) = (𝐷 · 𝑌)))) |
22 | | eqidd 2611 |
. . . . . . . . 9
⊢ (𝑁 = 𝑀 → (𝐴 · 𝑉) = (𝐴 · 𝑉)) |
23 | 21, 22 | vtoclg 3239 |
. . . . . . . 8
⊢ (𝑀 ∈ (𝑀...𝑁) → (𝑁 = 𝑀 → (𝐸 · 𝑍) = (𝐷 · 𝑌))) |
24 | 23 | imp 444 |
. . . . . . 7
⊢ ((𝑀 ∈ (𝑀...𝑁) ∧ 𝑁 = 𝑀) → (𝐸 · 𝑍) = (𝐷 · 𝑌)) |
25 | 11, 24 | sylan 487 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 = 𝑀) → (𝐸 · 𝑍) = (𝐷 · 𝑌)) |
26 | 25 | oveq1d 6564 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 = 𝑀) → ((𝐸 · 𝑍) − (𝐷 · 𝑌)) = ((𝐷 · 𝑌) − (𝐷 · 𝑌))) |
27 | | fsumparts.2 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ) |
28 | 27 | ralrimiva 2949 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑘 ∈ (𝑀...𝑁)𝐴 ∈ ℂ) |
29 | 16 | simpld 474 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑀 → 𝐴 = 𝐷) |
30 | 29 | eleq1d 2672 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑀 → (𝐴 ∈ ℂ ↔ 𝐷 ∈ ℂ)) |
31 | 30 | rspcv 3278 |
. . . . . . . . 9
⊢ (𝑀 ∈ (𝑀...𝑁) → (∀𝑘 ∈ (𝑀...𝑁)𝐴 ∈ ℂ → 𝐷 ∈ ℂ)) |
32 | 11, 28, 31 | sylc 63 |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ∈ ℂ) |
33 | | fsumparts.3 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝑉 ∈ ℂ) |
34 | 33 | ralrimiva 2949 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑘 ∈ (𝑀...𝑁)𝑉 ∈ ℂ) |
35 | 16 | simprd 478 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑀 → 𝑉 = 𝑌) |
36 | 35 | eleq1d 2672 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑀 → (𝑉 ∈ ℂ ↔ 𝑌 ∈ ℂ)) |
37 | 36 | rspcv 3278 |
. . . . . . . . 9
⊢ (𝑀 ∈ (𝑀...𝑁) → (∀𝑘 ∈ (𝑀...𝑁)𝑉 ∈ ℂ → 𝑌 ∈ ℂ)) |
38 | 11, 34, 37 | sylc 63 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ ℂ) |
39 | 32, 38 | mulcld 9939 |
. . . . . . 7
⊢ (𝜑 → (𝐷 · 𝑌) ∈ ℂ) |
40 | 39 | subidd 10259 |
. . . . . 6
⊢ (𝜑 → ((𝐷 · 𝑌) − (𝐷 · 𝑌)) = 0) |
41 | 40 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 = 𝑀) → ((𝐷 · 𝑌) − (𝐷 · 𝑌)) = 0) |
42 | 26, 41 | eqtrd 2644 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 = 𝑀) → ((𝐸 · 𝑍) − (𝐷 · 𝑌)) = 0) |
43 | 7 | sumeq1d 14279 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 = 𝑀) → Σ𝑗 ∈ (𝑀..^𝑁)((𝐶 − 𝐵) · 𝑋) = Σ𝑗 ∈ ∅ ((𝐶 − 𝐵) · 𝑋)) |
44 | | sum0 14299 |
. . . . 5
⊢
Σ𝑗 ∈
∅ ((𝐶 − 𝐵) · 𝑋) = 0 |
45 | 43, 44 | syl6eq 2660 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 = 𝑀) → Σ𝑗 ∈ (𝑀..^𝑁)((𝐶 − 𝐵) · 𝑋) = 0) |
46 | 42, 45 | oveq12d 6567 |
. . 3
⊢ ((𝜑 ∧ 𝑁 = 𝑀) → (((𝐸 · 𝑍) − (𝐷 · 𝑌)) − Σ𝑗 ∈ (𝑀..^𝑁)((𝐶 − 𝐵) · 𝑋)) = (0 − 0)) |
47 | 3, 8, 46 | 3eqtr4a 2670 |
. 2
⊢ ((𝜑 ∧ 𝑁 = 𝑀) → Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 · (𝑋 − 𝑊)) = (((𝐸 · 𝑍) − (𝐷 · 𝑌)) − Σ𝑗 ∈ (𝑀..^𝑁)((𝐶 − 𝐵) · 𝑋))) |
48 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) |
49 | | eluzel2 11568 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
50 | 9, 49 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ ℤ) |
51 | 50 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑀 ∈ ℤ) |
52 | | fzp1ss 12262 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℤ → ((𝑀 + 1)...𝑁) ⊆ (𝑀...𝑁)) |
53 | 51, 52 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝑀 + 1)...𝑁) ⊆ (𝑀...𝑁)) |
54 | 53 | sselda 3568 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) ∧ 𝑘 ∈ ((𝑀 + 1)...𝑁)) → 𝑘 ∈ (𝑀...𝑁)) |
55 | 27, 33 | mulcld 9939 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐴 · 𝑉) ∈ ℂ) |
56 | 55 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐴 · 𝑉) ∈ ℂ) |
57 | 54, 56 | syldan 486 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) ∧ 𝑘 ∈ ((𝑀 + 1)...𝑁)) → (𝐴 · 𝑉) ∈ ℂ) |
58 | 13, 14 | syl 17 |
. . . . . . . . 9
⊢ (𝑘 = 𝑁 → (𝐴 · 𝑉) = (𝐸 · 𝑍)) |
59 | 48, 57, 58 | fsumm1 14324 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → Σ𝑘 ∈ ((𝑀 + 1)...𝑁)(𝐴 · 𝑉) = (Σ𝑘 ∈ ((𝑀 + 1)...(𝑁 − 1))(𝐴 · 𝑉) + (𝐸 · 𝑍))) |
60 | | eluzelz 11573 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
61 | 9, 60 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℤ) |
62 | 61 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑁 ∈ ℤ) |
63 | | fzoval 12340 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1))) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑀..^𝑁) = (𝑀...(𝑁 − 1))) |
65 | 51 | zcnd 11359 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑀 ∈ ℂ) |
66 | | ax-1cn 9873 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
67 | | pncan 10166 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑀 + 1)
− 1) = 𝑀) |
68 | 65, 66, 67 | sylancl 693 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝑀 + 1) − 1) = 𝑀) |
69 | 68 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (((𝑀 + 1) − 1)...(𝑁 − 1)) = (𝑀...(𝑁 − 1))) |
70 | 64, 69 | eqtr4d 2647 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑀..^𝑁) = (((𝑀 + 1) − 1)...(𝑁 − 1))) |
71 | 70 | sumeq1d 14279 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → Σ𝑗 ∈ (𝑀..^𝑁)(𝐶 · 𝑋) = Σ𝑗 ∈ (((𝑀 + 1) − 1)...(𝑁 − 1))(𝐶 · 𝑋)) |
72 | | 1zzd 11285 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 1 ∈
ℤ) |
73 | 51 | peano2zd 11361 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑀 + 1) ∈
ℤ) |
74 | | fsumparts.c |
. . . . . . . . . . 11
⊢ (𝑘 = (𝑗 + 1) → (𝐴 = 𝐶 ∧ 𝑉 = 𝑋)) |
75 | | oveq12 6558 |
. . . . . . . . . . 11
⊢ ((𝐴 = 𝐶 ∧ 𝑉 = 𝑋) → (𝐴 · 𝑉) = (𝐶 · 𝑋)) |
76 | 74, 75 | syl 17 |
. . . . . . . . . 10
⊢ (𝑘 = (𝑗 + 1) → (𝐴 · 𝑉) = (𝐶 · 𝑋)) |
77 | 72, 73, 62, 57, 76 | fsumshftm 14355 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → Σ𝑘 ∈ ((𝑀 + 1)...𝑁)(𝐴 · 𝑉) = Σ𝑗 ∈ (((𝑀 + 1) − 1)...(𝑁 − 1))(𝐶 · 𝑋)) |
78 | 71, 77 | eqtr4d 2647 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → Σ𝑗 ∈ (𝑀..^𝑁)(𝐶 · 𝑋) = Σ𝑘 ∈ ((𝑀 + 1)...𝑁)(𝐴 · 𝑉)) |
79 | | fzoval 12340 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ → ((𝑀 + 1)..^𝑁) = ((𝑀 + 1)...(𝑁 − 1))) |
80 | 62, 79 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝑀 + 1)..^𝑁) = ((𝑀 + 1)...(𝑁 − 1))) |
81 | 80 | sumeq1d 14279 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)(𝐴 · 𝑉) = Σ𝑘 ∈ ((𝑀 + 1)...(𝑁 − 1))(𝐴 · 𝑉)) |
82 | 81 | oveq1d 6564 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)(𝐴 · 𝑉) + (𝐸 · 𝑍)) = (Σ𝑘 ∈ ((𝑀 + 1)...(𝑁 − 1))(𝐴 · 𝑉) + (𝐸 · 𝑍))) |
83 | 59, 78, 82 | 3eqtr4d 2654 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → Σ𝑗 ∈ (𝑀..^𝑁)(𝐶 · 𝑋) = (Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)(𝐴 · 𝑉) + (𝐸 · 𝑍))) |
84 | | fzofi 12635 |
. . . . . . . . . 10
⊢ ((𝑀 + 1)..^𝑁) ∈ Fin |
85 | 84 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝑀 + 1)..^𝑁) ∈ Fin) |
86 | | uzid 11578 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
(ℤ≥‘𝑀)) |
87 | | peano2uz 11617 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈
(ℤ≥‘𝑀) → (𝑀 + 1) ∈
(ℤ≥‘𝑀)) |
88 | | fzoss1 12364 |
. . . . . . . . . . . 12
⊢ ((𝑀 + 1) ∈
(ℤ≥‘𝑀) → ((𝑀 + 1)..^𝑁) ⊆ (𝑀..^𝑁)) |
89 | 51, 86, 87, 88 | 4syl 19 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝑀 + 1)..^𝑁) ⊆ (𝑀..^𝑁)) |
90 | 89 | sselda 3568 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ (𝑀..^𝑁)) |
91 | | elfzofz 12354 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (𝑀..^𝑁) → 𝑘 ∈ (𝑀...𝑁)) |
92 | 91, 55 | sylan2 490 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝐴 · 𝑉) ∈ ℂ) |
93 | 92 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝐴 · 𝑉) ∈ ℂ) |
94 | 90, 93 | syldan 486 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝐴 · 𝑉) ∈ ℂ) |
95 | 85, 94 | fsumcl 14311 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)(𝐴 · 𝑉) ∈ ℂ) |
96 | | eluzfz2 12220 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁)) |
97 | 9, 96 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ (𝑀...𝑁)) |
98 | 13 | simpld 474 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑁 → 𝐴 = 𝐸) |
99 | 98 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑁 → (𝐴 ∈ ℂ ↔ 𝐸 ∈ ℂ)) |
100 | 99 | rspcv 3278 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ (𝑀...𝑁) → (∀𝑘 ∈ (𝑀...𝑁)𝐴 ∈ ℂ → 𝐸 ∈ ℂ)) |
101 | 97, 28, 100 | sylc 63 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐸 ∈ ℂ) |
102 | 13 | simprd 478 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑁 → 𝑉 = 𝑍) |
103 | 102 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑁 → (𝑉 ∈ ℂ ↔ 𝑍 ∈ ℂ)) |
104 | 103 | rspcv 3278 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ (𝑀...𝑁) → (∀𝑘 ∈ (𝑀...𝑁)𝑉 ∈ ℂ → 𝑍 ∈ ℂ)) |
105 | 97, 34, 104 | sylc 63 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑍 ∈ ℂ) |
106 | 101, 105 | mulcld 9939 |
. . . . . . . . 9
⊢ (𝜑 → (𝐸 · 𝑍) ∈ ℂ) |
107 | 106 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (𝐸 · 𝑍) ∈ ℂ) |
108 | 95, 107 | addcomd 10117 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)(𝐴 · 𝑉) + (𝐸 · 𝑍)) = ((𝐸 · 𝑍) + Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)(𝐴 · 𝑉))) |
109 | 83, 108 | eqtrd 2644 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → Σ𝑗 ∈ (𝑀..^𝑁)(𝐶 · 𝑋) = ((𝐸 · 𝑍) + Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)(𝐴 · 𝑉))) |
110 | 109 | oveq1d 6564 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (Σ𝑗 ∈ (𝑀..^𝑁)(𝐶 · 𝑋) − Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 · 𝑋)) = (((𝐸 · 𝑍) + Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)(𝐴 · 𝑉)) − Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 · 𝑋))) |
111 | | fzofzp1 12431 |
. . . . . . . . . 10
⊢ (𝑗 ∈ (𝑀..^𝑁) → (𝑗 + 1) ∈ (𝑀...𝑁)) |
112 | 74 | simpld 474 |
. . . . . . . . . . . 12
⊢ (𝑘 = (𝑗 + 1) → 𝐴 = 𝐶) |
113 | 112 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝑗 + 1) → (𝐴 ∈ ℂ ↔ 𝐶 ∈ ℂ)) |
114 | 113 | rspccva 3281 |
. . . . . . . . . 10
⊢
((∀𝑘 ∈
(𝑀...𝑁)𝐴 ∈ ℂ ∧ (𝑗 + 1) ∈ (𝑀...𝑁)) → 𝐶 ∈ ℂ) |
115 | 28, 111, 114 | syl2an 493 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝐶 ∈ ℂ) |
116 | | elfzofz 12354 |
. . . . . . . . . 10
⊢ (𝑗 ∈ (𝑀..^𝑁) → 𝑗 ∈ (𝑀...𝑁)) |
117 | | fsumparts.b |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑗 → (𝐴 = 𝐵 ∧ 𝑉 = 𝑊)) |
118 | 117 | simpld 474 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑗 → 𝐴 = 𝐵) |
119 | 118 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑗 → (𝐴 ∈ ℂ ↔ 𝐵 ∈ ℂ)) |
120 | 119 | rspccva 3281 |
. . . . . . . . . 10
⊢
((∀𝑘 ∈
(𝑀...𝑁)𝐴 ∈ ℂ ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝐵 ∈ ℂ) |
121 | 28, 116, 120 | syl2an 493 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝐵 ∈ ℂ) |
122 | 74 | simprd 478 |
. . . . . . . . . . . 12
⊢ (𝑘 = (𝑗 + 1) → 𝑉 = 𝑋) |
123 | 122 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝑗 + 1) → (𝑉 ∈ ℂ ↔ 𝑋 ∈ ℂ)) |
124 | 123 | rspccva 3281 |
. . . . . . . . . 10
⊢
((∀𝑘 ∈
(𝑀...𝑁)𝑉 ∈ ℂ ∧ (𝑗 + 1) ∈ (𝑀...𝑁)) → 𝑋 ∈ ℂ) |
125 | 34, 111, 124 | syl2an 493 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝑋 ∈ ℂ) |
126 | 115, 121,
125 | subdird 10366 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → ((𝐶 − 𝐵) · 𝑋) = ((𝐶 · 𝑋) − (𝐵 · 𝑋))) |
127 | 126 | sumeq2dv 14281 |
. . . . . . 7
⊢ (𝜑 → Σ𝑗 ∈ (𝑀..^𝑁)((𝐶 − 𝐵) · 𝑋) = Σ𝑗 ∈ (𝑀..^𝑁)((𝐶 · 𝑋) − (𝐵 · 𝑋))) |
128 | | fzofi 12635 |
. . . . . . . . 9
⊢ (𝑀..^𝑁) ∈ Fin |
129 | 128 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (𝑀..^𝑁) ∈ Fin) |
130 | 115, 125 | mulcld 9939 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (𝐶 · 𝑋) ∈ ℂ) |
131 | 121, 125 | mulcld 9939 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (𝐵 · 𝑋) ∈ ℂ) |
132 | 129, 130,
131 | fsumsub 14362 |
. . . . . . 7
⊢ (𝜑 → Σ𝑗 ∈ (𝑀..^𝑁)((𝐶 · 𝑋) − (𝐵 · 𝑋)) = (Σ𝑗 ∈ (𝑀..^𝑁)(𝐶 · 𝑋) − Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 · 𝑋))) |
133 | 127, 132 | eqtrd 2644 |
. . . . . 6
⊢ (𝜑 → Σ𝑗 ∈ (𝑀..^𝑁)((𝐶 − 𝐵) · 𝑋) = (Σ𝑗 ∈ (𝑀..^𝑁)(𝐶 · 𝑋) − Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 · 𝑋))) |
134 | 133 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → Σ𝑗 ∈ (𝑀..^𝑁)((𝐶 − 𝐵) · 𝑋) = (Σ𝑗 ∈ (𝑀..^𝑁)(𝐶 · 𝑋) − Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 · 𝑋))) |
135 | 129, 131 | fsumcl 14311 |
. . . . . . 7
⊢ (𝜑 → Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 · 𝑋) ∈ ℂ) |
136 | 135 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 · 𝑋) ∈ ℂ) |
137 | 107, 136,
95 | subsub3d 10301 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝐸 · 𝑍) − (Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 · 𝑋) − Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)(𝐴 · 𝑉))) = (((𝐸 · 𝑍) + Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)(𝐴 · 𝑉)) − Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 · 𝑋))) |
138 | 110, 134,
137 | 3eqtr4d 2654 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → Σ𝑗 ∈ (𝑀..^𝑁)((𝐶 − 𝐵) · 𝑋) = ((𝐸 · 𝑍) − (Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 · 𝑋) − Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)(𝐴 · 𝑉)))) |
139 | 138 | oveq2d 6565 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (((𝐸 · 𝑍) − (𝐷 · 𝑌)) − Σ𝑗 ∈ (𝑀..^𝑁)((𝐶 − 𝐵) · 𝑋)) = (((𝐸 · 𝑍) − (𝐷 · 𝑌)) − ((𝐸 · 𝑍) − (Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 · 𝑋) − Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)(𝐴 · 𝑉))))) |
140 | 39 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (𝐷 · 𝑌) ∈ ℂ) |
141 | 136, 95 | subcld 10271 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 · 𝑋) − Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)(𝐴 · 𝑉)) ∈ ℂ) |
142 | 107, 140,
141 | nnncan1d 10305 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (((𝐸 · 𝑍) − (𝐷 · 𝑌)) − ((𝐸 · 𝑍) − (Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 · 𝑋) − Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)(𝐴 · 𝑉)))) = ((Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 · 𝑋) − Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)(𝐴 · 𝑉)) − (𝐷 · 𝑌))) |
143 | 95, 140 | addcomd 10117 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)(𝐴 · 𝑉) + (𝐷 · 𝑌)) = ((𝐷 · 𝑌) + Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)(𝐴 · 𝑉))) |
144 | | eluzp1m1 11587 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → (𝑁 − 1) ∈
(ℤ≥‘𝑀)) |
145 | 50, 144 | sylan 487 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑁 − 1) ∈
(ℤ≥‘𝑀)) |
146 | 64 | eleq2d 2673 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑘 ∈ (𝑀..^𝑁) ↔ 𝑘 ∈ (𝑀...(𝑁 − 1)))) |
147 | 146 | biimpar 501 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → 𝑘 ∈ (𝑀..^𝑁)) |
148 | 147, 93 | syldan 486 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐴 · 𝑉) ∈ ℂ) |
149 | 145, 148,
18 | fsum1p 14326 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → Σ𝑘 ∈ (𝑀...(𝑁 − 1))(𝐴 · 𝑉) = ((𝐷 · 𝑌) + Σ𝑘 ∈ ((𝑀 + 1)...(𝑁 − 1))(𝐴 · 𝑉))) |
150 | 64 | sumeq1d 14279 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → Σ𝑘 ∈ (𝑀..^𝑁)(𝐴 · 𝑉) = Σ𝑘 ∈ (𝑀...(𝑁 − 1))(𝐴 · 𝑉)) |
151 | 81 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝐷 · 𝑌) + Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)(𝐴 · 𝑉)) = ((𝐷 · 𝑌) + Σ𝑘 ∈ ((𝑀 + 1)...(𝑁 − 1))(𝐴 · 𝑉))) |
152 | 149, 150,
151 | 3eqtr4d 2654 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → Σ𝑘 ∈ (𝑀..^𝑁)(𝐴 · 𝑉) = ((𝐷 · 𝑌) + Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)(𝐴 · 𝑉))) |
153 | 143, 152 | eqtr4d 2647 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)(𝐴 · 𝑉) + (𝐷 · 𝑌)) = Σ𝑘 ∈ (𝑀..^𝑁)(𝐴 · 𝑉)) |
154 | | oveq12 6558 |
. . . . . . . 8
⊢ ((𝐴 = 𝐵 ∧ 𝑉 = 𝑊) → (𝐴 · 𝑉) = (𝐵 · 𝑊)) |
155 | 117, 154 | syl 17 |
. . . . . . 7
⊢ (𝑘 = 𝑗 → (𝐴 · 𝑉) = (𝐵 · 𝑊)) |
156 | 155 | cbvsumv 14274 |
. . . . . 6
⊢
Σ𝑘 ∈
(𝑀..^𝑁)(𝐴 · 𝑉) = Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 · 𝑊) |
157 | 153, 156 | syl6eq 2660 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)(𝐴 · 𝑉) + (𝐷 · 𝑌)) = Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 · 𝑊)) |
158 | 157 | oveq2d 6565 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 · 𝑋) − (Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)(𝐴 · 𝑉) + (𝐷 · 𝑌))) = (Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 · 𝑋) − Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 · 𝑊))) |
159 | 136, 95, 140 | subsub4d 10302 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → ((Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 · 𝑋) − Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)(𝐴 · 𝑉)) − (𝐷 · 𝑌)) = (Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 · 𝑋) − (Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)(𝐴 · 𝑉) + (𝐷 · 𝑌)))) |
160 | 117 | simprd 478 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑗 → 𝑉 = 𝑊) |
161 | 160 | eleq1d 2672 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑗 → (𝑉 ∈ ℂ ↔ 𝑊 ∈ ℂ)) |
162 | 161 | rspccva 3281 |
. . . . . . . . 9
⊢
((∀𝑘 ∈
(𝑀...𝑁)𝑉 ∈ ℂ ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝑊 ∈ ℂ) |
163 | 34, 116, 162 | syl2an 493 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝑊 ∈ ℂ) |
164 | 121, 125,
163 | subdid 10365 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (𝐵 · (𝑋 − 𝑊)) = ((𝐵 · 𝑋) − (𝐵 · 𝑊))) |
165 | 164 | sumeq2dv 14281 |
. . . . . 6
⊢ (𝜑 → Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 · (𝑋 − 𝑊)) = Σ𝑗 ∈ (𝑀..^𝑁)((𝐵 · 𝑋) − (𝐵 · 𝑊))) |
166 | 121, 163 | mulcld 9939 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (𝐵 · 𝑊) ∈ ℂ) |
167 | 129, 131,
166 | fsumsub 14362 |
. . . . . 6
⊢ (𝜑 → Σ𝑗 ∈ (𝑀..^𝑁)((𝐵 · 𝑋) − (𝐵 · 𝑊)) = (Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 · 𝑋) − Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 · 𝑊))) |
168 | 165, 167 | eqtrd 2644 |
. . . . 5
⊢ (𝜑 → Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 · (𝑋 − 𝑊)) = (Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 · 𝑋) − Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 · 𝑊))) |
169 | 168 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 · (𝑋 − 𝑊)) = (Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 · 𝑋) − Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 · 𝑊))) |
170 | 158, 159,
169 | 3eqtr4d 2654 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → ((Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 · 𝑋) − Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)(𝐴 · 𝑉)) − (𝐷 · 𝑌)) = Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 · (𝑋 − 𝑊))) |
171 | 139, 142,
170 | 3eqtrrd 2649 |
. 2
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 · (𝑋 − 𝑊)) = (((𝐸 · 𝑍) − (𝐷 · 𝑌)) − Σ𝑗 ∈ (𝑀..^𝑁)((𝐶 − 𝐵) · 𝑋))) |
172 | | uzp1 11597 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑁 = 𝑀 ∨ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) |
173 | 9, 172 | syl 17 |
. 2
⊢ (𝜑 → (𝑁 = 𝑀 ∨ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) |
174 | 47, 171, 173 | mpjaodan 823 |
1
⊢ (𝜑 → Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 · (𝑋 − 𝑊)) = (((𝐸 · 𝑍) − (𝐷 · 𝑌)) − Σ𝑗 ∈ (𝑀..^𝑁)((𝐶 − 𝐵) · 𝑋))) |