Step | Hyp | Ref
| Expression |
1 | | iseqhomo.3 |
. 2
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
2 | | fveq2 5198 |
. . . . . 6
⊢ (𝑤 = 𝑀 → (seq𝑀( + , 𝐹, 𝑆)‘𝑤) = (seq𝑀( + , 𝐹, 𝑆)‘𝑀)) |
3 | 2 | fveq2d 5202 |
. . . . 5
⊢ (𝑤 = 𝑀 → (𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑤)) = (𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑀))) |
4 | | fveq2 5198 |
. . . . 5
⊢ (𝑤 = 𝑀 → (seq𝑀(𝑄, 𝐺, 𝑆)‘𝑤) = (seq𝑀(𝑄, 𝐺, 𝑆)‘𝑀)) |
5 | 3, 4 | eqeq12d 2095 |
. . . 4
⊢ (𝑤 = 𝑀 → ((𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑤)) = (seq𝑀(𝑄, 𝐺, 𝑆)‘𝑤) ↔ (𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑀)) = (seq𝑀(𝑄, 𝐺, 𝑆)‘𝑀))) |
6 | 5 | imbi2d 228 |
. . 3
⊢ (𝑤 = 𝑀 → ((𝜑 → (𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑤)) = (seq𝑀(𝑄, 𝐺, 𝑆)‘𝑤)) ↔ (𝜑 → (𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑀)) = (seq𝑀(𝑄, 𝐺, 𝑆)‘𝑀)))) |
7 | | fveq2 5198 |
. . . . . 6
⊢ (𝑤 = 𝑛 → (seq𝑀( + , 𝐹, 𝑆)‘𝑤) = (seq𝑀( + , 𝐹, 𝑆)‘𝑛)) |
8 | 7 | fveq2d 5202 |
. . . . 5
⊢ (𝑤 = 𝑛 → (𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑤)) = (𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑛))) |
9 | | fveq2 5198 |
. . . . 5
⊢ (𝑤 = 𝑛 → (seq𝑀(𝑄, 𝐺, 𝑆)‘𝑤) = (seq𝑀(𝑄, 𝐺, 𝑆)‘𝑛)) |
10 | 8, 9 | eqeq12d 2095 |
. . . 4
⊢ (𝑤 = 𝑛 → ((𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑤)) = (seq𝑀(𝑄, 𝐺, 𝑆)‘𝑤) ↔ (𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑛)) = (seq𝑀(𝑄, 𝐺, 𝑆)‘𝑛))) |
11 | 10 | imbi2d 228 |
. . 3
⊢ (𝑤 = 𝑛 → ((𝜑 → (𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑤)) = (seq𝑀(𝑄, 𝐺, 𝑆)‘𝑤)) ↔ (𝜑 → (𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑛)) = (seq𝑀(𝑄, 𝐺, 𝑆)‘𝑛)))) |
12 | | fveq2 5198 |
. . . . . 6
⊢ (𝑤 = (𝑛 + 1) → (seq𝑀( + , 𝐹, 𝑆)‘𝑤) = (seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1))) |
13 | 12 | fveq2d 5202 |
. . . . 5
⊢ (𝑤 = (𝑛 + 1) → (𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑤)) = (𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1)))) |
14 | | fveq2 5198 |
. . . . 5
⊢ (𝑤 = (𝑛 + 1) → (seq𝑀(𝑄, 𝐺, 𝑆)‘𝑤) = (seq𝑀(𝑄, 𝐺, 𝑆)‘(𝑛 + 1))) |
15 | 13, 14 | eqeq12d 2095 |
. . . 4
⊢ (𝑤 = (𝑛 + 1) → ((𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑤)) = (seq𝑀(𝑄, 𝐺, 𝑆)‘𝑤) ↔ (𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1))) = (seq𝑀(𝑄, 𝐺, 𝑆)‘(𝑛 + 1)))) |
16 | 15 | imbi2d 228 |
. . 3
⊢ (𝑤 = (𝑛 + 1) → ((𝜑 → (𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑤)) = (seq𝑀(𝑄, 𝐺, 𝑆)‘𝑤)) ↔ (𝜑 → (𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1))) = (seq𝑀(𝑄, 𝐺, 𝑆)‘(𝑛 + 1))))) |
17 | | fveq2 5198 |
. . . . . 6
⊢ (𝑤 = 𝑁 → (seq𝑀( + , 𝐹, 𝑆)‘𝑤) = (seq𝑀( + , 𝐹, 𝑆)‘𝑁)) |
18 | 17 | fveq2d 5202 |
. . . . 5
⊢ (𝑤 = 𝑁 → (𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑤)) = (𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑁))) |
19 | | fveq2 5198 |
. . . . 5
⊢ (𝑤 = 𝑁 → (seq𝑀(𝑄, 𝐺, 𝑆)‘𝑤) = (seq𝑀(𝑄, 𝐺, 𝑆)‘𝑁)) |
20 | 18, 19 | eqeq12d 2095 |
. . . 4
⊢ (𝑤 = 𝑁 → ((𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑤)) = (seq𝑀(𝑄, 𝐺, 𝑆)‘𝑤) ↔ (𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑁)) = (seq𝑀(𝑄, 𝐺, 𝑆)‘𝑁))) |
21 | 20 | imbi2d 228 |
. . 3
⊢ (𝑤 = 𝑁 → ((𝜑 → (𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑤)) = (seq𝑀(𝑄, 𝐺, 𝑆)‘𝑤)) ↔ (𝜑 → (𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑁)) = (seq𝑀(𝑄, 𝐺, 𝑆)‘𝑁)))) |
22 | | eluzel2 8624 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
23 | 1, 22 | syl 14 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℤ) |
24 | | uzid 8633 |
. . . . . . 7
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
(ℤ≥‘𝑀)) |
25 | 23, 24 | syl 14 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑀)) |
26 | | iseqhomo.5 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐻‘(𝐹‘𝑥)) = (𝐺‘𝑥)) |
27 | 26 | ralrimiva 2434 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ (ℤ≥‘𝑀)(𝐻‘(𝐹‘𝑥)) = (𝐺‘𝑥)) |
28 | | fveq2 5198 |
. . . . . . . . 9
⊢ (𝑥 = 𝑀 → (𝐹‘𝑥) = (𝐹‘𝑀)) |
29 | 28 | fveq2d 5202 |
. . . . . . . 8
⊢ (𝑥 = 𝑀 → (𝐻‘(𝐹‘𝑥)) = (𝐻‘(𝐹‘𝑀))) |
30 | | fveq2 5198 |
. . . . . . . 8
⊢ (𝑥 = 𝑀 → (𝐺‘𝑥) = (𝐺‘𝑀)) |
31 | 29, 30 | eqeq12d 2095 |
. . . . . . 7
⊢ (𝑥 = 𝑀 → ((𝐻‘(𝐹‘𝑥)) = (𝐺‘𝑥) ↔ (𝐻‘(𝐹‘𝑀)) = (𝐺‘𝑀))) |
32 | 31 | rspcv 2697 |
. . . . . 6
⊢ (𝑀 ∈
(ℤ≥‘𝑀) → (∀𝑥 ∈ (ℤ≥‘𝑀)(𝐻‘(𝐹‘𝑥)) = (𝐺‘𝑥) → (𝐻‘(𝐹‘𝑀)) = (𝐺‘𝑀))) |
33 | 25, 27, 32 | sylc 61 |
. . . . 5
⊢ (𝜑 → (𝐻‘(𝐹‘𝑀)) = (𝐺‘𝑀)) |
34 | | iseqhomo.s |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈ 𝑉) |
35 | | iseqhomo.2 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆) |
36 | | iseqhomo.1 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
37 | 23, 34, 35, 36 | iseq1 9442 |
. . . . . 6
⊢ (𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘𝑀) = (𝐹‘𝑀)) |
38 | 37 | fveq2d 5202 |
. . . . 5
⊢ (𝜑 → (𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑀)) = (𝐻‘(𝐹‘𝑀))) |
39 | | iseqhomo.g |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑥) ∈ 𝑆) |
40 | | iseqhomo.qcl |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑄𝑦) ∈ 𝑆) |
41 | 23, 34, 39, 40 | iseq1 9442 |
. . . . 5
⊢ (𝜑 → (seq𝑀(𝑄, 𝐺, 𝑆)‘𝑀) = (𝐺‘𝑀)) |
42 | 33, 38, 41 | 3eqtr4d 2123 |
. . . 4
⊢ (𝜑 → (𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑀)) = (seq𝑀(𝑄, 𝐺, 𝑆)‘𝑀)) |
43 | 42 | a1i 9 |
. . 3
⊢ (𝑀 ∈ ℤ → (𝜑 → (𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑀)) = (seq𝑀(𝑄, 𝐺, 𝑆)‘𝑀))) |
44 | | oveq1 5539 |
. . . . . 6
⊢ ((𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑛)) = (seq𝑀(𝑄, 𝐺, 𝑆)‘𝑛) → ((𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑛))𝑄(𝐺‘(𝑛 + 1))) = ((seq𝑀(𝑄, 𝐺, 𝑆)‘𝑛)𝑄(𝐺‘(𝑛 + 1)))) |
45 | | simpr 108 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → 𝑛 ∈ (ℤ≥‘𝑀)) |
46 | 34 | adantr 270 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → 𝑆 ∈ 𝑉) |
47 | 35 | adantlr 460 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆) |
48 | 36 | adantlr 460 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
49 | 45, 46, 47, 48 | iseqp1 9445 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1)) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1)))) |
50 | 49 | fveq2d 5202 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1))) = (𝐻‘((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1))))) |
51 | | iseqhomo.4 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝐻‘(𝑥 + 𝑦)) = ((𝐻‘𝑥)𝑄(𝐻‘𝑦))) |
52 | 51 | ralrimivva 2443 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝐻‘(𝑥 + 𝑦)) = ((𝐻‘𝑥)𝑄(𝐻‘𝑦))) |
53 | 52 | adantr 270 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝐻‘(𝑥 + 𝑦)) = ((𝐻‘𝑥)𝑄(𝐻‘𝑦))) |
54 | 45, 46, 47, 48 | iseqcl 9443 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (seq𝑀( + , 𝐹, 𝑆)‘𝑛) ∈ 𝑆) |
55 | | peano2uz 8671 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → (𝑛 + 1) ∈
(ℤ≥‘𝑀)) |
56 | 45, 55 | syl 14 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (𝑛 + 1) ∈
(ℤ≥‘𝑀)) |
57 | 35 | ralrimiva 2434 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑥 ∈ (ℤ≥‘𝑀)(𝐹‘𝑥) ∈ 𝑆) |
58 | 57 | adantr 270 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → ∀𝑥 ∈
(ℤ≥‘𝑀)(𝐹‘𝑥) ∈ 𝑆) |
59 | | fveq2 5198 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑛 + 1) → (𝐹‘𝑥) = (𝐹‘(𝑛 + 1))) |
60 | 59 | eleq1d 2147 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑛 + 1) → ((𝐹‘𝑥) ∈ 𝑆 ↔ (𝐹‘(𝑛 + 1)) ∈ 𝑆)) |
61 | 60 | rspcv 2697 |
. . . . . . . . . . 11
⊢ ((𝑛 + 1) ∈
(ℤ≥‘𝑀) → (∀𝑥 ∈ (ℤ≥‘𝑀)(𝐹‘𝑥) ∈ 𝑆 → (𝐹‘(𝑛 + 1)) ∈ 𝑆)) |
62 | 56, 58, 61 | sylc 61 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (𝐹‘(𝑛 + 1)) ∈ 𝑆) |
63 | | oveq1 5539 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (seq𝑀( + , 𝐹, 𝑆)‘𝑛) → (𝑥 + 𝑦) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + 𝑦)) |
64 | 63 | fveq2d 5202 |
. . . . . . . . . . . 12
⊢ (𝑥 = (seq𝑀( + , 𝐹, 𝑆)‘𝑛) → (𝐻‘(𝑥 + 𝑦)) = (𝐻‘((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + 𝑦))) |
65 | | fveq2 5198 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (seq𝑀( + , 𝐹, 𝑆)‘𝑛) → (𝐻‘𝑥) = (𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑛))) |
66 | 65 | oveq1d 5547 |
. . . . . . . . . . . 12
⊢ (𝑥 = (seq𝑀( + , 𝐹, 𝑆)‘𝑛) → ((𝐻‘𝑥)𝑄(𝐻‘𝑦)) = ((𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑛))𝑄(𝐻‘𝑦))) |
67 | 64, 66 | eqeq12d 2095 |
. . . . . . . . . . 11
⊢ (𝑥 = (seq𝑀( + , 𝐹, 𝑆)‘𝑛) → ((𝐻‘(𝑥 + 𝑦)) = ((𝐻‘𝑥)𝑄(𝐻‘𝑦)) ↔ (𝐻‘((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + 𝑦)) = ((𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑛))𝑄(𝐻‘𝑦)))) |
68 | | oveq2 5540 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝐹‘(𝑛 + 1)) → ((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + 𝑦) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1)))) |
69 | 68 | fveq2d 5202 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝐹‘(𝑛 + 1)) → (𝐻‘((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + 𝑦)) = (𝐻‘((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1))))) |
70 | | fveq2 5198 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝐹‘(𝑛 + 1)) → (𝐻‘𝑦) = (𝐻‘(𝐹‘(𝑛 + 1)))) |
71 | 70 | oveq2d 5548 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝐹‘(𝑛 + 1)) → ((𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑛))𝑄(𝐻‘𝑦)) = ((𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑛))𝑄(𝐻‘(𝐹‘(𝑛 + 1))))) |
72 | 69, 71 | eqeq12d 2095 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝐹‘(𝑛 + 1)) → ((𝐻‘((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + 𝑦)) = ((𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑛))𝑄(𝐻‘𝑦)) ↔ (𝐻‘((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1)))) = ((𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑛))𝑄(𝐻‘(𝐹‘(𝑛 + 1)))))) |
73 | 67, 72 | rspc2v 2713 |
. . . . . . . . . 10
⊢
(((seq𝑀( + , 𝐹, 𝑆)‘𝑛) ∈ 𝑆 ∧ (𝐹‘(𝑛 + 1)) ∈ 𝑆) → (∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝐻‘(𝑥 + 𝑦)) = ((𝐻‘𝑥)𝑄(𝐻‘𝑦)) → (𝐻‘((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1)))) = ((𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑛))𝑄(𝐻‘(𝐹‘(𝑛 + 1)))))) |
74 | 54, 62, 73 | syl2anc 403 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝐻‘(𝑥 + 𝑦)) = ((𝐻‘𝑥)𝑄(𝐻‘𝑦)) → (𝐻‘((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1)))) = ((𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑛))𝑄(𝐻‘(𝐹‘(𝑛 + 1)))))) |
75 | 53, 74 | mpd 13 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (𝐻‘((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1)))) = ((𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑛))𝑄(𝐻‘(𝐹‘(𝑛 + 1))))) |
76 | 27 | adantr 270 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → ∀𝑥 ∈
(ℤ≥‘𝑀)(𝐻‘(𝐹‘𝑥)) = (𝐺‘𝑥)) |
77 | 59 | fveq2d 5202 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑛 + 1) → (𝐻‘(𝐹‘𝑥)) = (𝐻‘(𝐹‘(𝑛 + 1)))) |
78 | | fveq2 5198 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑛 + 1) → (𝐺‘𝑥) = (𝐺‘(𝑛 + 1))) |
79 | 77, 78 | eqeq12d 2095 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑛 + 1) → ((𝐻‘(𝐹‘𝑥)) = (𝐺‘𝑥) ↔ (𝐻‘(𝐹‘(𝑛 + 1))) = (𝐺‘(𝑛 + 1)))) |
80 | 79 | rspcv 2697 |
. . . . . . . . . 10
⊢ ((𝑛 + 1) ∈
(ℤ≥‘𝑀) → (∀𝑥 ∈ (ℤ≥‘𝑀)(𝐻‘(𝐹‘𝑥)) = (𝐺‘𝑥) → (𝐻‘(𝐹‘(𝑛 + 1))) = (𝐺‘(𝑛 + 1)))) |
81 | 56, 76, 80 | sylc 61 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (𝐻‘(𝐹‘(𝑛 + 1))) = (𝐺‘(𝑛 + 1))) |
82 | 81 | oveq2d 5548 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → ((𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑛))𝑄(𝐻‘(𝐹‘(𝑛 + 1)))) = ((𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑛))𝑄(𝐺‘(𝑛 + 1)))) |
83 | 50, 75, 82 | 3eqtrd 2117 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1))) = ((𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑛))𝑄(𝐺‘(𝑛 + 1)))) |
84 | 39 | adantlr 460 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑥) ∈ 𝑆) |
85 | 40 | adantlr 460 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑄𝑦) ∈ 𝑆) |
86 | 45, 46, 84, 85 | iseqp1 9445 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (seq𝑀(𝑄, 𝐺, 𝑆)‘(𝑛 + 1)) = ((seq𝑀(𝑄, 𝐺, 𝑆)‘𝑛)𝑄(𝐺‘(𝑛 + 1)))) |
87 | 83, 86 | eqeq12d 2095 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → ((𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1))) = (seq𝑀(𝑄, 𝐺, 𝑆)‘(𝑛 + 1)) ↔ ((𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑛))𝑄(𝐺‘(𝑛 + 1))) = ((seq𝑀(𝑄, 𝐺, 𝑆)‘𝑛)𝑄(𝐺‘(𝑛 + 1))))) |
88 | 44, 87 | syl5ibr 154 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → ((𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑛)) = (seq𝑀(𝑄, 𝐺, 𝑆)‘𝑛) → (𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1))) = (seq𝑀(𝑄, 𝐺, 𝑆)‘(𝑛 + 1)))) |
89 | 88 | expcom 114 |
. . . 4
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → (𝜑 → ((𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑛)) = (seq𝑀(𝑄, 𝐺, 𝑆)‘𝑛) → (𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1))) = (seq𝑀(𝑄, 𝐺, 𝑆)‘(𝑛 + 1))))) |
90 | 89 | a2d 26 |
. . 3
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → ((𝜑 → (𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑛)) = (seq𝑀(𝑄, 𝐺, 𝑆)‘𝑛)) → (𝜑 → (𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1))) = (seq𝑀(𝑄, 𝐺, 𝑆)‘(𝑛 + 1))))) |
91 | 6, 11, 16, 21, 43, 90 | uzind4 8676 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝜑 → (𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑁)) = (seq𝑀(𝑄, 𝐺, 𝑆)‘𝑁))) |
92 | 1, 91 | mpcom 36 |
1
⊢ (𝜑 → (𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑁)) = (seq𝑀(𝑄, 𝐺, 𝑆)‘𝑁)) |