| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | seqshft2.1 | . . 3
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) | 
| 2 |  | eluzfz2 13573 | . . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁)) | 
| 3 | 1, 2 | syl 17 | . 2
⊢ (𝜑 → 𝑁 ∈ (𝑀...𝑁)) | 
| 4 |  | eleq1 2828 | . . . . . 6
⊢ (𝑥 = 𝑀 → (𝑥 ∈ (𝑀...𝑁) ↔ 𝑀 ∈ (𝑀...𝑁))) | 
| 5 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑥 = 𝑀 → (seq𝑀( + , 𝐹)‘𝑥) = (seq𝑀( + , 𝐹)‘𝑀)) | 
| 6 |  | fvoveq1 7455 | . . . . . . 7
⊢ (𝑥 = 𝑀 → (seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑥 + 𝐾)) = (seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑀 + 𝐾))) | 
| 7 | 5, 6 | eqeq12d 2752 | . . . . . 6
⊢ (𝑥 = 𝑀 → ((seq𝑀( + , 𝐹)‘𝑥) = (seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑥 + 𝐾)) ↔ (seq𝑀( + , 𝐹)‘𝑀) = (seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑀 + 𝐾)))) | 
| 8 | 4, 7 | imbi12d 344 | . . . . 5
⊢ (𝑥 = 𝑀 → ((𝑥 ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹)‘𝑥) = (seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑥 + 𝐾))) ↔ (𝑀 ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹)‘𝑀) = (seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑀 + 𝐾))))) | 
| 9 | 8 | imbi2d 340 | . . . 4
⊢ (𝑥 = 𝑀 → ((𝜑 → (𝑥 ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹)‘𝑥) = (seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑥 + 𝐾)))) ↔ (𝜑 → (𝑀 ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹)‘𝑀) = (seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑀 + 𝐾)))))) | 
| 10 |  | eleq1 2828 | . . . . . 6
⊢ (𝑥 = 𝑛 → (𝑥 ∈ (𝑀...𝑁) ↔ 𝑛 ∈ (𝑀...𝑁))) | 
| 11 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑥 = 𝑛 → (seq𝑀( + , 𝐹)‘𝑥) = (seq𝑀( + , 𝐹)‘𝑛)) | 
| 12 |  | fvoveq1 7455 | . . . . . . 7
⊢ (𝑥 = 𝑛 → (seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑥 + 𝐾)) = (seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑛 + 𝐾))) | 
| 13 | 11, 12 | eqeq12d 2752 | . . . . . 6
⊢ (𝑥 = 𝑛 → ((seq𝑀( + , 𝐹)‘𝑥) = (seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑥 + 𝐾)) ↔ (seq𝑀( + , 𝐹)‘𝑛) = (seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑛 + 𝐾)))) | 
| 14 | 10, 13 | imbi12d 344 | . . . . 5
⊢ (𝑥 = 𝑛 → ((𝑥 ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹)‘𝑥) = (seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑥 + 𝐾))) ↔ (𝑛 ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹)‘𝑛) = (seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑛 + 𝐾))))) | 
| 15 | 14 | imbi2d 340 | . . . 4
⊢ (𝑥 = 𝑛 → ((𝜑 → (𝑥 ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹)‘𝑥) = (seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑥 + 𝐾)))) ↔ (𝜑 → (𝑛 ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹)‘𝑛) = (seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑛 + 𝐾)))))) | 
| 16 |  | eleq1 2828 | . . . . . 6
⊢ (𝑥 = (𝑛 + 1) → (𝑥 ∈ (𝑀...𝑁) ↔ (𝑛 + 1) ∈ (𝑀...𝑁))) | 
| 17 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑥 = (𝑛 + 1) → (seq𝑀( + , 𝐹)‘𝑥) = (seq𝑀( + , 𝐹)‘(𝑛 + 1))) | 
| 18 |  | fvoveq1 7455 | . . . . . . 7
⊢ (𝑥 = (𝑛 + 1) → (seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑥 + 𝐾)) = (seq(𝑀 + 𝐾)( + , 𝐺)‘((𝑛 + 1) + 𝐾))) | 
| 19 | 17, 18 | eqeq12d 2752 | . . . . . 6
⊢ (𝑥 = (𝑛 + 1) → ((seq𝑀( + , 𝐹)‘𝑥) = (seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑥 + 𝐾)) ↔ (seq𝑀( + , 𝐹)‘(𝑛 + 1)) = (seq(𝑀 + 𝐾)( + , 𝐺)‘((𝑛 + 1) + 𝐾)))) | 
| 20 | 16, 19 | imbi12d 344 | . . . . 5
⊢ (𝑥 = (𝑛 + 1) → ((𝑥 ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹)‘𝑥) = (seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑥 + 𝐾))) ↔ ((𝑛 + 1) ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹)‘(𝑛 + 1)) = (seq(𝑀 + 𝐾)( + , 𝐺)‘((𝑛 + 1) + 𝐾))))) | 
| 21 | 20 | imbi2d 340 | . . . 4
⊢ (𝑥 = (𝑛 + 1) → ((𝜑 → (𝑥 ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹)‘𝑥) = (seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑥 + 𝐾)))) ↔ (𝜑 → ((𝑛 + 1) ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹)‘(𝑛 + 1)) = (seq(𝑀 + 𝐾)( + , 𝐺)‘((𝑛 + 1) + 𝐾)))))) | 
| 22 |  | eleq1 2828 | . . . . . 6
⊢ (𝑥 = 𝑁 → (𝑥 ∈ (𝑀...𝑁) ↔ 𝑁 ∈ (𝑀...𝑁))) | 
| 23 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑥 = 𝑁 → (seq𝑀( + , 𝐹)‘𝑥) = (seq𝑀( + , 𝐹)‘𝑁)) | 
| 24 |  | fvoveq1 7455 | . . . . . . 7
⊢ (𝑥 = 𝑁 → (seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑥 + 𝐾)) = (seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑁 + 𝐾))) | 
| 25 | 23, 24 | eqeq12d 2752 | . . . . . 6
⊢ (𝑥 = 𝑁 → ((seq𝑀( + , 𝐹)‘𝑥) = (seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑥 + 𝐾)) ↔ (seq𝑀( + , 𝐹)‘𝑁) = (seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑁 + 𝐾)))) | 
| 26 | 22, 25 | imbi12d 344 | . . . . 5
⊢ (𝑥 = 𝑁 → ((𝑥 ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹)‘𝑥) = (seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑥 + 𝐾))) ↔ (𝑁 ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹)‘𝑁) = (seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑁 + 𝐾))))) | 
| 27 | 26 | imbi2d 340 | . . . 4
⊢ (𝑥 = 𝑁 → ((𝜑 → (𝑥 ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹)‘𝑥) = (seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑥 + 𝐾)))) ↔ (𝜑 → (𝑁 ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹)‘𝑁) = (seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑁 + 𝐾)))))) | 
| 28 |  | fveq2 6905 | . . . . . . . 8
⊢ (𝑘 = 𝑀 → (𝐹‘𝑘) = (𝐹‘𝑀)) | 
| 29 |  | fvoveq1 7455 | . . . . . . . 8
⊢ (𝑘 = 𝑀 → (𝐺‘(𝑘 + 𝐾)) = (𝐺‘(𝑀 + 𝐾))) | 
| 30 | 28, 29 | eqeq12d 2752 | . . . . . . 7
⊢ (𝑘 = 𝑀 → ((𝐹‘𝑘) = (𝐺‘(𝑘 + 𝐾)) ↔ (𝐹‘𝑀) = (𝐺‘(𝑀 + 𝐾)))) | 
| 31 |  | seqshft2.3 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) = (𝐺‘(𝑘 + 𝐾))) | 
| 32 | 31 | ralrimiva 3145 | . . . . . . 7
⊢ (𝜑 → ∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) = (𝐺‘(𝑘 + 𝐾))) | 
| 33 |  | eluzfz1 13572 | . . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁)) | 
| 34 | 1, 33 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝑀 ∈ (𝑀...𝑁)) | 
| 35 | 30, 32, 34 | rspcdva 3622 | . . . . . 6
⊢ (𝜑 → (𝐹‘𝑀) = (𝐺‘(𝑀 + 𝐾))) | 
| 36 |  | eluzel2 12884 | . . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) | 
| 37 | 1, 36 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 38 |  | seq1 14056 | . . . . . . 7
⊢ (𝑀 ∈ ℤ → (seq𝑀( + , 𝐹)‘𝑀) = (𝐹‘𝑀)) | 
| 39 | 37, 38 | syl 17 | . . . . . 6
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑀) = (𝐹‘𝑀)) | 
| 40 |  | seqshft2.2 | . . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ ℤ) | 
| 41 | 37, 40 | zaddcld 12728 | . . . . . . 7
⊢ (𝜑 → (𝑀 + 𝐾) ∈ ℤ) | 
| 42 |  | seq1 14056 | . . . . . . 7
⊢ ((𝑀 + 𝐾) ∈ ℤ → (seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑀 + 𝐾)) = (𝐺‘(𝑀 + 𝐾))) | 
| 43 | 41, 42 | syl 17 | . . . . . 6
⊢ (𝜑 → (seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑀 + 𝐾)) = (𝐺‘(𝑀 + 𝐾))) | 
| 44 | 35, 39, 43 | 3eqtr4d 2786 | . . . . 5
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑀) = (seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑀 + 𝐾))) | 
| 45 | 44 | a1i13 27 | . . . 4
⊢ (𝑀 ∈ ℤ → (𝜑 → (𝑀 ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹)‘𝑀) = (seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑀 + 𝐾))))) | 
| 46 |  | peano2fzr 13578 | . . . . . . . 8
⊢ ((𝑛 ∈
(ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → 𝑛 ∈ (𝑀...𝑁)) | 
| 47 | 46 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → 𝑛 ∈ (𝑀...𝑁)) | 
| 48 | 47 | expr 456 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → ((𝑛 + 1) ∈ (𝑀...𝑁) → 𝑛 ∈ (𝑀...𝑁))) | 
| 49 | 48 | imim1d 82 | . . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → ((𝑛 ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹)‘𝑛) = (seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑛 + 𝐾))) → ((𝑛 + 1) ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹)‘𝑛) = (seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑛 + 𝐾))))) | 
| 50 |  | oveq1 7439 | . . . . . 6
⊢
((seq𝑀( + , 𝐹)‘𝑛) = (seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑛 + 𝐾)) → ((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1))) = ((seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑛 + 𝐾)) + (𝐹‘(𝑛 + 1)))) | 
| 51 |  | simprl 770 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → 𝑛 ∈ (ℤ≥‘𝑀)) | 
| 52 |  | seqp1 14058 | . . . . . . . 8
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → (seq𝑀( + , 𝐹)‘(𝑛 + 1)) = ((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1)))) | 
| 53 | 51, 52 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (seq𝑀( + , 𝐹)‘(𝑛 + 1)) = ((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1)))) | 
| 54 | 40 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → 𝐾 ∈ ℤ) | 
| 55 |  | eluzadd 12908 | . . . . . . . . . 10
⊢ ((𝑛 ∈
(ℤ≥‘𝑀) ∧ 𝐾 ∈ ℤ) → (𝑛 + 𝐾) ∈
(ℤ≥‘(𝑀 + 𝐾))) | 
| 56 | 51, 54, 55 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (𝑛 + 𝐾) ∈
(ℤ≥‘(𝑀 + 𝐾))) | 
| 57 |  | seqp1 14058 | . . . . . . . . 9
⊢ ((𝑛 + 𝐾) ∈
(ℤ≥‘(𝑀 + 𝐾)) → (seq(𝑀 + 𝐾)( + , 𝐺)‘((𝑛 + 𝐾) + 1)) = ((seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑛 + 𝐾)) + (𝐺‘((𝑛 + 𝐾) + 1)))) | 
| 58 | 56, 57 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (seq(𝑀 + 𝐾)( + , 𝐺)‘((𝑛 + 𝐾) + 1)) = ((seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑛 + 𝐾)) + (𝐺‘((𝑛 + 𝐾) + 1)))) | 
| 59 |  | eluzelz 12889 | . . . . . . . . . . 11
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → 𝑛 ∈ ℤ) | 
| 60 | 51, 59 | syl 17 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → 𝑛 ∈ ℤ) | 
| 61 |  | zcn 12620 | . . . . . . . . . . 11
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℂ) | 
| 62 |  | zcn 12620 | . . . . . . . . . . 11
⊢ (𝐾 ∈ ℤ → 𝐾 ∈
ℂ) | 
| 63 |  | ax-1cn 11214 | . . . . . . . . . . . 12
⊢ 1 ∈
ℂ | 
| 64 |  | add32 11481 | . . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ ∧ 𝐾 ∈
ℂ) → ((𝑛 + 1) +
𝐾) = ((𝑛 + 𝐾) + 1)) | 
| 65 | 63, 64 | mp3an2 1450 | . . . . . . . . . . 11
⊢ ((𝑛 ∈ ℂ ∧ 𝐾 ∈ ℂ) → ((𝑛 + 1) + 𝐾) = ((𝑛 + 𝐾) + 1)) | 
| 66 | 61, 62, 65 | syl2an 596 | . . . . . . . . . 10
⊢ ((𝑛 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑛 + 1) + 𝐾) = ((𝑛 + 𝐾) + 1)) | 
| 67 | 60, 54, 66 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → ((𝑛 + 1) + 𝐾) = ((𝑛 + 𝐾) + 1)) | 
| 68 | 67 | fveq2d 6909 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (seq(𝑀 + 𝐾)( + , 𝐺)‘((𝑛 + 1) + 𝐾)) = (seq(𝑀 + 𝐾)( + , 𝐺)‘((𝑛 + 𝐾) + 1))) | 
| 69 |  | fveq2 6905 | . . . . . . . . . . . 12
⊢ (𝑘 = (𝑛 + 1) → (𝐹‘𝑘) = (𝐹‘(𝑛 + 1))) | 
| 70 |  | fvoveq1 7455 | . . . . . . . . . . . 12
⊢ (𝑘 = (𝑛 + 1) → (𝐺‘(𝑘 + 𝐾)) = (𝐺‘((𝑛 + 1) + 𝐾))) | 
| 71 | 69, 70 | eqeq12d 2752 | . . . . . . . . . . 11
⊢ (𝑘 = (𝑛 + 1) → ((𝐹‘𝑘) = (𝐺‘(𝑘 + 𝐾)) ↔ (𝐹‘(𝑛 + 1)) = (𝐺‘((𝑛 + 1) + 𝐾)))) | 
| 72 | 32 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → ∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) = (𝐺‘(𝑘 + 𝐾))) | 
| 73 |  | simprr 772 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (𝑛 + 1) ∈ (𝑀...𝑁)) | 
| 74 | 71, 72, 73 | rspcdva 3622 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (𝐹‘(𝑛 + 1)) = (𝐺‘((𝑛 + 1) + 𝐾))) | 
| 75 | 67 | fveq2d 6909 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (𝐺‘((𝑛 + 1) + 𝐾)) = (𝐺‘((𝑛 + 𝐾) + 1))) | 
| 76 | 74, 75 | eqtrd 2776 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (𝐹‘(𝑛 + 1)) = (𝐺‘((𝑛 + 𝐾) + 1))) | 
| 77 | 76 | oveq2d 7448 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → ((seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑛 + 𝐾)) + (𝐹‘(𝑛 + 1))) = ((seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑛 + 𝐾)) + (𝐺‘((𝑛 + 𝐾) + 1)))) | 
| 78 | 58, 68, 77 | 3eqtr4d 2786 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (seq(𝑀 + 𝐾)( + , 𝐺)‘((𝑛 + 1) + 𝐾)) = ((seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑛 + 𝐾)) + (𝐹‘(𝑛 + 1)))) | 
| 79 | 53, 78 | eqeq12d 2752 | . . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → ((seq𝑀( + , 𝐹)‘(𝑛 + 1)) = (seq(𝑀 + 𝐾)( + , 𝐺)‘((𝑛 + 1) + 𝐾)) ↔ ((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1))) = ((seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑛 + 𝐾)) + (𝐹‘(𝑛 + 1))))) | 
| 80 | 50, 79 | imbitrrid 246 | . . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → ((seq𝑀( + , 𝐹)‘𝑛) = (seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑛 + 𝐾)) → (seq𝑀( + , 𝐹)‘(𝑛 + 1)) = (seq(𝑀 + 𝐾)( + , 𝐺)‘((𝑛 + 1) + 𝐾)))) | 
| 81 | 49, 80 | animpimp2impd 846 | . . . 4
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → ((𝜑 → (𝑛 ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹)‘𝑛) = (seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑛 + 𝐾)))) → (𝜑 → ((𝑛 + 1) ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹)‘(𝑛 + 1)) = (seq(𝑀 + 𝐾)( + , 𝐺)‘((𝑛 + 1) + 𝐾)))))) | 
| 82 | 9, 15, 21, 27, 45, 81 | uzind4 12949 | . . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝜑 → (𝑁 ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹)‘𝑁) = (seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑁 + 𝐾))))) | 
| 83 | 1, 82 | mpcom 38 | . 2
⊢ (𝜑 → (𝑁 ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹)‘𝑁) = (seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑁 + 𝐾)))) | 
| 84 | 3, 83 | mpd 15 | 1
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = (seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑁 + 𝐾))) |