Step | Hyp | Ref
| Expression |
1 | | gsumncl.p |
. . 3
⊢ (𝜑 → 𝑃 ∈ (ℤ≥‘𝑁)) |
2 | | seqp1 12678 |
. . 3
⊢ (𝑃 ∈
(ℤ≥‘𝑁) → (seq𝑁( + , (𝑘 ∈ (𝑁...(𝑃 + 1)) ↦ 𝐵))‘(𝑃 + 1)) = ((seq𝑁( + , (𝑘 ∈ (𝑁...(𝑃 + 1)) ↦ 𝐵))‘𝑃) + ((𝑘 ∈ (𝑁...(𝑃 + 1)) ↦ 𝐵)‘(𝑃 + 1)))) |
3 | 1, 2 | syl 17 |
. 2
⊢ (𝜑 → (seq𝑁( + , (𝑘 ∈ (𝑁...(𝑃 + 1)) ↦ 𝐵))‘(𝑃 + 1)) = ((seq𝑁( + , (𝑘 ∈ (𝑁...(𝑃 + 1)) ↦ 𝐵))‘𝑃) + ((𝑘 ∈ (𝑁...(𝑃 + 1)) ↦ 𝐵)‘(𝑃 + 1)))) |
4 | | gsumncl.k |
. . 3
⊢ 𝐾 = (Base‘𝑀) |
5 | | gsumnunsn.a |
. . 3
⊢ + =
(+g‘𝑀) |
6 | | gsumncl.w |
. . 3
⊢ (𝜑 → 𝑀 ∈ Mnd) |
7 | | peano2uz 11617 |
. . . 4
⊢ (𝑃 ∈
(ℤ≥‘𝑁) → (𝑃 + 1) ∈
(ℤ≥‘𝑁)) |
8 | 1, 7 | syl 17 |
. . 3
⊢ (𝜑 → (𝑃 + 1) ∈
(ℤ≥‘𝑁)) |
9 | | gsumncl.b |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑁...𝑃)) → 𝐵 ∈ 𝐾) |
10 | 9 | adantlr 747 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑁...(𝑃 + 1))) ∧ 𝑘 ∈ (𝑁...𝑃)) → 𝐵 ∈ 𝐾) |
11 | | gsumnunsn.c |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 = (𝑃 + 1)) → 𝐵 = 𝐶) |
12 | 11 | adantlr 747 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑁...(𝑃 + 1))) ∧ 𝑘 = (𝑃 + 1)) → 𝐵 = 𝐶) |
13 | | gsumnunsn.l |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ 𝐾) |
14 | 13 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑁...(𝑃 + 1))) ∧ 𝑘 = (𝑃 + 1)) → 𝐶 ∈ 𝐾) |
15 | 12, 14 | eqeltrd 2688 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑁...(𝑃 + 1))) ∧ 𝑘 = (𝑃 + 1)) → 𝐵 ∈ 𝐾) |
16 | | elfzp1 12261 |
. . . . . . 7
⊢ (𝑃 ∈
(ℤ≥‘𝑁) → (𝑘 ∈ (𝑁...(𝑃 + 1)) ↔ (𝑘 ∈ (𝑁...𝑃) ∨ 𝑘 = (𝑃 + 1)))) |
17 | 1, 16 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑘 ∈ (𝑁...(𝑃 + 1)) ↔ (𝑘 ∈ (𝑁...𝑃) ∨ 𝑘 = (𝑃 + 1)))) |
18 | 17 | biimpa 500 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑁...(𝑃 + 1))) → (𝑘 ∈ (𝑁...𝑃) ∨ 𝑘 = (𝑃 + 1))) |
19 | 10, 15, 18 | mpjaodan 823 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑁...(𝑃 + 1))) → 𝐵 ∈ 𝐾) |
20 | | eqid 2610 |
. . . 4
⊢ (𝑘 ∈ (𝑁...(𝑃 + 1)) ↦ 𝐵) = (𝑘 ∈ (𝑁...(𝑃 + 1)) ↦ 𝐵) |
21 | 19, 20 | fmptd 6292 |
. . 3
⊢ (𝜑 → (𝑘 ∈ (𝑁...(𝑃 + 1)) ↦ 𝐵):(𝑁...(𝑃 + 1))⟶𝐾) |
22 | 4, 5, 6, 8, 21 | gsumval2 17103 |
. 2
⊢ (𝜑 → (𝑀 Σg (𝑘 ∈ (𝑁...(𝑃 + 1)) ↦ 𝐵)) = (seq𝑁( + , (𝑘 ∈ (𝑁...(𝑃 + 1)) ↦ 𝐵))‘(𝑃 + 1))) |
23 | | eqid 2610 |
. . . . . 6
⊢ (𝑘 ∈ (𝑁...𝑃) ↦ 𝐵) = (𝑘 ∈ (𝑁...𝑃) ↦ 𝐵) |
24 | 9, 23 | fmptd 6292 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ (𝑁...𝑃) ↦ 𝐵):(𝑁...𝑃)⟶𝐾) |
25 | 4, 5, 6, 1, 24 | gsumval2 17103 |
. . . 4
⊢ (𝜑 → (𝑀 Σg (𝑘 ∈ (𝑁...𝑃) ↦ 𝐵)) = (seq𝑁( + , (𝑘 ∈ (𝑁...𝑃) ↦ 𝐵))‘𝑃)) |
26 | | fzssp1 12255 |
. . . . . . . 8
⊢ (𝑁...𝑃) ⊆ (𝑁...(𝑃 + 1)) |
27 | | resmpt 5369 |
. . . . . . . 8
⊢ ((𝑁...𝑃) ⊆ (𝑁...(𝑃 + 1)) → ((𝑘 ∈ (𝑁...(𝑃 + 1)) ↦ 𝐵) ↾ (𝑁...𝑃)) = (𝑘 ∈ (𝑁...𝑃) ↦ 𝐵)) |
28 | 26, 27 | ax-mp 5 |
. . . . . . 7
⊢ ((𝑘 ∈ (𝑁...(𝑃 + 1)) ↦ 𝐵) ↾ (𝑁...𝑃)) = (𝑘 ∈ (𝑁...𝑃) ↦ 𝐵) |
29 | 28 | fveq1i 6104 |
. . . . . 6
⊢ (((𝑘 ∈ (𝑁...(𝑃 + 1)) ↦ 𝐵) ↾ (𝑁...𝑃))‘𝑖) = ((𝑘 ∈ (𝑁...𝑃) ↦ 𝐵)‘𝑖) |
30 | | fvres 6117 |
. . . . . . 7
⊢ (𝑖 ∈ (𝑁...𝑃) → (((𝑘 ∈ (𝑁...(𝑃 + 1)) ↦ 𝐵) ↾ (𝑁...𝑃))‘𝑖) = ((𝑘 ∈ (𝑁...(𝑃 + 1)) ↦ 𝐵)‘𝑖)) |
31 | 30 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁...𝑃)) → (((𝑘 ∈ (𝑁...(𝑃 + 1)) ↦ 𝐵) ↾ (𝑁...𝑃))‘𝑖) = ((𝑘 ∈ (𝑁...(𝑃 + 1)) ↦ 𝐵)‘𝑖)) |
32 | 29, 31 | syl5reqr 2659 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁...𝑃)) → ((𝑘 ∈ (𝑁...(𝑃 + 1)) ↦ 𝐵)‘𝑖) = ((𝑘 ∈ (𝑁...𝑃) ↦ 𝐵)‘𝑖)) |
33 | 1, 32 | seqfveq 12687 |
. . . 4
⊢ (𝜑 → (seq𝑁( + , (𝑘 ∈ (𝑁...(𝑃 + 1)) ↦ 𝐵))‘𝑃) = (seq𝑁( + , (𝑘 ∈ (𝑁...𝑃) ↦ 𝐵))‘𝑃)) |
34 | 25, 33 | eqtr4d 2647 |
. . 3
⊢ (𝜑 → (𝑀 Σg (𝑘 ∈ (𝑁...𝑃) ↦ 𝐵)) = (seq𝑁( + , (𝑘 ∈ (𝑁...(𝑃 + 1)) ↦ 𝐵))‘𝑃)) |
35 | | eqidd 2611 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ (𝑁...(𝑃 + 1)) ↦ 𝐵) = (𝑘 ∈ (𝑁...(𝑃 + 1)) ↦ 𝐵)) |
36 | | eluzfz2 12220 |
. . . . . 6
⊢ ((𝑃 + 1) ∈
(ℤ≥‘𝑁) → (𝑃 + 1) ∈ (𝑁...(𝑃 + 1))) |
37 | 8, 36 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑃 + 1) ∈ (𝑁...(𝑃 + 1))) |
38 | 35, 11, 37, 13 | fvmptd 6197 |
. . . 4
⊢ (𝜑 → ((𝑘 ∈ (𝑁...(𝑃 + 1)) ↦ 𝐵)‘(𝑃 + 1)) = 𝐶) |
39 | 38 | eqcomd 2616 |
. . 3
⊢ (𝜑 → 𝐶 = ((𝑘 ∈ (𝑁...(𝑃 + 1)) ↦ 𝐵)‘(𝑃 + 1))) |
40 | 34, 39 | oveq12d 6567 |
. 2
⊢ (𝜑 → ((𝑀 Σg (𝑘 ∈ (𝑁...𝑃) ↦ 𝐵)) + 𝐶) = ((seq𝑁( + , (𝑘 ∈ (𝑁...(𝑃 + 1)) ↦ 𝐵))‘𝑃) + ((𝑘 ∈ (𝑁...(𝑃 + 1)) ↦ 𝐵)‘(𝑃 + 1)))) |
41 | 3, 22, 40 | 3eqtr4d 2654 |
1
⊢ (𝜑 → (𝑀 Σg (𝑘 ∈ (𝑁...(𝑃 + 1)) ↦ 𝐵)) = ((𝑀 Σg (𝑘 ∈ (𝑁...𝑃) ↦ 𝐵)) + 𝐶)) |