Step | Hyp | Ref
| Expression |
1 | | iseqf1o.4 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
2 | | elfzle2 9930 |
. . . . . 6
⊢ (𝑘 ∈ (𝑀...𝑁) → 𝑘 ≤ 𝑁) |
3 | 2 | iftrued 3512 |
. . . . 5
⊢ (𝑘 ∈ (𝑀...𝑁) → if(𝑘 ≤ 𝑁, (𝐺‘(𝐹‘𝑘)), (𝐺‘𝑀)) = (𝐺‘(𝐹‘𝑘))) |
4 | 3 | adantl 275 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → if(𝑘 ≤ 𝑁, (𝐺‘(𝐹‘𝑘)), (𝐺‘𝑀)) = (𝐺‘(𝐹‘𝑘))) |
5 | | elfzuz 9924 |
. . . . 5
⊢ (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ (ℤ≥‘𝑀)) |
6 | | fveq2 5468 |
. . . . . . . 8
⊢ (𝑥 = (𝐹‘𝑘) → (𝐺‘𝑥) = (𝐺‘(𝐹‘𝑘))) |
7 | 6 | eleq1d 2226 |
. . . . . . 7
⊢ (𝑥 = (𝐹‘𝑘) → ((𝐺‘𝑥) ∈ 𝑆 ↔ (𝐺‘(𝐹‘𝑘)) ∈ 𝑆)) |
8 | | iseqf1o.7 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑥) ∈ 𝑆) |
9 | 8 | ralrimiva 2530 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ (ℤ≥‘𝑀)(𝐺‘𝑥) ∈ 𝑆) |
10 | 9 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → ∀𝑥 ∈ (ℤ≥‘𝑀)(𝐺‘𝑥) ∈ 𝑆) |
11 | | iseqf1o.6 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) |
12 | | f1of 5414 |
. . . . . . . . . 10
⊢ (𝐹:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) → 𝐹:(𝑀...𝑁)⟶(𝑀...𝑁)) |
13 | 11, 12 | syl 14 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:(𝑀...𝑁)⟶(𝑀...𝑁)) |
14 | 13 | ffvelrnda 5602 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ (𝑀...𝑁)) |
15 | | elfzuz 9924 |
. . . . . . . 8
⊢ ((𝐹‘𝑘) ∈ (𝑀...𝑁) → (𝐹‘𝑘) ∈ (ℤ≥‘𝑀)) |
16 | 14, 15 | syl 14 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ (ℤ≥‘𝑀)) |
17 | 7, 10, 16 | rspcdva 2821 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘(𝐹‘𝑘)) ∈ 𝑆) |
18 | 4, 17 | eqeltrd 2234 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → if(𝑘 ≤ 𝑁, (𝐺‘(𝐹‘𝑘)), (𝐺‘𝑀)) ∈ 𝑆) |
19 | | breq1 3968 |
. . . . . . 7
⊢ (𝑎 = 𝑘 → (𝑎 ≤ 𝑁 ↔ 𝑘 ≤ 𝑁)) |
20 | | 2fveq3 5473 |
. . . . . . 7
⊢ (𝑎 = 𝑘 → (𝐺‘(𝐹‘𝑎)) = (𝐺‘(𝐹‘𝑘))) |
21 | 19, 20 | ifbieq1d 3527 |
. . . . . 6
⊢ (𝑎 = 𝑘 → if(𝑎 ≤ 𝑁, (𝐺‘(𝐹‘𝑎)), (𝐺‘𝑀)) = if(𝑘 ≤ 𝑁, (𝐺‘(𝐹‘𝑘)), (𝐺‘𝑀))) |
22 | | eqid 2157 |
. . . . . 6
⊢ (𝑎 ∈
(ℤ≥‘𝑀) ↦ if(𝑎 ≤ 𝑁, (𝐺‘(𝐹‘𝑎)), (𝐺‘𝑀))) = (𝑎 ∈ (ℤ≥‘𝑀) ↦ if(𝑎 ≤ 𝑁, (𝐺‘(𝐹‘𝑎)), (𝐺‘𝑀))) |
23 | 21, 22 | fvmptg 5544 |
. . . . 5
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ if(𝑘 ≤ 𝑁, (𝐺‘(𝐹‘𝑘)), (𝐺‘𝑀)) ∈ 𝑆) → ((𝑎 ∈ (ℤ≥‘𝑀) ↦ if(𝑎 ≤ 𝑁, (𝐺‘(𝐹‘𝑎)), (𝐺‘𝑀)))‘𝑘) = if(𝑘 ≤ 𝑁, (𝐺‘(𝐹‘𝑘)), (𝐺‘𝑀))) |
24 | 5, 18, 23 | syl2an2 584 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → ((𝑎 ∈ (ℤ≥‘𝑀) ↦ if(𝑎 ≤ 𝑁, (𝐺‘(𝐹‘𝑎)), (𝐺‘𝑀)))‘𝑘) = if(𝑘 ≤ 𝑁, (𝐺‘(𝐹‘𝑘)), (𝐺‘𝑀))) |
25 | | iseqf1o.8 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐻‘𝑘) = (𝐺‘(𝐹‘𝑘))) |
26 | 4, 24, 25 | 3eqtr4rd 2201 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐻‘𝑘) = ((𝑎 ∈ (ℤ≥‘𝑀) ↦ if(𝑎 ≤ 𝑁, (𝐺‘(𝐹‘𝑎)), (𝐺‘𝑀)))‘𝑘)) |
27 | | iseqf1o.h |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐻‘𝑥) ∈ 𝑆) |
28 | | simpr 109 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → 𝑥 ∈ (ℤ≥‘𝑀)) |
29 | | fveq2 5468 |
. . . . . . . 8
⊢ (𝑏 = (𝐹‘𝑥) → (𝐺‘𝑏) = (𝐺‘(𝐹‘𝑥))) |
30 | 29 | eleq1d 2226 |
. . . . . . 7
⊢ (𝑏 = (𝐹‘𝑥) → ((𝐺‘𝑏) ∈ 𝑆 ↔ (𝐺‘(𝐹‘𝑥)) ∈ 𝑆)) |
31 | | fveq2 5468 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑏 → (𝐺‘𝑥) = (𝐺‘𝑏)) |
32 | 31 | eleq1d 2226 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑏 → ((𝐺‘𝑥) ∈ 𝑆 ↔ (𝐺‘𝑏) ∈ 𝑆)) |
33 | 32 | cbvralv 2680 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
(ℤ≥‘𝑀)(𝐺‘𝑥) ∈ 𝑆 ↔ ∀𝑏 ∈ (ℤ≥‘𝑀)(𝐺‘𝑏) ∈ 𝑆) |
34 | 9, 33 | sylib 121 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑏 ∈ (ℤ≥‘𝑀)(𝐺‘𝑏) ∈ 𝑆) |
35 | 34 | ad2antrr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) ∧ 𝑥 ≤ 𝑁) → ∀𝑏 ∈ (ℤ≥‘𝑀)(𝐺‘𝑏) ∈ 𝑆) |
36 | 13 | ad2antrr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) ∧ 𝑥 ≤ 𝑁) → 𝐹:(𝑀...𝑁)⟶(𝑀...𝑁)) |
37 | | eluzel2 9444 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
38 | 1, 37 | syl 14 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℤ) |
39 | 38 | ad2antrr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) ∧ 𝑥 ≤ 𝑁) → 𝑀 ∈ ℤ) |
40 | | eluzelz 9448 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
41 | 1, 40 | syl 14 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℤ) |
42 | 41 | ad2antrr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) ∧ 𝑥 ≤ 𝑁) → 𝑁 ∈ ℤ) |
43 | | eluzelz 9448 |
. . . . . . . . . . 11
⊢ (𝑥 ∈
(ℤ≥‘𝑀) → 𝑥 ∈ ℤ) |
44 | 43 | ad2antlr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) ∧ 𝑥 ≤ 𝑁) → 𝑥 ∈ ℤ) |
45 | | eluzle 9451 |
. . . . . . . . . . 11
⊢ (𝑥 ∈
(ℤ≥‘𝑀) → 𝑀 ≤ 𝑥) |
46 | 45 | ad2antlr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) ∧ 𝑥 ≤ 𝑁) → 𝑀 ≤ 𝑥) |
47 | | simpr 109 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) ∧ 𝑥 ≤ 𝑁) → 𝑥 ≤ 𝑁) |
48 | | elfz4 9921 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑥 ∈ ℤ) ∧ (𝑀 ≤ 𝑥 ∧ 𝑥 ≤ 𝑁)) → 𝑥 ∈ (𝑀...𝑁)) |
49 | 39, 42, 44, 46, 47, 48 | syl32anc 1228 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) ∧ 𝑥 ≤ 𝑁) → 𝑥 ∈ (𝑀...𝑁)) |
50 | 36, 49 | ffvelrnd 5603 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) ∧ 𝑥 ≤ 𝑁) → (𝐹‘𝑥) ∈ (𝑀...𝑁)) |
51 | | elfzuz 9924 |
. . . . . . . 8
⊢ ((𝐹‘𝑥) ∈ (𝑀...𝑁) → (𝐹‘𝑥) ∈ (ℤ≥‘𝑀)) |
52 | 50, 51 | syl 14 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) ∧ 𝑥 ≤ 𝑁) → (𝐹‘𝑥) ∈ (ℤ≥‘𝑀)) |
53 | 30, 35, 52 | rspcdva 2821 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) ∧ 𝑥 ≤ 𝑁) → (𝐺‘(𝐹‘𝑥)) ∈ 𝑆) |
54 | | fveq2 5468 |
. . . . . . . . 9
⊢ (𝑥 = 𝑀 → (𝐺‘𝑥) = (𝐺‘𝑀)) |
55 | 54 | eleq1d 2226 |
. . . . . . . 8
⊢ (𝑥 = 𝑀 → ((𝐺‘𝑥) ∈ 𝑆 ↔ (𝐺‘𝑀) ∈ 𝑆)) |
56 | | uzid 9453 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
(ℤ≥‘𝑀)) |
57 | 38, 56 | syl 14 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑀)) |
58 | 55, 9, 57 | rspcdva 2821 |
. . . . . . 7
⊢ (𝜑 → (𝐺‘𝑀) ∈ 𝑆) |
59 | 58 | ad2antrr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) ∧ ¬ 𝑥 ≤ 𝑁) → (𝐺‘𝑀) ∈ 𝑆) |
60 | 41 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → 𝑁 ∈ ℤ) |
61 | | zdcle 9240 |
. . . . . . 7
⊢ ((𝑥 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
DECID 𝑥 ≤
𝑁) |
62 | 43, 60, 61 | syl2an2 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → DECID
𝑥 ≤ 𝑁) |
63 | 53, 59, 62 | ifcldadc 3534 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → if(𝑥 ≤ 𝑁, (𝐺‘(𝐹‘𝑥)), (𝐺‘𝑀)) ∈ 𝑆) |
64 | | breq1 3968 |
. . . . . . 7
⊢ (𝑎 = 𝑥 → (𝑎 ≤ 𝑁 ↔ 𝑥 ≤ 𝑁)) |
65 | | 2fveq3 5473 |
. . . . . . 7
⊢ (𝑎 = 𝑥 → (𝐺‘(𝐹‘𝑎)) = (𝐺‘(𝐹‘𝑥))) |
66 | 64, 65 | ifbieq1d 3527 |
. . . . . 6
⊢ (𝑎 = 𝑥 → if(𝑎 ≤ 𝑁, (𝐺‘(𝐹‘𝑎)), (𝐺‘𝑀)) = if(𝑥 ≤ 𝑁, (𝐺‘(𝐹‘𝑥)), (𝐺‘𝑀))) |
67 | 66, 22 | fvmptg 5544 |
. . . . 5
⊢ ((𝑥 ∈
(ℤ≥‘𝑀) ∧ if(𝑥 ≤ 𝑁, (𝐺‘(𝐹‘𝑥)), (𝐺‘𝑀)) ∈ 𝑆) → ((𝑎 ∈ (ℤ≥‘𝑀) ↦ if(𝑎 ≤ 𝑁, (𝐺‘(𝐹‘𝑎)), (𝐺‘𝑀)))‘𝑥) = if(𝑥 ≤ 𝑁, (𝐺‘(𝐹‘𝑥)), (𝐺‘𝑀))) |
68 | 28, 63, 67 | syl2anc 409 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → ((𝑎 ∈ (ℤ≥‘𝑀) ↦ if(𝑎 ≤ 𝑁, (𝐺‘(𝐹‘𝑎)), (𝐺‘𝑀)))‘𝑥) = if(𝑥 ≤ 𝑁, (𝐺‘(𝐹‘𝑥)), (𝐺‘𝑀))) |
69 | 68, 63 | eqeltrd 2234 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → ((𝑎 ∈ (ℤ≥‘𝑀) ↦ if(𝑎 ≤ 𝑁, (𝐺‘(𝐹‘𝑎)), (𝐺‘𝑀)))‘𝑥) ∈ 𝑆) |
70 | | iseqf1o.1 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
71 | 1, 26, 27, 69, 70 | seq3fveq 10370 |
. 2
⊢ (𝜑 → (seq𝑀( + , 𝐻)‘𝑁) = (seq𝑀( + , (𝑎 ∈ (ℤ≥‘𝑀) ↦ if(𝑎 ≤ 𝑁, (𝐺‘(𝐹‘𝑎)), (𝐺‘𝑀))))‘𝑁)) |
72 | | iseqf1o.2 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) |
73 | | iseqf1o.3 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) |
74 | 66 | cbvmptv 4060 |
. . 3
⊢ (𝑎 ∈
(ℤ≥‘𝑀) ↦ if(𝑎 ≤ 𝑁, (𝐺‘(𝐹‘𝑎)), (𝐺‘𝑀))) = (𝑥 ∈ (ℤ≥‘𝑀) ↦ if(𝑥 ≤ 𝑁, (𝐺‘(𝐹‘𝑥)), (𝐺‘𝑀))) |
75 | 70, 72, 73, 1, 11, 8, 74 | seq3f1oleml 10402 |
. 2
⊢ (𝜑 → (seq𝑀( + , (𝑎 ∈ (ℤ≥‘𝑀) ↦ if(𝑎 ≤ 𝑁, (𝐺‘(𝐹‘𝑎)), (𝐺‘𝑀))))‘𝑁) = (seq𝑀( + , 𝐺)‘𝑁)) |
76 | 71, 75 | eqtrd 2190 |
1
⊢ (𝜑 → (seq𝑀( + , 𝐻)‘𝑁) = (seq𝑀( + , 𝐺)‘𝑁)) |