Proof of Theorem seqcoll2
Step | Hyp | Ref
| Expression |
1 | | seqcoll2.1b |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → (𝑘 + 𝑍) = 𝑘) |
2 | | fzssuz 12767 |
. . . 4
⊢ (𝑀...𝑁) ⊆
(ℤ≥‘𝑀) |
3 | | seqcoll2.5 |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ (𝑀...𝑁)) |
4 | | seqcoll2.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴)) |
5 | | isof1o 6901 |
. . . . . . . 8
⊢ (𝐺 Isom < , <
((1...(♯‘𝐴)),
𝐴) → 𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴) |
6 | 4, 5 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴) |
7 | | f1of 6446 |
. . . . . . 7
⊢ (𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴 → 𝐺:(1...(♯‘𝐴))⟶𝐴) |
8 | 6, 7 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐺:(1...(♯‘𝐴))⟶𝐴) |
9 | | seqcoll2.3 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ≠ ∅) |
10 | | fzfi 13158 |
. . . . . . . . . . . . 13
⊢ (𝑀...𝑁) ∈ Fin |
11 | | ssfi 8535 |
. . . . . . . . . . . . 13
⊢ (((𝑀...𝑁) ∈ Fin ∧ 𝐴 ⊆ (𝑀...𝑁)) → 𝐴 ∈ Fin) |
12 | 10, 3, 11 | sylancr 578 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ Fin) |
13 | | hasheq0 13542 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ Fin →
((♯‘𝐴) = 0
↔ 𝐴 =
∅)) |
14 | 12, 13 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((♯‘𝐴) = 0 ↔ 𝐴 = ∅)) |
15 | 14 | necon3bbid 3004 |
. . . . . . . . . 10
⊢ (𝜑 → (¬
(♯‘𝐴) = 0
↔ 𝐴 ≠
∅)) |
16 | 9, 15 | mpbird 249 |
. . . . . . . . 9
⊢ (𝜑 → ¬ (♯‘𝐴) = 0) |
17 | | hashcl 13535 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ Fin →
(♯‘𝐴) ∈
ℕ0) |
18 | 12, 17 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (♯‘𝐴) ∈
ℕ0) |
19 | | elnn0 11712 |
. . . . . . . . . . 11
⊢
((♯‘𝐴)
∈ ℕ0 ↔ ((♯‘𝐴) ∈ ℕ ∨ (♯‘𝐴) = 0)) |
20 | 18, 19 | sylib 210 |
. . . . . . . . . 10
⊢ (𝜑 → ((♯‘𝐴) ∈ ℕ ∨
(♯‘𝐴) =
0)) |
21 | 20 | ord 850 |
. . . . . . . . 9
⊢ (𝜑 → (¬
(♯‘𝐴) ∈
ℕ → (♯‘𝐴) = 0)) |
22 | 16, 21 | mt3d 143 |
. . . . . . . 8
⊢ (𝜑 → (♯‘𝐴) ∈
ℕ) |
23 | | nnuz 12098 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) |
24 | 22, 23 | syl6eleq 2876 |
. . . . . . 7
⊢ (𝜑 → (♯‘𝐴) ∈
(ℤ≥‘1)) |
25 | | eluzfz2 12734 |
. . . . . . 7
⊢
((♯‘𝐴)
∈ (ℤ≥‘1) → (♯‘𝐴) ∈ (1...(♯‘𝐴))) |
26 | 24, 25 | syl 17 |
. . . . . 6
⊢ (𝜑 → (♯‘𝐴) ∈
(1...(♯‘𝐴))) |
27 | 8, 26 | ffvelrnd 6679 |
. . . . 5
⊢ (𝜑 → (𝐺‘(♯‘𝐴)) ∈ 𝐴) |
28 | 3, 27 | sseldd 3861 |
. . . 4
⊢ (𝜑 → (𝐺‘(♯‘𝐴)) ∈ (𝑀...𝑁)) |
29 | 2, 28 | sseldi 3858 |
. . 3
⊢ (𝜑 → (𝐺‘(♯‘𝐴)) ∈
(ℤ≥‘𝑀)) |
30 | | elfzuz3 12724 |
. . . 4
⊢ ((𝐺‘(♯‘𝐴)) ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘(𝐺‘(♯‘𝐴)))) |
31 | 28, 30 | syl 17 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝐺‘(♯‘𝐴)))) |
32 | | fzss2 12766 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘(𝐺‘(♯‘𝐴))) → (𝑀...(𝐺‘(♯‘𝐴))) ⊆ (𝑀...𝑁)) |
33 | 31, 32 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑀...(𝐺‘(♯‘𝐴))) ⊆ (𝑀...𝑁)) |
34 | 33 | sselda 3860 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴)))) → 𝑘 ∈ (𝑀...𝑁)) |
35 | | seqcoll2.6 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ 𝑆) |
36 | 34, 35 | syldan 582 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴)))) → (𝐹‘𝑘) ∈ 𝑆) |
37 | | seqcoll2.c |
. . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑆 ∧ 𝑛 ∈ 𝑆)) → (𝑘 + 𝑛) ∈ 𝑆) |
38 | 29, 36, 37 | seqcl 13208 |
. . 3
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝐺‘(♯‘𝐴))) ∈ 𝑆) |
39 | | peano2uz 12118 |
. . . . . . . 8
⊢ ((𝐺‘(♯‘𝐴)) ∈
(ℤ≥‘𝑀) → ((𝐺‘(♯‘𝐴)) + 1) ∈
(ℤ≥‘𝑀)) |
40 | 29, 39 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝐺‘(♯‘𝐴)) + 1) ∈
(ℤ≥‘𝑀)) |
41 | | fzss1 12765 |
. . . . . . 7
⊢ (((𝐺‘(♯‘𝐴)) + 1) ∈
(ℤ≥‘𝑀) → (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ⊆ (𝑀...𝑁)) |
42 | 40, 41 | syl 17 |
. . . . . 6
⊢ (𝜑 → (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ⊆ (𝑀...𝑁)) |
43 | 42 | sselda 3860 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁)) → 𝑘 ∈ (𝑀...𝑁)) |
44 | | eluzelre 12072 |
. . . . . . . . 9
⊢ ((𝐺‘(♯‘𝐴)) ∈
(ℤ≥‘𝑀) → (𝐺‘(♯‘𝐴)) ∈ ℝ) |
45 | 29, 44 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐺‘(♯‘𝐴)) ∈ ℝ) |
46 | 45 | adantr 473 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁)) → (𝐺‘(♯‘𝐴)) ∈ ℝ) |
47 | | peano2re 10615 |
. . . . . . . 8
⊢ ((𝐺‘(♯‘𝐴)) ∈ ℝ → ((𝐺‘(♯‘𝐴)) + 1) ∈
ℝ) |
48 | 46, 47 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁)) → ((𝐺‘(♯‘𝐴)) + 1) ∈ ℝ) |
49 | | elfzelz 12727 |
. . . . . . . . 9
⊢ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) → 𝑘 ∈ ℤ) |
50 | 49 | zred 11903 |
. . . . . . . 8
⊢ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) → 𝑘 ∈ ℝ) |
51 | 50 | adantl 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁)) → 𝑘 ∈ ℝ) |
52 | 46 | ltp1d 11373 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁)) → (𝐺‘(♯‘𝐴)) < ((𝐺‘(♯‘𝐴)) + 1)) |
53 | | elfzle1 12729 |
. . . . . . . 8
⊢ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) → ((𝐺‘(♯‘𝐴)) + 1) ≤ 𝑘) |
54 | 53 | adantl 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁)) → ((𝐺‘(♯‘𝐴)) + 1) ≤ 𝑘) |
55 | 46, 48, 51, 52, 54 | ltletrd 10602 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁)) → (𝐺‘(♯‘𝐴)) < 𝑘) |
56 | 6 | adantr 473 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → 𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴) |
57 | | f1ocnv 6458 |
. . . . . . . . . . . . . 14
⊢ (𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴 → ◡𝐺:𝐴–1-1-onto→(1...(♯‘𝐴))) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → ◡𝐺:𝐴–1-1-onto→(1...(♯‘𝐴))) |
59 | | f1of 6446 |
. . . . . . . . . . . . 13
⊢ (◡𝐺:𝐴–1-1-onto→(1...(♯‘𝐴)) → ◡𝐺:𝐴⟶(1...(♯‘𝐴))) |
60 | 58, 59 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → ◡𝐺:𝐴⟶(1...(♯‘𝐴))) |
61 | | simprr 760 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → 𝑘 ∈ 𝐴) |
62 | 60, 61 | ffvelrnd 6679 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → (◡𝐺‘𝑘) ∈ (1...(♯‘𝐴))) |
63 | | elfzelz 12727 |
. . . . . . . . . . 11
⊢ ((◡𝐺‘𝑘) ∈ (1...(♯‘𝐴)) → (◡𝐺‘𝑘) ∈ ℤ) |
64 | 62, 63 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → (◡𝐺‘𝑘) ∈ ℤ) |
65 | 64 | zred 11903 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → (◡𝐺‘𝑘) ∈ ℝ) |
66 | 18 | adantr 473 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → (♯‘𝐴) ∈
ℕ0) |
67 | 66 | nn0red 11771 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → (♯‘𝐴) ∈ ℝ) |
68 | | elfzle2 12730 |
. . . . . . . . . 10
⊢ ((◡𝐺‘𝑘) ∈ (1...(♯‘𝐴)) → (◡𝐺‘𝑘) ≤ (♯‘𝐴)) |
69 | 62, 68 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → (◡𝐺‘𝑘) ≤ (♯‘𝐴)) |
70 | 65, 67, 69 | lensymd 10593 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → ¬ (♯‘𝐴) < (◡𝐺‘𝑘)) |
71 | 4 | adantr 473 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → 𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴)) |
72 | 26 | adantr 473 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → (♯‘𝐴) ∈ (1...(♯‘𝐴))) |
73 | | isorel 6904 |
. . . . . . . . . 10
⊢ ((𝐺 Isom < , <
((1...(♯‘𝐴)),
𝐴) ∧
((♯‘𝐴) ∈
(1...(♯‘𝐴))
∧ (◡𝐺‘𝑘) ∈ (1...(♯‘𝐴)))) →
((♯‘𝐴) <
(◡𝐺‘𝑘) ↔ (𝐺‘(♯‘𝐴)) < (𝐺‘(◡𝐺‘𝑘)))) |
74 | 71, 72, 62, 73 | syl12anc 824 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → ((♯‘𝐴) < (◡𝐺‘𝑘) ↔ (𝐺‘(♯‘𝐴)) < (𝐺‘(◡𝐺‘𝑘)))) |
75 | | f1ocnvfv2 6861 |
. . . . . . . . . . 11
⊢ ((𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴 ∧ 𝑘 ∈ 𝐴) → (𝐺‘(◡𝐺‘𝑘)) = 𝑘) |
76 | 56, 61, 75 | syl2anc 576 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → (𝐺‘(◡𝐺‘𝑘)) = 𝑘) |
77 | 76 | breq2d 4942 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → ((𝐺‘(♯‘𝐴)) < (𝐺‘(◡𝐺‘𝑘)) ↔ (𝐺‘(♯‘𝐴)) < 𝑘)) |
78 | 74, 77 | bitrd 271 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → ((♯‘𝐴) < (◡𝐺‘𝑘) ↔ (𝐺‘(♯‘𝐴)) < 𝑘)) |
79 | 70, 78 | mtbid 316 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → ¬ (𝐺‘(♯‘𝐴)) < 𝑘) |
80 | 79 | expr 449 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁)) → (𝑘 ∈ 𝐴 → ¬ (𝐺‘(♯‘𝐴)) < 𝑘)) |
81 | 55, 80 | mt2d 134 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁)) → ¬ 𝑘 ∈ 𝐴) |
82 | 43, 81 | eldifd 3842 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁)) → 𝑘 ∈ ((𝑀...𝑁) ∖ 𝐴)) |
83 | | seqcoll2.7 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀...𝑁) ∖ 𝐴)) → (𝐹‘𝑘) = 𝑍) |
84 | 82, 83 | syldan 582 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁)) → (𝐹‘𝑘) = 𝑍) |
85 | 1, 29, 31, 38, 84 | seqid2 13234 |
. 2
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝐺‘(♯‘𝐴))) = (seq𝑀( + , 𝐹)‘𝑁)) |
86 | | seqcoll2.1 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → (𝑍 + 𝑘) = 𝑘) |
87 | | seqcoll2.a |
. . 3
⊢ (𝜑 → 𝑍 ∈ 𝑆) |
88 | 3, 2 | syl6ss 3872 |
. . 3
⊢ (𝜑 → 𝐴 ⊆ (ℤ≥‘𝑀)) |
89 | 33 | ssdifd 4009 |
. . . . 5
⊢ (𝜑 → ((𝑀...(𝐺‘(♯‘𝐴))) ∖ 𝐴) ⊆ ((𝑀...𝑁) ∖ 𝐴)) |
90 | 89 | sselda 3860 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀...(𝐺‘(♯‘𝐴))) ∖ 𝐴)) → 𝑘 ∈ ((𝑀...𝑁) ∖ 𝐴)) |
91 | 90, 83 | syldan 582 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀...(𝐺‘(♯‘𝐴))) ∖ 𝐴)) → (𝐹‘𝑘) = 𝑍) |
92 | | seqcoll2.8 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (𝐻‘𝑛) = (𝐹‘(𝐺‘𝑛))) |
93 | 86, 1, 37, 87, 4, 26, 88, 36, 91, 92 | seqcoll 13638 |
. 2
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝐺‘(♯‘𝐴))) = (seq1( + , 𝐻)‘(♯‘𝐴))) |
94 | 85, 93 | eqtr3d 2816 |
1
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = (seq1( + , 𝐻)‘(♯‘𝐴))) |