Step | Hyp | Ref
| Expression |
1 | | iseqsplit.3 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) |
2 | | eluzfz2 9051 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) → 𝑁 ∈ ((𝑀 + 1)...𝑁)) |
3 | 1, 2 | syl 14 |
. 2
⊢ (𝜑 → 𝑁 ∈ ((𝑀 + 1)...𝑁)) |
4 | | eleq1 2141 |
. . . . . 6
⊢ (𝑥 = (𝑀 + 1) → (𝑥 ∈ ((𝑀 + 1)...𝑁) ↔ (𝑀 + 1) ∈ ((𝑀 + 1)...𝑁))) |
5 | | fveq2 5198 |
. . . . . . 7
⊢ (𝑥 = (𝑀 + 1) → (seq𝐾( + , 𝐹, 𝑆)‘𝑥) = (seq𝐾( + , 𝐹, 𝑆)‘(𝑀 + 1))) |
6 | | fveq2 5198 |
. . . . . . . 8
⊢ (𝑥 = (𝑀 + 1) → (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑥) = (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑀 + 1))) |
7 | 6 | oveq2d 5548 |
. . . . . . 7
⊢ (𝑥 = (𝑀 + 1) → ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑥)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑀 + 1)))) |
8 | 5, 7 | eqeq12d 2095 |
. . . . . 6
⊢ (𝑥 = (𝑀 + 1) → ((seq𝐾( + , 𝐹, 𝑆)‘𝑥) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑥)) ↔ (seq𝐾( + , 𝐹, 𝑆)‘(𝑀 + 1)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑀 + 1))))) |
9 | 4, 8 | imbi12d 232 |
. . . . 5
⊢ (𝑥 = (𝑀 + 1) → ((𝑥 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘𝑥) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑥))) ↔ ((𝑀 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘(𝑀 + 1)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑀 + 1)))))) |
10 | 9 | imbi2d 228 |
. . . 4
⊢ (𝑥 = (𝑀 + 1) → ((𝜑 → (𝑥 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘𝑥) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑥)))) ↔ (𝜑 → ((𝑀 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘(𝑀 + 1)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑀 + 1))))))) |
11 | | eleq1 2141 |
. . . . . 6
⊢ (𝑥 = 𝑛 → (𝑥 ∈ ((𝑀 + 1)...𝑁) ↔ 𝑛 ∈ ((𝑀 + 1)...𝑁))) |
12 | | fveq2 5198 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → (seq𝐾( + , 𝐹, 𝑆)‘𝑥) = (seq𝐾( + , 𝐹, 𝑆)‘𝑛)) |
13 | | fveq2 5198 |
. . . . . . . 8
⊢ (𝑥 = 𝑛 → (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑥) = (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛)) |
14 | 13 | oveq2d 5548 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑥)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛))) |
15 | 12, 14 | eqeq12d 2095 |
. . . . . 6
⊢ (𝑥 = 𝑛 → ((seq𝐾( + , 𝐹, 𝑆)‘𝑥) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑥)) ↔ (seq𝐾( + , 𝐹, 𝑆)‘𝑛) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛)))) |
16 | 11, 15 | imbi12d 232 |
. . . . 5
⊢ (𝑥 = 𝑛 → ((𝑥 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘𝑥) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑥))) ↔ (𝑛 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘𝑛) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛))))) |
17 | 16 | imbi2d 228 |
. . . 4
⊢ (𝑥 = 𝑛 → ((𝜑 → (𝑥 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘𝑥) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑥)))) ↔ (𝜑 → (𝑛 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘𝑛) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛)))))) |
18 | | eleq1 2141 |
. . . . . 6
⊢ (𝑥 = (𝑛 + 1) → (𝑥 ∈ ((𝑀 + 1)...𝑁) ↔ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) |
19 | | fveq2 5198 |
. . . . . . 7
⊢ (𝑥 = (𝑛 + 1) → (seq𝐾( + , 𝐹, 𝑆)‘𝑥) = (seq𝐾( + , 𝐹, 𝑆)‘(𝑛 + 1))) |
20 | | fveq2 5198 |
. . . . . . . 8
⊢ (𝑥 = (𝑛 + 1) → (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑥) = (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑛 + 1))) |
21 | 20 | oveq2d 5548 |
. . . . . . 7
⊢ (𝑥 = (𝑛 + 1) → ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑥)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑛 + 1)))) |
22 | 19, 21 | eqeq12d 2095 |
. . . . . 6
⊢ (𝑥 = (𝑛 + 1) → ((seq𝐾( + , 𝐹, 𝑆)‘𝑥) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑥)) ↔ (seq𝐾( + , 𝐹, 𝑆)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑛 + 1))))) |
23 | 18, 22 | imbi12d 232 |
. . . . 5
⊢ (𝑥 = (𝑛 + 1) → ((𝑥 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘𝑥) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑥))) ↔ ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑛 + 1)))))) |
24 | 23 | imbi2d 228 |
. . . 4
⊢ (𝑥 = (𝑛 + 1) → ((𝜑 → (𝑥 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘𝑥) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑥)))) ↔ (𝜑 → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑛 + 1))))))) |
25 | | eleq1 2141 |
. . . . . 6
⊢ (𝑥 = 𝑁 → (𝑥 ∈ ((𝑀 + 1)...𝑁) ↔ 𝑁 ∈ ((𝑀 + 1)...𝑁))) |
26 | | fveq2 5198 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → (seq𝐾( + , 𝐹, 𝑆)‘𝑥) = (seq𝐾( + , 𝐹, 𝑆)‘𝑁)) |
27 | | fveq2 5198 |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑥) = (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑁)) |
28 | 27 | oveq2d 5548 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑥)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑁))) |
29 | 26, 28 | eqeq12d 2095 |
. . . . . 6
⊢ (𝑥 = 𝑁 → ((seq𝐾( + , 𝐹, 𝑆)‘𝑥) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑥)) ↔ (seq𝐾( + , 𝐹, 𝑆)‘𝑁) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑁)))) |
30 | 25, 29 | imbi12d 232 |
. . . . 5
⊢ (𝑥 = 𝑁 → ((𝑥 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘𝑥) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑥))) ↔ (𝑁 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘𝑁) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑁))))) |
31 | 30 | imbi2d 228 |
. . . 4
⊢ (𝑥 = 𝑁 → ((𝜑 → (𝑥 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘𝑥) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑥)))) ↔ (𝜑 → (𝑁 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘𝑁) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑁)))))) |
32 | | iseqsplit.4 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝐾)) |
33 | | iseqsplit.s |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ 𝑉) |
34 | | iseqsplit.5 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝐾)) → (𝐹‘𝑥) ∈ 𝑆) |
35 | | iseqsplit.1 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
36 | 32, 33, 34, 35 | iseqp1 9445 |
. . . . . . 7
⊢ (𝜑 → (seq𝐾( + , 𝐹, 𝑆)‘(𝑀 + 1)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (𝐹‘(𝑀 + 1)))) |
37 | | eluzel2 8624 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) → (𝑀 + 1) ∈ ℤ) |
38 | 1, 37 | syl 14 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 + 1) ∈ ℤ) |
39 | | eluzelz 8628 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈
(ℤ≥‘𝐾) → 𝑀 ∈ ℤ) |
40 | 32, 39 | syl 14 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ ℤ) |
41 | | peano2uzr 8673 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ 𝑥 ∈
(ℤ≥‘(𝑀 + 1))) → 𝑥 ∈ (ℤ≥‘𝑀)) |
42 | 40, 41 | sylan 277 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑥 ∈
(ℤ≥‘𝑀)) |
43 | 32 | adantr 270 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑀 ∈ (ℤ≥‘𝐾)) |
44 | | uztrn 8635 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈
(ℤ≥‘𝑀) ∧ 𝑀 ∈ (ℤ≥‘𝐾)) → 𝑥 ∈ (ℤ≥‘𝐾)) |
45 | 42, 43, 44 | syl2anc 403 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑥 ∈
(ℤ≥‘𝐾)) |
46 | 45, 34 | syldan 276 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → (𝐹‘𝑥) ∈ 𝑆) |
47 | 38, 33, 46, 35 | iseq1 9442 |
. . . . . . . 8
⊢ (𝜑 → (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑀 + 1)) = (𝐹‘(𝑀 + 1))) |
48 | 47 | oveq2d 5548 |
. . . . . . 7
⊢ (𝜑 → ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑀 + 1))) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (𝐹‘(𝑀 + 1)))) |
49 | 36, 48 | eqtr4d 2116 |
. . . . . 6
⊢ (𝜑 → (seq𝐾( + , 𝐹, 𝑆)‘(𝑀 + 1)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑀 + 1)))) |
50 | 49 | a1d 22 |
. . . . 5
⊢ (𝜑 → ((𝑀 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘(𝑀 + 1)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑀 + 1))))) |
51 | 50 | a1i 9 |
. . . 4
⊢ ((𝑀 + 1) ∈ ℤ →
(𝜑 → ((𝑀 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘(𝑀 + 1)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑀 + 1)))))) |
52 | | peano2fzr 9056 |
. . . . . . . . . 10
⊢ ((𝑛 ∈
(ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁)) → 𝑛 ∈ ((𝑀 + 1)...𝑁)) |
53 | 52 | adantl 271 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → 𝑛 ∈ ((𝑀 + 1)...𝑁)) |
54 | 53 | expr 367 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → 𝑛 ∈ ((𝑀 + 1)...𝑁))) |
55 | 54 | imim1d 74 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝑛 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘𝑛) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛))) → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘𝑛) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛))))) |
56 | | oveq1 5539 |
. . . . . . . . . 10
⊢
((seq𝐾( + , 𝐹, 𝑆)‘𝑛) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛)) → ((seq𝐾( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1))) = (((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛)) + (𝐹‘(𝑛 + 1)))) |
57 | | simprl 497 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → 𝑛 ∈ (ℤ≥‘(𝑀 + 1))) |
58 | | peano2uz 8671 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈
(ℤ≥‘𝐾) → (𝑀 + 1) ∈
(ℤ≥‘𝐾)) |
59 | 32, 58 | syl 14 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀 + 1) ∈
(ℤ≥‘𝐾)) |
60 | 59 | adantr 270 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (𝑀 + 1) ∈
(ℤ≥‘𝐾)) |
61 | | uztrn 8635 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈
(ℤ≥‘(𝑀 + 1)) ∧ (𝑀 + 1) ∈
(ℤ≥‘𝐾)) → 𝑛 ∈ (ℤ≥‘𝐾)) |
62 | 57, 60, 61 | syl2anc 403 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → 𝑛 ∈ (ℤ≥‘𝐾)) |
63 | 33 | adantr 270 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → 𝑆 ∈ 𝑉) |
64 | 34 | adantlr 460 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) ∧ 𝑥 ∈ (ℤ≥‘𝐾)) → (𝐹‘𝑥) ∈ 𝑆) |
65 | 35 | adantlr 460 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
66 | 62, 63, 64, 65 | iseqp1 9445 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (seq𝐾( + , 𝐹, 𝑆)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1)))) |
67 | 46 | adantlr 460 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → (𝐹‘𝑥) ∈ 𝑆) |
68 | 57, 63, 67, 65 | iseqp1 9445 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑛 + 1)) = ((seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1)))) |
69 | 68 | oveq2d 5548 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑛 + 1))) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + ((seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1))))) |
70 | | simpl 107 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → 𝜑) |
71 | 32, 33, 34, 35 | iseqcl 9443 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (seq𝐾( + , 𝐹, 𝑆)‘𝑀) ∈ 𝑆) |
72 | 71 | adantr 270 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (seq𝐾( + , 𝐹, 𝑆)‘𝑀) ∈ 𝑆) |
73 | 57, 63, 67, 65 | iseqcl 9443 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛) ∈ 𝑆) |
74 | | fzss1 9081 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 + 1) ∈
(ℤ≥‘𝐾) → ((𝑀 + 1)...𝑁) ⊆ (𝐾...𝑁)) |
75 | 32, 58, 74 | 3syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑀 + 1)...𝑁) ⊆ (𝐾...𝑁)) |
76 | | simpr 108 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈
(ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁)) → (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁)) |
77 | | ssel2 2994 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑀 + 1)...𝑁) ⊆ (𝐾...𝑁) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁)) → (𝑛 + 1) ∈ (𝐾...𝑁)) |
78 | 75, 76, 77 | syl2an 283 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (𝑛 + 1) ∈ (𝐾...𝑁)) |
79 | | elfzuz 9041 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (𝐾...𝑁) → 𝑥 ∈ (ℤ≥‘𝐾)) |
80 | 79, 34 | sylan2 280 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑁)) → (𝐹‘𝑥) ∈ 𝑆) |
81 | 80 | ralrimiva 2434 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑥 ∈ (𝐾...𝑁)(𝐹‘𝑥) ∈ 𝑆) |
82 | 81 | adantr 270 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → ∀𝑥 ∈ (𝐾...𝑁)(𝐹‘𝑥) ∈ 𝑆) |
83 | | fveq2 5198 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝑛 + 1) → (𝐹‘𝑥) = (𝐹‘(𝑛 + 1))) |
84 | 83 | eleq1d 2147 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑛 + 1) → ((𝐹‘𝑥) ∈ 𝑆 ↔ (𝐹‘(𝑛 + 1)) ∈ 𝑆)) |
85 | 84 | rspcv 2697 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 + 1) ∈ (𝐾...𝑁) → (∀𝑥 ∈ (𝐾...𝑁)(𝐹‘𝑥) ∈ 𝑆 → (𝐹‘(𝑛 + 1)) ∈ 𝑆)) |
86 | 78, 82, 85 | sylc 61 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (𝐹‘(𝑛 + 1)) ∈ 𝑆) |
87 | | iseqsplit.2 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) |
88 | 87 | caovassg 5679 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) ∈ 𝑆 ∧ (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛) ∈ 𝑆 ∧ (𝐹‘(𝑛 + 1)) ∈ 𝑆)) → (((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛)) + (𝐹‘(𝑛 + 1))) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + ((seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1))))) |
89 | 70, 72, 73, 86, 88 | syl13anc 1171 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛)) + (𝐹‘(𝑛 + 1))) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + ((seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1))))) |
90 | 69, 89 | eqtr4d 2116 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑛 + 1))) = (((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛)) + (𝐹‘(𝑛 + 1)))) |
91 | 66, 90 | eqeq12d 2095 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → ((seq𝐾( + , 𝐹, 𝑆)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑛 + 1))) ↔ ((seq𝐾( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1))) = (((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛)) + (𝐹‘(𝑛 + 1))))) |
92 | 56, 91 | syl5ibr 154 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → ((seq𝐾( + , 𝐹, 𝑆)‘𝑛) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛)) → (seq𝐾( + , 𝐹, 𝑆)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑛 + 1))))) |
93 | 92 | expr 367 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → ((seq𝐾( + , 𝐹, 𝑆)‘𝑛) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛)) → (seq𝐾( + , 𝐹, 𝑆)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑛 + 1)))))) |
94 | 93 | a2d 26 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑀 + 1))) → (((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘𝑛) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛))) → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑛 + 1)))))) |
95 | 55, 94 | syld 44 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝑛 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘𝑛) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛))) → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑛 + 1)))))) |
96 | 95 | expcom 114 |
. . . . 5
⊢ (𝑛 ∈
(ℤ≥‘(𝑀 + 1)) → (𝜑 → ((𝑛 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘𝑛) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛))) → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑛 + 1))))))) |
97 | 96 | a2d 26 |
. . . 4
⊢ (𝑛 ∈
(ℤ≥‘(𝑀 + 1)) → ((𝜑 → (𝑛 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘𝑛) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛)))) → (𝜑 → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑛 + 1))))))) |
98 | 10, 17, 24, 31, 51, 97 | uzind4 8676 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) → (𝜑 → (𝑁 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘𝑁) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑁))))) |
99 | 1, 98 | mpcom 36 |
. 2
⊢ (𝜑 → (𝑁 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘𝑁) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑁)))) |
100 | 3, 99 | mpd 13 |
1
⊢ (𝜑 → (seq𝐾( + , 𝐹, 𝑆)‘𝑁) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑁))) |