Step | Hyp | Ref
| Expression |
1 | | iseqp1.m |
. . 3
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
2 | | eluzel2 8624 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
3 | 1, 2 | syl 14 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) |
4 | | eqid 2081 |
. . . 4
⊢
frec((𝑥 ∈
ℤ ↦ (𝑥 + 1)),
𝑀) = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 𝑀) |
5 | | iseqp1.ex |
. . . 4
⊢ (𝜑 → 𝑆 ∈ 𝑉) |
6 | | uzid 8633 |
. . . . . 6
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
(ℤ≥‘𝑀)) |
7 | 3, 6 | syl 14 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑀)) |
8 | | iseqp1.f |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆) |
9 | 8 | ralrimiva 2434 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ (ℤ≥‘𝑀)(𝐹‘𝑥) ∈ 𝑆) |
10 | | fveq2 5198 |
. . . . . . 7
⊢ (𝑥 = 𝑀 → (𝐹‘𝑥) = (𝐹‘𝑀)) |
11 | 10 | eleq1d 2147 |
. . . . . 6
⊢ (𝑥 = 𝑀 → ((𝐹‘𝑥) ∈ 𝑆 ↔ (𝐹‘𝑀) ∈ 𝑆)) |
12 | 11 | rspcv 2697 |
. . . . 5
⊢ (𝑀 ∈
(ℤ≥‘𝑀) → (∀𝑥 ∈ (ℤ≥‘𝑀)(𝐹‘𝑥) ∈ 𝑆 → (𝐹‘𝑀) ∈ 𝑆)) |
13 | 7, 9, 12 | sylc 61 |
. . . 4
⊢ (𝜑 → (𝐹‘𝑀) ∈ 𝑆) |
14 | | iseqp1.pl |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
15 | 8, 14 | iseqovex 9439 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝑆)) → (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) ∈ 𝑆) |
16 | | eqid 2081 |
. . . 4
⊢
frec((𝑥 ∈
(ℤ≥‘𝑀), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉), 〈𝑀, (𝐹‘𝑀)〉) = frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉), 〈𝑀, (𝐹‘𝑀)〉) |
17 | 16, 8, 14 | iseqval 9440 |
. . . 4
⊢ (𝜑 → seq𝑀( + , 𝐹, 𝑆) = ran frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉), 〈𝑀, (𝐹‘𝑀)〉)) |
18 | 3, 4, 5, 13, 15, 16, 17 | frecuzrdgsuc 9417 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → (seq𝑀( + , 𝐹, 𝑆)‘(𝑁 + 1)) = (𝑁(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(seq𝑀( + , 𝐹, 𝑆)‘𝑁))) |
19 | 1, 18 | mpdan 412 |
. 2
⊢ (𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘(𝑁 + 1)) = (𝑁(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(seq𝑀( + , 𝐹, 𝑆)‘𝑁))) |
20 | 1, 5, 8, 14 | iseqcl 9443 |
. . 3
⊢ (𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) ∈ 𝑆) |
21 | | peano2uz 8671 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑁 + 1) ∈
(ℤ≥‘𝑀)) |
22 | 1, 21 | syl 14 |
. . . . 5
⊢ (𝜑 → (𝑁 + 1) ∈
(ℤ≥‘𝑀)) |
23 | | fveq2 5198 |
. . . . . . 7
⊢ (𝑥 = (𝑁 + 1) → (𝐹‘𝑥) = (𝐹‘(𝑁 + 1))) |
24 | 23 | eleq1d 2147 |
. . . . . 6
⊢ (𝑥 = (𝑁 + 1) → ((𝐹‘𝑥) ∈ 𝑆 ↔ (𝐹‘(𝑁 + 1)) ∈ 𝑆)) |
25 | 24 | rspcv 2697 |
. . . . 5
⊢ ((𝑁 + 1) ∈
(ℤ≥‘𝑀) → (∀𝑥 ∈ (ℤ≥‘𝑀)(𝐹‘𝑥) ∈ 𝑆 → (𝐹‘(𝑁 + 1)) ∈ 𝑆)) |
26 | 22, 9, 25 | sylc 61 |
. . . 4
⊢ (𝜑 → (𝐹‘(𝑁 + 1)) ∈ 𝑆) |
27 | 14, 20, 26 | caovcld 5674 |
. . 3
⊢ (𝜑 → ((seq𝑀( + , 𝐹, 𝑆)‘𝑁) + (𝐹‘(𝑁 + 1))) ∈ 𝑆) |
28 | | oveq1 5539 |
. . . . . 6
⊢ (𝑧 = 𝑁 → (𝑧 + 1) = (𝑁 + 1)) |
29 | 28 | fveq2d 5202 |
. . . . 5
⊢ (𝑧 = 𝑁 → (𝐹‘(𝑧 + 1)) = (𝐹‘(𝑁 + 1))) |
30 | 29 | oveq2d 5548 |
. . . 4
⊢ (𝑧 = 𝑁 → (𝑤 + (𝐹‘(𝑧 + 1))) = (𝑤 + (𝐹‘(𝑁 + 1)))) |
31 | | oveq1 5539 |
. . . 4
⊢ (𝑤 = (seq𝑀( + , 𝐹, 𝑆)‘𝑁) → (𝑤 + (𝐹‘(𝑁 + 1))) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑁) + (𝐹‘(𝑁 + 1)))) |
32 | | eqid 2081 |
. . . 4
⊢ (𝑧 ∈
(ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1)))) = (𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1)))) |
33 | 30, 31, 32 | ovmpt2g 5655 |
. . 3
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ (seq𝑀( + , 𝐹, 𝑆)‘𝑁) ∈ 𝑆 ∧ ((seq𝑀( + , 𝐹, 𝑆)‘𝑁) + (𝐹‘(𝑁 + 1))) ∈ 𝑆) → (𝑁(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(seq𝑀( + , 𝐹, 𝑆)‘𝑁)) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑁) + (𝐹‘(𝑁 + 1)))) |
34 | 1, 20, 27, 33 | syl3anc 1169 |
. 2
⊢ (𝜑 → (𝑁(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(seq𝑀( + , 𝐹, 𝑆)‘𝑁)) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑁) + (𝐹‘(𝑁 + 1)))) |
35 | 19, 34 | eqtrd 2113 |
1
⊢ (𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑁) + (𝐹‘(𝑁 + 1)))) |