Step | Hyp | Ref
| Expression |
1 | | iseqid3s.2 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
2 | | eluzfz2 9051 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁)) |
3 | | fveq2 5198 |
. . . . . 6
⊢ (𝑤 = 𝑀 → (seq𝑀( + , 𝐹, 𝑆)‘𝑤) = (seq𝑀( + , 𝐹, 𝑆)‘𝑀)) |
4 | 3 | eqeq1d 2089 |
. . . . 5
⊢ (𝑤 = 𝑀 → ((seq𝑀( + , 𝐹, 𝑆)‘𝑤) = 𝑍 ↔ (seq𝑀( + , 𝐹, 𝑆)‘𝑀) = 𝑍)) |
5 | 4 | imbi2d 228 |
. . . 4
⊢ (𝑤 = 𝑀 → ((𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘𝑤) = 𝑍) ↔ (𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘𝑀) = 𝑍))) |
6 | | fveq2 5198 |
. . . . . 6
⊢ (𝑤 = 𝑘 → (seq𝑀( + , 𝐹, 𝑆)‘𝑤) = (seq𝑀( + , 𝐹, 𝑆)‘𝑘)) |
7 | 6 | eqeq1d 2089 |
. . . . 5
⊢ (𝑤 = 𝑘 → ((seq𝑀( + , 𝐹, 𝑆)‘𝑤) = 𝑍 ↔ (seq𝑀( + , 𝐹, 𝑆)‘𝑘) = 𝑍)) |
8 | 7 | imbi2d 228 |
. . . 4
⊢ (𝑤 = 𝑘 → ((𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘𝑤) = 𝑍) ↔ (𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘𝑘) = 𝑍))) |
9 | | fveq2 5198 |
. . . . . 6
⊢ (𝑤 = (𝑘 + 1) → (seq𝑀( + , 𝐹, 𝑆)‘𝑤) = (seq𝑀( + , 𝐹, 𝑆)‘(𝑘 + 1))) |
10 | 9 | eqeq1d 2089 |
. . . . 5
⊢ (𝑤 = (𝑘 + 1) → ((seq𝑀( + , 𝐹, 𝑆)‘𝑤) = 𝑍 ↔ (seq𝑀( + , 𝐹, 𝑆)‘(𝑘 + 1)) = 𝑍)) |
11 | 10 | imbi2d 228 |
. . . 4
⊢ (𝑤 = (𝑘 + 1) → ((𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘𝑤) = 𝑍) ↔ (𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘(𝑘 + 1)) = 𝑍))) |
12 | | fveq2 5198 |
. . . . . 6
⊢ (𝑤 = 𝑁 → (seq𝑀( + , 𝐹, 𝑆)‘𝑤) = (seq𝑀( + , 𝐹, 𝑆)‘𝑁)) |
13 | 12 | eqeq1d 2089 |
. . . . 5
⊢ (𝑤 = 𝑁 → ((seq𝑀( + , 𝐹, 𝑆)‘𝑤) = 𝑍 ↔ (seq𝑀( + , 𝐹, 𝑆)‘𝑁) = 𝑍)) |
14 | 13 | imbi2d 228 |
. . . 4
⊢ (𝑤 = 𝑁 → ((𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘𝑤) = 𝑍) ↔ (𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) = 𝑍))) |
15 | | eluzel2 8624 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
16 | 1, 15 | syl 14 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℤ) |
17 | | iseqid3s.s |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈ 𝑉) |
18 | | iseqid3s.f |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆) |
19 | | iseqid3s.cl |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
20 | 16, 17, 18, 19 | iseq1 9442 |
. . . . . 6
⊢ (𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘𝑀) = (𝐹‘𝑀)) |
21 | | iseqid3s.3 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) = 𝑍) |
22 | 21 | ralrimiva 2434 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ (𝑀...𝑁)(𝐹‘𝑥) = 𝑍) |
23 | | eluzfz1 9050 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁)) |
24 | | fveq2 5198 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑀 → (𝐹‘𝑥) = (𝐹‘𝑀)) |
25 | 24 | eqeq1d 2089 |
. . . . . . . . 9
⊢ (𝑥 = 𝑀 → ((𝐹‘𝑥) = 𝑍 ↔ (𝐹‘𝑀) = 𝑍)) |
26 | 25 | rspcv 2697 |
. . . . . . . 8
⊢ (𝑀 ∈ (𝑀...𝑁) → (∀𝑥 ∈ (𝑀...𝑁)(𝐹‘𝑥) = 𝑍 → (𝐹‘𝑀) = 𝑍)) |
27 | 1, 23, 26 | 3syl 17 |
. . . . . . 7
⊢ (𝜑 → (∀𝑥 ∈ (𝑀...𝑁)(𝐹‘𝑥) = 𝑍 → (𝐹‘𝑀) = 𝑍)) |
28 | 22, 27 | mpd 13 |
. . . . . 6
⊢ (𝜑 → (𝐹‘𝑀) = 𝑍) |
29 | 20, 28 | eqtrd 2113 |
. . . . 5
⊢ (𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘𝑀) = 𝑍) |
30 | 29 | a1i 9 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘𝑀) = 𝑍)) |
31 | | elfzouz 9161 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (𝑀..^𝑁) → 𝑘 ∈ (ℤ≥‘𝑀)) |
32 | 31 | adantl 271 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑘 ∈ (ℤ≥‘𝑀)) |
33 | 17 | adantr 270 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑆 ∈ 𝑉) |
34 | 18 | adantlr 460 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆) |
35 | 19 | adantlr 460 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
36 | 32, 33, 34, 35 | iseqp1 9445 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (seq𝑀( + , 𝐹, 𝑆)‘(𝑘 + 1)) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑘) + (𝐹‘(𝑘 + 1)))) |
37 | 36 | adantr 270 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ (seq𝑀( + , 𝐹, 𝑆)‘𝑘) = 𝑍) → (seq𝑀( + , 𝐹, 𝑆)‘(𝑘 + 1)) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑘) + (𝐹‘(𝑘 + 1)))) |
38 | | simpr 108 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ (seq𝑀( + , 𝐹, 𝑆)‘𝑘) = 𝑍) → (seq𝑀( + , 𝐹, 𝑆)‘𝑘) = 𝑍) |
39 | | fzofzp1 9236 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (𝑀..^𝑁) → (𝑘 + 1) ∈ (𝑀...𝑁)) |
40 | 39 | adantl 271 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ∈ (𝑀...𝑁)) |
41 | 22 | adantr 270 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ∀𝑥 ∈ (𝑀...𝑁)(𝐹‘𝑥) = 𝑍) |
42 | | fveq2 5198 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑘 + 1) → (𝐹‘𝑥) = (𝐹‘(𝑘 + 1))) |
43 | 42 | eqeq1d 2089 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑘 + 1) → ((𝐹‘𝑥) = 𝑍 ↔ (𝐹‘(𝑘 + 1)) = 𝑍)) |
44 | 43 | rspcv 2697 |
. . . . . . . . . . 11
⊢ ((𝑘 + 1) ∈ (𝑀...𝑁) → (∀𝑥 ∈ (𝑀...𝑁)(𝐹‘𝑥) = 𝑍 → (𝐹‘(𝑘 + 1)) = 𝑍)) |
45 | 40, 41, 44 | sylc 61 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝐹‘(𝑘 + 1)) = 𝑍) |
46 | 45 | adantr 270 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ (seq𝑀( + , 𝐹, 𝑆)‘𝑘) = 𝑍) → (𝐹‘(𝑘 + 1)) = 𝑍) |
47 | 38, 46 | oveq12d 5550 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ (seq𝑀( + , 𝐹, 𝑆)‘𝑘) = 𝑍) → ((seq𝑀( + , 𝐹, 𝑆)‘𝑘) + (𝐹‘(𝑘 + 1))) = (𝑍 + 𝑍)) |
48 | | iseqid3s.1 |
. . . . . . . . 9
⊢ (𝜑 → (𝑍 + 𝑍) = 𝑍) |
49 | 48 | ad2antrr 471 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ (seq𝑀( + , 𝐹, 𝑆)‘𝑘) = 𝑍) → (𝑍 + 𝑍) = 𝑍) |
50 | 37, 47, 49 | 3eqtrd 2117 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ (seq𝑀( + , 𝐹, 𝑆)‘𝑘) = 𝑍) → (seq𝑀( + , 𝐹, 𝑆)‘(𝑘 + 1)) = 𝑍) |
51 | 50 | ex 113 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((seq𝑀( + , 𝐹, 𝑆)‘𝑘) = 𝑍 → (seq𝑀( + , 𝐹, 𝑆)‘(𝑘 + 1)) = 𝑍)) |
52 | 51 | expcom 114 |
. . . . 5
⊢ (𝑘 ∈ (𝑀..^𝑁) → (𝜑 → ((seq𝑀( + , 𝐹, 𝑆)‘𝑘) = 𝑍 → (seq𝑀( + , 𝐹, 𝑆)‘(𝑘 + 1)) = 𝑍))) |
53 | 52 | a2d 26 |
. . . 4
⊢ (𝑘 ∈ (𝑀..^𝑁) → ((𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘𝑘) = 𝑍) → (𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘(𝑘 + 1)) = 𝑍))) |
54 | 5, 8, 11, 14, 30, 53 | fzind2 9248 |
. . 3
⊢ (𝑁 ∈ (𝑀...𝑁) → (𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) = 𝑍)) |
55 | 1, 2, 54 | 3syl 17 |
. 2
⊢ (𝜑 → (𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) = 𝑍)) |
56 | 55 | pm2.43i 48 |
1
⊢ (𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) = 𝑍) |