Proof of Theorem seqcoll2
Step | Hyp | Ref
| Expression |
1 | | seqcoll2.1b |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → (𝑘 + 𝑍) = 𝑘) |
2 | | fzssuz 12253 |
. . . 4
⊢ (𝑀...𝑁) ⊆
(ℤ≥‘𝑀) |
3 | | seqcoll2.5 |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ (𝑀...𝑁)) |
4 | | seqcoll2.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 Isom < , < ((1...(#‘𝐴)), 𝐴)) |
5 | | isof1o 6473 |
. . . . . . . 8
⊢ (𝐺 Isom < , <
((1...(#‘𝐴)), 𝐴) → 𝐺:(1...(#‘𝐴))–1-1-onto→𝐴) |
6 | 4, 5 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐺:(1...(#‘𝐴))–1-1-onto→𝐴) |
7 | | f1of 6050 |
. . . . . . 7
⊢ (𝐺:(1...(#‘𝐴))–1-1-onto→𝐴 → 𝐺:(1...(#‘𝐴))⟶𝐴) |
8 | 6, 7 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐺:(1...(#‘𝐴))⟶𝐴) |
9 | | seqcoll2.3 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ≠ ∅) |
10 | | fzfi 12633 |
. . . . . . . . . . . . 13
⊢ (𝑀...𝑁) ∈ Fin |
11 | | ssfi 8065 |
. . . . . . . . . . . . 13
⊢ (((𝑀...𝑁) ∈ Fin ∧ 𝐴 ⊆ (𝑀...𝑁)) → 𝐴 ∈ Fin) |
12 | 10, 3, 11 | sylancr 694 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ Fin) |
13 | | hasheq0 13015 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ Fin →
((#‘𝐴) = 0 ↔
𝐴 =
∅)) |
14 | 12, 13 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((#‘𝐴) = 0 ↔ 𝐴 = ∅)) |
15 | 14 | necon3bbid 2819 |
. . . . . . . . . 10
⊢ (𝜑 → (¬ (#‘𝐴) = 0 ↔ 𝐴 ≠ ∅)) |
16 | 9, 15 | mpbird 246 |
. . . . . . . . 9
⊢ (𝜑 → ¬ (#‘𝐴) = 0) |
17 | | hashcl 13009 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ Fin →
(#‘𝐴) ∈
ℕ0) |
18 | 12, 17 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (#‘𝐴) ∈
ℕ0) |
19 | | elnn0 11171 |
. . . . . . . . . . 11
⊢
((#‘𝐴) ∈
ℕ0 ↔ ((#‘𝐴) ∈ ℕ ∨ (#‘𝐴) = 0)) |
20 | 18, 19 | sylib 207 |
. . . . . . . . . 10
⊢ (𝜑 → ((#‘𝐴) ∈ ℕ ∨
(#‘𝐴) =
0)) |
21 | 20 | ord 391 |
. . . . . . . . 9
⊢ (𝜑 → (¬ (#‘𝐴) ∈ ℕ →
(#‘𝐴) =
0)) |
22 | 16, 21 | mt3d 139 |
. . . . . . . 8
⊢ (𝜑 → (#‘𝐴) ∈ ℕ) |
23 | | nnuz 11599 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) |
24 | 22, 23 | syl6eleq 2698 |
. . . . . . 7
⊢ (𝜑 → (#‘𝐴) ∈
(ℤ≥‘1)) |
25 | | eluzfz2 12220 |
. . . . . . 7
⊢
((#‘𝐴) ∈
(ℤ≥‘1) → (#‘𝐴) ∈ (1...(#‘𝐴))) |
26 | 24, 25 | syl 17 |
. . . . . 6
⊢ (𝜑 → (#‘𝐴) ∈ (1...(#‘𝐴))) |
27 | 8, 26 | ffvelrnd 6268 |
. . . . 5
⊢ (𝜑 → (𝐺‘(#‘𝐴)) ∈ 𝐴) |
28 | 3, 27 | sseldd 3569 |
. . . 4
⊢ (𝜑 → (𝐺‘(#‘𝐴)) ∈ (𝑀...𝑁)) |
29 | 2, 28 | sseldi 3566 |
. . 3
⊢ (𝜑 → (𝐺‘(#‘𝐴)) ∈
(ℤ≥‘𝑀)) |
30 | | elfzuz3 12210 |
. . . 4
⊢ ((𝐺‘(#‘𝐴)) ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘(𝐺‘(#‘𝐴)))) |
31 | 28, 30 | syl 17 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝐺‘(#‘𝐴)))) |
32 | | fzss2 12252 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘(𝐺‘(#‘𝐴))) → (𝑀...(𝐺‘(#‘𝐴))) ⊆ (𝑀...𝑁)) |
33 | 31, 32 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑀...(𝐺‘(#‘𝐴))) ⊆ (𝑀...𝑁)) |
34 | 33 | sselda 3568 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝐺‘(#‘𝐴)))) → 𝑘 ∈ (𝑀...𝑁)) |
35 | | seqcoll2.6 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ 𝑆) |
36 | 34, 35 | syldan 486 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝐺‘(#‘𝐴)))) → (𝐹‘𝑘) ∈ 𝑆) |
37 | | seqcoll2.c |
. . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑆 ∧ 𝑛 ∈ 𝑆)) → (𝑘 + 𝑛) ∈ 𝑆) |
38 | 29, 36, 37 | seqcl 12683 |
. . 3
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝐺‘(#‘𝐴))) ∈ 𝑆) |
39 | | peano2uz 11617 |
. . . . . . . 8
⊢ ((𝐺‘(#‘𝐴)) ∈
(ℤ≥‘𝑀) → ((𝐺‘(#‘𝐴)) + 1) ∈
(ℤ≥‘𝑀)) |
40 | 29, 39 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝐺‘(#‘𝐴)) + 1) ∈
(ℤ≥‘𝑀)) |
41 | | fzss1 12251 |
. . . . . . 7
⊢ (((𝐺‘(#‘𝐴)) + 1) ∈
(ℤ≥‘𝑀) → (((𝐺‘(#‘𝐴)) + 1)...𝑁) ⊆ (𝑀...𝑁)) |
42 | 40, 41 | syl 17 |
. . . . . 6
⊢ (𝜑 → (((𝐺‘(#‘𝐴)) + 1)...𝑁) ⊆ (𝑀...𝑁)) |
43 | 42 | sselda 3568 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (((𝐺‘(#‘𝐴)) + 1)...𝑁)) → 𝑘 ∈ (𝑀...𝑁)) |
44 | | eluzelre 11574 |
. . . . . . . . 9
⊢ ((𝐺‘(#‘𝐴)) ∈
(ℤ≥‘𝑀) → (𝐺‘(#‘𝐴)) ∈ ℝ) |
45 | 29, 44 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐺‘(#‘𝐴)) ∈ ℝ) |
46 | 45 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (((𝐺‘(#‘𝐴)) + 1)...𝑁)) → (𝐺‘(#‘𝐴)) ∈ ℝ) |
47 | | peano2re 10088 |
. . . . . . . 8
⊢ ((𝐺‘(#‘𝐴)) ∈ ℝ → ((𝐺‘(#‘𝐴)) + 1) ∈
ℝ) |
48 | 46, 47 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (((𝐺‘(#‘𝐴)) + 1)...𝑁)) → ((𝐺‘(#‘𝐴)) + 1) ∈ ℝ) |
49 | | elfzelz 12213 |
. . . . . . . . 9
⊢ (𝑘 ∈ (((𝐺‘(#‘𝐴)) + 1)...𝑁) → 𝑘 ∈ ℤ) |
50 | 49 | zred 11358 |
. . . . . . . 8
⊢ (𝑘 ∈ (((𝐺‘(#‘𝐴)) + 1)...𝑁) → 𝑘 ∈ ℝ) |
51 | 50 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (((𝐺‘(#‘𝐴)) + 1)...𝑁)) → 𝑘 ∈ ℝ) |
52 | 46 | ltp1d 10833 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (((𝐺‘(#‘𝐴)) + 1)...𝑁)) → (𝐺‘(#‘𝐴)) < ((𝐺‘(#‘𝐴)) + 1)) |
53 | | elfzle1 12215 |
. . . . . . . 8
⊢ (𝑘 ∈ (((𝐺‘(#‘𝐴)) + 1)...𝑁) → ((𝐺‘(#‘𝐴)) + 1) ≤ 𝑘) |
54 | 53 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (((𝐺‘(#‘𝐴)) + 1)...𝑁)) → ((𝐺‘(#‘𝐴)) + 1) ≤ 𝑘) |
55 | 46, 48, 51, 52, 54 | ltletrd 10076 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (((𝐺‘(#‘𝐴)) + 1)...𝑁)) → (𝐺‘(#‘𝐴)) < 𝑘) |
56 | 6 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(#‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → 𝐺:(1...(#‘𝐴))–1-1-onto→𝐴) |
57 | | f1ocnv 6062 |
. . . . . . . . . . . . 13
⊢ (𝐺:(1...(#‘𝐴))–1-1-onto→𝐴 → ◡𝐺:𝐴–1-1-onto→(1...(#‘𝐴))) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(#‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → ◡𝐺:𝐴–1-1-onto→(1...(#‘𝐴))) |
59 | | f1of 6050 |
. . . . . . . . . . . 12
⊢ (◡𝐺:𝐴–1-1-onto→(1...(#‘𝐴)) → ◡𝐺:𝐴⟶(1...(#‘𝐴))) |
60 | 58, 59 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(#‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → ◡𝐺:𝐴⟶(1...(#‘𝐴))) |
61 | | simprr 792 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(#‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → 𝑘 ∈ 𝐴) |
62 | 60, 61 | ffvelrnd 6268 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(#‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → (◡𝐺‘𝑘) ∈ (1...(#‘𝐴))) |
63 | | elfzle2 12216 |
. . . . . . . . . 10
⊢ ((◡𝐺‘𝑘) ∈ (1...(#‘𝐴)) → (◡𝐺‘𝑘) ≤ (#‘𝐴)) |
64 | 62, 63 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(#‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → (◡𝐺‘𝑘) ≤ (#‘𝐴)) |
65 | | elfzelz 12213 |
. . . . . . . . . . . 12
⊢ ((◡𝐺‘𝑘) ∈ (1...(#‘𝐴)) → (◡𝐺‘𝑘) ∈ ℤ) |
66 | 62, 65 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(#‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → (◡𝐺‘𝑘) ∈ ℤ) |
67 | 66 | zred 11358 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(#‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → (◡𝐺‘𝑘) ∈ ℝ) |
68 | 18 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(#‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → (#‘𝐴) ∈
ℕ0) |
69 | 68 | nn0red 11229 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(#‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → (#‘𝐴) ∈ ℝ) |
70 | 67, 69 | lenltd 10062 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(#‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → ((◡𝐺‘𝑘) ≤ (#‘𝐴) ↔ ¬ (#‘𝐴) < (◡𝐺‘𝑘))) |
71 | 64, 70 | mpbid 221 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(#‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → ¬ (#‘𝐴) < (◡𝐺‘𝑘)) |
72 | 4 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(#‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → 𝐺 Isom < , < ((1...(#‘𝐴)), 𝐴)) |
73 | 26 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(#‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → (#‘𝐴) ∈ (1...(#‘𝐴))) |
74 | | isorel 6476 |
. . . . . . . . . 10
⊢ ((𝐺 Isom < , <
((1...(#‘𝐴)), 𝐴) ∧ ((#‘𝐴) ∈ (1...(#‘𝐴)) ∧ (◡𝐺‘𝑘) ∈ (1...(#‘𝐴)))) → ((#‘𝐴) < (◡𝐺‘𝑘) ↔ (𝐺‘(#‘𝐴)) < (𝐺‘(◡𝐺‘𝑘)))) |
75 | 72, 73, 62, 74 | syl12anc 1316 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(#‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → ((#‘𝐴) < (◡𝐺‘𝑘) ↔ (𝐺‘(#‘𝐴)) < (𝐺‘(◡𝐺‘𝑘)))) |
76 | | f1ocnvfv2 6433 |
. . . . . . . . . . 11
⊢ ((𝐺:(1...(#‘𝐴))–1-1-onto→𝐴 ∧ 𝑘 ∈ 𝐴) → (𝐺‘(◡𝐺‘𝑘)) = 𝑘) |
77 | 56, 61, 76 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(#‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → (𝐺‘(◡𝐺‘𝑘)) = 𝑘) |
78 | 77 | breq2d 4595 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(#‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → ((𝐺‘(#‘𝐴)) < (𝐺‘(◡𝐺‘𝑘)) ↔ (𝐺‘(#‘𝐴)) < 𝑘)) |
79 | 75, 78 | bitrd 267 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(#‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → ((#‘𝐴) < (◡𝐺‘𝑘) ↔ (𝐺‘(#‘𝐴)) < 𝑘)) |
80 | 71, 79 | mtbid 313 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(#‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → ¬ (𝐺‘(#‘𝐴)) < 𝑘) |
81 | 80 | expr 641 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (((𝐺‘(#‘𝐴)) + 1)...𝑁)) → (𝑘 ∈ 𝐴 → ¬ (𝐺‘(#‘𝐴)) < 𝑘)) |
82 | 55, 81 | mt2d 130 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (((𝐺‘(#‘𝐴)) + 1)...𝑁)) → ¬ 𝑘 ∈ 𝐴) |
83 | 43, 82 | eldifd 3551 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (((𝐺‘(#‘𝐴)) + 1)...𝑁)) → 𝑘 ∈ ((𝑀...𝑁) ∖ 𝐴)) |
84 | | seqcoll2.7 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀...𝑁) ∖ 𝐴)) → (𝐹‘𝑘) = 𝑍) |
85 | 83, 84 | syldan 486 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (((𝐺‘(#‘𝐴)) + 1)...𝑁)) → (𝐹‘𝑘) = 𝑍) |
86 | 1, 29, 31, 38, 85 | seqid2 12709 |
. 2
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝐺‘(#‘𝐴))) = (seq𝑀( + , 𝐹)‘𝑁)) |
87 | | seqcoll2.1 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → (𝑍 + 𝑘) = 𝑘) |
88 | | seqcoll2.a |
. . 3
⊢ (𝜑 → 𝑍 ∈ 𝑆) |
89 | 3, 2 | syl6ss 3580 |
. . 3
⊢ (𝜑 → 𝐴 ⊆ (ℤ≥‘𝑀)) |
90 | 33 | ssdifd 3708 |
. . . . 5
⊢ (𝜑 → ((𝑀...(𝐺‘(#‘𝐴))) ∖ 𝐴) ⊆ ((𝑀...𝑁) ∖ 𝐴)) |
91 | 90 | sselda 3568 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀...(𝐺‘(#‘𝐴))) ∖ 𝐴)) → 𝑘 ∈ ((𝑀...𝑁) ∖ 𝐴)) |
92 | 91, 84 | syldan 486 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀...(𝐺‘(#‘𝐴))) ∖ 𝐴)) → (𝐹‘𝑘) = 𝑍) |
93 | | seqcoll2.8 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(#‘𝐴))) → (𝐻‘𝑛) = (𝐹‘(𝐺‘𝑛))) |
94 | 87, 1, 37, 88, 4, 26, 89, 36, 92, 93 | seqcoll 13105 |
. 2
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝐺‘(#‘𝐴))) = (seq1( + , 𝐻)‘(#‘𝐴))) |
95 | 86, 94 | eqtr3d 2646 |
1
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = (seq1( + , 𝐻)‘(#‘𝐴))) |