Proof of Theorem seqf1olem2
Step | Hyp | Ref
| Expression |
1 | | seqf1olem.6 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺:(𝑀...(𝑁 + 1))⟶𝐶) |
2 | | ffn 5958 |
. . . . . . . . . 10
⊢ (𝐺:(𝑀...(𝑁 + 1))⟶𝐶 → 𝐺 Fn (𝑀...(𝑁 + 1))) |
3 | 1, 2 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 Fn (𝑀...(𝑁 + 1))) |
4 | | fzssp1 12255 |
. . . . . . . . 9
⊢ (𝑀...𝑁) ⊆ (𝑀...(𝑁 + 1)) |
5 | | fnssres 5918 |
. . . . . . . . 9
⊢ ((𝐺 Fn (𝑀...(𝑁 + 1)) ∧ (𝑀...𝑁) ⊆ (𝑀...(𝑁 + 1))) → (𝐺 ↾ (𝑀...𝑁)) Fn (𝑀...𝑁)) |
6 | 3, 4, 5 | sylancl 693 |
. . . . . . . 8
⊢ (𝜑 → (𝐺 ↾ (𝑀...𝑁)) Fn (𝑀...𝑁)) |
7 | | fzfid 12634 |
. . . . . . . 8
⊢ (𝜑 → (𝑀...𝑁) ∈ Fin) |
8 | | fnfi 8123 |
. . . . . . . 8
⊢ (((𝐺 ↾ (𝑀...𝑁)) Fn (𝑀...𝑁) ∧ (𝑀...𝑁) ∈ Fin) → (𝐺 ↾ (𝑀...𝑁)) ∈ Fin) |
9 | 6, 7, 8 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (𝐺 ↾ (𝑀...𝑁)) ∈ Fin) |
10 | | elex 3185 |
. . . . . . 7
⊢ ((𝐺 ↾ (𝑀...𝑁)) ∈ Fin → (𝐺 ↾ (𝑀...𝑁)) ∈ V) |
11 | 9, 10 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐺 ↾ (𝑀...𝑁)) ∈ V) |
12 | | seqf1o.1 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
13 | | seqf1o.2 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) |
14 | | seqf1o.3 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) |
15 | | seqf1o.4 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
16 | | seqf1o.5 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ⊆ 𝑆) |
17 | | seqf1olem.5 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1))) |
18 | | seqf1olem.7 |
. . . . . . . . 9
⊢ 𝐽 = (𝑘 ∈ (𝑀...𝑁) ↦ (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))) |
19 | | seqf1olem.8 |
. . . . . . . . 9
⊢ 𝐾 = (◡𝐹‘(𝑁 + 1)) |
20 | 12, 13, 14, 15, 16, 17, 1, 18, 19 | seqf1olem1 12702 |
. . . . . . . 8
⊢ (𝜑 → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) |
21 | | f1of 6050 |
. . . . . . . 8
⊢ (𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) → 𝐽:(𝑀...𝑁)⟶(𝑀...𝑁)) |
22 | 20, 21 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐽:(𝑀...𝑁)⟶(𝑀...𝑁)) |
23 | | fex2 7014 |
. . . . . . 7
⊢ ((𝐽:(𝑀...𝑁)⟶(𝑀...𝑁) ∧ (𝑀...𝑁) ∈ Fin ∧ (𝑀...𝑁) ∈ Fin) → 𝐽 ∈ V) |
24 | 22, 7, 7, 23 | syl3anc 1318 |
. . . . . 6
⊢ (𝜑 → 𝐽 ∈ V) |
25 | 11, 24 | jca 553 |
. . . . 5
⊢ (𝜑 → ((𝐺 ↾ (𝑀...𝑁)) ∈ V ∧ 𝐽 ∈ V)) |
26 | | seqf1olem.9 |
. . . . 5
⊢ (𝜑 → ∀𝑔∀𝑓((𝑓:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ 𝑔:(𝑀...𝑁)⟶𝐶) → (seq𝑀( + , (𝑔 ∘ 𝑓))‘𝑁) = (seq𝑀( + , 𝑔)‘𝑁))) |
27 | | fssres 5983 |
. . . . . . 7
⊢ ((𝐺:(𝑀...(𝑁 + 1))⟶𝐶 ∧ (𝑀...𝑁) ⊆ (𝑀...(𝑁 + 1))) → (𝐺 ↾ (𝑀...𝑁)):(𝑀...𝑁)⟶𝐶) |
28 | 1, 4, 27 | sylancl 693 |
. . . . . 6
⊢ (𝜑 → (𝐺 ↾ (𝑀...𝑁)):(𝑀...𝑁)⟶𝐶) |
29 | 20, 28 | jca 553 |
. . . . 5
⊢ (𝜑 → (𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ (𝐺 ↾ (𝑀...𝑁)):(𝑀...𝑁)⟶𝐶)) |
30 | | f1oeq1 6040 |
. . . . . . . 8
⊢ (𝑓 = 𝐽 → (𝑓:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ↔ 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))) |
31 | | feq1 5939 |
. . . . . . . 8
⊢ (𝑔 = (𝐺 ↾ (𝑀...𝑁)) → (𝑔:(𝑀...𝑁)⟶𝐶 ↔ (𝐺 ↾ (𝑀...𝑁)):(𝑀...𝑁)⟶𝐶)) |
32 | 30, 31 | bi2anan9r 914 |
. . . . . . 7
⊢ ((𝑔 = (𝐺 ↾ (𝑀...𝑁)) ∧ 𝑓 = 𝐽) → ((𝑓:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ 𝑔:(𝑀...𝑁)⟶𝐶) ↔ (𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ (𝐺 ↾ (𝑀...𝑁)):(𝑀...𝑁)⟶𝐶))) |
33 | | coeq1 5201 |
. . . . . . . . . . 11
⊢ (𝑔 = (𝐺 ↾ (𝑀...𝑁)) → (𝑔 ∘ 𝑓) = ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝑓)) |
34 | | coeq2 5202 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝐽 → ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝑓) = ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)) |
35 | 33, 34 | sylan9eq 2664 |
. . . . . . . . . 10
⊢ ((𝑔 = (𝐺 ↾ (𝑀...𝑁)) ∧ 𝑓 = 𝐽) → (𝑔 ∘ 𝑓) = ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)) |
36 | 35 | seqeq3d 12671 |
. . . . . . . . 9
⊢ ((𝑔 = (𝐺 ↾ (𝑀...𝑁)) ∧ 𝑓 = 𝐽) → seq𝑀( + , (𝑔 ∘ 𝑓)) = seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))) |
37 | 36 | fveq1d 6105 |
. . . . . . . 8
⊢ ((𝑔 = (𝐺 ↾ (𝑀...𝑁)) ∧ 𝑓 = 𝐽) → (seq𝑀( + , (𝑔 ∘ 𝑓))‘𝑁) = (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁)) |
38 | | simpl 472 |
. . . . . . . . . 10
⊢ ((𝑔 = (𝐺 ↾ (𝑀...𝑁)) ∧ 𝑓 = 𝐽) → 𝑔 = (𝐺 ↾ (𝑀...𝑁))) |
39 | 38 | seqeq3d 12671 |
. . . . . . . . 9
⊢ ((𝑔 = (𝐺 ↾ (𝑀...𝑁)) ∧ 𝑓 = 𝐽) → seq𝑀( + , 𝑔) = seq𝑀( + , (𝐺 ↾ (𝑀...𝑁)))) |
40 | 39 | fveq1d 6105 |
. . . . . . . 8
⊢ ((𝑔 = (𝐺 ↾ (𝑀...𝑁)) ∧ 𝑓 = 𝐽) → (seq𝑀( + , 𝑔)‘𝑁) = (seq𝑀( + , (𝐺 ↾ (𝑀...𝑁)))‘𝑁)) |
41 | 37, 40 | eqeq12d 2625 |
. . . . . . 7
⊢ ((𝑔 = (𝐺 ↾ (𝑀...𝑁)) ∧ 𝑓 = 𝐽) → ((seq𝑀( + , (𝑔 ∘ 𝑓))‘𝑁) = (seq𝑀( + , 𝑔)‘𝑁) ↔ (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) = (seq𝑀( + , (𝐺 ↾ (𝑀...𝑁)))‘𝑁))) |
42 | 32, 41 | imbi12d 333 |
. . . . . 6
⊢ ((𝑔 = (𝐺 ↾ (𝑀...𝑁)) ∧ 𝑓 = 𝐽) → (((𝑓:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ 𝑔:(𝑀...𝑁)⟶𝐶) → (seq𝑀( + , (𝑔 ∘ 𝑓))‘𝑁) = (seq𝑀( + , 𝑔)‘𝑁)) ↔ ((𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ (𝐺 ↾ (𝑀...𝑁)):(𝑀...𝑁)⟶𝐶) → (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) = (seq𝑀( + , (𝐺 ↾ (𝑀...𝑁)))‘𝑁)))) |
43 | 42 | spc2gv 3269 |
. . . . 5
⊢ (((𝐺 ↾ (𝑀...𝑁)) ∈ V ∧ 𝐽 ∈ V) → (∀𝑔∀𝑓((𝑓:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ 𝑔:(𝑀...𝑁)⟶𝐶) → (seq𝑀( + , (𝑔 ∘ 𝑓))‘𝑁) = (seq𝑀( + , 𝑔)‘𝑁)) → ((𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ (𝐺 ↾ (𝑀...𝑁)):(𝑀...𝑁)⟶𝐶) → (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) = (seq𝑀( + , (𝐺 ↾ (𝑀...𝑁)))‘𝑁)))) |
44 | 25, 26, 29, 43 | syl3c 64 |
. . . 4
⊢ (𝜑 → (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) = (seq𝑀( + , (𝐺 ↾ (𝑀...𝑁)))‘𝑁)) |
45 | | fvres 6117 |
. . . . . 6
⊢ (𝑥 ∈ (𝑀...𝑁) → ((𝐺 ↾ (𝑀...𝑁))‘𝑥) = (𝐺‘𝑥)) |
46 | 45 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐺 ↾ (𝑀...𝑁))‘𝑥) = (𝐺‘𝑥)) |
47 | 15, 46 | seqfveq 12687 |
. . . 4
⊢ (𝜑 → (seq𝑀( + , (𝐺 ↾ (𝑀...𝑁)))‘𝑁) = (seq𝑀( + , 𝐺)‘𝑁)) |
48 | 44, 47 | eqtrd 2644 |
. . 3
⊢ (𝜑 → (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) = (seq𝑀( + , 𝐺)‘𝑁)) |
49 | 48 | oveq1d 6564 |
. 2
⊢ (𝜑 → ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))) = ((seq𝑀( + , 𝐺)‘𝑁) + (𝐺‘(𝑁 + 1)))) |
50 | 12 | adantlr 747 |
. . . . 5
⊢ (((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
51 | 14 | adantlr 747 |
. . . . 5
⊢ (((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) |
52 | | elfzuz3 12210 |
. . . . . . 7
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝐾)) |
53 | 52 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) → 𝑁 ∈ (ℤ≥‘𝐾)) |
54 | | eluzp1p1 11589 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝐾) → (𝑁 + 1) ∈
(ℤ≥‘(𝐾 + 1))) |
55 | 53, 54 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) → (𝑁 + 1) ∈
(ℤ≥‘(𝐾 + 1))) |
56 | | elfzuz 12209 |
. . . . . 6
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ≥‘𝑀)) |
57 | 56 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) → 𝐾 ∈ (ℤ≥‘𝑀)) |
58 | | f1of 6050 |
. . . . . . . . . 10
⊢ (𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1))) |
59 | 17, 58 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1))) |
60 | | fco 5971 |
. . . . . . . . 9
⊢ ((𝐺:(𝑀...(𝑁 + 1))⟶𝐶 ∧ 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1))) → (𝐺 ∘ 𝐹):(𝑀...(𝑁 + 1))⟶𝐶) |
61 | 1, 59, 60 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → (𝐺 ∘ 𝐹):(𝑀...(𝑁 + 1))⟶𝐶) |
62 | 61, 16 | fssd 5970 |
. . . . . . 7
⊢ (𝜑 → (𝐺 ∘ 𝐹):(𝑀...(𝑁 + 1))⟶𝑆) |
63 | 62 | ffvelrnda 6267 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...(𝑁 + 1))) → ((𝐺 ∘ 𝐹)‘𝑥) ∈ 𝑆) |
64 | 63 | adantlr 747 |
. . . . 5
⊢ (((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) ∧ 𝑥 ∈ (𝑀...(𝑁 + 1))) → ((𝐺 ∘ 𝐹)‘𝑥) ∈ 𝑆) |
65 | 50, 51, 55, 57, 64 | seqsplit 12696 |
. . . 4
⊢ ((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) → (seq𝑀( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1)) = ((seq𝑀( + , (𝐺 ∘ 𝐹))‘𝐾) + (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1)))) |
66 | | elfzp12 12288 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 = 𝑀 ∨ 𝐾 ∈ ((𝑀 + 1)...𝑁)))) |
67 | 66 | biimpa 500 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝐾 ∈ (𝑀...𝑁)) → (𝐾 = 𝑀 ∨ 𝐾 ∈ ((𝑀 + 1)...𝑁))) |
68 | 15, 67 | sylan 487 |
. . . . 5
⊢ ((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) → (𝐾 = 𝑀 ∨ 𝐾 ∈ ((𝑀 + 1)...𝑁))) |
69 | | seqeq1 12666 |
. . . . . . . . . . 11
⊢ (𝐾 = 𝑀 → seq𝐾( + , (𝐺 ∘ 𝐹)) = seq𝑀( + , (𝐺 ∘ 𝐹))) |
70 | 69 | eqcomd 2616 |
. . . . . . . . . 10
⊢ (𝐾 = 𝑀 → seq𝑀( + , (𝐺 ∘ 𝐹)) = seq𝐾( + , (𝐺 ∘ 𝐹))) |
71 | 70 | fveq1d 6105 |
. . . . . . . . 9
⊢ (𝐾 = 𝑀 → (seq𝑀( + , (𝐺 ∘ 𝐹))‘𝐾) = (seq𝐾( + , (𝐺 ∘ 𝐹))‘𝐾)) |
72 | | f1ocnv 6062 |
. . . . . . . . . . . . 13
⊢ (𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) → ◡𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1))) |
73 | | f1of 6050 |
. . . . . . . . . . . . 13
⊢ (◡𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) → ◡𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1))) |
74 | 17, 72, 73 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → ◡𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1))) |
75 | | peano2uz 11617 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑁 + 1) ∈
(ℤ≥‘𝑀)) |
76 | | eluzfz2 12220 |
. . . . . . . . . . . . 13
⊢ ((𝑁 + 1) ∈
(ℤ≥‘𝑀) → (𝑁 + 1) ∈ (𝑀...(𝑁 + 1))) |
77 | 15, 75, 76 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 + 1) ∈ (𝑀...(𝑁 + 1))) |
78 | 74, 77 | ffvelrnd 6268 |
. . . . . . . . . . 11
⊢ (𝜑 → (◡𝐹‘(𝑁 + 1)) ∈ (𝑀...(𝑁 + 1))) |
79 | 19, 78 | syl5eqel 2692 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈ (𝑀...(𝑁 + 1))) |
80 | | elfzelz 12213 |
. . . . . . . . . 10
⊢ (𝐾 ∈ (𝑀...(𝑁 + 1)) → 𝐾 ∈ ℤ) |
81 | | seq1 12676 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℤ → (seq𝐾( + , (𝐺 ∘ 𝐹))‘𝐾) = ((𝐺 ∘ 𝐹)‘𝐾)) |
82 | 79, 80, 81 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → (seq𝐾( + , (𝐺 ∘ 𝐹))‘𝐾) = ((𝐺 ∘ 𝐹)‘𝐾)) |
83 | 71, 82 | sylan9eqr 2666 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐾 = 𝑀) → (seq𝑀( + , (𝐺 ∘ 𝐹))‘𝐾) = ((𝐺 ∘ 𝐹)‘𝐾)) |
84 | 83 | oveq1d 6564 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐾 = 𝑀) → ((seq𝑀( + , (𝐺 ∘ 𝐹))‘𝐾) + (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1))) = (((𝐺 ∘ 𝐹)‘𝐾) + (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1)))) |
85 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐾 = 𝑀) → 𝐾 = 𝑀) |
86 | | eluzfz1 12219 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁)) |
87 | 15, 86 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ (𝑀...𝑁)) |
88 | 87 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐾 = 𝑀) → 𝑀 ∈ (𝑀...𝑁)) |
89 | 85, 88 | eqeltrd 2688 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐾 = 𝑀) → 𝐾 ∈ (𝑀...𝑁)) |
90 | 13 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) |
91 | 16 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) → 𝐶 ⊆ 𝑆) |
92 | 61 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) → (𝐺 ∘ 𝐹):(𝑀...(𝑁 + 1))⟶𝐶) |
93 | 79 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) → 𝐾 ∈ (𝑀...(𝑁 + 1))) |
94 | | peano2uz 11617 |
. . . . . . . . . . 11
⊢ (𝐾 ∈
(ℤ≥‘𝑀) → (𝐾 + 1) ∈
(ℤ≥‘𝑀)) |
95 | | fzss1 12251 |
. . . . . . . . . . 11
⊢ ((𝐾 + 1) ∈
(ℤ≥‘𝑀) → ((𝐾 + 1)...(𝑁 + 1)) ⊆ (𝑀...(𝑁 + 1))) |
96 | 57, 94, 95 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) → ((𝐾 + 1)...(𝑁 + 1)) ⊆ (𝑀...(𝑁 + 1))) |
97 | 50, 90, 51, 55, 91, 92, 93, 96 | seqf1olem2a 12701 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) → (((𝐺 ∘ 𝐹)‘𝐾) + (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1))) = ((seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1)) + ((𝐺 ∘ 𝐹)‘𝐾))) |
98 | | 1zzd 11285 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) → 1 ∈ ℤ) |
99 | | elfzuz 12209 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐾 ∈ (𝑀...(𝑁 + 1)) → 𝐾 ∈ (ℤ≥‘𝑀)) |
100 | | fzss1 12251 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐾 ∈
(ℤ≥‘𝑀) → (𝐾...𝑁) ⊆ (𝑀...𝑁)) |
101 | 79, 99, 100 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐾...𝑁) ⊆ (𝑀...𝑁)) |
102 | 101 | sselda 3568 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑁)) → 𝑥 ∈ (𝑀...𝑁)) |
103 | 22 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐽‘𝑥) ∈ (𝑀...𝑁)) |
104 | 102, 103 | syldan 486 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑁)) → (𝐽‘𝑥) ∈ (𝑀...𝑁)) |
105 | | fvres 6117 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽‘𝑥) ∈ (𝑀...𝑁) → ((𝐺 ↾ (𝑀...𝑁))‘(𝐽‘𝑥)) = (𝐺‘(𝐽‘𝑥))) |
106 | 104, 105 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑁)) → ((𝐺 ↾ (𝑀...𝑁))‘(𝐽‘𝑥)) = (𝐺‘(𝐽‘𝑥))) |
107 | | breq1 4586 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑥 → (𝑘 < 𝐾 ↔ 𝑥 < 𝐾)) |
108 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑥 → 𝑘 = 𝑥) |
109 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑥 → (𝑘 + 1) = (𝑥 + 1)) |
110 | 107, 108,
109 | ifbieq12d 4063 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑥 → if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)) = if(𝑥 < 𝐾, 𝑥, (𝑥 + 1))) |
111 | 110 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑥 → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1)))) |
112 | | fvex 6113 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1))) ∈ V |
113 | 111, 18, 112 | fvmpt 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (𝑀...𝑁) → (𝐽‘𝑥) = (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1)))) |
114 | 102, 113 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑁)) → (𝐽‘𝑥) = (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1)))) |
115 | | elfzle1 12215 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (𝐾...𝑁) → 𝐾 ≤ 𝑥) |
116 | 115 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑁)) → 𝐾 ≤ 𝑥) |
117 | 79, 80 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐾 ∈ ℤ) |
118 | 117 | zred 11358 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐾 ∈ ℝ) |
119 | 118 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑁)) → 𝐾 ∈ ℝ) |
120 | | elfzelz 12213 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ (𝐾...𝑁) → 𝑥 ∈ ℤ) |
121 | 120 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑁)) → 𝑥 ∈ ℤ) |
122 | 121 | zred 11358 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑁)) → 𝑥 ∈ ℝ) |
123 | 119, 122 | lenltd 10062 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑁)) → (𝐾 ≤ 𝑥 ↔ ¬ 𝑥 < 𝐾)) |
124 | 116, 123 | mpbid 221 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑁)) → ¬ 𝑥 < 𝐾) |
125 | | iffalse 4045 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
𝑥 < 𝐾 → if(𝑥 < 𝐾, 𝑥, (𝑥 + 1)) = (𝑥 + 1)) |
126 | 125 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑥 < 𝐾 → (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1))) = (𝐹‘(𝑥 + 1))) |
127 | 124, 126 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑁)) → (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1))) = (𝐹‘(𝑥 + 1))) |
128 | 114, 127 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑁)) → (𝐽‘𝑥) = (𝐹‘(𝑥 + 1))) |
129 | 128 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑁)) → (𝐺‘(𝐽‘𝑥)) = (𝐺‘(𝐹‘(𝑥 + 1)))) |
130 | 106, 129 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑁)) → ((𝐺 ↾ (𝑀...𝑁))‘(𝐽‘𝑥)) = (𝐺‘(𝐹‘(𝑥 + 1)))) |
131 | | fvco3 6185 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽:(𝑀...𝑁)⟶(𝑀...𝑁) ∧ 𝑥 ∈ (𝑀...𝑁)) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) = ((𝐺 ↾ (𝑀...𝑁))‘(𝐽‘𝑥))) |
132 | 22, 131 | sylan 487 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) = ((𝐺 ↾ (𝑀...𝑁))‘(𝐽‘𝑥))) |
133 | 102, 132 | syldan 486 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑁)) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) = ((𝐺 ↾ (𝑀...𝑁))‘(𝐽‘𝑥))) |
134 | | fzp1elp1 12264 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝑀...𝑁) → (𝑥 + 1) ∈ (𝑀...(𝑁 + 1))) |
135 | 102, 134 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑁)) → (𝑥 + 1) ∈ (𝑀...(𝑁 + 1))) |
136 | | fvco3 6185 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)) ∧ (𝑥 + 1) ∈ (𝑀...(𝑁 + 1))) → ((𝐺 ∘ 𝐹)‘(𝑥 + 1)) = (𝐺‘(𝐹‘(𝑥 + 1)))) |
137 | 59, 136 | sylan 487 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 + 1) ∈ (𝑀...(𝑁 + 1))) → ((𝐺 ∘ 𝐹)‘(𝑥 + 1)) = (𝐺‘(𝐹‘(𝑥 + 1)))) |
138 | 135, 137 | syldan 486 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑁)) → ((𝐺 ∘ 𝐹)‘(𝑥 + 1)) = (𝐺‘(𝐹‘(𝑥 + 1)))) |
139 | 130, 133,
138 | 3eqtr4d 2654 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑁)) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) = ((𝐺 ∘ 𝐹)‘(𝑥 + 1))) |
140 | 139 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) ∧ 𝑥 ∈ (𝐾...𝑁)) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) = ((𝐺 ∘ 𝐹)‘(𝑥 + 1))) |
141 | 53, 98, 140 | seqshft2 12689 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) → (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) = (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1))) |
142 | | fvco3 6185 |
. . . . . . . . . . . . 13
⊢ ((𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)) ∧ 𝐾 ∈ (𝑀...(𝑁 + 1))) → ((𝐺 ∘ 𝐹)‘𝐾) = (𝐺‘(𝐹‘𝐾))) |
143 | 59, 79, 142 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐺 ∘ 𝐹)‘𝐾) = (𝐺‘(𝐹‘𝐾))) |
144 | 19 | fveq2i 6106 |
. . . . . . . . . . . . . 14
⊢ (𝐹‘𝐾) = (𝐹‘(◡𝐹‘(𝑁 + 1))) |
145 | | f1ocnvfv2 6433 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ (𝑁 + 1) ∈ (𝑀...(𝑁 + 1))) → (𝐹‘(◡𝐹‘(𝑁 + 1))) = (𝑁 + 1)) |
146 | 17, 77, 145 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹‘(◡𝐹‘(𝑁 + 1))) = (𝑁 + 1)) |
147 | 144, 146 | syl5eq 2656 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹‘𝐾) = (𝑁 + 1)) |
148 | 147 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐺‘(𝐹‘𝐾)) = (𝐺‘(𝑁 + 1))) |
149 | 143, 148 | eqtr2d 2645 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺‘(𝑁 + 1)) = ((𝐺 ∘ 𝐹)‘𝐾)) |
150 | 149 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) → (𝐺‘(𝑁 + 1)) = ((𝐺 ∘ 𝐹)‘𝐾)) |
151 | 141, 150 | oveq12d 6567 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) → ((seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))) = ((seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1)) + ((𝐺 ∘ 𝐹)‘𝐾))) |
152 | 97, 151 | eqtr4d 2647 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) → (((𝐺 ∘ 𝐹)‘𝐾) + (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1))) = ((seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1)))) |
153 | 89, 152 | syldan 486 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐾 = 𝑀) → (((𝐺 ∘ 𝐹)‘𝐾) + (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1))) = ((seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1)))) |
154 | 85 | seqeq1d 12669 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐾 = 𝑀) → seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)) = seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))) |
155 | 154 | fveq1d 6105 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐾 = 𝑀) → (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) = (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁)) |
156 | 155 | oveq1d 6564 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐾 = 𝑀) → ((seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1)))) |
157 | 84, 153, 156 | 3eqtrd 2648 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐾 = 𝑀) → ((seq𝑀( + , (𝐺 ∘ 𝐹))‘𝐾) + (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1))) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1)))) |
158 | | eluzel2 11568 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
159 | 15, 158 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℤ) |
160 | | elfzuz 12209 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ ((𝑀 + 1)...𝑁) → 𝐾 ∈ (ℤ≥‘(𝑀 + 1))) |
161 | | eluzp1m1 11587 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈
(ℤ≥‘(𝑀 + 1))) → (𝐾 − 1) ∈
(ℤ≥‘𝑀)) |
162 | 159, 160,
161 | syl2an 493 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → (𝐾 − 1) ∈
(ℤ≥‘𝑀)) |
163 | | eluzelz 11573 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
164 | 15, 163 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑁 ∈ ℤ) |
165 | 164 | zcnd 11359 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈ ℂ) |
166 | | ax-1cn 9873 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℂ |
167 | | pncan 10166 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 + 1)
− 1) = 𝑁) |
168 | 165, 166,
167 | sylancl 693 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑁 + 1) − 1) = 𝑁) |
169 | | peano2zm 11297 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐾 ∈ ℤ → (𝐾 − 1) ∈
ℤ) |
170 | 79, 80, 169 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐾 − 1) ∈ ℤ) |
171 | | elfzuz3 12210 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐾 ∈ (𝑀...(𝑁 + 1)) → (𝑁 + 1) ∈
(ℤ≥‘𝐾)) |
172 | 79, 171 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑁 + 1) ∈
(ℤ≥‘𝐾)) |
173 | 117 | zcnd 11359 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝐾 ∈ ℂ) |
174 | | npcan 10169 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐾 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝐾 −
1) + 1) = 𝐾) |
175 | 173, 166,
174 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝐾 − 1) + 1) = 𝐾) |
176 | 175 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 →
(ℤ≥‘((𝐾 − 1) + 1)) =
(ℤ≥‘𝐾)) |
177 | 172, 176 | eleqtrrd 2691 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑁 + 1) ∈
(ℤ≥‘((𝐾 − 1) + 1))) |
178 | | eluzp1m1 11587 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐾 − 1) ∈ ℤ ∧
(𝑁 + 1) ∈
(ℤ≥‘((𝐾 − 1) + 1))) → ((𝑁 + 1) − 1) ∈
(ℤ≥‘(𝐾 − 1))) |
179 | 170, 177,
178 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑁 + 1) − 1) ∈
(ℤ≥‘(𝐾 − 1))) |
180 | 168, 179 | eqeltrrd 2689 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝐾 − 1))) |
181 | | fzss2 12252 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈
(ℤ≥‘(𝐾 − 1)) → (𝑀...(𝐾 − 1)) ⊆ (𝑀...𝑁)) |
182 | 180, 181 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑀...(𝐾 − 1)) ⊆ (𝑀...𝑁)) |
183 | 182 | sselda 3568 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → 𝑥 ∈ (𝑀...𝑁)) |
184 | 183, 103 | syldan 486 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → (𝐽‘𝑥) ∈ (𝑀...𝑁)) |
185 | 184, 105 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → ((𝐺 ↾ (𝑀...𝑁))‘(𝐽‘𝑥)) = (𝐺‘(𝐽‘𝑥))) |
186 | 183, 113 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → (𝐽‘𝑥) = (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1)))) |
187 | | elfzm11 12280 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑥 ∈ (𝑀...(𝐾 − 1)) ↔ (𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥 ∧ 𝑥 < 𝐾))) |
188 | 159, 117,
187 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑥 ∈ (𝑀...(𝐾 − 1)) ↔ (𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥 ∧ 𝑥 < 𝐾))) |
189 | 188 | biimpa 500 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → (𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥 ∧ 𝑥 < 𝐾)) |
190 | 189 | simp3d 1068 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → 𝑥 < 𝐾) |
191 | | iftrue 4042 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 < 𝐾 → if(𝑥 < 𝐾, 𝑥, (𝑥 + 1)) = 𝑥) |
192 | 191 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 < 𝐾 → (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1))) = (𝐹‘𝑥)) |
193 | 190, 192 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1))) = (𝐹‘𝑥)) |
194 | 186, 193 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → (𝐽‘𝑥) = (𝐹‘𝑥)) |
195 | 194 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → (𝐺‘(𝐽‘𝑥)) = (𝐺‘(𝐹‘𝑥))) |
196 | 185, 195 | eqtr2d 2645 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → (𝐺‘(𝐹‘𝑥)) = ((𝐺 ↾ (𝑀...𝑁))‘(𝐽‘𝑥))) |
197 | | peano2uz 11617 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘(𝐾 − 1)) → (𝑁 + 1) ∈
(ℤ≥‘(𝐾 − 1))) |
198 | | fzss2 12252 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 + 1) ∈
(ℤ≥‘(𝐾 − 1)) → (𝑀...(𝐾 − 1)) ⊆ (𝑀...(𝑁 + 1))) |
199 | 180, 197,
198 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀...(𝐾 − 1)) ⊆ (𝑀...(𝑁 + 1))) |
200 | 199 | sselda 3568 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → 𝑥 ∈ (𝑀...(𝑁 + 1))) |
201 | | fvco3 6185 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...(𝑁 + 1))) → ((𝐺 ∘ 𝐹)‘𝑥) = (𝐺‘(𝐹‘𝑥))) |
202 | 59, 201 | sylan 487 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...(𝑁 + 1))) → ((𝐺 ∘ 𝐹)‘𝑥) = (𝐺‘(𝐹‘𝑥))) |
203 | 200, 202 | syldan 486 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → ((𝐺 ∘ 𝐹)‘𝑥) = (𝐺‘(𝐹‘𝑥))) |
204 | 183, 132 | syldan 486 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) = ((𝐺 ↾ (𝑀...𝑁))‘(𝐽‘𝑥))) |
205 | 196, 203,
204 | 3eqtr4d 2654 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → ((𝐺 ∘ 𝐹)‘𝑥) = (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥)) |
206 | 205 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → ((𝐺 ∘ 𝐹)‘𝑥) = (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥)) |
207 | 162, 206 | seqfveq 12687 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → (seq𝑀( + , (𝐺 ∘ 𝐹))‘(𝐾 − 1)) = (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1))) |
208 | | fzp1ss 12262 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℤ → ((𝑀 + 1)...𝑁) ⊆ (𝑀...𝑁)) |
209 | 15, 158, 208 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑀 + 1)...𝑁) ⊆ (𝑀...𝑁)) |
210 | 209 | sselda 3568 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → 𝐾 ∈ (𝑀...𝑁)) |
211 | 210, 152 | syldan 486 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → (((𝐺 ∘ 𝐹)‘𝐾) + (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1))) = ((seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1)))) |
212 | 207, 211 | oveq12d 6567 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → ((seq𝑀( + , (𝐺 ∘ 𝐹))‘(𝐾 − 1)) + (((𝐺 ∘ 𝐹)‘𝐾) + (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1)))) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + ((seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))))) |
213 | 200, 63 | syldan 486 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → ((𝐺 ∘ 𝐹)‘𝑥) ∈ 𝑆) |
214 | 213 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → ((𝐺 ∘ 𝐹)‘𝑥) ∈ 𝑆) |
215 | 12 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
216 | 162, 214,
215 | seqcl 12683 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → (seq𝑀( + , (𝐺 ∘ 𝐹))‘(𝐾 − 1)) ∈ 𝑆) |
217 | 61, 79 | ffvelrnd 6268 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐺 ∘ 𝐹)‘𝐾) ∈ 𝐶) |
218 | 16, 217 | sseldd 3569 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐺 ∘ 𝐹)‘𝐾) ∈ 𝑆) |
219 | 218 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → ((𝐺 ∘ 𝐹)‘𝐾) ∈ 𝑆) |
220 | 96 | sselda 3568 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) ∧ 𝑥 ∈ ((𝐾 + 1)...(𝑁 + 1))) → 𝑥 ∈ (𝑀...(𝑁 + 1))) |
221 | 220, 64 | syldan 486 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) ∧ 𝑥 ∈ ((𝐾 + 1)...(𝑁 + 1))) → ((𝐺 ∘ 𝐹)‘𝑥) ∈ 𝑆) |
222 | 55, 221, 50 | seqcl 12683 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) → (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1)) ∈ 𝑆) |
223 | 210, 222 | syldan 486 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1)) ∈ 𝑆) |
224 | 216, 219,
223 | 3jca 1235 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → ((seq𝑀( + , (𝐺 ∘ 𝐹))‘(𝐾 − 1)) ∈ 𝑆 ∧ ((𝐺 ∘ 𝐹)‘𝐾) ∈ 𝑆 ∧ (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1)) ∈ 𝑆)) |
225 | 14 | caovassg 6730 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((seq𝑀( + , (𝐺 ∘ 𝐹))‘(𝐾 − 1)) ∈ 𝑆 ∧ ((𝐺 ∘ 𝐹)‘𝐾) ∈ 𝑆 ∧ (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1)) ∈ 𝑆)) → (((seq𝑀( + , (𝐺 ∘ 𝐹))‘(𝐾 − 1)) + ((𝐺 ∘ 𝐹)‘𝐾)) + (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1))) = ((seq𝑀( + , (𝐺 ∘ 𝐹))‘(𝐾 − 1)) + (((𝐺 ∘ 𝐹)‘𝐾) + (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1))))) |
226 | 224, 225 | syldan 486 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → (((seq𝑀( + , (𝐺 ∘ 𝐹))‘(𝐾 − 1)) + ((𝐺 ∘ 𝐹)‘𝐾)) + (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1))) = ((seq𝑀( + , (𝐺 ∘ 𝐹))‘(𝐾 − 1)) + (((𝐺 ∘ 𝐹)‘𝐾) + (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1))))) |
227 | 1, 16 | fssd 5970 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐺:(𝑀...(𝑁 + 1))⟶𝑆) |
228 | | fssres 5983 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺:(𝑀...(𝑁 + 1))⟶𝑆 ∧ (𝑀...𝑁) ⊆ (𝑀...(𝑁 + 1))) → (𝐺 ↾ (𝑀...𝑁)):(𝑀...𝑁)⟶𝑆) |
229 | 227, 4, 228 | sylancl 693 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐺 ↾ (𝑀...𝑁)):(𝑀...𝑁)⟶𝑆) |
230 | | fco 5971 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ↾ (𝑀...𝑁)):(𝑀...𝑁)⟶𝑆 ∧ 𝐽:(𝑀...𝑁)⟶(𝑀...𝑁)) → ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽):(𝑀...𝑁)⟶𝑆) |
231 | 229, 22, 230 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽):(𝑀...𝑁)⟶𝑆) |
232 | 231 | ffvelrnda 6267 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) ∈ 𝑆) |
233 | 183, 232 | syldan 486 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) ∈ 𝑆) |
234 | 233 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) ∈ 𝑆) |
235 | 162, 234,
215 | seqcl 12683 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) ∈ 𝑆) |
236 | | elfzuz3 12210 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ ((𝑀 + 1)...𝑁) → 𝑁 ∈ (ℤ≥‘𝐾)) |
237 | 236 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → 𝑁 ∈ (ℤ≥‘𝐾)) |
238 | 102, 232 | syldan 486 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑁)) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) ∈ 𝑆) |
239 | 238 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) ∧ 𝑥 ∈ (𝐾...𝑁)) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) ∈ 𝑆) |
240 | 237, 239,
215 | seqcl 12683 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) ∈ 𝑆) |
241 | 227, 77 | ffvelrnd 6268 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺‘(𝑁 + 1)) ∈ 𝑆) |
242 | 241 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → (𝐺‘(𝑁 + 1)) ∈ 𝑆) |
243 | 235, 240,
242 | 3jca 1235 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) ∈ 𝑆 ∧ (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) ∈ 𝑆 ∧ (𝐺‘(𝑁 + 1)) ∈ 𝑆)) |
244 | 14 | caovassg 6730 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) ∈ 𝑆 ∧ (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) ∈ 𝑆 ∧ (𝐺‘(𝑁 + 1)) ∈ 𝑆)) → (((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁)) + (𝐺‘(𝑁 + 1))) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + ((seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))))) |
245 | 243, 244 | syldan 486 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → (((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁)) + (𝐺‘(𝑁 + 1))) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + ((seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))))) |
246 | 212, 226,
245 | 3eqtr4d 2654 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → (((seq𝑀( + , (𝐺 ∘ 𝐹))‘(𝐾 − 1)) + ((𝐺 ∘ 𝐹)‘𝐾)) + (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1))) = (((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁)) + (𝐺‘(𝑁 + 1)))) |
247 | | seqm1 12680 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈
(ℤ≥‘(𝑀 + 1))) → (seq𝑀( + , (𝐺 ∘ 𝐹))‘𝐾) = ((seq𝑀( + , (𝐺 ∘ 𝐹))‘(𝐾 − 1)) + ((𝐺 ∘ 𝐹)‘𝐾))) |
248 | 159, 160,
247 | syl2an 493 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → (seq𝑀( + , (𝐺 ∘ 𝐹))‘𝐾) = ((seq𝑀( + , (𝐺 ∘ 𝐹))‘(𝐾 − 1)) + ((𝐺 ∘ 𝐹)‘𝐾))) |
249 | 248 | oveq1d 6564 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → ((seq𝑀( + , (𝐺 ∘ 𝐹))‘𝐾) + (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1))) = (((seq𝑀( + , (𝐺 ∘ 𝐹))‘(𝐾 − 1)) + ((𝐺 ∘ 𝐹)‘𝐾)) + (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1)))) |
250 | 14 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) |
251 | | elfzelz 12213 |
. . . . . . . . . . . . . . 15
⊢ (𝐾 ∈ ((𝑀 + 1)...𝑁) → 𝐾 ∈ ℤ) |
252 | 251 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → 𝐾 ∈ ℤ) |
253 | 252 | zcnd 11359 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → 𝐾 ∈ ℂ) |
254 | 253, 166,
174 | sylancl 693 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → ((𝐾 − 1) + 1) = 𝐾) |
255 | 254 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) →
(ℤ≥‘((𝐾 − 1) + 1)) =
(ℤ≥‘𝐾)) |
256 | 237, 255 | eleqtrrd 2691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → 𝑁 ∈
(ℤ≥‘((𝐾 − 1) + 1))) |
257 | 232 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) ∈ 𝑆) |
258 | 215, 250,
256, 162, 257 | seqsplit 12696 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + (seq((𝐾 − 1) + 1)( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁))) |
259 | 254 | seqeq1d 12669 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → seq((𝐾 − 1) + 1)( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)) = seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))) |
260 | 259 | fveq1d 6105 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → (seq((𝐾 − 1) + 1)( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) = (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁)) |
261 | 260 | oveq2d 6565 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + (seq((𝐾 − 1) + 1)( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁)) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁))) |
262 | 258, 261 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁))) |
263 | 262 | oveq1d 6564 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))) = (((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁)) + (𝐺‘(𝑁 + 1)))) |
264 | 246, 249,
263 | 3eqtr4d 2654 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐾 ∈ ((𝑀 + 1)...𝑁)) → ((seq𝑀( + , (𝐺 ∘ 𝐹))‘𝐾) + (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1))) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1)))) |
265 | 157, 264 | jaodan 822 |
. . . . 5
⊢ ((𝜑 ∧ (𝐾 = 𝑀 ∨ 𝐾 ∈ ((𝑀 + 1)...𝑁))) → ((seq𝑀( + , (𝐺 ∘ 𝐹))‘𝐾) + (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1))) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1)))) |
266 | 68, 265 | syldan 486 |
. . . 4
⊢ ((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) → ((seq𝑀( + , (𝐺 ∘ 𝐹))‘𝐾) + (seq(𝐾 + 1)( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1))) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1)))) |
267 | 65, 266 | eqtrd 2644 |
. . 3
⊢ ((𝜑 ∧ 𝐾 ∈ (𝑀...𝑁)) → (seq𝑀( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1)) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1)))) |
268 | 15 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐾 = (𝑁 + 1)) → 𝑁 ∈ (ℤ≥‘𝑀)) |
269 | | seqp1 12678 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (seq𝑀( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1)) = ((seq𝑀( + , (𝐺 ∘ 𝐹))‘𝑁) + ((𝐺 ∘ 𝐹)‘(𝑁 + 1)))) |
270 | 268, 269 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝐾 = (𝑁 + 1)) → (seq𝑀( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1)) = ((seq𝑀( + , (𝐺 ∘ 𝐹))‘𝑁) + ((𝐺 ∘ 𝐹)‘(𝑁 + 1)))) |
271 | 113 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐽‘𝑥) = (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1)))) |
272 | | elfzelz 12213 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (𝑀...𝑁) → 𝑥 ∈ ℤ) |
273 | 272 | zred 11358 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝑀...𝑁) → 𝑥 ∈ ℝ) |
274 | 273 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ ℝ) |
275 | 164 | zred 11358 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈ ℝ) |
276 | 275 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑁 ∈ ℝ) |
277 | | peano2re 10088 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℝ → (𝑁 + 1) ∈
ℝ) |
278 | 276, 277 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝑁 + 1) ∈ ℝ) |
279 | | elfzle2 12216 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝑀...𝑁) → 𝑥 ≤ 𝑁) |
280 | 279 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ≤ 𝑁) |
281 | 276 | ltp1d 10833 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑁 < (𝑁 + 1)) |
282 | 274, 276,
278, 280, 281 | lelttrd 10074 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 < (𝑁 + 1)) |
283 | 282 | adantlr 747 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 < (𝑁 + 1)) |
284 | | simplr 788 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝐾 = (𝑁 + 1)) |
285 | 283, 284 | breqtrrd 4611 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 < 𝐾) |
286 | 285, 192 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1))) = (𝐹‘𝑥)) |
287 | 271, 286 | eqtrd 2644 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐽‘𝑥) = (𝐹‘𝑥)) |
288 | 287 | fveq2d 6107 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐺 ↾ (𝑀...𝑁))‘(𝐽‘𝑥)) = ((𝐺 ↾ (𝑀...𝑁))‘(𝐹‘𝑥))) |
289 | 273 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ ℝ) |
290 | 289, 285 | gtned 10051 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝐾 ≠ 𝑥) |
291 | 59 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1))) |
292 | | fzelp1 12263 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (𝑀...𝑁) → 𝑥 ∈ (𝑀...(𝑁 + 1))) |
293 | 292 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ (𝑀...(𝑁 + 1))) |
294 | 291, 293 | ffvelrnd 6268 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) ∈ (𝑀...(𝑁 + 1))) |
295 | 15 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑁 ∈ (ℤ≥‘𝑀)) |
296 | | elfzp1 12261 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((𝐹‘𝑥) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘𝑥) ∈ (𝑀...𝑁) ∨ (𝐹‘𝑥) = (𝑁 + 1)))) |
297 | 295, 296 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐹‘𝑥) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘𝑥) ∈ (𝑀...𝑁) ∨ (𝐹‘𝑥) = (𝑁 + 1)))) |
298 | 294, 297 | mpbid 221 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐹‘𝑥) ∈ (𝑀...𝑁) ∨ (𝐹‘𝑥) = (𝑁 + 1))) |
299 | 298 | ord 391 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (¬ (𝐹‘𝑥) ∈ (𝑀...𝑁) → (𝐹‘𝑥) = (𝑁 + 1))) |
300 | 17 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1))) |
301 | | f1ocnvfv 6434 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...(𝑁 + 1))) → ((𝐹‘𝑥) = (𝑁 + 1) → (◡𝐹‘(𝑁 + 1)) = 𝑥)) |
302 | 300, 293,
301 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐹‘𝑥) = (𝑁 + 1) → (◡𝐹‘(𝑁 + 1)) = 𝑥)) |
303 | 19 | eqeq1i 2615 |
. . . . . . . . . . . . 13
⊢ (𝐾 = 𝑥 ↔ (◡𝐹‘(𝑁 + 1)) = 𝑥) |
304 | 302, 303 | syl6ibr 241 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐹‘𝑥) = (𝑁 + 1) → 𝐾 = 𝑥)) |
305 | 299, 304 | syld 46 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (¬ (𝐹‘𝑥) ∈ (𝑀...𝑁) → 𝐾 = 𝑥)) |
306 | 305 | necon1ad 2799 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐾 ≠ 𝑥 → (𝐹‘𝑥) ∈ (𝑀...𝑁))) |
307 | 290, 306 | mpd 15 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) ∈ (𝑀...𝑁)) |
308 | | fvres 6117 |
. . . . . . . . 9
⊢ ((𝐹‘𝑥) ∈ (𝑀...𝑁) → ((𝐺 ↾ (𝑀...𝑁))‘(𝐹‘𝑥)) = (𝐺‘(𝐹‘𝑥))) |
309 | 307, 308 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐺 ↾ (𝑀...𝑁))‘(𝐹‘𝑥)) = (𝐺‘(𝐹‘𝑥))) |
310 | 288, 309 | eqtr2d 2645 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐺‘(𝐹‘𝑥)) = ((𝐺 ↾ (𝑀...𝑁))‘(𝐽‘𝑥))) |
311 | 59, 292, 201 | syl2an 493 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐺 ∘ 𝐹)‘𝑥) = (𝐺‘(𝐹‘𝑥))) |
312 | 311 | adantlr 747 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐺 ∘ 𝐹)‘𝑥) = (𝐺‘(𝐹‘𝑥))) |
313 | 132 | adantlr 747 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) = ((𝐺 ↾ (𝑀...𝑁))‘(𝐽‘𝑥))) |
314 | 310, 312,
313 | 3eqtr4d 2654 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐺 ∘ 𝐹)‘𝑥) = (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥)) |
315 | 268, 314 | seqfveq 12687 |
. . . . 5
⊢ ((𝜑 ∧ 𝐾 = (𝑁 + 1)) → (seq𝑀( + , (𝐺 ∘ 𝐹))‘𝑁) = (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁)) |
316 | | fvco3 6185 |
. . . . . . . 8
⊢ ((𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)) ∧ (𝑁 + 1) ∈ (𝑀...(𝑁 + 1))) → ((𝐺 ∘ 𝐹)‘(𝑁 + 1)) = (𝐺‘(𝐹‘(𝑁 + 1)))) |
317 | 59, 77, 316 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → ((𝐺 ∘ 𝐹)‘(𝑁 + 1)) = (𝐺‘(𝐹‘(𝑁 + 1)))) |
318 | 317 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐾 = (𝑁 + 1)) → ((𝐺 ∘ 𝐹)‘(𝑁 + 1)) = (𝐺‘(𝐹‘(𝑁 + 1)))) |
319 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐾 = (𝑁 + 1)) → 𝐾 = (𝑁 + 1)) |
320 | 19, 319 | syl5eqr 2658 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐾 = (𝑁 + 1)) → (◡𝐹‘(𝑁 + 1)) = (𝑁 + 1)) |
321 | 320 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐾 = (𝑁 + 1)) → (𝐹‘(◡𝐹‘(𝑁 + 1))) = (𝐹‘(𝑁 + 1))) |
322 | 146 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐾 = (𝑁 + 1)) → (𝐹‘(◡𝐹‘(𝑁 + 1))) = (𝑁 + 1)) |
323 | 321, 322 | eqtr3d 2646 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐾 = (𝑁 + 1)) → (𝐹‘(𝑁 + 1)) = (𝑁 + 1)) |
324 | 323 | fveq2d 6107 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐾 = (𝑁 + 1)) → (𝐺‘(𝐹‘(𝑁 + 1))) = (𝐺‘(𝑁 + 1))) |
325 | 318, 324 | eqtrd 2644 |
. . . . 5
⊢ ((𝜑 ∧ 𝐾 = (𝑁 + 1)) → ((𝐺 ∘ 𝐹)‘(𝑁 + 1)) = (𝐺‘(𝑁 + 1))) |
326 | 315, 325 | oveq12d 6567 |
. . . 4
⊢ ((𝜑 ∧ 𝐾 = (𝑁 + 1)) → ((seq𝑀( + , (𝐺 ∘ 𝐹))‘𝑁) + ((𝐺 ∘ 𝐹)‘(𝑁 + 1))) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1)))) |
327 | 270, 326 | eqtrd 2644 |
. . 3
⊢ ((𝜑 ∧ 𝐾 = (𝑁 + 1)) → (seq𝑀( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1)) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1)))) |
328 | | elfzp1 12261 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝐾 ∈ (𝑀...(𝑁 + 1)) ↔ (𝐾 ∈ (𝑀...𝑁) ∨ 𝐾 = (𝑁 + 1)))) |
329 | 15, 328 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐾 ∈ (𝑀...(𝑁 + 1)) ↔ (𝐾 ∈ (𝑀...𝑁) ∨ 𝐾 = (𝑁 + 1)))) |
330 | 79, 329 | mpbid 221 |
. . 3
⊢ (𝜑 → (𝐾 ∈ (𝑀...𝑁) ∨ 𝐾 = (𝑁 + 1))) |
331 | 267, 327,
330 | mpjaodan 823 |
. 2
⊢ (𝜑 → (seq𝑀( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1)) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1)))) |
332 | | seqp1 12678 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (seq𝑀( + , 𝐺)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐺)‘𝑁) + (𝐺‘(𝑁 + 1)))) |
333 | 15, 332 | syl 17 |
. 2
⊢ (𝜑 → (seq𝑀( + , 𝐺)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐺)‘𝑁) + (𝐺‘(𝑁 + 1)))) |
334 | 49, 331, 333 | 3eqtr4d 2654 |
1
⊢ (𝜑 → (seq𝑀( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1)) = (seq𝑀( + , 𝐺)‘(𝑁 + 1))) |