Step | Hyp | Ref
| Expression |
1 | | iseqcaopr2.1 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
2 | | iseqcaopr2.2 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑄𝑦) ∈ 𝑆) |
3 | | iseqcaopr2.4 |
. 2
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
4 | | iseqcaopr2.5 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ 𝑆) |
5 | | iseqcaopr2.6 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑘) ∈ 𝑆) |
6 | | iseqcaopr2.7 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐻‘𝑘) = ((𝐹‘𝑘)𝑄(𝐺‘𝑘))) |
7 | | elfzouz 9008 |
. . . . 5
⊢ (𝑛 ∈ (𝑀..^𝑁) → 𝑛 ∈ (ℤ≥‘𝑀)) |
8 | 7 | adantl 262 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → 𝑛 ∈ (ℤ≥‘𝑀)) |
9 | | iseqcaopr2.s |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ 𝑉) |
10 | 9 | adantr 261 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → 𝑆 ∈ 𝑉) |
11 | 5 | ralrimiva 2392 |
. . . . . 6
⊢ (𝜑 → ∀𝑘 ∈ (ℤ≥‘𝑀)(𝐺‘𝑘) ∈ 𝑆) |
12 | 11 | adantr 261 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → ∀𝑘 ∈ (ℤ≥‘𝑀)(𝐺‘𝑘) ∈ 𝑆) |
13 | | fveq2 5178 |
. . . . . . 7
⊢ (𝑘 = 𝑥 → (𝐺‘𝑘) = (𝐺‘𝑥)) |
14 | 13 | eleq1d 2106 |
. . . . . 6
⊢ (𝑘 = 𝑥 → ((𝐺‘𝑘) ∈ 𝑆 ↔ (𝐺‘𝑥) ∈ 𝑆)) |
15 | 14 | rspccva 2655 |
. . . . 5
⊢
((∀𝑘 ∈
(ℤ≥‘𝑀)(𝐺‘𝑘) ∈ 𝑆 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑥) ∈ 𝑆) |
16 | 12, 15 | sylan 267 |
. . . 4
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑥) ∈ 𝑆) |
17 | 1 | adantlr 446 |
. . . 4
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
18 | 8, 10, 16, 17 | iseqcl 9223 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (seq𝑀( + , 𝐺, 𝑆)‘𝑛) ∈ 𝑆) |
19 | | fzssuz 8928 |
. . . . 5
⊢ (𝑀...𝑁) ⊆
(ℤ≥‘𝑀) |
20 | | fzofzp1 9083 |
. . . . 5
⊢ (𝑛 ∈ (𝑀..^𝑁) → (𝑛 + 1) ∈ (𝑀...𝑁)) |
21 | 19, 20 | sseldi 2943 |
. . . 4
⊢ (𝑛 ∈ (𝑀..^𝑁) → (𝑛 + 1) ∈
(ℤ≥‘𝑀)) |
22 | | fveq2 5178 |
. . . . . 6
⊢ (𝑘 = (𝑛 + 1) → (𝐺‘𝑘) = (𝐺‘(𝑛 + 1))) |
23 | 22 | eleq1d 2106 |
. . . . 5
⊢ (𝑘 = (𝑛 + 1) → ((𝐺‘𝑘) ∈ 𝑆 ↔ (𝐺‘(𝑛 + 1)) ∈ 𝑆)) |
24 | 23 | rspccva 2655 |
. . . 4
⊢
((∀𝑘 ∈
(ℤ≥‘𝑀)(𝐺‘𝑘) ∈ 𝑆 ∧ (𝑛 + 1) ∈
(ℤ≥‘𝑀)) → (𝐺‘(𝑛 + 1)) ∈ 𝑆) |
25 | 11, 21, 24 | syl2an 273 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (𝐺‘(𝑛 + 1)) ∈ 𝑆) |
26 | 4 | ralrimiva 2392 |
. . . . . . 7
⊢ (𝜑 → ∀𝑘 ∈ (ℤ≥‘𝑀)(𝐹‘𝑘) ∈ 𝑆) |
27 | | fveq2 5178 |
. . . . . . . . 9
⊢ (𝑘 = 𝑥 → (𝐹‘𝑘) = (𝐹‘𝑥)) |
28 | 27 | eleq1d 2106 |
. . . . . . . 8
⊢ (𝑘 = 𝑥 → ((𝐹‘𝑘) ∈ 𝑆 ↔ (𝐹‘𝑥) ∈ 𝑆)) |
29 | 28 | rspccva 2655 |
. . . . . . 7
⊢
((∀𝑘 ∈
(ℤ≥‘𝑀)(𝐹‘𝑘) ∈ 𝑆 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆) |
30 | 26, 29 | sylan 267 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆) |
31 | 30 | adantlr 446 |
. . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆) |
32 | 8, 10, 31, 17 | iseqcl 9223 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (seq𝑀( + , 𝐹, 𝑆)‘𝑛) ∈ 𝑆) |
33 | | fveq2 5178 |
. . . . . . 7
⊢ (𝑘 = (𝑛 + 1) → (𝐹‘𝑘) = (𝐹‘(𝑛 + 1))) |
34 | 33 | eleq1d 2106 |
. . . . . 6
⊢ (𝑘 = (𝑛 + 1) → ((𝐹‘𝑘) ∈ 𝑆 ↔ (𝐹‘(𝑛 + 1)) ∈ 𝑆)) |
35 | 34 | rspccva 2655 |
. . . . 5
⊢
((∀𝑘 ∈
(ℤ≥‘𝑀)(𝐹‘𝑘) ∈ 𝑆 ∧ (𝑛 + 1) ∈
(ℤ≥‘𝑀)) → (𝐹‘(𝑛 + 1)) ∈ 𝑆) |
36 | 26, 21, 35 | syl2an 273 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (𝐹‘(𝑛 + 1)) ∈ 𝑆) |
37 | | iseqcaopr2.3 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆))) → ((𝑥𝑄𝑧) + (𝑦𝑄𝑤)) = ((𝑥 + 𝑦)𝑄(𝑧 + 𝑤))) |
38 | 37 | anassrs 380 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → ((𝑥𝑄𝑧) + (𝑦𝑄𝑤)) = ((𝑥 + 𝑦)𝑄(𝑧 + 𝑤))) |
39 | 38 | ralrimivva 2401 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → ∀𝑧 ∈ 𝑆 ∀𝑤 ∈ 𝑆 ((𝑥𝑄𝑧) + (𝑦𝑄𝑤)) = ((𝑥 + 𝑦)𝑄(𝑧 + 𝑤))) |
40 | 39 | ralrimivva 2401 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 ∀𝑤 ∈ 𝑆 ((𝑥𝑄𝑧) + (𝑦𝑄𝑤)) = ((𝑥 + 𝑦)𝑄(𝑧 + 𝑤))) |
41 | 40 | adantr 261 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 ∀𝑤 ∈ 𝑆 ((𝑥𝑄𝑧) + (𝑦𝑄𝑤)) = ((𝑥 + 𝑦)𝑄(𝑧 + 𝑤))) |
42 | | oveq1 5519 |
. . . . . . . 8
⊢ (𝑥 = (seq𝑀( + , 𝐹, 𝑆)‘𝑛) → (𝑥𝑄𝑧) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑛)𝑄𝑧)) |
43 | 42 | oveq1d 5527 |
. . . . . . 7
⊢ (𝑥 = (seq𝑀( + , 𝐹, 𝑆)‘𝑛) → ((𝑥𝑄𝑧) + (𝑦𝑄𝑤)) = (((seq𝑀( + , 𝐹, 𝑆)‘𝑛)𝑄𝑧) + (𝑦𝑄𝑤))) |
44 | | oveq1 5519 |
. . . . . . . 8
⊢ (𝑥 = (seq𝑀( + , 𝐹, 𝑆)‘𝑛) → (𝑥 + 𝑦) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + 𝑦)) |
45 | 44 | oveq1d 5527 |
. . . . . . 7
⊢ (𝑥 = (seq𝑀( + , 𝐹, 𝑆)‘𝑛) → ((𝑥 + 𝑦)𝑄(𝑧 + 𝑤)) = (((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + 𝑦)𝑄(𝑧 + 𝑤))) |
46 | 43, 45 | eqeq12d 2054 |
. . . . . 6
⊢ (𝑥 = (seq𝑀( + , 𝐹, 𝑆)‘𝑛) → (((𝑥𝑄𝑧) + (𝑦𝑄𝑤)) = ((𝑥 + 𝑦)𝑄(𝑧 + 𝑤)) ↔ (((seq𝑀( + , 𝐹, 𝑆)‘𝑛)𝑄𝑧) + (𝑦𝑄𝑤)) = (((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + 𝑦)𝑄(𝑧 + 𝑤)))) |
47 | 46 | 2ralbidv 2348 |
. . . . 5
⊢ (𝑥 = (seq𝑀( + , 𝐹, 𝑆)‘𝑛) → (∀𝑧 ∈ 𝑆 ∀𝑤 ∈ 𝑆 ((𝑥𝑄𝑧) + (𝑦𝑄𝑤)) = ((𝑥 + 𝑦)𝑄(𝑧 + 𝑤)) ↔ ∀𝑧 ∈ 𝑆 ∀𝑤 ∈ 𝑆 (((seq𝑀( + , 𝐹, 𝑆)‘𝑛)𝑄𝑧) + (𝑦𝑄𝑤)) = (((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + 𝑦)𝑄(𝑧 + 𝑤)))) |
48 | | oveq1 5519 |
. . . . . . . 8
⊢ (𝑦 = (𝐹‘(𝑛 + 1)) → (𝑦𝑄𝑤) = ((𝐹‘(𝑛 + 1))𝑄𝑤)) |
49 | 48 | oveq2d 5528 |
. . . . . . 7
⊢ (𝑦 = (𝐹‘(𝑛 + 1)) → (((seq𝑀( + , 𝐹, 𝑆)‘𝑛)𝑄𝑧) + (𝑦𝑄𝑤)) = (((seq𝑀( + , 𝐹, 𝑆)‘𝑛)𝑄𝑧) + ((𝐹‘(𝑛 + 1))𝑄𝑤))) |
50 | | oveq2 5520 |
. . . . . . . 8
⊢ (𝑦 = (𝐹‘(𝑛 + 1)) → ((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + 𝑦) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1)))) |
51 | 50 | oveq1d 5527 |
. . . . . . 7
⊢ (𝑦 = (𝐹‘(𝑛 + 1)) → (((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + 𝑦)𝑄(𝑧 + 𝑤)) = (((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1)))𝑄(𝑧 + 𝑤))) |
52 | 49, 51 | eqeq12d 2054 |
. . . . . 6
⊢ (𝑦 = (𝐹‘(𝑛 + 1)) → ((((seq𝑀( + , 𝐹, 𝑆)‘𝑛)𝑄𝑧) + (𝑦𝑄𝑤)) = (((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + 𝑦)𝑄(𝑧 + 𝑤)) ↔ (((seq𝑀( + , 𝐹, 𝑆)‘𝑛)𝑄𝑧) + ((𝐹‘(𝑛 + 1))𝑄𝑤)) = (((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1)))𝑄(𝑧 + 𝑤)))) |
53 | 52 | 2ralbidv 2348 |
. . . . 5
⊢ (𝑦 = (𝐹‘(𝑛 + 1)) → (∀𝑧 ∈ 𝑆 ∀𝑤 ∈ 𝑆 (((seq𝑀( + , 𝐹, 𝑆)‘𝑛)𝑄𝑧) + (𝑦𝑄𝑤)) = (((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + 𝑦)𝑄(𝑧 + 𝑤)) ↔ ∀𝑧 ∈ 𝑆 ∀𝑤 ∈ 𝑆 (((seq𝑀( + , 𝐹, 𝑆)‘𝑛)𝑄𝑧) + ((𝐹‘(𝑛 + 1))𝑄𝑤)) = (((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1)))𝑄(𝑧 + 𝑤)))) |
54 | 47, 53 | rspc2va 2663 |
. . . 4
⊢
((((seq𝑀( + , 𝐹, 𝑆)‘𝑛) ∈ 𝑆 ∧ (𝐹‘(𝑛 + 1)) ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 ∀𝑤 ∈ 𝑆 ((𝑥𝑄𝑧) + (𝑦𝑄𝑤)) = ((𝑥 + 𝑦)𝑄(𝑧 + 𝑤))) → ∀𝑧 ∈ 𝑆 ∀𝑤 ∈ 𝑆 (((seq𝑀( + , 𝐹, 𝑆)‘𝑛)𝑄𝑧) + ((𝐹‘(𝑛 + 1))𝑄𝑤)) = (((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1)))𝑄(𝑧 + 𝑤))) |
55 | 32, 36, 41, 54 | syl21anc 1134 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → ∀𝑧 ∈ 𝑆 ∀𝑤 ∈ 𝑆 (((seq𝑀( + , 𝐹, 𝑆)‘𝑛)𝑄𝑧) + ((𝐹‘(𝑛 + 1))𝑄𝑤)) = (((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1)))𝑄(𝑧 + 𝑤))) |
56 | | oveq2 5520 |
. . . . . 6
⊢ (𝑧 = (seq𝑀( + , 𝐺, 𝑆)‘𝑛) → ((seq𝑀( + , 𝐹, 𝑆)‘𝑛)𝑄𝑧) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑛)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑛))) |
57 | 56 | oveq1d 5527 |
. . . . 5
⊢ (𝑧 = (seq𝑀( + , 𝐺, 𝑆)‘𝑛) → (((seq𝑀( + , 𝐹, 𝑆)‘𝑛)𝑄𝑧) + ((𝐹‘(𝑛 + 1))𝑄𝑤)) = (((seq𝑀( + , 𝐹, 𝑆)‘𝑛)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑛)) + ((𝐹‘(𝑛 + 1))𝑄𝑤))) |
58 | | oveq1 5519 |
. . . . . 6
⊢ (𝑧 = (seq𝑀( + , 𝐺, 𝑆)‘𝑛) → (𝑧 + 𝑤) = ((seq𝑀( + , 𝐺, 𝑆)‘𝑛) + 𝑤)) |
59 | 58 | oveq2d 5528 |
. . . . 5
⊢ (𝑧 = (seq𝑀( + , 𝐺, 𝑆)‘𝑛) → (((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1)))𝑄(𝑧 + 𝑤)) = (((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1)))𝑄((seq𝑀( + , 𝐺, 𝑆)‘𝑛) + 𝑤))) |
60 | 57, 59 | eqeq12d 2054 |
. . . 4
⊢ (𝑧 = (seq𝑀( + , 𝐺, 𝑆)‘𝑛) → ((((seq𝑀( + , 𝐹, 𝑆)‘𝑛)𝑄𝑧) + ((𝐹‘(𝑛 + 1))𝑄𝑤)) = (((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1)))𝑄(𝑧 + 𝑤)) ↔ (((seq𝑀( + , 𝐹, 𝑆)‘𝑛)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑛)) + ((𝐹‘(𝑛 + 1))𝑄𝑤)) = (((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1)))𝑄((seq𝑀( + , 𝐺, 𝑆)‘𝑛) + 𝑤)))) |
61 | | oveq2 5520 |
. . . . . 6
⊢ (𝑤 = (𝐺‘(𝑛 + 1)) → ((𝐹‘(𝑛 + 1))𝑄𝑤) = ((𝐹‘(𝑛 + 1))𝑄(𝐺‘(𝑛 + 1)))) |
62 | 61 | oveq2d 5528 |
. . . . 5
⊢ (𝑤 = (𝐺‘(𝑛 + 1)) → (((seq𝑀( + , 𝐹, 𝑆)‘𝑛)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑛)) + ((𝐹‘(𝑛 + 1))𝑄𝑤)) = (((seq𝑀( + , 𝐹, 𝑆)‘𝑛)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑛)) + ((𝐹‘(𝑛 + 1))𝑄(𝐺‘(𝑛 + 1))))) |
63 | | oveq2 5520 |
. . . . . 6
⊢ (𝑤 = (𝐺‘(𝑛 + 1)) → ((seq𝑀( + , 𝐺, 𝑆)‘𝑛) + 𝑤) = ((seq𝑀( + , 𝐺, 𝑆)‘𝑛) + (𝐺‘(𝑛 + 1)))) |
64 | 63 | oveq2d 5528 |
. . . . 5
⊢ (𝑤 = (𝐺‘(𝑛 + 1)) → (((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1)))𝑄((seq𝑀( + , 𝐺, 𝑆)‘𝑛) + 𝑤)) = (((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1)))𝑄((seq𝑀( + , 𝐺, 𝑆)‘𝑛) + (𝐺‘(𝑛 + 1))))) |
65 | 62, 64 | eqeq12d 2054 |
. . . 4
⊢ (𝑤 = (𝐺‘(𝑛 + 1)) → ((((seq𝑀( + , 𝐹, 𝑆)‘𝑛)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑛)) + ((𝐹‘(𝑛 + 1))𝑄𝑤)) = (((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1)))𝑄((seq𝑀( + , 𝐺, 𝑆)‘𝑛) + 𝑤)) ↔ (((seq𝑀( + , 𝐹, 𝑆)‘𝑛)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑛)) + ((𝐹‘(𝑛 + 1))𝑄(𝐺‘(𝑛 + 1)))) = (((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1)))𝑄((seq𝑀( + , 𝐺, 𝑆)‘𝑛) + (𝐺‘(𝑛 + 1)))))) |
66 | 60, 65 | rspc2va 2663 |
. . 3
⊢
((((seq𝑀( + , 𝐺, 𝑆)‘𝑛) ∈ 𝑆 ∧ (𝐺‘(𝑛 + 1)) ∈ 𝑆) ∧ ∀𝑧 ∈ 𝑆 ∀𝑤 ∈ 𝑆 (((seq𝑀( + , 𝐹, 𝑆)‘𝑛)𝑄𝑧) + ((𝐹‘(𝑛 + 1))𝑄𝑤)) = (((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1)))𝑄(𝑧 + 𝑤))) → (((seq𝑀( + , 𝐹, 𝑆)‘𝑛)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑛)) + ((𝐹‘(𝑛 + 1))𝑄(𝐺‘(𝑛 + 1)))) = (((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1)))𝑄((seq𝑀( + , 𝐺, 𝑆)‘𝑛) + (𝐺‘(𝑛 + 1))))) |
67 | 18, 25, 55, 66 | syl21anc 1134 |
. 2
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (((seq𝑀( + , 𝐹, 𝑆)‘𝑛)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑛)) + ((𝐹‘(𝑛 + 1))𝑄(𝐺‘(𝑛 + 1)))) = (((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1)))𝑄((seq𝑀( + , 𝐺, 𝑆)‘𝑛) + (𝐺‘(𝑛 + 1))))) |
68 | 1, 2, 3, 4, 5, 6, 67, 9 | iseqcaopr3 9240 |
1
⊢ (𝜑 → (seq𝑀( + , 𝐻, 𝑆)‘𝑁) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑁)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑁))) |