| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | seqsplit.3 | . . 3
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) | 
| 2 |  | eluzfz2 13573 | . . 3
⊢ (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) → 𝑁 ∈ ((𝑀 + 1)...𝑁)) | 
| 3 | 1, 2 | syl 17 | . 2
⊢ (𝜑 → 𝑁 ∈ ((𝑀 + 1)...𝑁)) | 
| 4 |  | eleq1 2828 | . . . . . 6
⊢ (𝑥 = (𝑀 + 1) → (𝑥 ∈ ((𝑀 + 1)...𝑁) ↔ (𝑀 + 1) ∈ ((𝑀 + 1)...𝑁))) | 
| 5 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑥 = (𝑀 + 1) → (seq𝐾( + , 𝐹)‘𝑥) = (seq𝐾( + , 𝐹)‘(𝑀 + 1))) | 
| 6 |  | fveq2 6905 | . . . . . . . 8
⊢ (𝑥 = (𝑀 + 1) → (seq(𝑀 + 1)( + , 𝐹)‘𝑥) = (seq(𝑀 + 1)( + , 𝐹)‘(𝑀 + 1))) | 
| 7 | 6 | oveq2d 7448 | . . . . . . 7
⊢ (𝑥 = (𝑀 + 1) → ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑀 + 1)))) | 
| 8 | 5, 7 | eqeq12d 2752 | . . . . . 6
⊢ (𝑥 = (𝑀 + 1) → ((seq𝐾( + , 𝐹)‘𝑥) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥)) ↔ (seq𝐾( + , 𝐹)‘(𝑀 + 1)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑀 + 1))))) | 
| 9 | 4, 8 | imbi12d 344 | . . . . 5
⊢ (𝑥 = (𝑀 + 1) → ((𝑥 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑥) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥))) ↔ ((𝑀 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘(𝑀 + 1)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑀 + 1)))))) | 
| 10 | 9 | imbi2d 340 | . . . 4
⊢ (𝑥 = (𝑀 + 1) → ((𝜑 → (𝑥 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑥) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥)))) ↔ (𝜑 → ((𝑀 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘(𝑀 + 1)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑀 + 1))))))) | 
| 11 |  | eleq1 2828 | . . . . . 6
⊢ (𝑥 = 𝑛 → (𝑥 ∈ ((𝑀 + 1)...𝑁) ↔ 𝑛 ∈ ((𝑀 + 1)...𝑁))) | 
| 12 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑥 = 𝑛 → (seq𝐾( + , 𝐹)‘𝑥) = (seq𝐾( + , 𝐹)‘𝑛)) | 
| 13 |  | fveq2 6905 | . . . . . . . 8
⊢ (𝑥 = 𝑛 → (seq(𝑀 + 1)( + , 𝐹)‘𝑥) = (seq(𝑀 + 1)( + , 𝐹)‘𝑛)) | 
| 14 | 13 | oveq2d 7448 | . . . . . . 7
⊢ (𝑥 = 𝑛 → ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑛))) | 
| 15 | 12, 14 | eqeq12d 2752 | . . . . . 6
⊢ (𝑥 = 𝑛 → ((seq𝐾( + , 𝐹)‘𝑥) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥)) ↔ (seq𝐾( + , 𝐹)‘𝑛) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑛)))) | 
| 16 | 11, 15 | imbi12d 344 | . . . . 5
⊢ (𝑥 = 𝑛 → ((𝑥 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑥) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥))) ↔ (𝑛 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑛) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑛))))) | 
| 17 | 16 | imbi2d 340 | . . . 4
⊢ (𝑥 = 𝑛 → ((𝜑 → (𝑥 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑥) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥)))) ↔ (𝜑 → (𝑛 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑛) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑛)))))) | 
| 18 |  | eleq1 2828 | . . . . . 6
⊢ (𝑥 = (𝑛 + 1) → (𝑥 ∈ ((𝑀 + 1)...𝑁) ↔ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) | 
| 19 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑥 = (𝑛 + 1) → (seq𝐾( + , 𝐹)‘𝑥) = (seq𝐾( + , 𝐹)‘(𝑛 + 1))) | 
| 20 |  | fveq2 6905 | . . . . . . . 8
⊢ (𝑥 = (𝑛 + 1) → (seq(𝑀 + 1)( + , 𝐹)‘𝑥) = (seq(𝑀 + 1)( + , 𝐹)‘(𝑛 + 1))) | 
| 21 | 20 | oveq2d 7448 | . . . . . . 7
⊢ (𝑥 = (𝑛 + 1) → ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑛 + 1)))) | 
| 22 | 19, 21 | eqeq12d 2752 | . . . . . 6
⊢ (𝑥 = (𝑛 + 1) → ((seq𝐾( + , 𝐹)‘𝑥) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥)) ↔ (seq𝐾( + , 𝐹)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑛 + 1))))) | 
| 23 | 18, 22 | imbi12d 344 | . . . . 5
⊢ (𝑥 = (𝑛 + 1) → ((𝑥 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑥) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥))) ↔ ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑛 + 1)))))) | 
| 24 | 23 | imbi2d 340 | . . . 4
⊢ (𝑥 = (𝑛 + 1) → ((𝜑 → (𝑥 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑥) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥)))) ↔ (𝜑 → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑛 + 1))))))) | 
| 25 |  | eleq1 2828 | . . . . . 6
⊢ (𝑥 = 𝑁 → (𝑥 ∈ ((𝑀 + 1)...𝑁) ↔ 𝑁 ∈ ((𝑀 + 1)...𝑁))) | 
| 26 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑥 = 𝑁 → (seq𝐾( + , 𝐹)‘𝑥) = (seq𝐾( + , 𝐹)‘𝑁)) | 
| 27 |  | fveq2 6905 | . . . . . . . 8
⊢ (𝑥 = 𝑁 → (seq(𝑀 + 1)( + , 𝐹)‘𝑥) = (seq(𝑀 + 1)( + , 𝐹)‘𝑁)) | 
| 28 | 27 | oveq2d 7448 | . . . . . . 7
⊢ (𝑥 = 𝑁 → ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑁))) | 
| 29 | 26, 28 | eqeq12d 2752 | . . . . . 6
⊢ (𝑥 = 𝑁 → ((seq𝐾( + , 𝐹)‘𝑥) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥)) ↔ (seq𝐾( + , 𝐹)‘𝑁) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑁)))) | 
| 30 | 25, 29 | imbi12d 344 | . . . . 5
⊢ (𝑥 = 𝑁 → ((𝑥 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑥) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥))) ↔ (𝑁 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑁) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑁))))) | 
| 31 | 30 | imbi2d 340 | . . . 4
⊢ (𝑥 = 𝑁 → ((𝜑 → (𝑥 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑥) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥)))) ↔ (𝜑 → (𝑁 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑁) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑁)))))) | 
| 32 |  | seqsplit.4 | . . . . . . 7
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝐾)) | 
| 33 |  | seqp1 14058 | . . . . . . 7
⊢ (𝑀 ∈
(ℤ≥‘𝐾) → (seq𝐾( + , 𝐹)‘(𝑀 + 1)) = ((seq𝐾( + , 𝐹)‘𝑀) + (𝐹‘(𝑀 + 1)))) | 
| 34 | 32, 33 | syl 17 | . . . . . 6
⊢ (𝜑 → (seq𝐾( + , 𝐹)‘(𝑀 + 1)) = ((seq𝐾( + , 𝐹)‘𝑀) + (𝐹‘(𝑀 + 1)))) | 
| 35 |  | eluzel2 12884 | . . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) → (𝑀 + 1) ∈ ℤ) | 
| 36 |  | seq1 14056 | . . . . . . . 8
⊢ ((𝑀 + 1) ∈ ℤ →
(seq(𝑀 + 1)( + , 𝐹)‘(𝑀 + 1)) = (𝐹‘(𝑀 + 1))) | 
| 37 | 1, 35, 36 | 3syl 18 | . . . . . . 7
⊢ (𝜑 → (seq(𝑀 + 1)( + , 𝐹)‘(𝑀 + 1)) = (𝐹‘(𝑀 + 1))) | 
| 38 | 37 | oveq2d 7448 | . . . . . 6
⊢ (𝜑 → ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑀 + 1))) = ((seq𝐾( + , 𝐹)‘𝑀) + (𝐹‘(𝑀 + 1)))) | 
| 39 | 34, 38 | eqtr4d 2779 | . . . . 5
⊢ (𝜑 → (seq𝐾( + , 𝐹)‘(𝑀 + 1)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑀 + 1)))) | 
| 40 | 39 | a1i13 27 | . . . 4
⊢ ((𝑀 + 1) ∈ ℤ →
(𝜑 → ((𝑀 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘(𝑀 + 1)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑀 + 1)))))) | 
| 41 |  | peano2fzr 13578 | . . . . . . . 8
⊢ ((𝑛 ∈
(ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁)) → 𝑛 ∈ ((𝑀 + 1)...𝑁)) | 
| 42 | 41 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → 𝑛 ∈ ((𝑀 + 1)...𝑁)) | 
| 43 | 42 | expr 456 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → 𝑛 ∈ ((𝑀 + 1)...𝑁))) | 
| 44 | 43 | imim1d 82 | . . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝑛 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑛) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑛))) → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑛) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑛))))) | 
| 45 |  | oveq1 7439 | . . . . . 6
⊢
((seq𝐾( + , 𝐹)‘𝑛) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑛)) → ((seq𝐾( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1))) = (((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑛)) + (𝐹‘(𝑛 + 1)))) | 
| 46 |  | simprl 770 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → 𝑛 ∈ (ℤ≥‘(𝑀 + 1))) | 
| 47 |  | peano2uz 12944 | . . . . . . . . . . 11
⊢ (𝑀 ∈
(ℤ≥‘𝐾) → (𝑀 + 1) ∈
(ℤ≥‘𝐾)) | 
| 48 | 32, 47 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (𝑀 + 1) ∈
(ℤ≥‘𝐾)) | 
| 49 | 48 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (𝑀 + 1) ∈
(ℤ≥‘𝐾)) | 
| 50 |  | uztrn 12897 | . . . . . . . . 9
⊢ ((𝑛 ∈
(ℤ≥‘(𝑀 + 1)) ∧ (𝑀 + 1) ∈
(ℤ≥‘𝐾)) → 𝑛 ∈ (ℤ≥‘𝐾)) | 
| 51 | 46, 49, 50 | syl2anc 584 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → 𝑛 ∈ (ℤ≥‘𝐾)) | 
| 52 |  | seqp1 14058 | . . . . . . . 8
⊢ (𝑛 ∈
(ℤ≥‘𝐾) → (seq𝐾( + , 𝐹)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1)))) | 
| 53 | 51, 52 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (seq𝐾( + , 𝐹)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1)))) | 
| 54 |  | seqp1 14058 | . . . . . . . . . 10
⊢ (𝑛 ∈
(ℤ≥‘(𝑀 + 1)) → (seq(𝑀 + 1)( + , 𝐹)‘(𝑛 + 1)) = ((seq(𝑀 + 1)( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1)))) | 
| 55 | 46, 54 | syl 17 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (seq(𝑀 + 1)( + , 𝐹)‘(𝑛 + 1)) = ((seq(𝑀 + 1)( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1)))) | 
| 56 | 55 | oveq2d 7448 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑛 + 1))) = ((seq𝐾( + , 𝐹)‘𝑀) + ((seq(𝑀 + 1)( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1))))) | 
| 57 |  | simpl 482 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → 𝜑) | 
| 58 |  | eluzelz 12889 | . . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈
(ℤ≥‘𝐾) → 𝑀 ∈ ℤ) | 
| 59 | 32, 58 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 60 |  | peano2uzr 12946 | . . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → 𝑁 ∈ (ℤ≥‘𝑀)) | 
| 61 | 59, 1, 60 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) | 
| 62 |  | fzss2 13605 | . . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝐾...𝑀) ⊆ (𝐾...𝑁)) | 
| 63 | 61, 62 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐾...𝑀) ⊆ (𝐾...𝑁)) | 
| 64 | 63 | sselda 3982 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑀)) → 𝑥 ∈ (𝐾...𝑁)) | 
| 65 |  | seqsplit.5 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑁)) → (𝐹‘𝑥) ∈ 𝑆) | 
| 66 | 64, 65 | syldan 591 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑀)) → (𝐹‘𝑥) ∈ 𝑆) | 
| 67 |  | seqsplit.1 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) | 
| 68 | 32, 66, 67 | seqcl 14064 | . . . . . . . . . 10
⊢ (𝜑 → (seq𝐾( + , 𝐹)‘𝑀) ∈ 𝑆) | 
| 69 | 68 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (seq𝐾( + , 𝐹)‘𝑀) ∈ 𝑆) | 
| 70 |  | elfzuz3 13562 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ((𝑀 + 1)...𝑁) → 𝑁 ∈ (ℤ≥‘𝑛)) | 
| 71 |  | fzss2 13605 | . . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘𝑛) → ((𝑀 + 1)...𝑛) ⊆ ((𝑀 + 1)...𝑁)) | 
| 72 | 42, 70, 71 | 3syl 18 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → ((𝑀 + 1)...𝑛) ⊆ ((𝑀 + 1)...𝑁)) | 
| 73 |  | fzss1 13604 | . . . . . . . . . . . . . . 15
⊢ ((𝑀 + 1) ∈
(ℤ≥‘𝐾) → ((𝑀 + 1)...𝑁) ⊆ (𝐾...𝑁)) | 
| 74 | 32, 47, 73 | 3syl 18 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑀 + 1)...𝑁) ⊆ (𝐾...𝑁)) | 
| 75 | 74 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → ((𝑀 + 1)...𝑁) ⊆ (𝐾...𝑁)) | 
| 76 | 72, 75 | sstrd 3993 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → ((𝑀 + 1)...𝑛) ⊆ (𝐾...𝑁)) | 
| 77 | 76 | sselda 3982 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) ∧ 𝑥 ∈ ((𝑀 + 1)...𝑛)) → 𝑥 ∈ (𝐾...𝑁)) | 
| 78 | 65 | adantlr 715 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) ∧ 𝑥 ∈ (𝐾...𝑁)) → (𝐹‘𝑥) ∈ 𝑆) | 
| 79 | 77, 78 | syldan 591 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) ∧ 𝑥 ∈ ((𝑀 + 1)...𝑛)) → (𝐹‘𝑥) ∈ 𝑆) | 
| 80 | 67 | adantlr 715 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) | 
| 81 | 46, 79, 80 | seqcl 14064 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (seq(𝑀 + 1)( + , 𝐹)‘𝑛) ∈ 𝑆) | 
| 82 |  | fveq2 6905 | . . . . . . . . . . 11
⊢ (𝑥 = (𝑛 + 1) → (𝐹‘𝑥) = (𝐹‘(𝑛 + 1))) | 
| 83 | 82 | eleq1d 2825 | . . . . . . . . . 10
⊢ (𝑥 = (𝑛 + 1) → ((𝐹‘𝑥) ∈ 𝑆 ↔ (𝐹‘(𝑛 + 1)) ∈ 𝑆)) | 
| 84 | 65 | ralrimiva 3145 | . . . . . . . . . . 11
⊢ (𝜑 → ∀𝑥 ∈ (𝐾...𝑁)(𝐹‘𝑥) ∈ 𝑆) | 
| 85 | 84 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → ∀𝑥 ∈ (𝐾...𝑁)(𝐹‘𝑥) ∈ 𝑆) | 
| 86 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((𝑛 ∈
(ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁)) → (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁)) | 
| 87 |  | ssel2 3977 | . . . . . . . . . . 11
⊢ ((((𝑀 + 1)...𝑁) ⊆ (𝐾...𝑁) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁)) → (𝑛 + 1) ∈ (𝐾...𝑁)) | 
| 88 | 74, 86, 87 | syl2an 596 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (𝑛 + 1) ∈ (𝐾...𝑁)) | 
| 89 | 83, 85, 88 | rspcdva 3622 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (𝐹‘(𝑛 + 1)) ∈ 𝑆) | 
| 90 |  | seqsplit.2 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) | 
| 91 | 90 | caovassg 7632 | . . . . . . . . 9
⊢ ((𝜑 ∧ ((seq𝐾( + , 𝐹)‘𝑀) ∈ 𝑆 ∧ (seq(𝑀 + 1)( + , 𝐹)‘𝑛) ∈ 𝑆 ∧ (𝐹‘(𝑛 + 1)) ∈ 𝑆)) → (((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑛)) + (𝐹‘(𝑛 + 1))) = ((seq𝐾( + , 𝐹)‘𝑀) + ((seq(𝑀 + 1)( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1))))) | 
| 92 | 57, 69, 81, 89, 91 | syl13anc 1373 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑛)) + (𝐹‘(𝑛 + 1))) = ((seq𝐾( + , 𝐹)‘𝑀) + ((seq(𝑀 + 1)( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1))))) | 
| 93 | 56, 92 | eqtr4d 2779 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑛 + 1))) = (((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑛)) + (𝐹‘(𝑛 + 1)))) | 
| 94 | 53, 93 | eqeq12d 2752 | . . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → ((seq𝐾( + , 𝐹)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑛 + 1))) ↔ ((seq𝐾( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1))) = (((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑛)) + (𝐹‘(𝑛 + 1))))) | 
| 95 | 45, 94 | imbitrrid 246 | . . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → ((seq𝐾( + , 𝐹)‘𝑛) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑛)) → (seq𝐾( + , 𝐹)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑛 + 1))))) | 
| 96 | 44, 95 | animpimp2impd 846 | . . . 4
⊢ (𝑛 ∈
(ℤ≥‘(𝑀 + 1)) → ((𝜑 → (𝑛 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑛) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑛)))) → (𝜑 → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑛 + 1))))))) | 
| 97 | 10, 17, 24, 31, 40, 96 | uzind4 12949 | . . 3
⊢ (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) → (𝜑 → (𝑁 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑁) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑁))))) | 
| 98 | 1, 97 | mpcom 38 | . 2
⊢ (𝜑 → (𝑁 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑁) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑁)))) | 
| 99 | 3, 98 | mpd 15 | 1
⊢ (𝜑 → (seq𝐾( + , 𝐹)‘𝑁) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑁))) |