Step | Hyp | Ref
| Expression |
1 | | iseqid.3 |
. 2
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
2 | | eluzelz 8628 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
3 | 1, 2 | syl 14 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℤ) |
4 | | iseqid.s |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ 𝑉) |
5 | | simpr 108 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑁)) → 𝑥 ∈ (ℤ≥‘𝑁)) |
6 | 1 | adantr 270 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑁)) → 𝑁 ∈ (ℤ≥‘𝑀)) |
7 | | uztrn 8635 |
. . . . . . 7
⊢ ((𝑥 ∈
(ℤ≥‘𝑁) ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → 𝑥 ∈ (ℤ≥‘𝑀)) |
8 | 5, 6, 7 | syl2anc 403 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑁)) → 𝑥 ∈ (ℤ≥‘𝑀)) |
9 | | iseqid.f |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆) |
10 | 8, 9 | syldan 276 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑁)) → (𝐹‘𝑥) ∈ 𝑆) |
11 | | iseqid.cl |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
12 | 3, 4, 10, 11 | iseq1 9442 |
. . . 4
⊢ (𝜑 → (seq𝑁( + , 𝐹, 𝑆)‘𝑁) = (𝐹‘𝑁)) |
13 | | iseqeq1 9434 |
. . . . . 6
⊢ (𝑁 = 𝑀 → seq𝑁( + , 𝐹, 𝑆) = seq𝑀( + , 𝐹, 𝑆)) |
14 | 13 | fveq1d 5200 |
. . . . 5
⊢ (𝑁 = 𝑀 → (seq𝑁( + , 𝐹, 𝑆)‘𝑁) = (seq𝑀( + , 𝐹, 𝑆)‘𝑁)) |
15 | 14 | eqeq1d 2089 |
. . . 4
⊢ (𝑁 = 𝑀 → ((seq𝑁( + , 𝐹, 𝑆)‘𝑁) = (𝐹‘𝑁) ↔ (seq𝑀( + , 𝐹, 𝑆)‘𝑁) = (𝐹‘𝑁))) |
16 | 12, 15 | syl5ibcom 153 |
. . 3
⊢ (𝜑 → (𝑁 = 𝑀 → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) = (𝐹‘𝑁))) |
17 | | eluzel2 8624 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
18 | 1, 17 | syl 14 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℤ) |
19 | 18 | adantr 270 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑀 ∈ ℤ) |
20 | | simpr 108 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) |
21 | 4 | adantr 270 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑆 ∈ 𝑉) |
22 | 9 | adantlr 460 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆) |
23 | 11 | adantlr 460 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
24 | 19, 20, 21, 22, 23 | iseqm1 9447 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) = ((seq𝑀( + , 𝐹, 𝑆)‘(𝑁 − 1)) + (𝐹‘𝑁))) |
25 | | iseqid.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝑍 ∈ 𝑆) |
26 | | iseqid.1 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑍 + 𝑥) = 𝑥) |
27 | 26 | ralrimiva 2434 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 (𝑍 + 𝑥) = 𝑥) |
28 | | oveq2 5540 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑍 → (𝑍 + 𝑥) = (𝑍 + 𝑍)) |
29 | | id 19 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑍 → 𝑥 = 𝑍) |
30 | 28, 29 | eqeq12d 2095 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑍 → ((𝑍 + 𝑥) = 𝑥 ↔ (𝑍 + 𝑍) = 𝑍)) |
31 | 30 | rspcv 2697 |
. . . . . . . . 9
⊢ (𝑍 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 (𝑍 + 𝑥) = 𝑥 → (𝑍 + 𝑍) = 𝑍)) |
32 | 25, 27, 31 | sylc 61 |
. . . . . . . 8
⊢ (𝜑 → (𝑍 + 𝑍) = 𝑍) |
33 | 32 | adantr 270 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑍 + 𝑍) = 𝑍) |
34 | | eluzp1m1 8642 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → (𝑁 − 1) ∈
(ℤ≥‘𝑀)) |
35 | 18, 34 | sylan 277 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑁 − 1) ∈
(ℤ≥‘𝑀)) |
36 | | iseqid.5 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘𝑥) = 𝑍) |
37 | 36 | adantlr 460 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) ∧ 𝑥 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘𝑥) = 𝑍) |
38 | 25 | adantr 270 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑍 ∈ 𝑆) |
39 | 33, 35, 37, 38, 21, 22, 23 | iseqid3s 9466 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (seq𝑀( + , 𝐹, 𝑆)‘(𝑁 − 1)) = 𝑍) |
40 | 39 | oveq1d 5547 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → ((seq𝑀( + , 𝐹, 𝑆)‘(𝑁 − 1)) + (𝐹‘𝑁)) = (𝑍 + (𝐹‘𝑁))) |
41 | | iseqid.4 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘𝑁) ∈ 𝑆) |
42 | 41 | adantr 270 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (𝐹‘𝑁) ∈ 𝑆) |
43 | 27 | adantr 270 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → ∀𝑥 ∈ 𝑆 (𝑍 + 𝑥) = 𝑥) |
44 | | oveq2 5540 |
. . . . . . . 8
⊢ (𝑥 = (𝐹‘𝑁) → (𝑍 + 𝑥) = (𝑍 + (𝐹‘𝑁))) |
45 | | id 19 |
. . . . . . . 8
⊢ (𝑥 = (𝐹‘𝑁) → 𝑥 = (𝐹‘𝑁)) |
46 | 44, 45 | eqeq12d 2095 |
. . . . . . 7
⊢ (𝑥 = (𝐹‘𝑁) → ((𝑍 + 𝑥) = 𝑥 ↔ (𝑍 + (𝐹‘𝑁)) = (𝐹‘𝑁))) |
47 | 46 | rspcv 2697 |
. . . . . 6
⊢ ((𝐹‘𝑁) ∈ 𝑆 → (∀𝑥 ∈ 𝑆 (𝑍 + 𝑥) = 𝑥 → (𝑍 + (𝐹‘𝑁)) = (𝐹‘𝑁))) |
48 | 42, 43, 47 | sylc 61 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑍 + (𝐹‘𝑁)) = (𝐹‘𝑁)) |
49 | 24, 40, 48 | 3eqtrd 2117 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) = (𝐹‘𝑁)) |
50 | 49 | ex 113 |
. . 3
⊢ (𝜑 → (𝑁 ∈ (ℤ≥‘(𝑀 + 1)) → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) = (𝐹‘𝑁))) |
51 | | uzp1 8652 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑁 = 𝑀 ∨ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) |
52 | 1, 51 | syl 14 |
. . 3
⊢ (𝜑 → (𝑁 = 𝑀 ∨ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) |
53 | 16, 50, 52 | mpjaod 670 |
. 2
⊢ (𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) = (𝐹‘𝑁)) |
54 | | eqidd 2082 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
55 | 1, 53, 4, 9, 10, 11, 54 | iseqfeq2 9449 |
1
⊢ (𝜑 → (seq𝑀( + , 𝐹, 𝑆) ↾
(ℤ≥‘𝑁)) = seq𝑁( + , 𝐹, 𝑆)) |