Step | Hyp | Ref
| Expression |
1 | | iseqss.m |
. . 3
⊢ (𝜑 → 𝑀 ∈ ℤ) |
2 | | iseqss.t |
. . . 4
⊢ (𝜑 → 𝑇 ∈ 𝑉) |
3 | | iseqss.ss |
. . . 4
⊢ (𝜑 → 𝑆 ⊆ 𝑇) |
4 | 2, 3 | ssexd 3918 |
. . 3
⊢ (𝜑 → 𝑆 ∈ V) |
5 | | iseqss.f |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆) |
6 | | iseqss.pl |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
7 | 1, 4, 5, 6 | iseqfn 9441 |
. 2
⊢ (𝜑 → seq𝑀( + , 𝐹, 𝑆) Fn (ℤ≥‘𝑀)) |
8 | 3 | sseld 2998 |
. . . . 5
⊢ (𝜑 → ((𝐹‘𝑥) ∈ 𝑆 → (𝐹‘𝑥) ∈ 𝑇)) |
9 | 8 | adantr 270 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → ((𝐹‘𝑥) ∈ 𝑆 → (𝐹‘𝑥) ∈ 𝑇)) |
10 | 5, 9 | mpd 13 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑇) |
11 | | iseqss.plt |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑇)) → (𝑥 + 𝑦) ∈ 𝑇) |
12 | 1, 2, 10, 11 | iseqfn 9441 |
. 2
⊢ (𝜑 → seq𝑀( + , 𝐹, 𝑇) Fn (ℤ≥‘𝑀)) |
13 | | fveq2 5198 |
. . . . . 6
⊢ (𝑤 = 𝑀 → (seq𝑀( + , 𝐹, 𝑆)‘𝑤) = (seq𝑀( + , 𝐹, 𝑆)‘𝑀)) |
14 | | fveq2 5198 |
. . . . . 6
⊢ (𝑤 = 𝑀 → (seq𝑀( + , 𝐹, 𝑇)‘𝑤) = (seq𝑀( + , 𝐹, 𝑇)‘𝑀)) |
15 | 13, 14 | eqeq12d 2095 |
. . . . 5
⊢ (𝑤 = 𝑀 → ((seq𝑀( + , 𝐹, 𝑆)‘𝑤) = (seq𝑀( + , 𝐹, 𝑇)‘𝑤) ↔ (seq𝑀( + , 𝐹, 𝑆)‘𝑀) = (seq𝑀( + , 𝐹, 𝑇)‘𝑀))) |
16 | 15 | imbi2d 228 |
. . . 4
⊢ (𝑤 = 𝑀 → ((𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘𝑤) = (seq𝑀( + , 𝐹, 𝑇)‘𝑤)) ↔ (𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘𝑀) = (seq𝑀( + , 𝐹, 𝑇)‘𝑀)))) |
17 | | fveq2 5198 |
. . . . . 6
⊢ (𝑤 = 𝑘 → (seq𝑀( + , 𝐹, 𝑆)‘𝑤) = (seq𝑀( + , 𝐹, 𝑆)‘𝑘)) |
18 | | fveq2 5198 |
. . . . . 6
⊢ (𝑤 = 𝑘 → (seq𝑀( + , 𝐹, 𝑇)‘𝑤) = (seq𝑀( + , 𝐹, 𝑇)‘𝑘)) |
19 | 17, 18 | eqeq12d 2095 |
. . . . 5
⊢ (𝑤 = 𝑘 → ((seq𝑀( + , 𝐹, 𝑆)‘𝑤) = (seq𝑀( + , 𝐹, 𝑇)‘𝑤) ↔ (seq𝑀( + , 𝐹, 𝑆)‘𝑘) = (seq𝑀( + , 𝐹, 𝑇)‘𝑘))) |
20 | 19 | imbi2d 228 |
. . . 4
⊢ (𝑤 = 𝑘 → ((𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘𝑤) = (seq𝑀( + , 𝐹, 𝑇)‘𝑤)) ↔ (𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘𝑘) = (seq𝑀( + , 𝐹, 𝑇)‘𝑘)))) |
21 | | fveq2 5198 |
. . . . . 6
⊢ (𝑤 = (𝑘 + 1) → (seq𝑀( + , 𝐹, 𝑆)‘𝑤) = (seq𝑀( + , 𝐹, 𝑆)‘(𝑘 + 1))) |
22 | | fveq2 5198 |
. . . . . 6
⊢ (𝑤 = (𝑘 + 1) → (seq𝑀( + , 𝐹, 𝑇)‘𝑤) = (seq𝑀( + , 𝐹, 𝑇)‘(𝑘 + 1))) |
23 | 21, 22 | eqeq12d 2095 |
. . . . 5
⊢ (𝑤 = (𝑘 + 1) → ((seq𝑀( + , 𝐹, 𝑆)‘𝑤) = (seq𝑀( + , 𝐹, 𝑇)‘𝑤) ↔ (seq𝑀( + , 𝐹, 𝑆)‘(𝑘 + 1)) = (seq𝑀( + , 𝐹, 𝑇)‘(𝑘 + 1)))) |
24 | 23 | imbi2d 228 |
. . . 4
⊢ (𝑤 = (𝑘 + 1) → ((𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘𝑤) = (seq𝑀( + , 𝐹, 𝑇)‘𝑤)) ↔ (𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘(𝑘 + 1)) = (seq𝑀( + , 𝐹, 𝑇)‘(𝑘 + 1))))) |
25 | | fveq2 5198 |
. . . . . 6
⊢ (𝑤 = 𝑛 → (seq𝑀( + , 𝐹, 𝑆)‘𝑤) = (seq𝑀( + , 𝐹, 𝑆)‘𝑛)) |
26 | | fveq2 5198 |
. . . . . 6
⊢ (𝑤 = 𝑛 → (seq𝑀( + , 𝐹, 𝑇)‘𝑤) = (seq𝑀( + , 𝐹, 𝑇)‘𝑛)) |
27 | 25, 26 | eqeq12d 2095 |
. . . . 5
⊢ (𝑤 = 𝑛 → ((seq𝑀( + , 𝐹, 𝑆)‘𝑤) = (seq𝑀( + , 𝐹, 𝑇)‘𝑤) ↔ (seq𝑀( + , 𝐹, 𝑆)‘𝑛) = (seq𝑀( + , 𝐹, 𝑇)‘𝑛))) |
28 | 27 | imbi2d 228 |
. . . 4
⊢ (𝑤 = 𝑛 → ((𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘𝑤) = (seq𝑀( + , 𝐹, 𝑇)‘𝑤)) ↔ (𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘𝑛) = (seq𝑀( + , 𝐹, 𝑇)‘𝑛)))) |
29 | 1, 4, 5, 6 | iseq1 9442 |
. . . . . 6
⊢ (𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘𝑀) = (𝐹‘𝑀)) |
30 | 1, 2, 10, 11 | iseq1 9442 |
. . . . . 6
⊢ (𝜑 → (seq𝑀( + , 𝐹, 𝑇)‘𝑀) = (𝐹‘𝑀)) |
31 | 29, 30 | eqtr4d 2116 |
. . . . 5
⊢ (𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘𝑀) = (seq𝑀( + , 𝐹, 𝑇)‘𝑀)) |
32 | 31 | a1i 9 |
. . . 4
⊢ (𝑀 ∈ ℤ → (𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘𝑀) = (seq𝑀( + , 𝐹, 𝑇)‘𝑀))) |
33 | | oveq1 5539 |
. . . . . . 7
⊢
((seq𝑀( + , 𝐹, 𝑆)‘𝑘) = (seq𝑀( + , 𝐹, 𝑇)‘𝑘) → ((seq𝑀( + , 𝐹, 𝑆)‘𝑘) + (𝐹‘(𝑘 + 1))) = ((seq𝑀( + , 𝐹, 𝑇)‘𝑘) + (𝐹‘(𝑘 + 1)))) |
34 | | simpr 108 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → 𝑘 ∈ (ℤ≥‘𝑀)) |
35 | 4 | adantr 270 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → 𝑆 ∈ V) |
36 | 5 | adantlr 460 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆) |
37 | 6 | adantlr 460 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
38 | 34, 35, 36, 37 | iseqp1 9445 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (seq𝑀( + , 𝐹, 𝑆)‘(𝑘 + 1)) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑘) + (𝐹‘(𝑘 + 1)))) |
39 | 2 | adantr 270 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → 𝑇 ∈ 𝑉) |
40 | 10 | adantlr 460 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑇) |
41 | 11 | adantlr 460 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) ∧ (𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑇)) → (𝑥 + 𝑦) ∈ 𝑇) |
42 | 34, 39, 40, 41 | iseqp1 9445 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (seq𝑀( + , 𝐹, 𝑇)‘(𝑘 + 1)) = ((seq𝑀( + , 𝐹, 𝑇)‘𝑘) + (𝐹‘(𝑘 + 1)))) |
43 | 38, 42 | eqeq12d 2095 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((seq𝑀( + , 𝐹, 𝑆)‘(𝑘 + 1)) = (seq𝑀( + , 𝐹, 𝑇)‘(𝑘 + 1)) ↔ ((seq𝑀( + , 𝐹, 𝑆)‘𝑘) + (𝐹‘(𝑘 + 1))) = ((seq𝑀( + , 𝐹, 𝑇)‘𝑘) + (𝐹‘(𝑘 + 1))))) |
44 | 33, 43 | syl5ibr 154 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((seq𝑀( + , 𝐹, 𝑆)‘𝑘) = (seq𝑀( + , 𝐹, 𝑇)‘𝑘) → (seq𝑀( + , 𝐹, 𝑆)‘(𝑘 + 1)) = (seq𝑀( + , 𝐹, 𝑇)‘(𝑘 + 1)))) |
45 | 44 | expcom 114 |
. . . . 5
⊢ (𝑘 ∈
(ℤ≥‘𝑀) → (𝜑 → ((seq𝑀( + , 𝐹, 𝑆)‘𝑘) = (seq𝑀( + , 𝐹, 𝑇)‘𝑘) → (seq𝑀( + , 𝐹, 𝑆)‘(𝑘 + 1)) = (seq𝑀( + , 𝐹, 𝑇)‘(𝑘 + 1))))) |
46 | 45 | a2d 26 |
. . . 4
⊢ (𝑘 ∈
(ℤ≥‘𝑀) → ((𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘𝑘) = (seq𝑀( + , 𝐹, 𝑇)‘𝑘)) → (𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘(𝑘 + 1)) = (seq𝑀( + , 𝐹, 𝑇)‘(𝑘 + 1))))) |
47 | 16, 20, 24, 28, 32, 46 | uzind4 8676 |
. . 3
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → (𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘𝑛) = (seq𝑀( + , 𝐹, 𝑇)‘𝑛))) |
48 | 47 | impcom 123 |
. 2
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (seq𝑀( + , 𝐹, 𝑆)‘𝑛) = (seq𝑀( + , 𝐹, 𝑇)‘𝑛)) |
49 | 7, 12, 48 | eqfnfvd 5289 |
1
⊢ (𝜑 → seq𝑀( + , 𝐹, 𝑆) = seq𝑀( + , 𝐹, 𝑇)) |