Step | Hyp | Ref
| Expression |
1 | | seqfveq2.3 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝐾)) |
2 | | eluzfz2 12220 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝐾) → 𝑁 ∈ (𝐾...𝑁)) |
3 | 1, 2 | syl 17 |
. 2
⊢ (𝜑 → 𝑁 ∈ (𝐾...𝑁)) |
4 | | eleq1 2676 |
. . . . . 6
⊢ (𝑥 = 𝐾 → (𝑥 ∈ (𝐾...𝑁) ↔ 𝐾 ∈ (𝐾...𝑁))) |
5 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑥 = 𝐾 → (seq𝑀( + , 𝐹)‘𝑥) = (seq𝑀( + , 𝐹)‘𝐾)) |
6 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑥 = 𝐾 → (seq𝐾( + , 𝐺)‘𝑥) = (seq𝐾( + , 𝐺)‘𝐾)) |
7 | 5, 6 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑥 = 𝐾 → ((seq𝑀( + , 𝐹)‘𝑥) = (seq𝐾( + , 𝐺)‘𝑥) ↔ (seq𝑀( + , 𝐹)‘𝐾) = (seq𝐾( + , 𝐺)‘𝐾))) |
8 | 4, 7 | imbi12d 333 |
. . . . 5
⊢ (𝑥 = 𝐾 → ((𝑥 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝑥) = (seq𝐾( + , 𝐺)‘𝑥)) ↔ (𝐾 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝐾( + , 𝐺)‘𝐾)))) |
9 | 8 | imbi2d 329 |
. . . 4
⊢ (𝑥 = 𝐾 → ((𝜑 → (𝑥 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝑥) = (seq𝐾( + , 𝐺)‘𝑥))) ↔ (𝜑 → (𝐾 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝐾( + , 𝐺)‘𝐾))))) |
10 | | eleq1 2676 |
. . . . . 6
⊢ (𝑥 = 𝑛 → (𝑥 ∈ (𝐾...𝑁) ↔ 𝑛 ∈ (𝐾...𝑁))) |
11 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → (seq𝑀( + , 𝐹)‘𝑥) = (seq𝑀( + , 𝐹)‘𝑛)) |
12 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → (seq𝐾( + , 𝐺)‘𝑥) = (seq𝐾( + , 𝐺)‘𝑛)) |
13 | 11, 12 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑥 = 𝑛 → ((seq𝑀( + , 𝐹)‘𝑥) = (seq𝐾( + , 𝐺)‘𝑥) ↔ (seq𝑀( + , 𝐹)‘𝑛) = (seq𝐾( + , 𝐺)‘𝑛))) |
14 | 10, 13 | imbi12d 333 |
. . . . 5
⊢ (𝑥 = 𝑛 → ((𝑥 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝑥) = (seq𝐾( + , 𝐺)‘𝑥)) ↔ (𝑛 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝑛) = (seq𝐾( + , 𝐺)‘𝑛)))) |
15 | 14 | imbi2d 329 |
. . . 4
⊢ (𝑥 = 𝑛 → ((𝜑 → (𝑥 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝑥) = (seq𝐾( + , 𝐺)‘𝑥))) ↔ (𝜑 → (𝑛 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝑛) = (seq𝐾( + , 𝐺)‘𝑛))))) |
16 | | eleq1 2676 |
. . . . . 6
⊢ (𝑥 = (𝑛 + 1) → (𝑥 ∈ (𝐾...𝑁) ↔ (𝑛 + 1) ∈ (𝐾...𝑁))) |
17 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑥 = (𝑛 + 1) → (seq𝑀( + , 𝐹)‘𝑥) = (seq𝑀( + , 𝐹)‘(𝑛 + 1))) |
18 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑥 = (𝑛 + 1) → (seq𝐾( + , 𝐺)‘𝑥) = (seq𝐾( + , 𝐺)‘(𝑛 + 1))) |
19 | 17, 18 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑥 = (𝑛 + 1) → ((seq𝑀( + , 𝐹)‘𝑥) = (seq𝐾( + , 𝐺)‘𝑥) ↔ (seq𝑀( + , 𝐹)‘(𝑛 + 1)) = (seq𝐾( + , 𝐺)‘(𝑛 + 1)))) |
20 | 16, 19 | imbi12d 333 |
. . . . 5
⊢ (𝑥 = (𝑛 + 1) → ((𝑥 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝑥) = (seq𝐾( + , 𝐺)‘𝑥)) ↔ ((𝑛 + 1) ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘(𝑛 + 1)) = (seq𝐾( + , 𝐺)‘(𝑛 + 1))))) |
21 | 20 | imbi2d 329 |
. . . 4
⊢ (𝑥 = (𝑛 + 1) → ((𝜑 → (𝑥 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝑥) = (seq𝐾( + , 𝐺)‘𝑥))) ↔ (𝜑 → ((𝑛 + 1) ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘(𝑛 + 1)) = (seq𝐾( + , 𝐺)‘(𝑛 + 1)))))) |
22 | | eleq1 2676 |
. . . . . 6
⊢ (𝑥 = 𝑁 → (𝑥 ∈ (𝐾...𝑁) ↔ 𝑁 ∈ (𝐾...𝑁))) |
23 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → (seq𝑀( + , 𝐹)‘𝑥) = (seq𝑀( + , 𝐹)‘𝑁)) |
24 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → (seq𝐾( + , 𝐺)‘𝑥) = (seq𝐾( + , 𝐺)‘𝑁)) |
25 | 23, 24 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑥 = 𝑁 → ((seq𝑀( + , 𝐹)‘𝑥) = (seq𝐾( + , 𝐺)‘𝑥) ↔ (seq𝑀( + , 𝐹)‘𝑁) = (seq𝐾( + , 𝐺)‘𝑁))) |
26 | 22, 25 | imbi12d 333 |
. . . . 5
⊢ (𝑥 = 𝑁 → ((𝑥 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝑥) = (seq𝐾( + , 𝐺)‘𝑥)) ↔ (𝑁 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝑁) = (seq𝐾( + , 𝐺)‘𝑁)))) |
27 | 26 | imbi2d 329 |
. . . 4
⊢ (𝑥 = 𝑁 → ((𝜑 → (𝑥 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝑥) = (seq𝐾( + , 𝐺)‘𝑥))) ↔ (𝜑 → (𝑁 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝑁) = (seq𝐾( + , 𝐺)‘𝑁))))) |
28 | | seqfveq2.2 |
. . . . . . 7
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) = (𝐺‘𝐾)) |
29 | | seqfveq2.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘𝑀)) |
30 | | eluzelz 11573 |
. . . . . . . . 9
⊢ (𝐾 ∈
(ℤ≥‘𝑀) → 𝐾 ∈ ℤ) |
31 | 29, 30 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ ℤ) |
32 | | seq1 12676 |
. . . . . . . 8
⊢ (𝐾 ∈ ℤ → (seq𝐾( + , 𝐺)‘𝐾) = (𝐺‘𝐾)) |
33 | 31, 32 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (seq𝐾( + , 𝐺)‘𝐾) = (𝐺‘𝐾)) |
34 | 28, 33 | eqtr4d 2647 |
. . . . . 6
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝐾( + , 𝐺)‘𝐾)) |
35 | 34 | a1d 25 |
. . . . 5
⊢ (𝜑 → (𝐾 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝐾( + , 𝐺)‘𝐾))) |
36 | 35 | a1i 11 |
. . . 4
⊢ (𝐾 ∈ ℤ → (𝜑 → (𝐾 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝐾( + , 𝐺)‘𝐾)))) |
37 | | peano2fzr 12225 |
. . . . . . . . . 10
⊢ ((𝑛 ∈
(ℤ≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁)) → 𝑛 ∈ (𝐾...𝑁)) |
38 | 37 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → 𝑛 ∈ (𝐾...𝑁)) |
39 | 38 | expr 641 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝐾)) → ((𝑛 + 1) ∈ (𝐾...𝑁) → 𝑛 ∈ (𝐾...𝑁))) |
40 | 39 | imim1d 80 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝐾)) → ((𝑛 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝑛) = (seq𝐾( + , 𝐺)‘𝑛)) → ((𝑛 + 1) ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝑛) = (seq𝐾( + , 𝐺)‘𝑛)))) |
41 | | oveq1 6556 |
. . . . . . . . . 10
⊢
((seq𝑀( + , 𝐹)‘𝑛) = (seq𝐾( + , 𝐺)‘𝑛) → ((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1))) = ((seq𝐾( + , 𝐺)‘𝑛) + (𝐹‘(𝑛 + 1)))) |
42 | | simpl 472 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈
(ℤ≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁)) → 𝑛 ∈ (ℤ≥‘𝐾)) |
43 | | uztrn 11580 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈
(ℤ≥‘𝐾) ∧ 𝐾 ∈ (ℤ≥‘𝑀)) → 𝑛 ∈ (ℤ≥‘𝑀)) |
44 | 42, 29, 43 | syl2anr 494 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → 𝑛 ∈ (ℤ≥‘𝑀)) |
45 | | seqp1 12678 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → (seq𝑀( + , 𝐹)‘(𝑛 + 1)) = ((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1)))) |
46 | 44, 45 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → (seq𝑀( + , 𝐹)‘(𝑛 + 1)) = ((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1)))) |
47 | | seqp1 12678 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈
(ℤ≥‘𝐾) → (seq𝐾( + , 𝐺)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐺)‘𝑛) + (𝐺‘(𝑛 + 1)))) |
48 | 47 | ad2antrl 760 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → (seq𝐾( + , 𝐺)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐺)‘𝑛) + (𝐺‘(𝑛 + 1)))) |
49 | | eluzp1p1 11589 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈
(ℤ≥‘𝐾) → (𝑛 + 1) ∈
(ℤ≥‘(𝐾 + 1))) |
50 | 49 | ad2antrl 760 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → (𝑛 + 1) ∈
(ℤ≥‘(𝐾 + 1))) |
51 | | elfzuz3 12210 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 + 1) ∈ (𝐾...𝑁) → 𝑁 ∈ (ℤ≥‘(𝑛 + 1))) |
52 | 51 | ad2antll 761 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → 𝑁 ∈ (ℤ≥‘(𝑛 + 1))) |
53 | | elfzuzb 12207 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 + 1) ∈ ((𝐾 + 1)...𝑁) ↔ ((𝑛 + 1) ∈
(ℤ≥‘(𝐾 + 1)) ∧ 𝑁 ∈ (ℤ≥‘(𝑛 + 1)))) |
54 | 50, 52, 53 | sylanbrc 695 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → (𝑛 + 1) ∈ ((𝐾 + 1)...𝑁)) |
55 | | seqfveq2.4 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝐹‘𝑘) = (𝐺‘𝑘)) |
56 | 55 | ralrimiva 2949 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑘 ∈ ((𝐾 + 1)...𝑁)(𝐹‘𝑘) = (𝐺‘𝑘)) |
57 | 56 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → ∀𝑘 ∈ ((𝐾 + 1)...𝑁)(𝐹‘𝑘) = (𝐺‘𝑘)) |
58 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = (𝑛 + 1) → (𝐹‘𝑘) = (𝐹‘(𝑛 + 1))) |
59 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = (𝑛 + 1) → (𝐺‘𝑘) = (𝐺‘(𝑛 + 1))) |
60 | 58, 59 | eqeq12d 2625 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = (𝑛 + 1) → ((𝐹‘𝑘) = (𝐺‘𝑘) ↔ (𝐹‘(𝑛 + 1)) = (𝐺‘(𝑛 + 1)))) |
61 | 60 | rspcv 3278 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 + 1) ∈ ((𝐾 + 1)...𝑁) → (∀𝑘 ∈ ((𝐾 + 1)...𝑁)(𝐹‘𝑘) = (𝐺‘𝑘) → (𝐹‘(𝑛 + 1)) = (𝐺‘(𝑛 + 1)))) |
62 | 54, 57, 61 | sylc 63 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → (𝐹‘(𝑛 + 1)) = (𝐺‘(𝑛 + 1))) |
63 | 62 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → ((seq𝐾( + , 𝐺)‘𝑛) + (𝐹‘(𝑛 + 1))) = ((seq𝐾( + , 𝐺)‘𝑛) + (𝐺‘(𝑛 + 1)))) |
64 | 48, 63 | eqtr4d 2647 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → (seq𝐾( + , 𝐺)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐺)‘𝑛) + (𝐹‘(𝑛 + 1)))) |
65 | 46, 64 | eqeq12d 2625 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → ((seq𝑀( + , 𝐹)‘(𝑛 + 1)) = (seq𝐾( + , 𝐺)‘(𝑛 + 1)) ↔ ((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1))) = ((seq𝐾( + , 𝐺)‘𝑛) + (𝐹‘(𝑛 + 1))))) |
66 | 41, 65 | syl5ibr 235 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → ((seq𝑀( + , 𝐹)‘𝑛) = (seq𝐾( + , 𝐺)‘𝑛) → (seq𝑀( + , 𝐹)‘(𝑛 + 1)) = (seq𝐾( + , 𝐺)‘(𝑛 + 1)))) |
67 | 66 | expr 641 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝐾)) → ((𝑛 + 1) ∈ (𝐾...𝑁) → ((seq𝑀( + , 𝐹)‘𝑛) = (seq𝐾( + , 𝐺)‘𝑛) → (seq𝑀( + , 𝐹)‘(𝑛 + 1)) = (seq𝐾( + , 𝐺)‘(𝑛 + 1))))) |
68 | 67 | a2d 29 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝐾)) → (((𝑛 + 1) ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝑛) = (seq𝐾( + , 𝐺)‘𝑛)) → ((𝑛 + 1) ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘(𝑛 + 1)) = (seq𝐾( + , 𝐺)‘(𝑛 + 1))))) |
69 | 40, 68 | syld 46 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝐾)) → ((𝑛 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝑛) = (seq𝐾( + , 𝐺)‘𝑛)) → ((𝑛 + 1) ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘(𝑛 + 1)) = (seq𝐾( + , 𝐺)‘(𝑛 + 1))))) |
70 | 69 | expcom 450 |
. . . . 5
⊢ (𝑛 ∈
(ℤ≥‘𝐾) → (𝜑 → ((𝑛 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝑛) = (seq𝐾( + , 𝐺)‘𝑛)) → ((𝑛 + 1) ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘(𝑛 + 1)) = (seq𝐾( + , 𝐺)‘(𝑛 + 1)))))) |
71 | 70 | a2d 29 |
. . . 4
⊢ (𝑛 ∈
(ℤ≥‘𝐾) → ((𝜑 → (𝑛 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝑛) = (seq𝐾( + , 𝐺)‘𝑛))) → (𝜑 → ((𝑛 + 1) ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘(𝑛 + 1)) = (seq𝐾( + , 𝐺)‘(𝑛 + 1)))))) |
72 | 9, 15, 21, 27, 36, 71 | uzind4 11622 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝐾) → (𝜑 → (𝑁 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝑁) = (seq𝐾( + , 𝐺)‘𝑁)))) |
73 | 1, 72 | mpcom 37 |
. 2
⊢ (𝜑 → (𝑁 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝑁) = (seq𝐾( + , 𝐺)‘𝑁))) |
74 | 3, 73 | mpd 15 |
1
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = (seq𝐾( + , 𝐺)‘𝑁)) |