Step | Hyp | Ref
| Expression |
1 | | seqfveq2.3 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝐾)) |
2 | | eluzfz2 10088 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝐾) → 𝑁 ∈ (𝐾...𝑁)) |
3 | 1, 2 | syl 14 |
. 2
⊢ (𝜑 → 𝑁 ∈ (𝐾...𝑁)) |
4 | | eleq1 2256 |
. . . . . 6
⊢ (𝑥 = 𝐾 → (𝑥 ∈ (𝐾...𝑁) ↔ 𝐾 ∈ (𝐾...𝑁))) |
5 | | fveq2 5546 |
. . . . . . 7
⊢ (𝑥 = 𝐾 → (seq𝑀( + , 𝐹)‘𝑥) = (seq𝑀( + , 𝐹)‘𝐾)) |
6 | | fveq2 5546 |
. . . . . . 7
⊢ (𝑥 = 𝐾 → (seq𝐾( + , 𝐺)‘𝑥) = (seq𝐾( + , 𝐺)‘𝐾)) |
7 | 5, 6 | eqeq12d 2208 |
. . . . . 6
⊢ (𝑥 = 𝐾 → ((seq𝑀( + , 𝐹)‘𝑥) = (seq𝐾( + , 𝐺)‘𝑥) ↔ (seq𝑀( + , 𝐹)‘𝐾) = (seq𝐾( + , 𝐺)‘𝐾))) |
8 | 4, 7 | imbi12d 234 |
. . . . 5
⊢ (𝑥 = 𝐾 → ((𝑥 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝑥) = (seq𝐾( + , 𝐺)‘𝑥)) ↔ (𝐾 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝐾( + , 𝐺)‘𝐾)))) |
9 | 8 | imbi2d 230 |
. . . 4
⊢ (𝑥 = 𝐾 → ((𝜑 → (𝑥 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝑥) = (seq𝐾( + , 𝐺)‘𝑥))) ↔ (𝜑 → (𝐾 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝐾( + , 𝐺)‘𝐾))))) |
10 | | eleq1 2256 |
. . . . . 6
⊢ (𝑥 = 𝑛 → (𝑥 ∈ (𝐾...𝑁) ↔ 𝑛 ∈ (𝐾...𝑁))) |
11 | | fveq2 5546 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → (seq𝑀( + , 𝐹)‘𝑥) = (seq𝑀( + , 𝐹)‘𝑛)) |
12 | | fveq2 5546 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → (seq𝐾( + , 𝐺)‘𝑥) = (seq𝐾( + , 𝐺)‘𝑛)) |
13 | 11, 12 | eqeq12d 2208 |
. . . . . 6
⊢ (𝑥 = 𝑛 → ((seq𝑀( + , 𝐹)‘𝑥) = (seq𝐾( + , 𝐺)‘𝑥) ↔ (seq𝑀( + , 𝐹)‘𝑛) = (seq𝐾( + , 𝐺)‘𝑛))) |
14 | 10, 13 | imbi12d 234 |
. . . . 5
⊢ (𝑥 = 𝑛 → ((𝑥 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝑥) = (seq𝐾( + , 𝐺)‘𝑥)) ↔ (𝑛 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝑛) = (seq𝐾( + , 𝐺)‘𝑛)))) |
15 | 14 | imbi2d 230 |
. . . 4
⊢ (𝑥 = 𝑛 → ((𝜑 → (𝑥 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝑥) = (seq𝐾( + , 𝐺)‘𝑥))) ↔ (𝜑 → (𝑛 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝑛) = (seq𝐾( + , 𝐺)‘𝑛))))) |
16 | | eleq1 2256 |
. . . . . 6
⊢ (𝑥 = (𝑛 + 1) → (𝑥 ∈ (𝐾...𝑁) ↔ (𝑛 + 1) ∈ (𝐾...𝑁))) |
17 | | fveq2 5546 |
. . . . . . 7
⊢ (𝑥 = (𝑛 + 1) → (seq𝑀( + , 𝐹)‘𝑥) = (seq𝑀( + , 𝐹)‘(𝑛 + 1))) |
18 | | fveq2 5546 |
. . . . . . 7
⊢ (𝑥 = (𝑛 + 1) → (seq𝐾( + , 𝐺)‘𝑥) = (seq𝐾( + , 𝐺)‘(𝑛 + 1))) |
19 | 17, 18 | eqeq12d 2208 |
. . . . . 6
⊢ (𝑥 = (𝑛 + 1) → ((seq𝑀( + , 𝐹)‘𝑥) = (seq𝐾( + , 𝐺)‘𝑥) ↔ (seq𝑀( + , 𝐹)‘(𝑛 + 1)) = (seq𝐾( + , 𝐺)‘(𝑛 + 1)))) |
20 | 16, 19 | imbi12d 234 |
. . . . 5
⊢ (𝑥 = (𝑛 + 1) → ((𝑥 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝑥) = (seq𝐾( + , 𝐺)‘𝑥)) ↔ ((𝑛 + 1) ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘(𝑛 + 1)) = (seq𝐾( + , 𝐺)‘(𝑛 + 1))))) |
21 | 20 | imbi2d 230 |
. . . 4
⊢ (𝑥 = (𝑛 + 1) → ((𝜑 → (𝑥 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝑥) = (seq𝐾( + , 𝐺)‘𝑥))) ↔ (𝜑 → ((𝑛 + 1) ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘(𝑛 + 1)) = (seq𝐾( + , 𝐺)‘(𝑛 + 1)))))) |
22 | | eleq1 2256 |
. . . . . 6
⊢ (𝑥 = 𝑁 → (𝑥 ∈ (𝐾...𝑁) ↔ 𝑁 ∈ (𝐾...𝑁))) |
23 | | fveq2 5546 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → (seq𝑀( + , 𝐹)‘𝑥) = (seq𝑀( + , 𝐹)‘𝑁)) |
24 | | fveq2 5546 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → (seq𝐾( + , 𝐺)‘𝑥) = (seq𝐾( + , 𝐺)‘𝑁)) |
25 | 23, 24 | eqeq12d 2208 |
. . . . . 6
⊢ (𝑥 = 𝑁 → ((seq𝑀( + , 𝐹)‘𝑥) = (seq𝐾( + , 𝐺)‘𝑥) ↔ (seq𝑀( + , 𝐹)‘𝑁) = (seq𝐾( + , 𝐺)‘𝑁))) |
26 | 22, 25 | imbi12d 234 |
. . . . 5
⊢ (𝑥 = 𝑁 → ((𝑥 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝑥) = (seq𝐾( + , 𝐺)‘𝑥)) ↔ (𝑁 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝑁) = (seq𝐾( + , 𝐺)‘𝑁)))) |
27 | 26 | imbi2d 230 |
. . . 4
⊢ (𝑥 = 𝑁 → ((𝜑 → (𝑥 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝑥) = (seq𝐾( + , 𝐺)‘𝑥))) ↔ (𝜑 → (𝑁 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝑁) = (seq𝐾( + , 𝐺)‘𝑁))))) |
28 | | seqfveq2.2 |
. . . . . 6
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) = (𝐺‘𝐾)) |
29 | | seqfveq2.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘𝑀)) |
30 | | eluzelz 9591 |
. . . . . . . 8
⊢ (𝐾 ∈
(ℤ≥‘𝑀) → 𝐾 ∈ ℤ) |
31 | 29, 30 | syl 14 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ ℤ) |
32 | | seqfveq2g.g |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ 𝑋) |
33 | | seqfveq2g.p |
. . . . . . 7
⊢ (𝜑 → + ∈ 𝑉) |
34 | | seq1g 10524 |
. . . . . . 7
⊢ ((𝐾 ∈ ℤ ∧ 𝐺 ∈ 𝑋 ∧ + ∈ 𝑉) → (seq𝐾( + , 𝐺)‘𝐾) = (𝐺‘𝐾)) |
35 | 31, 32, 33, 34 | syl3anc 1249 |
. . . . . 6
⊢ (𝜑 → (seq𝐾( + , 𝐺)‘𝐾) = (𝐺‘𝐾)) |
36 | 28, 35 | eqtr4d 2229 |
. . . . 5
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝐾( + , 𝐺)‘𝐾)) |
37 | 36 | a1d 22 |
. . . 4
⊢ (𝜑 → (𝐾 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝐾( + , 𝐺)‘𝐾))) |
38 | | peano2fzr 10093 |
. . . . . . . 8
⊢ ((𝑛 ∈
(ℤ≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁)) → 𝑛 ∈ (𝐾...𝑁)) |
39 | 38 | adantl 277 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → 𝑛 ∈ (𝐾...𝑁)) |
40 | 39 | expr 375 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝐾)) → ((𝑛 + 1) ∈ (𝐾...𝑁) → 𝑛 ∈ (𝐾...𝑁))) |
41 | 40 | imim1d 75 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝐾)) → ((𝑛 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝑛) = (seq𝐾( + , 𝐺)‘𝑛)) → ((𝑛 + 1) ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝑛) = (seq𝐾( + , 𝐺)‘𝑛)))) |
42 | | oveq1 5917 |
. . . . . 6
⊢
((seq𝑀( + , 𝐹)‘𝑛) = (seq𝐾( + , 𝐺)‘𝑛) → ((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1))) = ((seq𝐾( + , 𝐺)‘𝑛) + (𝐹‘(𝑛 + 1)))) |
43 | | simpl 109 |
. . . . . . . . 9
⊢ ((𝑛 ∈
(ℤ≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁)) → 𝑛 ∈ (ℤ≥‘𝐾)) |
44 | | uztrn 9599 |
. . . . . . . . 9
⊢ ((𝑛 ∈
(ℤ≥‘𝐾) ∧ 𝐾 ∈ (ℤ≥‘𝑀)) → 𝑛 ∈ (ℤ≥‘𝑀)) |
45 | 43, 29, 44 | syl2anr 290 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → 𝑛 ∈ (ℤ≥‘𝑀)) |
46 | | seqfveq2g.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ 𝑊) |
47 | 46 | adantr 276 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → 𝐹 ∈ 𝑊) |
48 | 33 | adantr 276 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → + ∈ 𝑉) |
49 | | seqp1g 10527 |
. . . . . . . 8
⊢ ((𝑛 ∈
(ℤ≥‘𝑀) ∧ 𝐹 ∈ 𝑊 ∧ + ∈ 𝑉) → (seq𝑀( + , 𝐹)‘(𝑛 + 1)) = ((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1)))) |
50 | 45, 47, 48, 49 | syl3anc 1249 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → (seq𝑀( + , 𝐹)‘(𝑛 + 1)) = ((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1)))) |
51 | 43 | adantl 277 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → 𝑛 ∈ (ℤ≥‘𝐾)) |
52 | 32 | adantr 276 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → 𝐺 ∈ 𝑋) |
53 | | seqp1g 10527 |
. . . . . . . . 9
⊢ ((𝑛 ∈
(ℤ≥‘𝐾) ∧ 𝐺 ∈ 𝑋 ∧ + ∈ 𝑉) → (seq𝐾( + , 𝐺)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐺)‘𝑛) + (𝐺‘(𝑛 + 1)))) |
54 | 51, 52, 48, 53 | syl3anc 1249 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → (seq𝐾( + , 𝐺)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐺)‘𝑛) + (𝐺‘(𝑛 + 1)))) |
55 | | fveq2 5546 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝑛 + 1) → (𝐹‘𝑘) = (𝐹‘(𝑛 + 1))) |
56 | | fveq2 5546 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝑛 + 1) → (𝐺‘𝑘) = (𝐺‘(𝑛 + 1))) |
57 | 55, 56 | eqeq12d 2208 |
. . . . . . . . . 10
⊢ (𝑘 = (𝑛 + 1) → ((𝐹‘𝑘) = (𝐺‘𝑘) ↔ (𝐹‘(𝑛 + 1)) = (𝐺‘(𝑛 + 1)))) |
58 | | seqfveq2.4 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝐹‘𝑘) = (𝐺‘𝑘)) |
59 | 58 | ralrimiva 2567 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑘 ∈ ((𝐾 + 1)...𝑁)(𝐹‘𝑘) = (𝐺‘𝑘)) |
60 | 59 | adantr 276 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → ∀𝑘 ∈ ((𝐾 + 1)...𝑁)(𝐹‘𝑘) = (𝐺‘𝑘)) |
61 | | eluzp1p1 9608 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈
(ℤ≥‘𝐾) → (𝑛 + 1) ∈
(ℤ≥‘(𝐾 + 1))) |
62 | 61 | ad2antrl 490 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → (𝑛 + 1) ∈
(ℤ≥‘(𝐾 + 1))) |
63 | | elfzuz3 10078 |
. . . . . . . . . . . 12
⊢ ((𝑛 + 1) ∈ (𝐾...𝑁) → 𝑁 ∈ (ℤ≥‘(𝑛 + 1))) |
64 | 63 | ad2antll 491 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → 𝑁 ∈ (ℤ≥‘(𝑛 + 1))) |
65 | | elfzuzb 10075 |
. . . . . . . . . . 11
⊢ ((𝑛 + 1) ∈ ((𝐾 + 1)...𝑁) ↔ ((𝑛 + 1) ∈
(ℤ≥‘(𝐾 + 1)) ∧ 𝑁 ∈ (ℤ≥‘(𝑛 + 1)))) |
66 | 62, 64, 65 | sylanbrc 417 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → (𝑛 + 1) ∈ ((𝐾 + 1)...𝑁)) |
67 | 57, 60, 66 | rspcdva 2869 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → (𝐹‘(𝑛 + 1)) = (𝐺‘(𝑛 + 1))) |
68 | 67 | oveq2d 5926 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → ((seq𝐾( + , 𝐺)‘𝑛) + (𝐹‘(𝑛 + 1))) = ((seq𝐾( + , 𝐺)‘𝑛) + (𝐺‘(𝑛 + 1)))) |
69 | 54, 68 | eqtr4d 2229 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → (seq𝐾( + , 𝐺)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐺)‘𝑛) + (𝐹‘(𝑛 + 1)))) |
70 | 50, 69 | eqeq12d 2208 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → ((seq𝑀( + , 𝐹)‘(𝑛 + 1)) = (seq𝐾( + , 𝐺)‘(𝑛 + 1)) ↔ ((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1))) = ((seq𝐾( + , 𝐺)‘𝑛) + (𝐹‘(𝑛 + 1))))) |
71 | 42, 70 | imbitrrid 156 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → ((seq𝑀( + , 𝐹)‘𝑛) = (seq𝐾( + , 𝐺)‘𝑛) → (seq𝑀( + , 𝐹)‘(𝑛 + 1)) = (seq𝐾( + , 𝐺)‘(𝑛 + 1)))) |
72 | 41, 71 | animpimp2impd 559 |
. . . 4
⊢ (𝑛 ∈
(ℤ≥‘𝐾) → ((𝜑 → (𝑛 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝑛) = (seq𝐾( + , 𝐺)‘𝑛))) → (𝜑 → ((𝑛 + 1) ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘(𝑛 + 1)) = (seq𝐾( + , 𝐺)‘(𝑛 + 1)))))) |
73 | 9, 15, 21, 27, 37, 72 | uzind4i 9647 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝐾) → (𝜑 → (𝑁 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝑁) = (seq𝐾( + , 𝐺)‘𝑁)))) |
74 | 1, 73 | mpcom 36 |
. 2
⊢ (𝜑 → (𝑁 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝑁) = (seq𝐾( + , 𝐺)‘𝑁))) |
75 | 3, 74 | mpd 13 |
1
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = (seq𝐾( + , 𝐺)‘𝑁)) |