Step | Hyp | Ref
| Expression |
1 | | seqhomo.3 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
2 | | eluzfz2 12220 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁)) |
3 | 1, 2 | syl 17 |
. 2
⊢ (𝜑 → 𝑁 ∈ (𝑀...𝑁)) |
4 | | eleq1 2676 |
. . . . . 6
⊢ (𝑥 = 𝑀 → (𝑥 ∈ (𝑀...𝑁) ↔ 𝑀 ∈ (𝑀...𝑁))) |
5 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑥 = 𝑀 → (seq𝑀( + , 𝐹)‘𝑥) = (seq𝑀( + , 𝐹)‘𝑀)) |
6 | 5 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑥 = 𝑀 → (𝐻‘(seq𝑀( + , 𝐹)‘𝑥)) = (𝐻‘(seq𝑀( + , 𝐹)‘𝑀))) |
7 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑥 = 𝑀 → (seq𝑀(𝑄, 𝐺)‘𝑥) = (seq𝑀(𝑄, 𝐺)‘𝑀)) |
8 | 6, 7 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑥 = 𝑀 → ((𝐻‘(seq𝑀( + , 𝐹)‘𝑥)) = (seq𝑀(𝑄, 𝐺)‘𝑥) ↔ (𝐻‘(seq𝑀( + , 𝐹)‘𝑀)) = (seq𝑀(𝑄, 𝐺)‘𝑀))) |
9 | 4, 8 | imbi12d 333 |
. . . . 5
⊢ (𝑥 = 𝑀 → ((𝑥 ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑥)) = (seq𝑀(𝑄, 𝐺)‘𝑥)) ↔ (𝑀 ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑀)) = (seq𝑀(𝑄, 𝐺)‘𝑀)))) |
10 | 9 | imbi2d 329 |
. . . 4
⊢ (𝑥 = 𝑀 → ((𝜑 → (𝑥 ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑥)) = (seq𝑀(𝑄, 𝐺)‘𝑥))) ↔ (𝜑 → (𝑀 ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑀)) = (seq𝑀(𝑄, 𝐺)‘𝑀))))) |
11 | | eleq1 2676 |
. . . . . 6
⊢ (𝑥 = 𝑛 → (𝑥 ∈ (𝑀...𝑁) ↔ 𝑛 ∈ (𝑀...𝑁))) |
12 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑥 = 𝑛 → (seq𝑀( + , 𝐹)‘𝑥) = (seq𝑀( + , 𝐹)‘𝑛)) |
13 | 12 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → (𝐻‘(seq𝑀( + , 𝐹)‘𝑥)) = (𝐻‘(seq𝑀( + , 𝐹)‘𝑛))) |
14 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → (seq𝑀(𝑄, 𝐺)‘𝑥) = (seq𝑀(𝑄, 𝐺)‘𝑛)) |
15 | 13, 14 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑥 = 𝑛 → ((𝐻‘(seq𝑀( + , 𝐹)‘𝑥)) = (seq𝑀(𝑄, 𝐺)‘𝑥) ↔ (𝐻‘(seq𝑀( + , 𝐹)‘𝑛)) = (seq𝑀(𝑄, 𝐺)‘𝑛))) |
16 | 11, 15 | imbi12d 333 |
. . . . 5
⊢ (𝑥 = 𝑛 → ((𝑥 ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑥)) = (seq𝑀(𝑄, 𝐺)‘𝑥)) ↔ (𝑛 ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑛)) = (seq𝑀(𝑄, 𝐺)‘𝑛)))) |
17 | 16 | imbi2d 329 |
. . . 4
⊢ (𝑥 = 𝑛 → ((𝜑 → (𝑥 ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑥)) = (seq𝑀(𝑄, 𝐺)‘𝑥))) ↔ (𝜑 → (𝑛 ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑛)) = (seq𝑀(𝑄, 𝐺)‘𝑛))))) |
18 | | eleq1 2676 |
. . . . . 6
⊢ (𝑥 = (𝑛 + 1) → (𝑥 ∈ (𝑀...𝑁) ↔ (𝑛 + 1) ∈ (𝑀...𝑁))) |
19 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑥 = (𝑛 + 1) → (seq𝑀( + , 𝐹)‘𝑥) = (seq𝑀( + , 𝐹)‘(𝑛 + 1))) |
20 | 19 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑥 = (𝑛 + 1) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑥)) = (𝐻‘(seq𝑀( + , 𝐹)‘(𝑛 + 1)))) |
21 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑥 = (𝑛 + 1) → (seq𝑀(𝑄, 𝐺)‘𝑥) = (seq𝑀(𝑄, 𝐺)‘(𝑛 + 1))) |
22 | 20, 21 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑥 = (𝑛 + 1) → ((𝐻‘(seq𝑀( + , 𝐹)‘𝑥)) = (seq𝑀(𝑄, 𝐺)‘𝑥) ↔ (𝐻‘(seq𝑀( + , 𝐹)‘(𝑛 + 1))) = (seq𝑀(𝑄, 𝐺)‘(𝑛 + 1)))) |
23 | 18, 22 | imbi12d 333 |
. . . . 5
⊢ (𝑥 = (𝑛 + 1) → ((𝑥 ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑥)) = (seq𝑀(𝑄, 𝐺)‘𝑥)) ↔ ((𝑛 + 1) ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘(𝑛 + 1))) = (seq𝑀(𝑄, 𝐺)‘(𝑛 + 1))))) |
24 | 23 | imbi2d 329 |
. . . 4
⊢ (𝑥 = (𝑛 + 1) → ((𝜑 → (𝑥 ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑥)) = (seq𝑀(𝑄, 𝐺)‘𝑥))) ↔ (𝜑 → ((𝑛 + 1) ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘(𝑛 + 1))) = (seq𝑀(𝑄, 𝐺)‘(𝑛 + 1)))))) |
25 | | eleq1 2676 |
. . . . . 6
⊢ (𝑥 = 𝑁 → (𝑥 ∈ (𝑀...𝑁) ↔ 𝑁 ∈ (𝑀...𝑁))) |
26 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → (seq𝑀( + , 𝐹)‘𝑥) = (seq𝑀( + , 𝐹)‘𝑁)) |
27 | 26 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → (𝐻‘(seq𝑀( + , 𝐹)‘𝑥)) = (𝐻‘(seq𝑀( + , 𝐹)‘𝑁))) |
28 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → (seq𝑀(𝑄, 𝐺)‘𝑥) = (seq𝑀(𝑄, 𝐺)‘𝑁)) |
29 | 27, 28 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑥 = 𝑁 → ((𝐻‘(seq𝑀( + , 𝐹)‘𝑥)) = (seq𝑀(𝑄, 𝐺)‘𝑥) ↔ (𝐻‘(seq𝑀( + , 𝐹)‘𝑁)) = (seq𝑀(𝑄, 𝐺)‘𝑁))) |
30 | 25, 29 | imbi12d 333 |
. . . . 5
⊢ (𝑥 = 𝑁 → ((𝑥 ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑥)) = (seq𝑀(𝑄, 𝐺)‘𝑥)) ↔ (𝑁 ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑁)) = (seq𝑀(𝑄, 𝐺)‘𝑁)))) |
31 | 30 | imbi2d 329 |
. . . 4
⊢ (𝑥 = 𝑁 → ((𝜑 → (𝑥 ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑥)) = (seq𝑀(𝑄, 𝐺)‘𝑥))) ↔ (𝜑 → (𝑁 ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑁)) = (seq𝑀(𝑄, 𝐺)‘𝑁))))) |
32 | | eluzfz1 12219 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁)) |
33 | 1, 32 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ (𝑀...𝑁)) |
34 | | seqhomo.5 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐻‘(𝐹‘𝑥)) = (𝐺‘𝑥)) |
35 | 34 | ralrimiva 2949 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ (𝑀...𝑁)(𝐻‘(𝐹‘𝑥)) = (𝐺‘𝑥)) |
36 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑀 → (𝐹‘𝑥) = (𝐹‘𝑀)) |
37 | 36 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑀 → (𝐻‘(𝐹‘𝑥)) = (𝐻‘(𝐹‘𝑀))) |
38 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑀 → (𝐺‘𝑥) = (𝐺‘𝑀)) |
39 | 37, 38 | eqeq12d 2625 |
. . . . . . . . 9
⊢ (𝑥 = 𝑀 → ((𝐻‘(𝐹‘𝑥)) = (𝐺‘𝑥) ↔ (𝐻‘(𝐹‘𝑀)) = (𝐺‘𝑀))) |
40 | 39 | rspcv 3278 |
. . . . . . . 8
⊢ (𝑀 ∈ (𝑀...𝑁) → (∀𝑥 ∈ (𝑀...𝑁)(𝐻‘(𝐹‘𝑥)) = (𝐺‘𝑥) → (𝐻‘(𝐹‘𝑀)) = (𝐺‘𝑀))) |
41 | 33, 35, 40 | sylc 63 |
. . . . . . 7
⊢ (𝜑 → (𝐻‘(𝐹‘𝑀)) = (𝐺‘𝑀)) |
42 | | eluzel2 11568 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
43 | | seq1 12676 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℤ → (seq𝑀( + , 𝐹)‘𝑀) = (𝐹‘𝑀)) |
44 | 1, 42, 43 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑀) = (𝐹‘𝑀)) |
45 | 44 | fveq2d 6107 |
. . . . . . 7
⊢ (𝜑 → (𝐻‘(seq𝑀( + , 𝐹)‘𝑀)) = (𝐻‘(𝐹‘𝑀))) |
46 | | seq1 12676 |
. . . . . . . 8
⊢ (𝑀 ∈ ℤ → (seq𝑀(𝑄, 𝐺)‘𝑀) = (𝐺‘𝑀)) |
47 | 1, 42, 46 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (seq𝑀(𝑄, 𝐺)‘𝑀) = (𝐺‘𝑀)) |
48 | 41, 45, 47 | 3eqtr4d 2654 |
. . . . . 6
⊢ (𝜑 → (𝐻‘(seq𝑀( + , 𝐹)‘𝑀)) = (seq𝑀(𝑄, 𝐺)‘𝑀)) |
49 | 48 | a1d 25 |
. . . . 5
⊢ (𝜑 → (𝑀 ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑀)) = (seq𝑀(𝑄, 𝐺)‘𝑀))) |
50 | 49 | a1i 11 |
. . . 4
⊢ (𝑀 ∈ ℤ → (𝜑 → (𝑀 ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑀)) = (seq𝑀(𝑄, 𝐺)‘𝑀)))) |
51 | | simprl 790 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → 𝑛 ∈ (ℤ≥‘𝑀)) |
52 | | simprr 792 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (𝑛 + 1) ∈ (𝑀...𝑁)) |
53 | | peano2fzr 12225 |
. . . . . . . . . 10
⊢ ((𝑛 ∈
(ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → 𝑛 ∈ (𝑀...𝑁)) |
54 | 51, 52, 53 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → 𝑛 ∈ (𝑀...𝑁)) |
55 | 54 | expr 641 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → ((𝑛 + 1) ∈ (𝑀...𝑁) → 𝑛 ∈ (𝑀...𝑁))) |
56 | 55 | imim1d 80 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → ((𝑛 ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑛)) = (seq𝑀(𝑄, 𝐺)‘𝑛)) → ((𝑛 + 1) ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑛)) = (seq𝑀(𝑄, 𝐺)‘𝑛)))) |
57 | | oveq1 6556 |
. . . . . . . . . 10
⊢ ((𝐻‘(seq𝑀( + , 𝐹)‘𝑛)) = (seq𝑀(𝑄, 𝐺)‘𝑛) → ((𝐻‘(seq𝑀( + , 𝐹)‘𝑛))𝑄(𝐺‘(𝑛 + 1))) = ((seq𝑀(𝑄, 𝐺)‘𝑛)𝑄(𝐺‘(𝑛 + 1)))) |
58 | | seqp1 12678 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → (seq𝑀( + , 𝐹)‘(𝑛 + 1)) = ((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1)))) |
59 | 58 | ad2antrl 760 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (seq𝑀( + , 𝐹)‘(𝑛 + 1)) = ((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1)))) |
60 | 59 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (𝐻‘(seq𝑀( + , 𝐹)‘(𝑛 + 1))) = (𝐻‘((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1))))) |
61 | | seqhomo.4 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝐻‘(𝑥 + 𝑦)) = ((𝐻‘𝑥)𝑄(𝐻‘𝑦))) |
62 | 61 | ralrimivva 2954 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝐻‘(𝑥 + 𝑦)) = ((𝐻‘𝑥)𝑄(𝐻‘𝑦))) |
63 | 62 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝐻‘(𝑥 + 𝑦)) = ((𝐻‘𝑥)𝑄(𝐻‘𝑦))) |
64 | | elfzuz3 12210 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝑛)) |
65 | | fzss2 12252 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈
(ℤ≥‘𝑛) → (𝑀...𝑛) ⊆ (𝑀...𝑁)) |
66 | 54, 64, 65 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (𝑀...𝑛) ⊆ (𝑀...𝑁)) |
67 | 66 | sselda 3568 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) ∧ 𝑥 ∈ (𝑀...𝑛)) → 𝑥 ∈ (𝑀...𝑁)) |
68 | | seqhomo.2 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) ∈ 𝑆) |
69 | 68 | adantlr 747 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) ∈ 𝑆) |
70 | 67, 69 | syldan 486 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) ∧ 𝑥 ∈ (𝑀...𝑛)) → (𝐹‘𝑥) ∈ 𝑆) |
71 | | seqhomo.1 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
72 | 71 | adantlr 747 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
73 | 51, 70, 72 | seqcl 12683 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (seq𝑀( + , 𝐹)‘𝑛) ∈ 𝑆) |
74 | 68 | ralrimiva 2949 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∀𝑥 ∈ (𝑀...𝑁)(𝐹‘𝑥) ∈ 𝑆) |
75 | 74 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → ∀𝑥 ∈ (𝑀...𝑁)(𝐹‘𝑥) ∈ 𝑆) |
76 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (𝑛 + 1) → (𝐹‘𝑥) = (𝐹‘(𝑛 + 1))) |
77 | 76 | eleq1d 2672 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝑛 + 1) → ((𝐹‘𝑥) ∈ 𝑆 ↔ (𝐹‘(𝑛 + 1)) ∈ 𝑆)) |
78 | 77 | rspcv 3278 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 + 1) ∈ (𝑀...𝑁) → (∀𝑥 ∈ (𝑀...𝑁)(𝐹‘𝑥) ∈ 𝑆 → (𝐹‘(𝑛 + 1)) ∈ 𝑆)) |
79 | 52, 75, 78 | sylc 63 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (𝐹‘(𝑛 + 1)) ∈ 𝑆) |
80 | | oveq1 6556 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (seq𝑀( + , 𝐹)‘𝑛) → (𝑥 + 𝑦) = ((seq𝑀( + , 𝐹)‘𝑛) + 𝑦)) |
81 | 80 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (seq𝑀( + , 𝐹)‘𝑛) → (𝐻‘(𝑥 + 𝑦)) = (𝐻‘((seq𝑀( + , 𝐹)‘𝑛) + 𝑦))) |
82 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (seq𝑀( + , 𝐹)‘𝑛) → (𝐻‘𝑥) = (𝐻‘(seq𝑀( + , 𝐹)‘𝑛))) |
83 | 82 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (seq𝑀( + , 𝐹)‘𝑛) → ((𝐻‘𝑥)𝑄(𝐻‘𝑦)) = ((𝐻‘(seq𝑀( + , 𝐹)‘𝑛))𝑄(𝐻‘𝑦))) |
84 | 81, 83 | eqeq12d 2625 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (seq𝑀( + , 𝐹)‘𝑛) → ((𝐻‘(𝑥 + 𝑦)) = ((𝐻‘𝑥)𝑄(𝐻‘𝑦)) ↔ (𝐻‘((seq𝑀( + , 𝐹)‘𝑛) + 𝑦)) = ((𝐻‘(seq𝑀( + , 𝐹)‘𝑛))𝑄(𝐻‘𝑦)))) |
85 | | oveq2 6557 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = (𝐹‘(𝑛 + 1)) → ((seq𝑀( + , 𝐹)‘𝑛) + 𝑦) = ((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1)))) |
86 | 85 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = (𝐹‘(𝑛 + 1)) → (𝐻‘((seq𝑀( + , 𝐹)‘𝑛) + 𝑦)) = (𝐻‘((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1))))) |
87 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = (𝐹‘(𝑛 + 1)) → (𝐻‘𝑦) = (𝐻‘(𝐹‘(𝑛 + 1)))) |
88 | 87 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = (𝐹‘(𝑛 + 1)) → ((𝐻‘(seq𝑀( + , 𝐹)‘𝑛))𝑄(𝐻‘𝑦)) = ((𝐻‘(seq𝑀( + , 𝐹)‘𝑛))𝑄(𝐻‘(𝐹‘(𝑛 + 1))))) |
89 | 86, 88 | eqeq12d 2625 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝐹‘(𝑛 + 1)) → ((𝐻‘((seq𝑀( + , 𝐹)‘𝑛) + 𝑦)) = ((𝐻‘(seq𝑀( + , 𝐹)‘𝑛))𝑄(𝐻‘𝑦)) ↔ (𝐻‘((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1)))) = ((𝐻‘(seq𝑀( + , 𝐹)‘𝑛))𝑄(𝐻‘(𝐹‘(𝑛 + 1)))))) |
90 | 84, 89 | rspc2v 3293 |
. . . . . . . . . . . . . 14
⊢
(((seq𝑀( + , 𝐹)‘𝑛) ∈ 𝑆 ∧ (𝐹‘(𝑛 + 1)) ∈ 𝑆) → (∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝐻‘(𝑥 + 𝑦)) = ((𝐻‘𝑥)𝑄(𝐻‘𝑦)) → (𝐻‘((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1)))) = ((𝐻‘(seq𝑀( + , 𝐹)‘𝑛))𝑄(𝐻‘(𝐹‘(𝑛 + 1)))))) |
91 | 73, 79, 90 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝐻‘(𝑥 + 𝑦)) = ((𝐻‘𝑥)𝑄(𝐻‘𝑦)) → (𝐻‘((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1)))) = ((𝐻‘(seq𝑀( + , 𝐹)‘𝑛))𝑄(𝐻‘(𝐹‘(𝑛 + 1)))))) |
92 | 63, 91 | mpd 15 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (𝐻‘((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1)))) = ((𝐻‘(seq𝑀( + , 𝐹)‘𝑛))𝑄(𝐻‘(𝐹‘(𝑛 + 1))))) |
93 | 35 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → ∀𝑥 ∈ (𝑀...𝑁)(𝐻‘(𝐹‘𝑥)) = (𝐺‘𝑥)) |
94 | 76 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝑛 + 1) → (𝐻‘(𝐹‘𝑥)) = (𝐻‘(𝐹‘(𝑛 + 1)))) |
95 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝑛 + 1) → (𝐺‘𝑥) = (𝐺‘(𝑛 + 1))) |
96 | 94, 95 | eqeq12d 2625 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑛 + 1) → ((𝐻‘(𝐹‘𝑥)) = (𝐺‘𝑥) ↔ (𝐻‘(𝐹‘(𝑛 + 1))) = (𝐺‘(𝑛 + 1)))) |
97 | 96 | rspcv 3278 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 + 1) ∈ (𝑀...𝑁) → (∀𝑥 ∈ (𝑀...𝑁)(𝐻‘(𝐹‘𝑥)) = (𝐺‘𝑥) → (𝐻‘(𝐹‘(𝑛 + 1))) = (𝐺‘(𝑛 + 1)))) |
98 | 52, 93, 97 | sylc 63 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (𝐻‘(𝐹‘(𝑛 + 1))) = (𝐺‘(𝑛 + 1))) |
99 | 98 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → ((𝐻‘(seq𝑀( + , 𝐹)‘𝑛))𝑄(𝐻‘(𝐹‘(𝑛 + 1)))) = ((𝐻‘(seq𝑀( + , 𝐹)‘𝑛))𝑄(𝐺‘(𝑛 + 1)))) |
100 | 60, 92, 99 | 3eqtrd 2648 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (𝐻‘(seq𝑀( + , 𝐹)‘(𝑛 + 1))) = ((𝐻‘(seq𝑀( + , 𝐹)‘𝑛))𝑄(𝐺‘(𝑛 + 1)))) |
101 | | seqp1 12678 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → (seq𝑀(𝑄, 𝐺)‘(𝑛 + 1)) = ((seq𝑀(𝑄, 𝐺)‘𝑛)𝑄(𝐺‘(𝑛 + 1)))) |
102 | 101 | ad2antrl 760 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (seq𝑀(𝑄, 𝐺)‘(𝑛 + 1)) = ((seq𝑀(𝑄, 𝐺)‘𝑛)𝑄(𝐺‘(𝑛 + 1)))) |
103 | 100, 102 | eqeq12d 2625 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → ((𝐻‘(seq𝑀( + , 𝐹)‘(𝑛 + 1))) = (seq𝑀(𝑄, 𝐺)‘(𝑛 + 1)) ↔ ((𝐻‘(seq𝑀( + , 𝐹)‘𝑛))𝑄(𝐺‘(𝑛 + 1))) = ((seq𝑀(𝑄, 𝐺)‘𝑛)𝑄(𝐺‘(𝑛 + 1))))) |
104 | 57, 103 | syl5ibr 235 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → ((𝐻‘(seq𝑀( + , 𝐹)‘𝑛)) = (seq𝑀(𝑄, 𝐺)‘𝑛) → (𝐻‘(seq𝑀( + , 𝐹)‘(𝑛 + 1))) = (seq𝑀(𝑄, 𝐺)‘(𝑛 + 1)))) |
105 | 104 | expr 641 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → ((𝑛 + 1) ∈ (𝑀...𝑁) → ((𝐻‘(seq𝑀( + , 𝐹)‘𝑛)) = (seq𝑀(𝑄, 𝐺)‘𝑛) → (𝐻‘(seq𝑀( + , 𝐹)‘(𝑛 + 1))) = (seq𝑀(𝑄, 𝐺)‘(𝑛 + 1))))) |
106 | 105 | a2d 29 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (((𝑛 + 1) ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑛)) = (seq𝑀(𝑄, 𝐺)‘𝑛)) → ((𝑛 + 1) ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘(𝑛 + 1))) = (seq𝑀(𝑄, 𝐺)‘(𝑛 + 1))))) |
107 | 56, 106 | syld 46 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → ((𝑛 ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑛)) = (seq𝑀(𝑄, 𝐺)‘𝑛)) → ((𝑛 + 1) ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘(𝑛 + 1))) = (seq𝑀(𝑄, 𝐺)‘(𝑛 + 1))))) |
108 | 107 | expcom 450 |
. . . . 5
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → (𝜑 → ((𝑛 ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑛)) = (seq𝑀(𝑄, 𝐺)‘𝑛)) → ((𝑛 + 1) ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘(𝑛 + 1))) = (seq𝑀(𝑄, 𝐺)‘(𝑛 + 1)))))) |
109 | 108 | a2d 29 |
. . . 4
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → ((𝜑 → (𝑛 ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑛)) = (seq𝑀(𝑄, 𝐺)‘𝑛))) → (𝜑 → ((𝑛 + 1) ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘(𝑛 + 1))) = (seq𝑀(𝑄, 𝐺)‘(𝑛 + 1)))))) |
110 | 10, 17, 24, 31, 50, 109 | uzind4 11622 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝜑 → (𝑁 ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑁)) = (seq𝑀(𝑄, 𝐺)‘𝑁)))) |
111 | 1, 110 | mpcom 37 |
. 2
⊢ (𝜑 → (𝑁 ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑁)) = (seq𝑀(𝑄, 𝐺)‘𝑁))) |
112 | 3, 111 | mpd 15 |
1
⊢ (𝜑 → (𝐻‘(seq𝑀( + , 𝐹)‘𝑁)) = (seq𝑀(𝑄, 𝐺)‘𝑁)) |