Step | Hyp | Ref
| Expression |
1 | | iseqfveq2.3 |
. . 3
⊢ (φ → 𝑁 ∈
(ℤ≥‘𝐾)) |
2 | | eluzfz2 8666 |
. . 3
⊢ (𝑁 ∈ (ℤ≥‘𝐾) → 𝑁 ∈ (𝐾...𝑁)) |
3 | 1, 2 | syl 14 |
. 2
⊢ (φ → 𝑁 ∈ (𝐾...𝑁)) |
4 | | eleq1 2097 |
. . . . . 6
⊢ (z = 𝐾 → (z ∈ (𝐾...𝑁) ↔ 𝐾 ∈ (𝐾...𝑁))) |
5 | | fveq2 5121 |
. . . . . . 7
⊢ (z = 𝐾 → (seq𝑀( + , 𝐹, 𝑆)‘z) = (seq𝑀( + , 𝐹, 𝑆)‘𝐾)) |
6 | | fveq2 5121 |
. . . . . . 7
⊢ (z = 𝐾 → (seq𝐾( + , 𝐺, 𝑆)‘z) = (seq𝐾( + , 𝐺, 𝑆)‘𝐾)) |
7 | 5, 6 | eqeq12d 2051 |
. . . . . 6
⊢ (z = 𝐾 → ((seq𝑀( + , 𝐹, 𝑆)‘z) = (seq𝐾( + , 𝐺, 𝑆)‘z) ↔ (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝐾( + , 𝐺, 𝑆)‘𝐾))) |
8 | 4, 7 | imbi12d 223 |
. . . . 5
⊢ (z = 𝐾 → ((z ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘z) = (seq𝐾( + , 𝐺, 𝑆)‘z)) ↔ (𝐾 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝐾( + , 𝐺, 𝑆)‘𝐾)))) |
9 | 8 | imbi2d 219 |
. . . 4
⊢ (z = 𝐾 → ((φ → (z ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘z) = (seq𝐾( + , 𝐺, 𝑆)‘z))) ↔ (φ → (𝐾 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝐾( + , 𝐺, 𝑆)‘𝐾))))) |
10 | | eleq1 2097 |
. . . . . 6
⊢ (z = w →
(z ∈
(𝐾...𝑁) ↔ w ∈ (𝐾...𝑁))) |
11 | | fveq2 5121 |
. . . . . . 7
⊢ (z = w →
(seq𝑀( + , 𝐹, 𝑆)‘z) = (seq𝑀( + , 𝐹, 𝑆)‘w)) |
12 | | fveq2 5121 |
. . . . . . 7
⊢ (z = w →
(seq𝐾( + , 𝐺, 𝑆)‘z) = (seq𝐾( + , 𝐺, 𝑆)‘w)) |
13 | 11, 12 | eqeq12d 2051 |
. . . . . 6
⊢ (z = w →
((seq𝑀( + , 𝐹, 𝑆)‘z) = (seq𝐾( + , 𝐺, 𝑆)‘z) ↔ (seq𝑀( + , 𝐹, 𝑆)‘w) = (seq𝐾( + , 𝐺, 𝑆)‘w))) |
14 | 10, 13 | imbi12d 223 |
. . . . 5
⊢ (z = w →
((z ∈
(𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘z) = (seq𝐾( + , 𝐺, 𝑆)‘z)) ↔ (w
∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘w) = (seq𝐾( + , 𝐺, 𝑆)‘w)))) |
15 | 14 | imbi2d 219 |
. . . 4
⊢ (z = w →
((φ → (z ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘z) = (seq𝐾( + , 𝐺, 𝑆)‘z))) ↔ (φ → (w ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘w) = (seq𝐾( + , 𝐺, 𝑆)‘w))))) |
16 | | eleq1 2097 |
. . . . . 6
⊢ (z = (w + 1)
→ (z ∈ (𝐾...𝑁) ↔ (w + 1) ∈ (𝐾...𝑁))) |
17 | | fveq2 5121 |
. . . . . . 7
⊢ (z = (w + 1)
→ (seq𝑀( + , 𝐹, 𝑆)‘z) = (seq𝑀( + , 𝐹, 𝑆)‘(w + 1))) |
18 | | fveq2 5121 |
. . . . . . 7
⊢ (z = (w + 1)
→ (seq𝐾( + , 𝐺, 𝑆)‘z) = (seq𝐾( + , 𝐺, 𝑆)‘(w + 1))) |
19 | 17, 18 | eqeq12d 2051 |
. . . . . 6
⊢ (z = (w + 1)
→ ((seq𝑀( + , 𝐹, 𝑆)‘z) = (seq𝐾( + , 𝐺, 𝑆)‘z) ↔ (seq𝑀( + , 𝐹, 𝑆)‘(w + 1)) = (seq𝐾( + , 𝐺, 𝑆)‘(w + 1)))) |
20 | 16, 19 | imbi12d 223 |
. . . . 5
⊢ (z = (w + 1)
→ ((z ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘z) = (seq𝐾( + , 𝐺, 𝑆)‘z)) ↔ ((w +
1) ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘(w + 1)) = (seq𝐾( + , 𝐺, 𝑆)‘(w + 1))))) |
21 | 20 | imbi2d 219 |
. . . 4
⊢ (z = (w + 1)
→ ((φ → (z ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘z) = (seq𝐾( + , 𝐺, 𝑆)‘z))) ↔ (φ → ((w + 1) ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘(w + 1)) = (seq𝐾( + , 𝐺, 𝑆)‘(w + 1)))))) |
22 | | eleq1 2097 |
. . . . . 6
⊢ (z = 𝑁 → (z ∈ (𝐾...𝑁) ↔ 𝑁 ∈ (𝐾...𝑁))) |
23 | | fveq2 5121 |
. . . . . . 7
⊢ (z = 𝑁 → (seq𝑀( + , 𝐹, 𝑆)‘z) = (seq𝑀( + , 𝐹, 𝑆)‘𝑁)) |
24 | | fveq2 5121 |
. . . . . . 7
⊢ (z = 𝑁 → (seq𝐾( + , 𝐺, 𝑆)‘z) = (seq𝐾( + , 𝐺, 𝑆)‘𝑁)) |
25 | 23, 24 | eqeq12d 2051 |
. . . . . 6
⊢ (z = 𝑁 → ((seq𝑀( + , 𝐹, 𝑆)‘z) = (seq𝐾( + , 𝐺, 𝑆)‘z) ↔ (seq𝑀( + , 𝐹, 𝑆)‘𝑁) = (seq𝐾( + , 𝐺, 𝑆)‘𝑁))) |
26 | 22, 25 | imbi12d 223 |
. . . . 5
⊢ (z = 𝑁 → ((z ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘z) = (seq𝐾( + , 𝐺, 𝑆)‘z)) ↔ (𝑁 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) = (seq𝐾( + , 𝐺, 𝑆)‘𝑁)))) |
27 | 26 | imbi2d 219 |
. . . 4
⊢ (z = 𝑁 → ((φ → (z ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘z) = (seq𝐾( + , 𝐺, 𝑆)‘z))) ↔ (φ → (𝑁 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) = (seq𝐾( + , 𝐺, 𝑆)‘𝑁))))) |
28 | | iseqfveq2.2 |
. . . . . . 7
⊢ (φ → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (𝐺‘𝐾)) |
29 | | iseqfveq2.1 |
. . . . . . . . 9
⊢ (φ → 𝐾 ∈
(ℤ≥‘𝑀)) |
30 | | eluzelz 8258 |
. . . . . . . . 9
⊢ (𝐾 ∈ (ℤ≥‘𝑀) → 𝐾 ∈
ℤ) |
31 | 29, 30 | syl 14 |
. . . . . . . 8
⊢ (φ → 𝐾 ∈
ℤ) |
32 | | iseqfveq2.s |
. . . . . . . 8
⊢ (φ → 𝑆 ∈ 𝑉) |
33 | | iseqfveq2.g |
. . . . . . . 8
⊢ ((φ ∧ x ∈
(ℤ≥‘𝐾)) → (𝐺‘x) ∈ 𝑆) |
34 | | iseqfveq2.pl |
. . . . . . . 8
⊢ ((φ ∧
(x ∈
𝑆 ∧ y ∈ 𝑆)) → (x + y) ∈ 𝑆) |
35 | 31, 32, 33, 34 | iseq1 8902 |
. . . . . . 7
⊢ (φ → (seq𝐾( + , 𝐺, 𝑆)‘𝐾) = (𝐺‘𝐾)) |
36 | 28, 35 | eqtr4d 2072 |
. . . . . 6
⊢ (φ → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝐾( + , 𝐺, 𝑆)‘𝐾)) |
37 | 36 | a1d 22 |
. . . . 5
⊢ (φ → (𝐾 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝐾( + , 𝐺, 𝑆)‘𝐾))) |
38 | 37 | a1i 9 |
. . . 4
⊢ (𝐾 ∈ ℤ → (φ → (𝐾 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝐾( + , 𝐺, 𝑆)‘𝐾)))) |
39 | | peano2fzr 8671 |
. . . . . . . . . 10
⊢
((w ∈ (ℤ≥‘𝐾) ∧
(w + 1) ∈
(𝐾...𝑁)) → w ∈ (𝐾...𝑁)) |
40 | 39 | adantl 262 |
. . . . . . . . 9
⊢ ((φ ∧
(w ∈
(ℤ≥‘𝐾) ∧
(w + 1) ∈
(𝐾...𝑁))) → w ∈ (𝐾...𝑁)) |
41 | 40 | expr 357 |
. . . . . . . 8
⊢ ((φ ∧ w ∈
(ℤ≥‘𝐾)) → ((w + 1) ∈ (𝐾...𝑁) → w ∈ (𝐾...𝑁))) |
42 | 41 | imim1d 69 |
. . . . . . 7
⊢ ((φ ∧ w ∈
(ℤ≥‘𝐾)) → ((w ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘w) = (seq𝐾( + , 𝐺, 𝑆)‘w)) → ((w +
1) ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘w) = (seq𝐾( + , 𝐺, 𝑆)‘w)))) |
43 | | oveq1 5462 |
. . . . . . . . . 10
⊢
((seq𝑀( + , 𝐹, 𝑆)‘w) = (seq𝐾( + , 𝐺, 𝑆)‘w) → ((seq𝑀( + , 𝐹, 𝑆)‘w) + (𝐹‘(w + 1))) = ((seq𝐾( + , 𝐺, 𝑆)‘w) + (𝐹‘(w + 1)))) |
44 | | simprl 483 |
. . . . . . . . . . . . 13
⊢ ((φ ∧
(w ∈
(ℤ≥‘𝐾) ∧
(w + 1) ∈
(𝐾...𝑁))) → w ∈
(ℤ≥‘𝐾)) |
45 | 29 | adantr 261 |
. . . . . . . . . . . . 13
⊢ ((φ ∧
(w ∈
(ℤ≥‘𝐾) ∧
(w + 1) ∈
(𝐾...𝑁))) → 𝐾 ∈
(ℤ≥‘𝑀)) |
46 | | uztrn 8265 |
. . . . . . . . . . . . 13
⊢
((w ∈ (ℤ≥‘𝐾) ∧ 𝐾 ∈ (ℤ≥‘𝑀)) → w ∈
(ℤ≥‘𝑀)) |
47 | 44, 45, 46 | syl2anc 391 |
. . . . . . . . . . . 12
⊢ ((φ ∧
(w ∈
(ℤ≥‘𝐾) ∧
(w + 1) ∈
(𝐾...𝑁))) → w ∈
(ℤ≥‘𝑀)) |
48 | 32 | adantr 261 |
. . . . . . . . . . . 12
⊢ ((φ ∧
(w ∈
(ℤ≥‘𝐾) ∧
(w + 1) ∈
(𝐾...𝑁))) → 𝑆 ∈ 𝑉) |
49 | | iseqfveq2.f |
. . . . . . . . . . . . 13
⊢ ((φ ∧ x ∈
(ℤ≥‘𝑀)) → (𝐹‘x) ∈ 𝑆) |
50 | 49 | adantlr 446 |
. . . . . . . . . . . 12
⊢ (((φ ∧
(w ∈
(ℤ≥‘𝐾) ∧
(w + 1) ∈
(𝐾...𝑁))) ∧
x ∈
(ℤ≥‘𝑀)) → (𝐹‘x) ∈ 𝑆) |
51 | 34 | adantlr 446 |
. . . . . . . . . . . 12
⊢ (((φ ∧
(w ∈
(ℤ≥‘𝐾) ∧
(w + 1) ∈
(𝐾...𝑁))) ∧
(x ∈
𝑆 ∧ y ∈ 𝑆)) → (x + y) ∈ 𝑆) |
52 | 47, 48, 50, 51 | iseqp1 8904 |
. . . . . . . . . . 11
⊢ ((φ ∧
(w ∈
(ℤ≥‘𝐾) ∧
(w + 1) ∈
(𝐾...𝑁))) → (seq𝑀( + , 𝐹, 𝑆)‘(w + 1)) = ((seq𝑀( + , 𝐹, 𝑆)‘w) + (𝐹‘(w + 1)))) |
53 | 33 | adantlr 446 |
. . . . . . . . . . . . 13
⊢ (((φ ∧
(w ∈
(ℤ≥‘𝐾) ∧
(w + 1) ∈
(𝐾...𝑁))) ∧
x ∈
(ℤ≥‘𝐾)) → (𝐺‘x) ∈ 𝑆) |
54 | 44, 48, 53, 51 | iseqp1 8904 |
. . . . . . . . . . . 12
⊢ ((φ ∧
(w ∈
(ℤ≥‘𝐾) ∧
(w + 1) ∈
(𝐾...𝑁))) → (seq𝐾( + , 𝐺, 𝑆)‘(w + 1)) = ((seq𝐾( + , 𝐺, 𝑆)‘w) + (𝐺‘(w + 1)))) |
55 | | eluzp1p1 8274 |
. . . . . . . . . . . . . . . 16
⊢ (w ∈
(ℤ≥‘𝐾) → (w + 1) ∈
(ℤ≥‘(𝐾 + 1))) |
56 | 55 | ad2antrl 459 |
. . . . . . . . . . . . . . 15
⊢ ((φ ∧
(w ∈
(ℤ≥‘𝐾) ∧
(w + 1) ∈
(𝐾...𝑁))) → (w + 1) ∈
(ℤ≥‘(𝐾 + 1))) |
57 | | elfzuz3 8657 |
. . . . . . . . . . . . . . . 16
⊢
((w + 1) ∈ (𝐾...𝑁) → 𝑁 ∈
(ℤ≥‘(w +
1))) |
58 | 57 | ad2antll 460 |
. . . . . . . . . . . . . . 15
⊢ ((φ ∧
(w ∈
(ℤ≥‘𝐾) ∧
(w + 1) ∈
(𝐾...𝑁))) → 𝑁 ∈
(ℤ≥‘(w +
1))) |
59 | | elfzuzb 8654 |
. . . . . . . . . . . . . . 15
⊢
((w + 1) ∈ ((𝐾 + 1)...𝑁) ↔ ((w + 1) ∈
(ℤ≥‘(𝐾 + 1)) ∧
𝑁 ∈ (ℤ≥‘(w + 1)))) |
60 | 56, 58, 59 | sylanbrc 394 |
. . . . . . . . . . . . . 14
⊢ ((φ ∧
(w ∈
(ℤ≥‘𝐾) ∧
(w + 1) ∈
(𝐾...𝑁))) → (w + 1) ∈ ((𝐾 + 1)...𝑁)) |
61 | | iseqfveq2.4 |
. . . . . . . . . . . . . . . 16
⊢ ((φ ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝐹‘𝑘) = (𝐺‘𝑘)) |
62 | 61 | ralrimiva 2386 |
. . . . . . . . . . . . . . 15
⊢ (φ → ∀𝑘 ∈ ((𝐾 + 1)...𝑁)(𝐹‘𝑘) = (𝐺‘𝑘)) |
63 | 62 | adantr 261 |
. . . . . . . . . . . . . 14
⊢ ((φ ∧
(w ∈
(ℤ≥‘𝐾) ∧
(w + 1) ∈
(𝐾...𝑁))) → ∀𝑘 ∈ ((𝐾 + 1)...𝑁)(𝐹‘𝑘) = (𝐺‘𝑘)) |
64 | | fveq2 5121 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = (w + 1) → (𝐹‘𝑘) = (𝐹‘(w + 1))) |
65 | | fveq2 5121 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = (w + 1) → (𝐺‘𝑘) = (𝐺‘(w + 1))) |
66 | 64, 65 | eqeq12d 2051 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = (w + 1) → ((𝐹‘𝑘) = (𝐺‘𝑘) ↔ (𝐹‘(w + 1)) = (𝐺‘(w + 1)))) |
67 | 66 | rspcv 2646 |
. . . . . . . . . . . . . 14
⊢
((w + 1) ∈ ((𝐾 + 1)...𝑁) → (∀𝑘 ∈ ((𝐾 + 1)...𝑁)(𝐹‘𝑘) = (𝐺‘𝑘) → (𝐹‘(w + 1)) = (𝐺‘(w + 1)))) |
68 | 60, 63, 67 | sylc 56 |
. . . . . . . . . . . . 13
⊢ ((φ ∧
(w ∈
(ℤ≥‘𝐾) ∧
(w + 1) ∈
(𝐾...𝑁))) → (𝐹‘(w + 1)) = (𝐺‘(w + 1))) |
69 | 68 | oveq2d 5471 |
. . . . . . . . . . . 12
⊢ ((φ ∧
(w ∈
(ℤ≥‘𝐾) ∧
(w + 1) ∈
(𝐾...𝑁))) → ((seq𝐾( + , 𝐺, 𝑆)‘w) + (𝐹‘(w + 1))) = ((seq𝐾( + , 𝐺, 𝑆)‘w) + (𝐺‘(w + 1)))) |
70 | 54, 69 | eqtr4d 2072 |
. . . . . . . . . . 11
⊢ ((φ ∧
(w ∈
(ℤ≥‘𝐾) ∧
(w + 1) ∈
(𝐾...𝑁))) → (seq𝐾( + , 𝐺, 𝑆)‘(w + 1)) = ((seq𝐾( + , 𝐺, 𝑆)‘w) + (𝐹‘(w + 1)))) |
71 | 52, 70 | eqeq12d 2051 |
. . . . . . . . . 10
⊢ ((φ ∧
(w ∈
(ℤ≥‘𝐾) ∧
(w + 1) ∈
(𝐾...𝑁))) → ((seq𝑀( + , 𝐹, 𝑆)‘(w + 1)) = (seq𝐾( + , 𝐺, 𝑆)‘(w + 1)) ↔ ((seq𝑀( + , 𝐹, 𝑆)‘w) + (𝐹‘(w + 1))) = ((seq𝐾( + , 𝐺, 𝑆)‘w) + (𝐹‘(w + 1))))) |
72 | 43, 71 | syl5ibr 145 |
. . . . . . . . 9
⊢ ((φ ∧
(w ∈
(ℤ≥‘𝐾) ∧
(w + 1) ∈
(𝐾...𝑁))) → ((seq𝑀( + , 𝐹, 𝑆)‘w) = (seq𝐾( + , 𝐺, 𝑆)‘w) → (seq𝑀( + , 𝐹, 𝑆)‘(w + 1)) = (seq𝐾( + , 𝐺, 𝑆)‘(w + 1)))) |
73 | 72 | expr 357 |
. . . . . . . 8
⊢ ((φ ∧ w ∈
(ℤ≥‘𝐾)) → ((w + 1) ∈ (𝐾...𝑁) → ((seq𝑀( + , 𝐹, 𝑆)‘w) = (seq𝐾( + , 𝐺, 𝑆)‘w) → (seq𝑀( + , 𝐹, 𝑆)‘(w + 1)) = (seq𝐾( + , 𝐺, 𝑆)‘(w + 1))))) |
74 | 73 | a2d 23 |
. . . . . . 7
⊢ ((φ ∧ w ∈
(ℤ≥‘𝐾)) → (((w + 1) ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘w) = (seq𝐾( + , 𝐺, 𝑆)‘w)) → ((w +
1) ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘(w + 1)) = (seq𝐾( + , 𝐺, 𝑆)‘(w + 1))))) |
75 | 42, 74 | syld 40 |
. . . . . 6
⊢ ((φ ∧ w ∈
(ℤ≥‘𝐾)) → ((w ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘w) = (seq𝐾( + , 𝐺, 𝑆)‘w)) → ((w +
1) ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘(w + 1)) = (seq𝐾( + , 𝐺, 𝑆)‘(w + 1))))) |
76 | 75 | expcom 109 |
. . . . 5
⊢ (w ∈
(ℤ≥‘𝐾) → (φ → ((w ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘w) = (seq𝐾( + , 𝐺, 𝑆)‘w)) → ((w +
1) ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘(w + 1)) = (seq𝐾( + , 𝐺, 𝑆)‘(w + 1)))))) |
77 | 76 | a2d 23 |
. . . 4
⊢ (w ∈
(ℤ≥‘𝐾) → ((φ → (w ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘w) = (seq𝐾( + , 𝐺, 𝑆)‘w))) → (φ → ((w + 1) ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘(w + 1)) = (seq𝐾( + , 𝐺, 𝑆)‘(w + 1)))))) |
78 | 9, 15, 21, 27, 38, 77 | uzind4 8307 |
. . 3
⊢ (𝑁 ∈ (ℤ≥‘𝐾) → (φ → (𝑁 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) = (seq𝐾( + , 𝐺, 𝑆)‘𝑁)))) |
79 | 1, 78 | mpcom 32 |
. 2
⊢ (φ → (𝑁 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) = (seq𝐾( + , 𝐺, 𝑆)‘𝑁))) |
80 | 3, 79 | mpd 13 |
1
⊢ (φ → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) = (seq𝐾( + , 𝐺, 𝑆)‘𝑁)) |