Proof of Theorem seqf1olem2
Step | Hyp | Ref
| Expression |
1 | | seqf1olem.6 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺:(𝑀...(𝑁 + 1))⟶𝐶) |
2 | 1 | ffnd 6506 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 Fn (𝑀...(𝑁 + 1))) |
3 | | fzssp1 13044 |
. . . . . . . . 9
⊢ (𝑀...𝑁) ⊆ (𝑀...(𝑁 + 1)) |
4 | | fnssres 6460 |
. . . . . . . . 9
⊢ ((𝐺 Fn (𝑀...(𝑁 + 1)) ∧ (𝑀...𝑁) ⊆ (𝑀...(𝑁 + 1))) → (𝐺 ↾ (𝑀...𝑁)) Fn (𝑀...𝑁)) |
5 | 2, 3, 4 | sylancl 589 |
. . . . . . . 8
⊢ (𝜑 → (𝐺 ↾ (𝑀...𝑁)) Fn (𝑀...𝑁)) |
6 | | fzfid 13435 |
. . . . . . . 8
⊢ (𝜑 → (𝑀...𝑁) ∈ Fin) |
7 | | fnfi 8781 |
. . . . . . . 8
⊢ (((𝐺 ↾ (𝑀...𝑁)) Fn (𝑀...𝑁) ∧ (𝑀...𝑁) ∈ Fin) → (𝐺 ↾ (𝑀...𝑁)) ∈ Fin) |
8 | 5, 6, 7 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → (𝐺 ↾ (𝑀...𝑁)) ∈ Fin) |
9 | 8 | elexd 3419 |
. . . . . 6
⊢ (𝜑 → (𝐺 ↾ (𝑀...𝑁)) ∈ V) |
10 | | seqf1o.1 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
11 | | seqf1o.2 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) |
12 | | seqf1o.3 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) |
13 | | seqf1o.4 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
14 | | seqf1o.5 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ⊆ 𝑆) |
15 | | seqf1olem.5 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1))) |
16 | | seqf1olem.7 |
. . . . . . . . 9
⊢ 𝐽 = (𝑘 ∈ (𝑀...𝑁) ↦ (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))) |
17 | | seqf1olem.8 |
. . . . . . . . 9
⊢ 𝐾 = (◡𝐹‘(𝑁 + 1)) |
18 | 10, 11, 12, 13, 14, 15, 1, 16, 17 | seqf1olem1 13504 |
. . . . . . . 8
⊢ (𝜑 → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) |
19 | | f1of 6621 |
. . . . . . . 8
⊢ (𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) → 𝐽:(𝑀...𝑁)⟶(𝑀...𝑁)) |
20 | 18, 19 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐽:(𝑀...𝑁)⟶(𝑀...𝑁)) |
21 | | fex2 7667 |
. . . . . . 7
⊢ ((𝐽:(𝑀...𝑁)⟶(𝑀...𝑁) ∧ (𝑀...𝑁) ∈ Fin ∧ (𝑀...𝑁) ∈ Fin) → 𝐽 ∈ V) |
22 | 20, 6, 6, 21 | syl3anc 1372 |
. . . . . 6
⊢ (𝜑 → 𝐽 ∈ V) |
23 | 9, 22 | jca 515 |
. . . . 5
⊢ (𝜑 → ((𝐺 ↾ (𝑀...𝑁)) ∈ V ∧ 𝐽 ∈ V)) |
24 | | seqf1olem.9 |
. . . . 5
⊢ (𝜑 → ∀𝑔∀𝑓((𝑓:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ 𝑔:(𝑀...𝑁)⟶𝐶) → (seq𝑀( + , (𝑔 ∘ 𝑓))‘𝑁) = (seq𝑀( + , 𝑔)‘𝑁))) |
25 | | fssres 6545 |
. . . . . . 7
⊢ ((𝐺:(𝑀...(𝑁 + 1))⟶𝐶 ∧ (𝑀...𝑁) ⊆ (𝑀...(𝑁 + 1))) → (𝐺 ↾ (𝑀...𝑁)):(𝑀...𝑁)⟶𝐶) |
26 | 1, 3, 25 | sylancl 589 |
. . . . . 6
⊢ (𝜑 → (𝐺 ↾ (𝑀...𝑁)):(𝑀...𝑁)⟶𝐶) |
27 | 18, 26 | jca 515 |
. . . . 5
⊢ (𝜑 → (𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ (𝐺 ↾ (𝑀...𝑁)):(𝑀...𝑁)⟶𝐶)) |
28 | | f1oeq1 6609 |
. . . . . . . 8
⊢ (𝑓 = 𝐽 → (𝑓:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ↔ 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))) |
29 | | feq1 6486 |
. . . . . . . 8
⊢ (𝑔 = (𝐺 ↾ (𝑀...𝑁)) → (𝑔:(𝑀...𝑁)⟶𝐶 ↔ (𝐺 ↾ (𝑀...𝑁)):(𝑀...𝑁)⟶𝐶)) |
30 | 28, 29 | bi2anan9r 640 |
. . . . . . 7
⊢ ((𝑔 = (𝐺 ↾ (𝑀...𝑁)) ∧ 𝑓 = 𝐽) → ((𝑓:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ 𝑔:(𝑀...𝑁)⟶𝐶) ↔ (𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ (𝐺 ↾ (𝑀...𝑁)):(𝑀...𝑁)⟶𝐶))) |
31 | | coeq1 5701 |
. . . . . . . . . . 11
⊢ (𝑔 = (𝐺 ↾ (𝑀...𝑁)) → (𝑔 ∘ 𝑓) = ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝑓)) |
32 | | coeq2 5702 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝐽 → ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝑓) = ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)) |
33 | 31, 32 | sylan9eq 2794 |
. . . . . . . . . 10
⊢ ((𝑔 = (𝐺 ↾ (𝑀...𝑁)) ∧ 𝑓 = 𝐽) → (𝑔 ∘ 𝑓) = ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)) |
34 | 33 | seqeq3d 13471 |
. . . . . . . . 9
⊢ ((𝑔 = (𝐺 ↾ (𝑀...𝑁)) ∧ 𝑓 = 𝐽) → seq𝑀( + , (𝑔 ∘ 𝑓)) = seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))) |
35 | 34 | fveq1d 6679 |
. . . . . . . 8
⊢ ((𝑔 = (𝐺 ↾ (𝑀...𝑁)) ∧ 𝑓 = 𝐽) → (seq𝑀( + , (𝑔 ∘ 𝑓))‘𝑁) = (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁)) |
36 | | simpl 486 |
. . . . . . . . . 10
⊢ ((𝑔 = (𝐺 ↾ (𝑀...𝑁)) ∧ 𝑓 = 𝐽) → 𝑔 = (𝐺 ↾ (𝑀...𝑁))) |
37 | 36 | seqeq3d 13471 |
. . . . . . . . 9
⊢ ((𝑔 = (𝐺 ↾ (𝑀...𝑁)) ∧ 𝑓 = 𝐽) → seq𝑀( + , 𝑔) = seq𝑀( + , (𝐺 ↾ (𝑀...𝑁)))) |
38 | 37 | fveq1d 6679 |
. . . . . . . 8
⊢ ((𝑔 = (𝐺 ↾ (𝑀...𝑁)) ∧ 𝑓 = 𝐽) → (seq𝑀( + , 𝑔)‘𝑁) = (seq𝑀( + , (𝐺 ↾ (𝑀...𝑁)))‘𝑁)) |
39 | 35, 38 | eqeq12d 2755 |
. . . . . . 7
⊢ ((𝑔 = (𝐺 ↾ (𝑀...𝑁)) ∧ 𝑓 = 𝐽) → ((seq𝑀( + , (𝑔 ∘ 𝑓))‘𝑁) = (seq𝑀( + , 𝑔)‘𝑁) ↔ (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) = (seq𝑀( + , (𝐺 ↾ (𝑀...𝑁)))‘𝑁))) |
40 | 30, 39 | imbi12d 348 |
. . . . . 6
⊢ ((𝑔 = (𝐺 ↾ (𝑀...𝑁)) ∧ 𝑓 = 𝐽) → (((𝑓:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ 𝑔:(𝑀...𝑁)⟶𝐶) → (seq𝑀( + , (𝑔 ∘ 𝑓))‘𝑁) = (seq𝑀( + , 𝑔)‘𝑁)) ↔ ((𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ (𝐺 ↾ (𝑀...𝑁)):(𝑀...𝑁)⟶𝐶) → (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) = (seq𝑀( + , (𝐺 ↾ (𝑀...𝑁)))‘𝑁)))) |
41 | 40 | spc2gv 3505 |
. . . . 5
⊢ (((𝐺 ↾ (𝑀...𝑁)) ∈ V ∧ 𝐽 ∈ V) → (∀𝑔∀𝑓((𝑓:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ 𝑔:(𝑀...𝑁)⟶𝐶) → (seq𝑀( + , (𝑔 ∘ 𝑓))‘𝑁) = (seq𝑀( + , 𝑔)‘𝑁)) → ((𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ (𝐺 ↾ (𝑀...𝑁)):(𝑀...𝑁)⟶𝐶) → (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) = (seq𝑀( + , (𝐺 ↾ (𝑀...𝑁)))‘𝑁)))) |
42 | 23, 24, 27, 41 | syl3c 66 |
. . . 4
⊢ (𝜑 → (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) = (seq𝑀( + , (𝐺 ↾ (𝑀...𝑁)))‘𝑁)) |
43 | | fvres 6696 |
. . . . . 6
⊢ (𝑥 ∈ (𝑀...𝑁) → ((𝐺 ↾ (𝑀...𝑁))‘𝑥) = (𝐺‘𝑥)) |
44 | 43 | adantl 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐺 ↾ (𝑀...𝑁))‘𝑥) = (𝐺‘𝑥)) |
45 | 13, 44 | seqfveq 13489 |
. . . 4
⊢ (𝜑 → (seq𝑀( + , (𝐺 ↾ (𝑀...𝑁)))‘𝑁) = (seq𝑀( + , 𝐺)‘𝑁)) |
46 | 42, 45 | eqtrd 2774 |
. . 3
⊢ (𝜑 → (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) = (seq𝑀( + , 𝐺)‘𝑁)) |
47 | 46 | oveq1d 7188 |
. 2
⊢ (𝜑 → ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))) = ((seq𝑀( + , 𝐺)‘𝑁) + (𝐺‘(𝑁 + 1)))) |
48 | 10 | adantlr 715 |
. . . . 5
⊢ (((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
49 | 12 | adantlr 715 |
. . . . 5
⊢ (((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) |
50 | | elfzuz3 12998 |
. . . . . . 7
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝐾)) |
51 | 50 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) → 𝑁 ∈ (ℤ≥‘𝐾)) |
52 | | eluzp1p1 12355 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝐾) → (𝑁 + 1) ∈
(ℤ≥‘(𝐾 + 1))) |
53 | 51, 52 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) → (𝑁 + 1) ∈
(ℤ≥‘(𝐾 + 1))) |
54 | | elfzuz 12997 |
. . . . . 6
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ≥‘𝑀)) |
55 | 54 | adantl 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) → 𝐾 ∈ (ℤ≥‘𝑀)) |
56 | | f1of 6621 |
. . . . . . . . . 10
⊢ (𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1))) |
57 | 15, 56 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1))) |
58 | | fco 6529 |
. . . . . . . . 9
⊢ ((𝐺:(𝑀...(𝑁 + 1))⟶𝐶 ∧ 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1))) → (𝐺 ∘ 𝐹):(𝑀...(𝑁 + 1))⟶𝐶) |
59 | 1, 57, 58 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 → (𝐺 ∘ 𝐹):(𝑀...(𝑁 + 1))⟶𝐶) |
60 | 59, 14 | fssd 6523 |
. . . . . . 7
⊢ (𝜑 → (𝐺 ∘ 𝐹):(𝑀...(𝑁 + 1))⟶𝑆) |
61 | 60 | ffvelrnda 6864 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...(𝑁 + 1))) → ((𝐺 ∘ 𝐹)‘𝑥) ∈ 𝑆) |
62 | 61 | adantlr 715 |
. . . . 5
⊢ (((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) ∧ 𝑥 ∈ (𝑀...(𝑁 + 1))) → ((𝐺 ∘ 𝐹)‘𝑥) ∈ 𝑆) |
63 | 48, 49, 53, 55, 62 | seqsplit 13498 |
. . . 4
⊢ ((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) → (seq𝑀( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1)) = ((seq𝑀( + , (𝐺 ∘ 𝐹))‘𝐾) + (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1)))) |
64 | | elfzp12 13080 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 = 𝑀 ∨ 𝐾 ∈ ((𝑀 + 1)...𝑁)))) |
65 | 64 | biimpa 480 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝐾 ∈ (𝑀...𝑁)) → (𝐾 = 𝑀 ∨ 𝐾 ∈ ((𝑀 + 1)...𝑁))) |
66 | 13, 65 | sylan 583 |
. . . . 5
⊢ ((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) → (𝐾 = 𝑀 ∨ 𝐾 ∈ ((𝑀 + 1)...𝑁))) |
67 | | seqeq1 13466 |
. . . . . . . . . . 11
⊢ (𝐾 = 𝑀 → seq𝐾( + , (𝐺 ∘ 𝐹)) = seq𝑀( + , (𝐺 ∘ 𝐹))) |
68 | 67 | eqcomd 2745 |
. . . . . . . . . 10
⊢ (𝐾 = 𝑀 → seq𝑀( + , (𝐺 ∘ 𝐹)) = seq𝐾( + , (𝐺 ∘ 𝐹))) |
69 | 68 | fveq1d 6679 |
. . . . . . . . 9
⊢ (𝐾 = 𝑀 → (seq𝑀( + , (𝐺 ∘ 𝐹))‘𝐾) = (seq𝐾( + , (𝐺 ∘ 𝐹))‘𝐾)) |
70 | | f1ocnv 6633 |
. . . . . . . . . . . . 13
⊢ (𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) → ◡𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1))) |
71 | | f1of 6621 |
. . . . . . . . . . . . 13
⊢ (◡𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) → ◡𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1))) |
72 | 15, 70, 71 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → ◡𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1))) |
73 | | peano2uz 12386 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑁 + 1) ∈
(ℤ≥‘𝑀)) |
74 | | eluzfz2 13009 |
. . . . . . . . . . . . 13
⊢ ((𝑁 + 1) ∈
(ℤ≥‘𝑀) → (𝑁 + 1) ∈ (𝑀...(𝑁 + 1))) |
75 | 13, 73, 74 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 + 1) ∈ (𝑀...(𝑁 + 1))) |
76 | 72, 75 | ffvelrnd 6865 |
. . . . . . . . . . 11
⊢ (𝜑 → (◡𝐹‘(𝑁 + 1)) ∈ (𝑀...(𝑁 + 1))) |
77 | 17, 76 | eqeltrid 2838 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈ (𝑀...(𝑁 + 1))) |
78 | | elfzelz 13001 |
. . . . . . . . . 10
⊢ (𝐾 ∈ (𝑀...(𝑁 + 1)) → 𝐾 ∈ ℤ) |
79 | | seq1 13476 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℤ → (seq𝐾( + , (𝐺 ∘ 𝐹))‘𝐾) = ((𝐺 ∘ 𝐹)‘𝐾)) |
80 | 77, 78, 79 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → (seq𝐾( + , (𝐺 ∘ 𝐹))‘𝐾) = ((𝐺 ∘ 𝐹)‘𝐾)) |
81 | 69, 80 | sylan9eqr 2796 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐾 = 𝑀) → (seq𝑀( + , (𝐺 ∘ 𝐹))‘𝐾) = ((𝐺 ∘ 𝐹)‘𝐾)) |
82 | 81 | oveq1d 7188 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐾 = 𝑀) → ((seq𝑀( + , (𝐺 ∘ 𝐹))‘𝐾) + (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1))) = (((𝐺 ∘ 𝐹)‘𝐾) + (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1)))) |
83 | | simpr 488 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐾 = 𝑀) → 𝐾 = 𝑀) |
84 | | eluzfz1 13008 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁)) |
85 | 13, 84 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ (𝑀...𝑁)) |
86 | 85 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐾 = 𝑀) → 𝑀 ∈ (𝑀...𝑁)) |
87 | 83, 86 | eqeltrd 2834 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐾 = 𝑀) → 𝐾 ∈ (𝑀...𝑁)) |
88 | 11 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) |
89 | 14 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) → 𝐶 ⊆ 𝑆) |
90 | 59 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) → (𝐺 ∘ 𝐹):(𝑀...(𝑁 + 1))⟶𝐶) |
91 | 77 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) → 𝐾 ∈ (𝑀...(𝑁 + 1))) |
92 | | peano2uz 12386 |
. . . . . . . . . . 11
⊢ (𝐾 ∈
(ℤ≥‘𝑀) → (𝐾 + 1) ∈
(ℤ≥‘𝑀)) |
93 | | fzss1 13040 |
. . . . . . . . . . 11
⊢ ((𝐾 + 1) ∈
(ℤ≥‘𝑀) → ((𝐾 + 1)...(𝑁 + 1)) ⊆ (𝑀...(𝑁 + 1))) |
94 | 55, 92, 93 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) → ((𝐾 + 1)...(𝑁 + 1)) ⊆ (𝑀...(𝑁 + 1))) |
95 | 48, 88, 49, 53, 89, 90, 91, 94 | seqf1olem2a 13503 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) → (((𝐺 ∘ 𝐹)‘𝐾) + (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1))) = ((seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1)) + ((𝐺 ∘ 𝐹)‘𝐾))) |
96 | | 1zzd 12097 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) → 1 ∈ ℤ) |
97 | | elfzuz 12997 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐾 ∈ (𝑀...(𝑁 + 1)) → 𝐾 ∈ (ℤ≥‘𝑀)) |
98 | | fzss1 13040 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐾 ∈
(ℤ≥‘𝑀) → (𝐾...𝑁) ⊆ (𝑀...𝑁)) |
99 | 77, 97, 98 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐾...𝑁) ⊆ (𝑀...𝑁)) |
100 | 99 | sselda 3878 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑁)) → 𝑥 ∈ (𝑀...𝑁)) |
101 | 20 | ffvelrnda 6864 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐽‘𝑥) ∈ (𝑀...𝑁)) |
102 | 100, 101 | syldan 594 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑁)) → (𝐽‘𝑥) ∈ (𝑀...𝑁)) |
103 | 102 | fvresd 6697 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑁)) → ((𝐺 ↾ (𝑀...𝑁))‘(𝐽‘𝑥)) = (𝐺‘(𝐽‘𝑥))) |
104 | | breq1 5034 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑥 → (𝑘 < 𝐾 ↔ 𝑥 < 𝐾)) |
105 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑥 → 𝑘 = 𝑥) |
106 | | oveq1 7180 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑥 → (𝑘 + 1) = (𝑥 + 1)) |
107 | 104, 105,
106 | ifbieq12d 4443 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑥 → if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)) = if(𝑥 < 𝐾, 𝑥, (𝑥 + 1))) |
108 | 107 | fveq2d 6681 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑥 → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1)))) |
109 | | fvex 6690 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1))) ∈ V |
110 | 108, 16, 109 | fvmpt 6778 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (𝑀...𝑁) → (𝐽‘𝑥) = (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1)))) |
111 | 100, 110 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑁)) → (𝐽‘𝑥) = (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1)))) |
112 | 77, 78 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐾 ∈ ℤ) |
113 | 112 | zred 12171 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐾 ∈ ℝ) |
114 | 113 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑁)) → 𝐾 ∈ ℝ) |
115 | | elfzelz 13001 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (𝐾...𝑁) → 𝑥 ∈ ℤ) |
116 | 115 | adantl 485 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑁)) → 𝑥 ∈ ℤ) |
117 | 116 | zred 12171 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑁)) → 𝑥 ∈ ℝ) |
118 | | elfzle1 13004 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (𝐾...𝑁) → 𝐾 ≤ 𝑥) |
119 | 118 | adantl 485 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑁)) → 𝐾 ≤ 𝑥) |
120 | 114, 117,
119 | lensymd 10872 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑁)) → ¬ 𝑥 < 𝐾) |
121 | | iffalse 4424 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
𝑥 < 𝐾 → if(𝑥 < 𝐾, 𝑥, (𝑥 + 1)) = (𝑥 + 1)) |
122 | 121 | fveq2d 6681 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑥 < 𝐾 → (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1))) = (𝐹‘(𝑥 + 1))) |
123 | 120, 122 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑁)) → (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1))) = (𝐹‘(𝑥 + 1))) |
124 | 111, 123 | eqtrd 2774 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑁)) → (𝐽‘𝑥) = (𝐹‘(𝑥 + 1))) |
125 | 124 | fveq2d 6681 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑁)) → (𝐺‘(𝐽‘𝑥)) = (𝐺‘(𝐹‘(𝑥 + 1)))) |
126 | 103, 125 | eqtrd 2774 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑁)) → ((𝐺 ↾ (𝑀...𝑁))‘(𝐽‘𝑥)) = (𝐺‘(𝐹‘(𝑥 + 1)))) |
127 | | fvco3 6770 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽:(𝑀...𝑁)⟶(𝑀...𝑁) ∧ 𝑥 ∈ (𝑀...𝑁)) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) = ((𝐺 ↾ (𝑀...𝑁))‘(𝐽‘𝑥))) |
128 | 20, 127 | sylan 583 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) = ((𝐺 ↾ (𝑀...𝑁))‘(𝐽‘𝑥))) |
129 | 100, 128 | syldan 594 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑁)) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) = ((𝐺 ↾ (𝑀...𝑁))‘(𝐽‘𝑥))) |
130 | | fzp1elp1 13054 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝑀...𝑁) → (𝑥 + 1) ∈ (𝑀...(𝑁 + 1))) |
131 | 100, 130 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑁)) → (𝑥 + 1) ∈ (𝑀...(𝑁 + 1))) |
132 | | fvco3 6770 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)) ∧ (𝑥 + 1) ∈ (𝑀...(𝑁 + 1))) → ((𝐺 ∘ 𝐹)‘(𝑥 + 1)) = (𝐺‘(𝐹‘(𝑥 + 1)))) |
133 | 57, 132 | sylan 583 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 + 1) ∈ (𝑀...(𝑁 + 1))) → ((𝐺 ∘ 𝐹)‘(𝑥 + 1)) = (𝐺‘(𝐹‘(𝑥 + 1)))) |
134 | 131, 133 | syldan 594 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑁)) → ((𝐺 ∘ 𝐹)‘(𝑥 + 1)) = (𝐺‘(𝐹‘(𝑥 + 1)))) |
135 | 126, 129,
134 | 3eqtr4d 2784 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑁)) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) = ((𝐺 ∘ 𝐹)‘(𝑥 + 1))) |
136 | 135 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) ∧ 𝑥 ∈ (𝐾...𝑁)) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) = ((𝐺 ∘ 𝐹)‘(𝑥 + 1))) |
137 | 51, 96, 136 | seqshft2 13491 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) → (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) = (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1))) |
138 | | fvco3 6770 |
. . . . . . . . . . . . 13
⊢ ((𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)) ∧ 𝐾 ∈ (𝑀...(𝑁 + 1))) → ((𝐺 ∘ 𝐹)‘𝐾) = (𝐺‘(𝐹‘𝐾))) |
139 | 57, 77, 138 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐺 ∘ 𝐹)‘𝐾) = (𝐺‘(𝐹‘𝐾))) |
140 | 17 | fveq2i 6680 |
. . . . . . . . . . . . . 14
⊢ (𝐹‘𝐾) = (𝐹‘(◡𝐹‘(𝑁 + 1))) |
141 | | f1ocnvfv2 7048 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ (𝑁 + 1) ∈ (𝑀...(𝑁 + 1))) → (𝐹‘(◡𝐹‘(𝑁 + 1))) = (𝑁 + 1)) |
142 | 15, 75, 141 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹‘(◡𝐹‘(𝑁 + 1))) = (𝑁 + 1)) |
143 | 140, 142 | syl5eq 2786 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹‘𝐾) = (𝑁 + 1)) |
144 | 143 | fveq2d 6681 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐺‘(𝐹‘𝐾)) = (𝐺‘(𝑁 + 1))) |
145 | 139, 144 | eqtr2d 2775 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺‘(𝑁 + 1)) = ((𝐺 ∘ 𝐹)‘𝐾)) |
146 | 145 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) → (𝐺‘(𝑁 + 1)) = ((𝐺 ∘ 𝐹)‘𝐾)) |
147 | 137, 146 | oveq12d 7191 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) → ((seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))) = ((seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1)) + ((𝐺 ∘ 𝐹)‘𝐾))) |
148 | 95, 147 | eqtr4d 2777 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) → (((𝐺 ∘ 𝐹)‘𝐾) + (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1))) = ((seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1)))) |
149 | 87, 148 | syldan 594 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐾 = 𝑀) → (((𝐺 ∘ 𝐹)‘𝐾) + (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1))) = ((seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1)))) |
150 | 83 | seqeq1d 13469 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐾 = 𝑀) → seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)) = seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))) |
151 | 150 | fveq1d 6679 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐾 = 𝑀) → (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) = (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁)) |
152 | 151 | oveq1d 7188 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐾 = 𝑀) → ((seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1)))) |
153 | 82, 149, 152 | 3eqtrd 2778 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐾 = 𝑀) → ((seq𝑀( + , (𝐺 ∘ 𝐹))‘𝐾) + (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1))) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1)))) |
154 | | eluzel2 12332 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
155 | 13, 154 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℤ) |
156 | | elfzuz 12997 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ ((𝑀 + 1)...𝑁) → 𝐾 ∈ (ℤ≥‘(𝑀 + 1))) |
157 | | eluzp1m1 12353 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈
(ℤ≥‘(𝑀 + 1))) → (𝐾 − 1) ∈
(ℤ≥‘𝑀)) |
158 | 155, 156,
157 | syl2an 599 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → (𝐾 − 1) ∈
(ℤ≥‘𝑀)) |
159 | | eluzelz 12337 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
160 | 13, 159 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑁 ∈ ℤ) |
161 | 160 | zcnd 12172 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈ ℂ) |
162 | | ax-1cn 10676 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℂ |
163 | | pncan 10973 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 + 1)
− 1) = 𝑁) |
164 | 161, 162,
163 | sylancl 589 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑁 + 1) − 1) = 𝑁) |
165 | | peano2zm 12109 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐾 ∈ ℤ → (𝐾 − 1) ∈
ℤ) |
166 | 77, 78, 165 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐾 − 1) ∈ ℤ) |
167 | | elfzuz3 12998 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐾 ∈ (𝑀...(𝑁 + 1)) → (𝑁 + 1) ∈
(ℤ≥‘𝐾)) |
168 | 77, 167 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑁 + 1) ∈
(ℤ≥‘𝐾)) |
169 | 112 | zcnd 12172 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝐾 ∈ ℂ) |
170 | | npcan 10976 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐾 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝐾 −
1) + 1) = 𝐾) |
171 | 169, 162,
170 | sylancl 589 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝐾 − 1) + 1) = 𝐾) |
172 | 171 | fveq2d 6681 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 →
(ℤ≥‘((𝐾 − 1) + 1)) =
(ℤ≥‘𝐾)) |
173 | 168, 172 | eleqtrrd 2837 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑁 + 1) ∈
(ℤ≥‘((𝐾 − 1) + 1))) |
174 | | eluzp1m1 12353 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐾 − 1) ∈ ℤ ∧
(𝑁 + 1) ∈
(ℤ≥‘((𝐾 − 1) + 1))) → ((𝑁 + 1) − 1) ∈
(ℤ≥‘(𝐾 − 1))) |
175 | 166, 173,
174 | syl2anc 587 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑁 + 1) − 1) ∈
(ℤ≥‘(𝐾 − 1))) |
176 | 164, 175 | eqeltrrd 2835 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝐾 − 1))) |
177 | | fzss2 13041 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈
(ℤ≥‘(𝐾 − 1)) → (𝑀...(𝐾 − 1)) ⊆ (𝑀...𝑁)) |
178 | 176, 177 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑀...(𝐾 − 1)) ⊆ (𝑀...𝑁)) |
179 | 178 | sselda 3878 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → 𝑥 ∈ (𝑀...𝑁)) |
180 | 179, 101 | syldan 594 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → (𝐽‘𝑥) ∈ (𝑀...𝑁)) |
181 | 180 | fvresd 6697 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → ((𝐺 ↾ (𝑀...𝑁))‘(𝐽‘𝑥)) = (𝐺‘(𝐽‘𝑥))) |
182 | 179, 110 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → (𝐽‘𝑥) = (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1)))) |
183 | | elfzm11 13072 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑥 ∈ (𝑀...(𝐾 − 1)) ↔ (𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥 ∧ 𝑥 < 𝐾))) |
184 | 155, 112,
183 | syl2anc 587 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑥 ∈ (𝑀...(𝐾 − 1)) ↔ (𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥 ∧ 𝑥 < 𝐾))) |
185 | 184 | biimpa 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → (𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥 ∧ 𝑥 < 𝐾)) |
186 | 185 | simp3d 1145 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → 𝑥 < 𝐾) |
187 | | iftrue 4421 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 < 𝐾 → if(𝑥 < 𝐾, 𝑥, (𝑥 + 1)) = 𝑥) |
188 | 187 | fveq2d 6681 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 < 𝐾 → (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1))) = (𝐹‘𝑥)) |
189 | 186, 188 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1))) = (𝐹‘𝑥)) |
190 | 182, 189 | eqtrd 2774 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → (𝐽‘𝑥) = (𝐹‘𝑥)) |
191 | 190 | fveq2d 6681 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → (𝐺‘(𝐽‘𝑥)) = (𝐺‘(𝐹‘𝑥))) |
192 | 181, 191 | eqtr2d 2775 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → (𝐺‘(𝐹‘𝑥)) = ((𝐺 ↾ (𝑀...𝑁))‘(𝐽‘𝑥))) |
193 | | peano2uz 12386 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘(𝐾 − 1)) → (𝑁 + 1) ∈
(ℤ≥‘(𝐾 − 1))) |
194 | | fzss2 13041 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 + 1) ∈
(ℤ≥‘(𝐾 − 1)) → (𝑀...(𝐾 − 1)) ⊆ (𝑀...(𝑁 + 1))) |
195 | 176, 193,
194 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀...(𝐾 − 1)) ⊆ (𝑀...(𝑁 + 1))) |
196 | 195 | sselda 3878 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → 𝑥 ∈ (𝑀...(𝑁 + 1))) |
197 | | fvco3 6770 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...(𝑁 + 1))) → ((𝐺 ∘ 𝐹)‘𝑥) = (𝐺‘(𝐹‘𝑥))) |
198 | 57, 197 | sylan 583 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...(𝑁 + 1))) → ((𝐺 ∘ 𝐹)‘𝑥) = (𝐺‘(𝐹‘𝑥))) |
199 | 196, 198 | syldan 594 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → ((𝐺 ∘ 𝐹)‘𝑥) = (𝐺‘(𝐹‘𝑥))) |
200 | 179, 128 | syldan 594 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) = ((𝐺 ↾ (𝑀...𝑁))‘(𝐽‘𝑥))) |
201 | 192, 199,
200 | 3eqtr4d 2784 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → ((𝐺 ∘ 𝐹)‘𝑥) = (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥)) |
202 | 201 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → ((𝐺 ∘ 𝐹)‘𝑥) = (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥)) |
203 | 158, 202 | seqfveq 13489 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → (seq𝑀( + , (𝐺 ∘ 𝐹))‘(𝐾 − 1)) = (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1))) |
204 | | fzp1ss 13052 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℤ → ((𝑀 + 1)...𝑁) ⊆ (𝑀...𝑁)) |
205 | 13, 154, 204 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑀 + 1)...𝑁) ⊆ (𝑀...𝑁)) |
206 | 205 | sselda 3878 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → 𝐾 ∈ (𝑀...𝑁)) |
207 | 206, 148 | syldan 594 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → (((𝐺 ∘ 𝐹)‘𝐾) + (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1))) = ((seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1)))) |
208 | 203, 207 | oveq12d 7191 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → ((seq𝑀( + , (𝐺 ∘ 𝐹))‘(𝐾 − 1)) + (((𝐺 ∘ 𝐹)‘𝐾) + (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1)))) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + ((seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))))) |
209 | 196, 61 | syldan 594 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → ((𝐺 ∘ 𝐹)‘𝑥) ∈ 𝑆) |
210 | 209 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → ((𝐺 ∘ 𝐹)‘𝑥) ∈ 𝑆) |
211 | 10 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
212 | 158, 210,
211 | seqcl 13485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → (seq𝑀( + , (𝐺 ∘ 𝐹))‘(𝐾 − 1)) ∈ 𝑆) |
213 | 59, 77 | ffvelrnd 6865 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐺 ∘ 𝐹)‘𝐾) ∈ 𝐶) |
214 | 14, 213 | sseldd 3879 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐺 ∘ 𝐹)‘𝐾) ∈ 𝑆) |
215 | 214 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → ((𝐺 ∘ 𝐹)‘𝐾) ∈ 𝑆) |
216 | 94 | sselda 3878 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) ∧ 𝑥 ∈ ((𝐾 + 1)...(𝑁 + 1))) → 𝑥 ∈ (𝑀...(𝑁 + 1))) |
217 | 216, 62 | syldan 594 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) ∧ 𝑥 ∈ ((𝐾 + 1)...(𝑁 + 1))) → ((𝐺 ∘ 𝐹)‘𝑥) ∈ 𝑆) |
218 | 53, 217, 48 | seqcl 13485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) → (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1)) ∈ 𝑆) |
219 | 206, 218 | syldan 594 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1)) ∈ 𝑆) |
220 | 212, 215,
219 | 3jca 1129 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → ((seq𝑀( + , (𝐺 ∘ 𝐹))‘(𝐾 − 1)) ∈ 𝑆 ∧ ((𝐺 ∘ 𝐹)‘𝐾) ∈ 𝑆 ∧ (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1)) ∈ 𝑆)) |
221 | 12 | caovassg 7365 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((seq𝑀( + , (𝐺 ∘ 𝐹))‘(𝐾 − 1)) ∈ 𝑆 ∧ ((𝐺 ∘ 𝐹)‘𝐾) ∈ 𝑆 ∧ (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1)) ∈ 𝑆)) → (((seq𝑀( + , (𝐺 ∘ 𝐹))‘(𝐾 − 1)) + ((𝐺 ∘ 𝐹)‘𝐾)) + (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1))) = ((seq𝑀( + , (𝐺 ∘ 𝐹))‘(𝐾 − 1)) + (((𝐺 ∘ 𝐹)‘𝐾) + (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1))))) |
222 | 220, 221 | syldan 594 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → (((seq𝑀( + , (𝐺 ∘ 𝐹))‘(𝐾 − 1)) + ((𝐺 ∘ 𝐹)‘𝐾)) + (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1))) = ((seq𝑀( + , (𝐺 ∘ 𝐹))‘(𝐾 − 1)) + (((𝐺 ∘ 𝐹)‘𝐾) + (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1))))) |
223 | 1, 14 | fssd 6523 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐺:(𝑀...(𝑁 + 1))⟶𝑆) |
224 | | fssres 6545 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺:(𝑀...(𝑁 + 1))⟶𝑆 ∧ (𝑀...𝑁) ⊆ (𝑀...(𝑁 + 1))) → (𝐺 ↾ (𝑀...𝑁)):(𝑀...𝑁)⟶𝑆) |
225 | 223, 3, 224 | sylancl 589 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐺 ↾ (𝑀...𝑁)):(𝑀...𝑁)⟶𝑆) |
226 | | fco 6529 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ↾ (𝑀...𝑁)):(𝑀...𝑁)⟶𝑆 ∧ 𝐽:(𝑀...𝑁)⟶(𝑀...𝑁)) → ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽):(𝑀...𝑁)⟶𝑆) |
227 | 225, 20, 226 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽):(𝑀...𝑁)⟶𝑆) |
228 | 227 | ffvelrnda 6864 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) ∈ 𝑆) |
229 | 179, 228 | syldan 594 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) ∈ 𝑆) |
230 | 229 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) ∈ 𝑆) |
231 | 158, 230,
211 | seqcl 13485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) ∈ 𝑆) |
232 | | elfzuz3 12998 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ ((𝑀 + 1)...𝑁) → 𝑁 ∈ (ℤ≥‘𝐾)) |
233 | 232 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → 𝑁 ∈ (ℤ≥‘𝐾)) |
234 | 100, 228 | syldan 594 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑁)) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) ∈ 𝑆) |
235 | 234 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) ∧ 𝑥 ∈ (𝐾...𝑁)) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) ∈ 𝑆) |
236 | 233, 235,
211 | seqcl 13485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) ∈ 𝑆) |
237 | 223, 75 | ffvelrnd 6865 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺‘(𝑁 + 1)) ∈ 𝑆) |
238 | 237 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → (𝐺‘(𝑁 + 1)) ∈ 𝑆) |
239 | 231, 236,
238 | 3jca 1129 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) ∈ 𝑆 ∧ (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) ∈ 𝑆 ∧ (𝐺‘(𝑁 + 1)) ∈ 𝑆)) |
240 | 12 | caovassg 7365 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) ∈ 𝑆 ∧ (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) ∈ 𝑆 ∧ (𝐺‘(𝑁 + 1)) ∈ 𝑆)) → (((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁)) + (𝐺‘(𝑁 + 1))) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + ((seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))))) |
241 | 239, 240 | syldan 594 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → (((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁)) + (𝐺‘(𝑁 + 1))) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + ((seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))))) |
242 | 208, 222,
241 | 3eqtr4d 2784 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → (((seq𝑀( + , (𝐺 ∘ 𝐹))‘(𝐾 − 1)) + ((𝐺 ∘ 𝐹)‘𝐾)) + (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1))) = (((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁)) + (𝐺‘(𝑁 + 1)))) |
243 | | seqm1 13482 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈
(ℤ≥‘(𝑀 + 1))) → (seq𝑀( + , (𝐺 ∘ 𝐹))‘𝐾) = ((seq𝑀( + , (𝐺 ∘ 𝐹))‘(𝐾 − 1)) + ((𝐺 ∘ 𝐹)‘𝐾))) |
244 | 155, 156,
243 | syl2an 599 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → (seq𝑀( + , (𝐺 ∘ 𝐹))‘𝐾) = ((seq𝑀( + , (𝐺 ∘ 𝐹))‘(𝐾 − 1)) + ((𝐺 ∘ 𝐹)‘𝐾))) |
245 | 244 | oveq1d 7188 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → ((seq𝑀( + , (𝐺 ∘ 𝐹))‘𝐾) + (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1))) = (((seq𝑀( + , (𝐺 ∘ 𝐹))‘(𝐾 − 1)) + ((𝐺 ∘ 𝐹)‘𝐾)) + (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1)))) |
246 | 12 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) |
247 | | elfzelz 13001 |
. . . . . . . . . . . . . . 15
⊢ (𝐾 ∈ ((𝑀 + 1)...𝑁) → 𝐾 ∈ ℤ) |
248 | 247 | adantl 485 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → 𝐾 ∈ ℤ) |
249 | 248 | zcnd 12172 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → 𝐾 ∈ ℂ) |
250 | 249, 162,
170 | sylancl 589 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → ((𝐾 − 1) + 1) = 𝐾) |
251 | 250 | fveq2d 6681 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) →
(ℤ≥‘((𝐾 − 1) + 1)) =
(ℤ≥‘𝐾)) |
252 | 233, 251 | eleqtrrd 2837 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → 𝑁 ∈
(ℤ≥‘((𝐾 − 1) + 1))) |
253 | 228 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) ∈ 𝑆) |
254 | 211, 246,
252, 158, 253 | seqsplit 13498 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + (seq((𝐾 − 1) + 1)( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁))) |
255 | 250 | seqeq1d 13469 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → seq((𝐾 − 1) + 1)( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)) = seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))) |
256 | 255 | fveq1d 6679 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → (seq((𝐾 − 1) + 1)( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) = (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁)) |
257 | 256 | oveq2d 7189 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + (seq((𝐾 − 1) + 1)( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁)) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁))) |
258 | 254, 257 | eqtrd 2774 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁))) |
259 | 258 | oveq1d 7188 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))) = (((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁)) + (𝐺‘(𝑁 + 1)))) |
260 | 242, 245,
259 | 3eqtr4d 2784 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → ((seq𝑀( + , (𝐺 ∘ 𝐹))‘𝐾) + (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1))) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1)))) |
261 | 153, 260 | jaodan 957 |
. . . . 5
⊢ ((𝜑 ∧ (𝐾 = 𝑀 ∨ 𝐾 ∈ ((𝑀 + 1)...𝑁))) → ((seq𝑀( + , (𝐺 ∘ 𝐹))‘𝐾) + (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1))) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1)))) |
262 | 66, 261 | syldan 594 |
. . . 4
⊢ ((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) → ((seq𝑀( + , (𝐺 ∘ 𝐹))‘𝐾) + (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1))) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1)))) |
263 | 63, 262 | eqtrd 2774 |
. . 3
⊢ ((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) → (seq𝑀( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1)) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1)))) |
264 | 13 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝐾 = (𝑁 + 1)) → 𝑁 ∈ (ℤ≥‘𝑀)) |
265 | | seqp1 13478 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (seq𝑀( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1)) = ((seq𝑀( + , (𝐺 ∘ 𝐹))‘𝑁) + ((𝐺 ∘ 𝐹)‘(𝑁 + 1)))) |
266 | 264, 265 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝐾 = (𝑁 + 1)) → (seq𝑀( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1)) = ((seq𝑀( + , (𝐺 ∘ 𝐹))‘𝑁) + ((𝐺 ∘ 𝐹)‘(𝑁 + 1)))) |
267 | 110 | adantl 485 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐽‘𝑥) = (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1)))) |
268 | | elfzelz 13001 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (𝑀...𝑁) → 𝑥 ∈ ℤ) |
269 | 268 | zred 12171 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝑀...𝑁) → 𝑥 ∈ ℝ) |
270 | 269 | adantl 485 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ ℝ) |
271 | 160 | zred 12171 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈ ℝ) |
272 | 271 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑁 ∈ ℝ) |
273 | | peano2re 10894 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℝ → (𝑁 + 1) ∈
ℝ) |
274 | 272, 273 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝑁 + 1) ∈ ℝ) |
275 | | elfzle2 13005 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝑀...𝑁) → 𝑥 ≤ 𝑁) |
276 | 275 | adantl 485 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ≤ 𝑁) |
277 | 272 | ltp1d 11651 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑁 < (𝑁 + 1)) |
278 | 270, 272,
274, 276, 277 | lelttrd 10879 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 < (𝑁 + 1)) |
279 | 278 | adantlr 715 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 < (𝑁 + 1)) |
280 | | simplr 769 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝐾 = (𝑁 + 1)) |
281 | 279, 280 | breqtrrd 5059 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 < 𝐾) |
282 | 281, 188 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1))) = (𝐹‘𝑥)) |
283 | 267, 282 | eqtrd 2774 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐽‘𝑥) = (𝐹‘𝑥)) |
284 | 283 | fveq2d 6681 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐺 ↾ (𝑀...𝑁))‘(𝐽‘𝑥)) = ((𝐺 ↾ (𝑀...𝑁))‘(𝐹‘𝑥))) |
285 | 269 | adantl 485 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ ℝ) |
286 | 285, 281 | gtned 10856 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝐾 ≠ 𝑥) |
287 | 57 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1))) |
288 | | fzelp1 13053 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (𝑀...𝑁) → 𝑥 ∈ (𝑀...(𝑁 + 1))) |
289 | 288 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ (𝑀...(𝑁 + 1))) |
290 | 287, 289 | ffvelrnd 6865 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) ∈ (𝑀...(𝑁 + 1))) |
291 | 13 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑁 ∈ (ℤ≥‘𝑀)) |
292 | | elfzp1 13051 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((𝐹‘𝑥) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘𝑥) ∈ (𝑀...𝑁) ∨ (𝐹‘𝑥) = (𝑁 + 1)))) |
293 | 291, 292 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐹‘𝑥) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘𝑥) ∈ (𝑀...𝑁) ∨ (𝐹‘𝑥) = (𝑁 + 1)))) |
294 | 290, 293 | mpbid 235 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐹‘𝑥) ∈ (𝑀...𝑁) ∨ (𝐹‘𝑥) = (𝑁 + 1))) |
295 | 294 | ord 863 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (¬ (𝐹‘𝑥) ∈ (𝑀...𝑁) → (𝐹‘𝑥) = (𝑁 + 1))) |
296 | 15 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1))) |
297 | | f1ocnvfv 7049 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...(𝑁 + 1))) → ((𝐹‘𝑥) = (𝑁 + 1) → (◡𝐹‘(𝑁 + 1)) = 𝑥)) |
298 | 296, 289,
297 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐹‘𝑥) = (𝑁 + 1) → (◡𝐹‘(𝑁 + 1)) = 𝑥)) |
299 | 17 | eqeq1i 2744 |
. . . . . . . . . . . . 13
⊢ (𝐾 = 𝑥 ↔ (◡𝐹‘(𝑁 + 1)) = 𝑥) |
300 | 298, 299 | syl6ibr 255 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐹‘𝑥) = (𝑁 + 1) → 𝐾 = 𝑥)) |
301 | 295, 300 | syld 47 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (¬ (𝐹‘𝑥) ∈ (𝑀...𝑁) → 𝐾 = 𝑥)) |
302 | 301 | necon1ad 2952 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐾 ≠ 𝑥 → (𝐹‘𝑥) ∈ (𝑀...𝑁))) |
303 | 286, 302 | mpd 15 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) ∈ (𝑀...𝑁)) |
304 | 303 | fvresd 6697 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐺 ↾ (𝑀...𝑁))‘(𝐹‘𝑥)) = (𝐺‘(𝐹‘𝑥))) |
305 | 284, 304 | eqtr2d 2775 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐺‘(𝐹‘𝑥)) = ((𝐺 ↾ (𝑀...𝑁))‘(𝐽‘𝑥))) |
306 | 57, 288, 197 | syl2an 599 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐺 ∘ 𝐹)‘𝑥) = (𝐺‘(𝐹‘𝑥))) |
307 | 306 | adantlr 715 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐺 ∘ 𝐹)‘𝑥) = (𝐺‘(𝐹‘𝑥))) |
308 | 128 | adantlr 715 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) = ((𝐺 ↾ (𝑀...𝑁))‘(𝐽‘𝑥))) |
309 | 305, 307,
308 | 3eqtr4d 2784 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐺 ∘ 𝐹)‘𝑥) = (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥)) |
310 | 264, 309 | seqfveq 13489 |
. . . . 5
⊢ ((𝜑 ∧ 𝐾 = (𝑁 + 1)) → (seq𝑀( + , (𝐺 ∘ 𝐹))‘𝑁) = (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁)) |
311 | | fvco3 6770 |
. . . . . . . 8
⊢ ((𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)) ∧ (𝑁 + 1) ∈ (𝑀...(𝑁 + 1))) → ((𝐺 ∘ 𝐹)‘(𝑁 + 1)) = (𝐺‘(𝐹‘(𝑁 + 1)))) |
312 | 57, 75, 311 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → ((𝐺 ∘ 𝐹)‘(𝑁 + 1)) = (𝐺‘(𝐹‘(𝑁 + 1)))) |
313 | 312 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐾 = (𝑁 + 1)) → ((𝐺 ∘ 𝐹)‘(𝑁 + 1)) = (𝐺‘(𝐹‘(𝑁 + 1)))) |
314 | | simpr 488 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐾 = (𝑁 + 1)) → 𝐾 = (𝑁 + 1)) |
315 | 17, 314 | eqtr3id 2788 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐾 = (𝑁 + 1)) → (◡𝐹‘(𝑁 + 1)) = (𝑁 + 1)) |
316 | 315 | fveq2d 6681 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐾 = (𝑁 + 1)) → (𝐹‘(◡𝐹‘(𝑁 + 1))) = (𝐹‘(𝑁 + 1))) |
317 | 142 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐾 = (𝑁 + 1)) → (𝐹‘(◡𝐹‘(𝑁 + 1))) = (𝑁 + 1)) |
318 | 316, 317 | eqtr3d 2776 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐾 = (𝑁 + 1)) → (𝐹‘(𝑁 + 1)) = (𝑁 + 1)) |
319 | 318 | fveq2d 6681 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐾 = (𝑁 + 1)) → (𝐺‘(𝐹‘(𝑁 + 1))) = (𝐺‘(𝑁 + 1))) |
320 | 313, 319 | eqtrd 2774 |
. . . . 5
⊢ ((𝜑 ∧ 𝐾 = (𝑁 + 1)) → ((𝐺 ∘ 𝐹)‘(𝑁 + 1)) = (𝐺‘(𝑁 + 1))) |
321 | 310, 320 | oveq12d 7191 |
. . . 4
⊢ ((𝜑 ∧ 𝐾 = (𝑁 + 1)) → ((seq𝑀( + , (𝐺 ∘ 𝐹))‘𝑁) + ((𝐺 ∘ 𝐹)‘(𝑁 + 1))) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1)))) |
322 | 266, 321 | eqtrd 2774 |
. . 3
⊢ ((𝜑 ∧ 𝐾 = (𝑁 + 1)) → (seq𝑀( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1)) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1)))) |
323 | | elfzp1 13051 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝐾 ∈ (𝑀...(𝑁 + 1)) ↔ (𝐾 ∈ (𝑀...𝑁) ∨ 𝐾 = (𝑁 + 1)))) |
324 | 13, 323 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐾 ∈ (𝑀...(𝑁 + 1)) ↔ (𝐾 ∈ (𝑀...𝑁) ∨ 𝐾 = (𝑁 + 1)))) |
325 | 77, 324 | mpbid 235 |
. . 3
⊢ (𝜑 → (𝐾 ∈ (𝑀...𝑁) ∨ 𝐾 = (𝑁 + 1))) |
326 | 263, 322,
325 | mpjaodan 958 |
. 2
⊢ (𝜑 → (seq𝑀( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1)) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1)))) |
327 | | seqp1 13478 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (seq𝑀( + , 𝐺)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐺)‘𝑁) + (𝐺‘(𝑁 + 1)))) |
328 | 13, 327 | syl 17 |
. 2
⊢ (𝜑 → (seq𝑀( + , 𝐺)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐺)‘𝑁) + (𝐺‘(𝑁 + 1)))) |
329 | 47, 326, 328 | 3eqtr4d 2784 |
1
⊢ (𝜑 → (seq𝑀( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1)) = (seq𝑀( + , 𝐺)‘(𝑁 + 1))) |