Step | Hyp | Ref
| Expression |
1 | | seqcaopr3.3 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
2 | | eluzfz2 10088 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁)) |
3 | 1, 2 | syl 14 |
. 2
⊢ (𝜑 → 𝑁 ∈ (𝑀...𝑁)) |
4 | | fveq2 5546 |
. . . . 5
⊢ (𝑧 = 𝑀 → (seq𝑀( + , 𝐻)‘𝑧) = (seq𝑀( + , 𝐻)‘𝑀)) |
5 | | fveq2 5546 |
. . . . . 6
⊢ (𝑧 = 𝑀 → (seq𝑀( + , 𝐹)‘𝑧) = (seq𝑀( + , 𝐹)‘𝑀)) |
6 | | fveq2 5546 |
. . . . . 6
⊢ (𝑧 = 𝑀 → (seq𝑀( + , 𝐺)‘𝑧) = (seq𝑀( + , 𝐺)‘𝑀)) |
7 | 5, 6 | oveq12d 5928 |
. . . . 5
⊢ (𝑧 = 𝑀 → ((seq𝑀( + , 𝐹)‘𝑧)𝑄(seq𝑀( + , 𝐺)‘𝑧)) = ((seq𝑀( + , 𝐹)‘𝑀)𝑄(seq𝑀( + , 𝐺)‘𝑀))) |
8 | 4, 7 | eqeq12d 2208 |
. . . 4
⊢ (𝑧 = 𝑀 → ((seq𝑀( + , 𝐻)‘𝑧) = ((seq𝑀( + , 𝐹)‘𝑧)𝑄(seq𝑀( + , 𝐺)‘𝑧)) ↔ (seq𝑀( + , 𝐻)‘𝑀) = ((seq𝑀( + , 𝐹)‘𝑀)𝑄(seq𝑀( + , 𝐺)‘𝑀)))) |
9 | 8 | imbi2d 230 |
. . 3
⊢ (𝑧 = 𝑀 → ((𝜑 → (seq𝑀( + , 𝐻)‘𝑧) = ((seq𝑀( + , 𝐹)‘𝑧)𝑄(seq𝑀( + , 𝐺)‘𝑧))) ↔ (𝜑 → (seq𝑀( + , 𝐻)‘𝑀) = ((seq𝑀( + , 𝐹)‘𝑀)𝑄(seq𝑀( + , 𝐺)‘𝑀))))) |
10 | | fveq2 5546 |
. . . . 5
⊢ (𝑧 = 𝑛 → (seq𝑀( + , 𝐻)‘𝑧) = (seq𝑀( + , 𝐻)‘𝑛)) |
11 | | fveq2 5546 |
. . . . . 6
⊢ (𝑧 = 𝑛 → (seq𝑀( + , 𝐹)‘𝑧) = (seq𝑀( + , 𝐹)‘𝑛)) |
12 | | fveq2 5546 |
. . . . . 6
⊢ (𝑧 = 𝑛 → (seq𝑀( + , 𝐺)‘𝑧) = (seq𝑀( + , 𝐺)‘𝑛)) |
13 | 11, 12 | oveq12d 5928 |
. . . . 5
⊢ (𝑧 = 𝑛 → ((seq𝑀( + , 𝐹)‘𝑧)𝑄(seq𝑀( + , 𝐺)‘𝑧)) = ((seq𝑀( + , 𝐹)‘𝑛)𝑄(seq𝑀( + , 𝐺)‘𝑛))) |
14 | 10, 13 | eqeq12d 2208 |
. . . 4
⊢ (𝑧 = 𝑛 → ((seq𝑀( + , 𝐻)‘𝑧) = ((seq𝑀( + , 𝐹)‘𝑧)𝑄(seq𝑀( + , 𝐺)‘𝑧)) ↔ (seq𝑀( + , 𝐻)‘𝑛) = ((seq𝑀( + , 𝐹)‘𝑛)𝑄(seq𝑀( + , 𝐺)‘𝑛)))) |
15 | 14 | imbi2d 230 |
. . 3
⊢ (𝑧 = 𝑛 → ((𝜑 → (seq𝑀( + , 𝐻)‘𝑧) = ((seq𝑀( + , 𝐹)‘𝑧)𝑄(seq𝑀( + , 𝐺)‘𝑧))) ↔ (𝜑 → (seq𝑀( + , 𝐻)‘𝑛) = ((seq𝑀( + , 𝐹)‘𝑛)𝑄(seq𝑀( + , 𝐺)‘𝑛))))) |
16 | | fveq2 5546 |
. . . . 5
⊢ (𝑧 = (𝑛 + 1) → (seq𝑀( + , 𝐻)‘𝑧) = (seq𝑀( + , 𝐻)‘(𝑛 + 1))) |
17 | | fveq2 5546 |
. . . . . 6
⊢ (𝑧 = (𝑛 + 1) → (seq𝑀( + , 𝐹)‘𝑧) = (seq𝑀( + , 𝐹)‘(𝑛 + 1))) |
18 | | fveq2 5546 |
. . . . . 6
⊢ (𝑧 = (𝑛 + 1) → (seq𝑀( + , 𝐺)‘𝑧) = (seq𝑀( + , 𝐺)‘(𝑛 + 1))) |
19 | 17, 18 | oveq12d 5928 |
. . . . 5
⊢ (𝑧 = (𝑛 + 1) → ((seq𝑀( + , 𝐹)‘𝑧)𝑄(seq𝑀( + , 𝐺)‘𝑧)) = ((seq𝑀( + , 𝐹)‘(𝑛 + 1))𝑄(seq𝑀( + , 𝐺)‘(𝑛 + 1)))) |
20 | 16, 19 | eqeq12d 2208 |
. . . 4
⊢ (𝑧 = (𝑛 + 1) → ((seq𝑀( + , 𝐻)‘𝑧) = ((seq𝑀( + , 𝐹)‘𝑧)𝑄(seq𝑀( + , 𝐺)‘𝑧)) ↔ (seq𝑀( + , 𝐻)‘(𝑛 + 1)) = ((seq𝑀( + , 𝐹)‘(𝑛 + 1))𝑄(seq𝑀( + , 𝐺)‘(𝑛 + 1))))) |
21 | 20 | imbi2d 230 |
. . 3
⊢ (𝑧 = (𝑛 + 1) → ((𝜑 → (seq𝑀( + , 𝐻)‘𝑧) = ((seq𝑀( + , 𝐹)‘𝑧)𝑄(seq𝑀( + , 𝐺)‘𝑧))) ↔ (𝜑 → (seq𝑀( + , 𝐻)‘(𝑛 + 1)) = ((seq𝑀( + , 𝐹)‘(𝑛 + 1))𝑄(seq𝑀( + , 𝐺)‘(𝑛 + 1)))))) |
22 | | fveq2 5546 |
. . . . 5
⊢ (𝑧 = 𝑁 → (seq𝑀( + , 𝐻)‘𝑧) = (seq𝑀( + , 𝐻)‘𝑁)) |
23 | | fveq2 5546 |
. . . . . 6
⊢ (𝑧 = 𝑁 → (seq𝑀( + , 𝐹)‘𝑧) = (seq𝑀( + , 𝐹)‘𝑁)) |
24 | | fveq2 5546 |
. . . . . 6
⊢ (𝑧 = 𝑁 → (seq𝑀( + , 𝐺)‘𝑧) = (seq𝑀( + , 𝐺)‘𝑁)) |
25 | 23, 24 | oveq12d 5928 |
. . . . 5
⊢ (𝑧 = 𝑁 → ((seq𝑀( + , 𝐹)‘𝑧)𝑄(seq𝑀( + , 𝐺)‘𝑧)) = ((seq𝑀( + , 𝐹)‘𝑁)𝑄(seq𝑀( + , 𝐺)‘𝑁))) |
26 | 22, 25 | eqeq12d 2208 |
. . . 4
⊢ (𝑧 = 𝑁 → ((seq𝑀( + , 𝐻)‘𝑧) = ((seq𝑀( + , 𝐹)‘𝑧)𝑄(seq𝑀( + , 𝐺)‘𝑧)) ↔ (seq𝑀( + , 𝐻)‘𝑁) = ((seq𝑀( + , 𝐹)‘𝑁)𝑄(seq𝑀( + , 𝐺)‘𝑁)))) |
27 | 26 | imbi2d 230 |
. . 3
⊢ (𝑧 = 𝑁 → ((𝜑 → (seq𝑀( + , 𝐻)‘𝑧) = ((seq𝑀( + , 𝐹)‘𝑧)𝑄(seq𝑀( + , 𝐺)‘𝑧))) ↔ (𝜑 → (seq𝑀( + , 𝐻)‘𝑁) = ((seq𝑀( + , 𝐹)‘𝑁)𝑄(seq𝑀( + , 𝐺)‘𝑁))))) |
28 | | fveq2 5546 |
. . . . . . 7
⊢ (𝑘 = 𝑀 → (𝐻‘𝑘) = (𝐻‘𝑀)) |
29 | | fveq2 5546 |
. . . . . . . 8
⊢ (𝑘 = 𝑀 → (𝐹‘𝑘) = (𝐹‘𝑀)) |
30 | | fveq2 5546 |
. . . . . . . 8
⊢ (𝑘 = 𝑀 → (𝐺‘𝑘) = (𝐺‘𝑀)) |
31 | 29, 30 | oveq12d 5928 |
. . . . . . 7
⊢ (𝑘 = 𝑀 → ((𝐹‘𝑘)𝑄(𝐺‘𝑘)) = ((𝐹‘𝑀)𝑄(𝐺‘𝑀))) |
32 | 28, 31 | eqeq12d 2208 |
. . . . . 6
⊢ (𝑘 = 𝑀 → ((𝐻‘𝑘) = ((𝐹‘𝑘)𝑄(𝐺‘𝑘)) ↔ (𝐻‘𝑀) = ((𝐹‘𝑀)𝑄(𝐺‘𝑀)))) |
33 | | seqcaopr3.6 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐻‘𝑘) = ((𝐹‘𝑘)𝑄(𝐺‘𝑘))) |
34 | 33 | ralrimiva 2567 |
. . . . . 6
⊢ (𝜑 → ∀𝑘 ∈ (𝑀...𝑁)(𝐻‘𝑘) = ((𝐹‘𝑘)𝑄(𝐺‘𝑘))) |
35 | | eluzfz1 10087 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁)) |
36 | 1, 35 | syl 14 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ (𝑀...𝑁)) |
37 | 32, 34, 36 | rspcdva 2869 |
. . . . 5
⊢ (𝜑 → (𝐻‘𝑀) = ((𝐹‘𝑀)𝑄(𝐺‘𝑀))) |
38 | | eluzel2 9587 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
39 | 1, 38 | syl 14 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℤ) |
40 | | seqcaopr3g.h |
. . . . . 6
⊢ (𝜑 → 𝐻 ∈ 𝑌) |
41 | | seqcaopr3g.p |
. . . . . 6
⊢ (𝜑 → + ∈ 𝑉) |
42 | | seq1g 10524 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝐻 ∈ 𝑌 ∧ + ∈ 𝑉) → (seq𝑀( + , 𝐻)‘𝑀) = (𝐻‘𝑀)) |
43 | 39, 40, 41, 42 | syl3anc 1249 |
. . . . 5
⊢ (𝜑 → (seq𝑀( + , 𝐻)‘𝑀) = (𝐻‘𝑀)) |
44 | | seqcaopr3g.f |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ 𝑊) |
45 | | seq1g 10524 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑊 ∧ + ∈ 𝑉) → (seq𝑀( + , 𝐹)‘𝑀) = (𝐹‘𝑀)) |
46 | 39, 44, 41, 45 | syl3anc 1249 |
. . . . . 6
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑀) = (𝐹‘𝑀)) |
47 | | seqcaopr3g.g |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ 𝑋) |
48 | | seq1g 10524 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝐺 ∈ 𝑋 ∧ + ∈ 𝑉) → (seq𝑀( + , 𝐺)‘𝑀) = (𝐺‘𝑀)) |
49 | 39, 47, 41, 48 | syl3anc 1249 |
. . . . . 6
⊢ (𝜑 → (seq𝑀( + , 𝐺)‘𝑀) = (𝐺‘𝑀)) |
50 | 46, 49 | oveq12d 5928 |
. . . . 5
⊢ (𝜑 → ((seq𝑀( + , 𝐹)‘𝑀)𝑄(seq𝑀( + , 𝐺)‘𝑀)) = ((𝐹‘𝑀)𝑄(𝐺‘𝑀))) |
51 | 37, 43, 50 | 3eqtr4d 2236 |
. . . 4
⊢ (𝜑 → (seq𝑀( + , 𝐻)‘𝑀) = ((seq𝑀( + , 𝐹)‘𝑀)𝑄(seq𝑀( + , 𝐺)‘𝑀))) |
52 | 51 | a1i 9 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝜑 → (seq𝑀( + , 𝐻)‘𝑀) = ((seq𝑀( + , 𝐹)‘𝑀)𝑄(seq𝑀( + , 𝐺)‘𝑀)))) |
53 | | oveq1 5917 |
. . . . . 6
⊢
((seq𝑀( + , 𝐻)‘𝑛) = ((seq𝑀( + , 𝐹)‘𝑛)𝑄(seq𝑀( + , 𝐺)‘𝑛)) → ((seq𝑀( + , 𝐻)‘𝑛) + (𝐻‘(𝑛 + 1))) = (((seq𝑀( + , 𝐹)‘𝑛)𝑄(seq𝑀( + , 𝐺)‘𝑛)) + (𝐻‘(𝑛 + 1)))) |
54 | | elfzouz 10207 |
. . . . . . . . 9
⊢ (𝑛 ∈ (𝑀..^𝑁) → 𝑛 ∈ (ℤ≥‘𝑀)) |
55 | 54 | adantl 277 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → 𝑛 ∈ (ℤ≥‘𝑀)) |
56 | 40 | adantr 276 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → 𝐻 ∈ 𝑌) |
57 | 41 | adantr 276 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → + ∈ 𝑉) |
58 | | seqp1g 10527 |
. . . . . . . 8
⊢ ((𝑛 ∈
(ℤ≥‘𝑀) ∧ 𝐻 ∈ 𝑌 ∧ + ∈ 𝑉) → (seq𝑀( + , 𝐻)‘(𝑛 + 1)) = ((seq𝑀( + , 𝐻)‘𝑛) + (𝐻‘(𝑛 + 1)))) |
59 | 55, 56, 57, 58 | syl3anc 1249 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (seq𝑀( + , 𝐻)‘(𝑛 + 1)) = ((seq𝑀( + , 𝐻)‘𝑛) + (𝐻‘(𝑛 + 1)))) |
60 | | seqcaopr3.7 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (((seq𝑀( + , 𝐹)‘𝑛)𝑄(seq𝑀( + , 𝐺)‘𝑛)) + ((𝐹‘(𝑛 + 1))𝑄(𝐺‘(𝑛 + 1)))) = (((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1)))𝑄((seq𝑀( + , 𝐺)‘𝑛) + (𝐺‘(𝑛 + 1))))) |
61 | | fveq2 5546 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝑛 + 1) → (𝐻‘𝑘) = (𝐻‘(𝑛 + 1))) |
62 | | fveq2 5546 |
. . . . . . . . . . . 12
⊢ (𝑘 = (𝑛 + 1) → (𝐹‘𝑘) = (𝐹‘(𝑛 + 1))) |
63 | | fveq2 5546 |
. . . . . . . . . . . 12
⊢ (𝑘 = (𝑛 + 1) → (𝐺‘𝑘) = (𝐺‘(𝑛 + 1))) |
64 | 62, 63 | oveq12d 5928 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝑛 + 1) → ((𝐹‘𝑘)𝑄(𝐺‘𝑘)) = ((𝐹‘(𝑛 + 1))𝑄(𝐺‘(𝑛 + 1)))) |
65 | 61, 64 | eqeq12d 2208 |
. . . . . . . . . 10
⊢ (𝑘 = (𝑛 + 1) → ((𝐻‘𝑘) = ((𝐹‘𝑘)𝑄(𝐺‘𝑘)) ↔ (𝐻‘(𝑛 + 1)) = ((𝐹‘(𝑛 + 1))𝑄(𝐺‘(𝑛 + 1))))) |
66 | 34 | adantr 276 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → ∀𝑘 ∈ (𝑀...𝑁)(𝐻‘𝑘) = ((𝐹‘𝑘)𝑄(𝐺‘𝑘))) |
67 | | fzofzp1 10284 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (𝑀..^𝑁) → (𝑛 + 1) ∈ (𝑀...𝑁)) |
68 | 67 | adantl 277 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (𝑛 + 1) ∈ (𝑀...𝑁)) |
69 | 65, 66, 68 | rspcdva 2869 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (𝐻‘(𝑛 + 1)) = ((𝐹‘(𝑛 + 1))𝑄(𝐺‘(𝑛 + 1)))) |
70 | 69 | oveq2d 5926 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (((seq𝑀( + , 𝐹)‘𝑛)𝑄(seq𝑀( + , 𝐺)‘𝑛)) + (𝐻‘(𝑛 + 1))) = (((seq𝑀( + , 𝐹)‘𝑛)𝑄(seq𝑀( + , 𝐺)‘𝑛)) + ((𝐹‘(𝑛 + 1))𝑄(𝐺‘(𝑛 + 1))))) |
71 | 44 | adantr 276 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → 𝐹 ∈ 𝑊) |
72 | | seqp1g 10527 |
. . . . . . . . . 10
⊢ ((𝑛 ∈
(ℤ≥‘𝑀) ∧ 𝐹 ∈ 𝑊 ∧ + ∈ 𝑉) → (seq𝑀( + , 𝐹)‘(𝑛 + 1)) = ((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1)))) |
73 | 55, 71, 57, 72 | syl3anc 1249 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (seq𝑀( + , 𝐹)‘(𝑛 + 1)) = ((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1)))) |
74 | 47 | adantr 276 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → 𝐺 ∈ 𝑋) |
75 | | seqp1g 10527 |
. . . . . . . . . 10
⊢ ((𝑛 ∈
(ℤ≥‘𝑀) ∧ 𝐺 ∈ 𝑋 ∧ + ∈ 𝑉) → (seq𝑀( + , 𝐺)‘(𝑛 + 1)) = ((seq𝑀( + , 𝐺)‘𝑛) + (𝐺‘(𝑛 + 1)))) |
76 | 55, 74, 57, 75 | syl3anc 1249 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (seq𝑀( + , 𝐺)‘(𝑛 + 1)) = ((seq𝑀( + , 𝐺)‘𝑛) + (𝐺‘(𝑛 + 1)))) |
77 | 73, 76 | oveq12d 5928 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → ((seq𝑀( + , 𝐹)‘(𝑛 + 1))𝑄(seq𝑀( + , 𝐺)‘(𝑛 + 1))) = (((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1)))𝑄((seq𝑀( + , 𝐺)‘𝑛) + (𝐺‘(𝑛 + 1))))) |
78 | 60, 70, 77 | 3eqtr4rd 2237 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → ((seq𝑀( + , 𝐹)‘(𝑛 + 1))𝑄(seq𝑀( + , 𝐺)‘(𝑛 + 1))) = (((seq𝑀( + , 𝐹)‘𝑛)𝑄(seq𝑀( + , 𝐺)‘𝑛)) + (𝐻‘(𝑛 + 1)))) |
79 | 59, 78 | eqeq12d 2208 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → ((seq𝑀( + , 𝐻)‘(𝑛 + 1)) = ((seq𝑀( + , 𝐹)‘(𝑛 + 1))𝑄(seq𝑀( + , 𝐺)‘(𝑛 + 1))) ↔ ((seq𝑀( + , 𝐻)‘𝑛) + (𝐻‘(𝑛 + 1))) = (((seq𝑀( + , 𝐹)‘𝑛)𝑄(seq𝑀( + , 𝐺)‘𝑛)) + (𝐻‘(𝑛 + 1))))) |
80 | 53, 79 | imbitrrid 156 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → ((seq𝑀( + , 𝐻)‘𝑛) = ((seq𝑀( + , 𝐹)‘𝑛)𝑄(seq𝑀( + , 𝐺)‘𝑛)) → (seq𝑀( + , 𝐻)‘(𝑛 + 1)) = ((seq𝑀( + , 𝐹)‘(𝑛 + 1))𝑄(seq𝑀( + , 𝐺)‘(𝑛 + 1))))) |
81 | 80 | expcom 116 |
. . . 4
⊢ (𝑛 ∈ (𝑀..^𝑁) → (𝜑 → ((seq𝑀( + , 𝐻)‘𝑛) = ((seq𝑀( + , 𝐹)‘𝑛)𝑄(seq𝑀( + , 𝐺)‘𝑛)) → (seq𝑀( + , 𝐻)‘(𝑛 + 1)) = ((seq𝑀( + , 𝐹)‘(𝑛 + 1))𝑄(seq𝑀( + , 𝐺)‘(𝑛 + 1)))))) |
82 | 81 | a2d 26 |
. . 3
⊢ (𝑛 ∈ (𝑀..^𝑁) → ((𝜑 → (seq𝑀( + , 𝐻)‘𝑛) = ((seq𝑀( + , 𝐹)‘𝑛)𝑄(seq𝑀( + , 𝐺)‘𝑛))) → (𝜑 → (seq𝑀( + , 𝐻)‘(𝑛 + 1)) = ((seq𝑀( + , 𝐹)‘(𝑛 + 1))𝑄(seq𝑀( + , 𝐺)‘(𝑛 + 1)))))) |
83 | 9, 15, 21, 27, 52, 82 | fzind2 10296 |
. 2
⊢ (𝑁 ∈ (𝑀...𝑁) → (𝜑 → (seq𝑀( + , 𝐻)‘𝑁) = ((seq𝑀( + , 𝐹)‘𝑁)𝑄(seq𝑀( + , 𝐺)‘𝑁)))) |
84 | 3, 83 | mpcom 36 |
1
⊢ (𝜑 → (seq𝑀( + , 𝐻)‘𝑁) = ((seq𝑀( + , 𝐹)‘𝑁)𝑄(seq𝑀( + , 𝐺)‘𝑁))) |