Proof of Theorem telfsumo
Step | Hyp | Ref
| Expression |
1 | | telfsumo.5 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
2 | | eluzfz1 12219 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁)) |
3 | 1, 2 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ (𝑀...𝑁)) |
4 | | telfsumo.6 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ) |
5 | 4 | ralrimiva 2949 |
. . . . . . 7
⊢ (𝜑 → ∀𝑘 ∈ (𝑀...𝑁)𝐴 ∈ ℂ) |
6 | | telfsumo.3 |
. . . . . . . . 9
⊢ (𝑘 = 𝑀 → 𝐴 = 𝐷) |
7 | 6 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑘 = 𝑀 → (𝐴 ∈ ℂ ↔ 𝐷 ∈ ℂ)) |
8 | 7 | rspcv 3278 |
. . . . . . 7
⊢ (𝑀 ∈ (𝑀...𝑁) → (∀𝑘 ∈ (𝑀...𝑁)𝐴 ∈ ℂ → 𝐷 ∈ ℂ)) |
9 | 3, 5, 8 | sylc 63 |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ ℂ) |
10 | 9 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 = 𝑀) → 𝐷 ∈ ℂ) |
11 | 10 | subidd 10259 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 = 𝑀) → (𝐷 − 𝐷) = 0) |
12 | | sum0 14299 |
. . . 4
⊢
Σ𝑗 ∈
∅ (𝐵 − 𝐶) = 0 |
13 | 11, 12 | syl6reqr 2663 |
. . 3
⊢ ((𝜑 ∧ 𝑁 = 𝑀) → Σ𝑗 ∈ ∅ (𝐵 − 𝐶) = (𝐷 − 𝐷)) |
14 | | oveq2 6557 |
. . . . . 6
⊢ (𝑁 = 𝑀 → (𝑀..^𝑁) = (𝑀..^𝑀)) |
15 | 14 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 = 𝑀) → (𝑀..^𝑁) = (𝑀..^𝑀)) |
16 | | fzo0 12361 |
. . . . 5
⊢ (𝑀..^𝑀) = ∅ |
17 | 15, 16 | syl6eq 2660 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 = 𝑀) → (𝑀..^𝑁) = ∅) |
18 | 17 | sumeq1d 14279 |
. . 3
⊢ ((𝜑 ∧ 𝑁 = 𝑀) → Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 − 𝐶) = Σ𝑗 ∈ ∅ (𝐵 − 𝐶)) |
19 | | eqeq1 2614 |
. . . . . . . 8
⊢ (𝑘 = 𝑁 → (𝑘 = 𝑀 ↔ 𝑁 = 𝑀)) |
20 | | telfsumo.4 |
. . . . . . . . 9
⊢ (𝑘 = 𝑁 → 𝐴 = 𝐸) |
21 | 20 | eqeq1d 2612 |
. . . . . . . 8
⊢ (𝑘 = 𝑁 → (𝐴 = 𝐷 ↔ 𝐸 = 𝐷)) |
22 | 19, 21 | imbi12d 333 |
. . . . . . 7
⊢ (𝑘 = 𝑁 → ((𝑘 = 𝑀 → 𝐴 = 𝐷) ↔ (𝑁 = 𝑀 → 𝐸 = 𝐷))) |
23 | 22, 6 | vtoclg 3239 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑁 = 𝑀 → 𝐸 = 𝐷)) |
24 | 23 | imp 444 |
. . . . 5
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → 𝐸 = 𝐷) |
25 | 1, 24 | sylan 487 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 = 𝑀) → 𝐸 = 𝐷) |
26 | 25 | oveq2d 6565 |
. . 3
⊢ ((𝜑 ∧ 𝑁 = 𝑀) → (𝐷 − 𝐸) = (𝐷 − 𝐷)) |
27 | 13, 18, 26 | 3eqtr4d 2654 |
. 2
⊢ ((𝜑 ∧ 𝑁 = 𝑀) → Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 − 𝐶) = (𝐷 − 𝐸)) |
28 | | fzofi 12635 |
. . . . . 6
⊢ (𝑀..^𝑁) ∈ Fin |
29 | 28 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝑀..^𝑁) ∈ Fin) |
30 | | elfzofz 12354 |
. . . . . . 7
⊢ (𝑗 ∈ (𝑀..^𝑁) → 𝑗 ∈ (𝑀...𝑁)) |
31 | 30 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝑗 ∈ (𝑀...𝑁)) |
32 | 5 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → ∀𝑘 ∈ (𝑀...𝑁)𝐴 ∈ ℂ) |
33 | | telfsumo.1 |
. . . . . . . 8
⊢ (𝑘 = 𝑗 → 𝐴 = 𝐵) |
34 | 33 | eleq1d 2672 |
. . . . . . 7
⊢ (𝑘 = 𝑗 → (𝐴 ∈ ℂ ↔ 𝐵 ∈ ℂ)) |
35 | 34 | rspcv 3278 |
. . . . . 6
⊢ (𝑗 ∈ (𝑀...𝑁) → (∀𝑘 ∈ (𝑀...𝑁)𝐴 ∈ ℂ → 𝐵 ∈ ℂ)) |
36 | 31, 32, 35 | sylc 63 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝐵 ∈ ℂ) |
37 | | fzofzp1 12431 |
. . . . . . 7
⊢ (𝑗 ∈ (𝑀..^𝑁) → (𝑗 + 1) ∈ (𝑀...𝑁)) |
38 | 37 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (𝑗 + 1) ∈ (𝑀...𝑁)) |
39 | | telfsumo.2 |
. . . . . . . 8
⊢ (𝑘 = (𝑗 + 1) → 𝐴 = 𝐶) |
40 | 39 | eleq1d 2672 |
. . . . . . 7
⊢ (𝑘 = (𝑗 + 1) → (𝐴 ∈ ℂ ↔ 𝐶 ∈ ℂ)) |
41 | 40 | rspcv 3278 |
. . . . . 6
⊢ ((𝑗 + 1) ∈ (𝑀...𝑁) → (∀𝑘 ∈ (𝑀...𝑁)𝐴 ∈ ℂ → 𝐶 ∈ ℂ)) |
42 | 38, 32, 41 | sylc 63 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝐶 ∈ ℂ) |
43 | 29, 36, 42 | fsumsub 14362 |
. . . 4
⊢ (𝜑 → Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 − 𝐶) = (Σ𝑗 ∈ (𝑀..^𝑁)𝐵 − Σ𝑗 ∈ (𝑀..^𝑁)𝐶)) |
44 | 43 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 − 𝐶) = (Σ𝑗 ∈ (𝑀..^𝑁)𝐵 − Σ𝑗 ∈ (𝑀..^𝑁)𝐶)) |
45 | 33 | cbvsumv 14274 |
. . . . . 6
⊢
Σ𝑘 ∈
(𝑀..^𝑁)𝐴 = Σ𝑗 ∈ (𝑀..^𝑁)𝐵 |
46 | | eluzel2 11568 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
47 | 1, 46 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℤ) |
48 | | eluzp1m1 11587 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → (𝑁 − 1) ∈
(ℤ≥‘𝑀)) |
49 | 47, 48 | sylan 487 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑁 − 1) ∈
(ℤ≥‘𝑀)) |
50 | | eluzelz 11573 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
51 | 1, 50 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℤ) |
52 | 51 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑁 ∈ ℤ) |
53 | | fzoval 12340 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1))) |
54 | 52, 53 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑀..^𝑁) = (𝑀...(𝑁 − 1))) |
55 | | fzossfz 12357 |
. . . . . . . . . . 11
⊢ (𝑀..^𝑁) ⊆ (𝑀...𝑁) |
56 | 54, 55 | syl6eqssr 3619 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑀...(𝑁 − 1)) ⊆ (𝑀...𝑁)) |
57 | 56 | sselda 3568 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → 𝑘 ∈ (𝑀...𝑁)) |
58 | 4 | adantlr 747 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ) |
59 | 57, 58 | syldan 486 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → 𝐴 ∈ ℂ) |
60 | 49, 59, 6 | fsum1p 14326 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 = (𝐷 + Σ𝑘 ∈ ((𝑀 + 1)...(𝑁 − 1))𝐴)) |
61 | 54 | sumeq1d 14279 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → Σ𝑘 ∈ (𝑀..^𝑁)𝐴 = Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴) |
62 | | fzoval 12340 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ → ((𝑀 + 1)..^𝑁) = ((𝑀 + 1)...(𝑁 − 1))) |
63 | 52, 62 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝑀 + 1)..^𝑁) = ((𝑀 + 1)...(𝑁 − 1))) |
64 | 63 | sumeq1d 14279 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)𝐴 = Σ𝑘 ∈ ((𝑀 + 1)...(𝑁 − 1))𝐴) |
65 | 64 | oveq2d 6565 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (𝐷 + Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)𝐴) = (𝐷 + Σ𝑘 ∈ ((𝑀 + 1)...(𝑁 − 1))𝐴)) |
66 | 60, 61, 65 | 3eqtr4d 2654 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → Σ𝑘 ∈ (𝑀..^𝑁)𝐴 = (𝐷 + Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)𝐴)) |
67 | 45, 66 | syl5eqr 2658 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → Σ𝑗 ∈ (𝑀..^𝑁)𝐵 = (𝐷 + Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)𝐴)) |
68 | | simpr 476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) |
69 | | fzp1ss 12262 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℤ → ((𝑀 + 1)...𝑁) ⊆ (𝑀...𝑁)) |
70 | 47, 69 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑀 + 1)...𝑁) ⊆ (𝑀...𝑁)) |
71 | 70 | sselda 3568 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝑁)) → 𝑘 ∈ (𝑀...𝑁)) |
72 | 71, 4 | syldan 486 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝑁)) → 𝐴 ∈ ℂ) |
73 | 72 | adantlr 747 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) ∧ 𝑘 ∈ ((𝑀 + 1)...𝑁)) → 𝐴 ∈ ℂ) |
74 | 68, 73, 20 | fsumm1 14324 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → Σ𝑘 ∈ ((𝑀 + 1)...𝑁)𝐴 = (Σ𝑘 ∈ ((𝑀 + 1)...(𝑁 − 1))𝐴 + 𝐸)) |
75 | | 1zzd 11285 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℤ) |
76 | 47 | peano2zd 11361 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 + 1) ∈ ℤ) |
77 | 75, 76, 51, 72, 39 | fsumshftm 14355 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑘 ∈ ((𝑀 + 1)...𝑁)𝐴 = Σ𝑗 ∈ (((𝑀 + 1) − 1)...(𝑁 − 1))𝐶) |
78 | 47 | zcnd 11359 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ ℂ) |
79 | | ax-1cn 9873 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℂ |
80 | | pncan 10166 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑀 + 1)
− 1) = 𝑀) |
81 | 78, 79, 80 | sylancl 693 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑀 + 1) − 1) = 𝑀) |
82 | 81 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑀 + 1) − 1)...(𝑁 − 1)) = (𝑀...(𝑁 − 1))) |
83 | 51, 53 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀..^𝑁) = (𝑀...(𝑁 − 1))) |
84 | 82, 83 | eqtr4d 2647 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑀 + 1) − 1)...(𝑁 − 1)) = (𝑀..^𝑁)) |
85 | 84 | sumeq1d 14279 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑗 ∈ (((𝑀 + 1) − 1)...(𝑁 − 1))𝐶 = Σ𝑗 ∈ (𝑀..^𝑁)𝐶) |
86 | 77, 85 | eqtrd 2644 |
. . . . . . 7
⊢ (𝜑 → Σ𝑘 ∈ ((𝑀 + 1)...𝑁)𝐴 = Σ𝑗 ∈ (𝑀..^𝑁)𝐶) |
87 | 86 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → Σ𝑘 ∈ ((𝑀 + 1)...𝑁)𝐴 = Σ𝑗 ∈ (𝑀..^𝑁)𝐶) |
88 | 51, 62 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑀 + 1)..^𝑁) = ((𝑀 + 1)...(𝑁 − 1))) |
89 | 88 | sumeq1d 14279 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)𝐴 = Σ𝑘 ∈ ((𝑀 + 1)...(𝑁 − 1))𝐴) |
90 | 89 | oveq1d 6564 |
. . . . . . . 8
⊢ (𝜑 → (Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)𝐴 + 𝐸) = (Σ𝑘 ∈ ((𝑀 + 1)...(𝑁 − 1))𝐴 + 𝐸)) |
91 | | fzofi 12635 |
. . . . . . . . . . 11
⊢ ((𝑀 + 1)..^𝑁) ∈ Fin |
92 | 91 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑀 + 1)..^𝑁) ∈ Fin) |
93 | | elfzofz 12354 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑘 ∈ ((𝑀 + 1)...𝑁)) |
94 | 93, 72 | sylan2 490 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝐴 ∈ ℂ) |
95 | 92, 94 | fsumcl 14311 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)𝐴 ∈ ℂ) |
96 | | eluzfz2 12220 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁)) |
97 | 1, 96 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ (𝑀...𝑁)) |
98 | 20 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑁 → (𝐴 ∈ ℂ ↔ 𝐸 ∈ ℂ)) |
99 | 98 | rspcv 3278 |
. . . . . . . . . 10
⊢ (𝑁 ∈ (𝑀...𝑁) → (∀𝑘 ∈ (𝑀...𝑁)𝐴 ∈ ℂ → 𝐸 ∈ ℂ)) |
100 | 97, 5, 99 | sylc 63 |
. . . . . . . . 9
⊢ (𝜑 → 𝐸 ∈ ℂ) |
101 | 95, 100 | addcomd 10117 |
. . . . . . . 8
⊢ (𝜑 → (Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)𝐴 + 𝐸) = (𝐸 + Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)𝐴)) |
102 | 90, 101 | eqtr3d 2646 |
. . . . . . 7
⊢ (𝜑 → (Σ𝑘 ∈ ((𝑀 + 1)...(𝑁 − 1))𝐴 + 𝐸) = (𝐸 + Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)𝐴)) |
103 | 102 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (Σ𝑘 ∈ ((𝑀 + 1)...(𝑁 − 1))𝐴 + 𝐸) = (𝐸 + Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)𝐴)) |
104 | 74, 87, 103 | 3eqtr3d 2652 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → Σ𝑗 ∈ (𝑀..^𝑁)𝐶 = (𝐸 + Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)𝐴)) |
105 | 67, 104 | oveq12d 6567 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (Σ𝑗 ∈ (𝑀..^𝑁)𝐵 − Σ𝑗 ∈ (𝑀..^𝑁)𝐶) = ((𝐷 + Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)𝐴) − (𝐸 + Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)𝐴))) |
106 | 9, 100, 95 | pnpcan2d 10309 |
. . . . 5
⊢ (𝜑 → ((𝐷 + Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)𝐴) − (𝐸 + Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)𝐴)) = (𝐷 − 𝐸)) |
107 | 106 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝐷 + Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)𝐴) − (𝐸 + Σ𝑘 ∈ ((𝑀 + 1)..^𝑁)𝐴)) = (𝐷 − 𝐸)) |
108 | 105, 107 | eqtrd 2644 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (Σ𝑗 ∈ (𝑀..^𝑁)𝐵 − Σ𝑗 ∈ (𝑀..^𝑁)𝐶) = (𝐷 − 𝐸)) |
109 | 44, 108 | eqtrd 2644 |
. 2
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 − 𝐶) = (𝐷 − 𝐸)) |
110 | | uzp1 11597 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑁 = 𝑀 ∨ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) |
111 | 1, 110 | syl 17 |
. 2
⊢ (𝜑 → (𝑁 = 𝑀 ∨ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) |
112 | 27, 109, 111 | mpjaodan 823 |
1
⊢ (𝜑 → Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 − 𝐶) = (𝐷 − 𝐸)) |