Proof of Theorem seqcoll2
| Step | Hyp | Ref
| Expression |
| 1 | | seqcoll2.1b |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → (𝑘 + 𝑍) = 𝑘) |
| 2 | | fzssuz 13605 |
. . . 4
⊢ (𝑀...𝑁) ⊆
(ℤ≥‘𝑀) |
| 3 | | seqcoll2.5 |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ (𝑀...𝑁)) |
| 4 | | seqcoll2.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴)) |
| 5 | | isof1o 7343 |
. . . . . . . 8
⊢ (𝐺 Isom < , <
((1...(♯‘𝐴)),
𝐴) → 𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴) |
| 6 | 4, 5 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴) |
| 7 | | f1of 6848 |
. . . . . . 7
⊢ (𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴 → 𝐺:(1...(♯‘𝐴))⟶𝐴) |
| 8 | 6, 7 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐺:(1...(♯‘𝐴))⟶𝐴) |
| 9 | | seqcoll2.3 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ≠ ∅) |
| 10 | | fzfi 14013 |
. . . . . . . . . . . . 13
⊢ (𝑀...𝑁) ∈ Fin |
| 11 | | ssfi 9213 |
. . . . . . . . . . . . 13
⊢ (((𝑀...𝑁) ∈ Fin ∧ 𝐴 ⊆ (𝑀...𝑁)) → 𝐴 ∈ Fin) |
| 12 | 10, 3, 11 | sylancr 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ Fin) |
| 13 | | hasheq0 14402 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ Fin →
((♯‘𝐴) = 0
↔ 𝐴 =
∅)) |
| 14 | 12, 13 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((♯‘𝐴) = 0 ↔ 𝐴 = ∅)) |
| 15 | 14 | necon3bbid 2978 |
. . . . . . . . . 10
⊢ (𝜑 → (¬
(♯‘𝐴) = 0
↔ 𝐴 ≠
∅)) |
| 16 | 9, 15 | mpbird 257 |
. . . . . . . . 9
⊢ (𝜑 → ¬ (♯‘𝐴) = 0) |
| 17 | | hashcl 14395 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ Fin →
(♯‘𝐴) ∈
ℕ0) |
| 18 | 12, 17 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (♯‘𝐴) ∈
ℕ0) |
| 19 | | elnn0 12528 |
. . . . . . . . . . 11
⊢
((♯‘𝐴)
∈ ℕ0 ↔ ((♯‘𝐴) ∈ ℕ ∨ (♯‘𝐴) = 0)) |
| 20 | 18, 19 | sylib 218 |
. . . . . . . . . 10
⊢ (𝜑 → ((♯‘𝐴) ∈ ℕ ∨
(♯‘𝐴) =
0)) |
| 21 | 20 | ord 865 |
. . . . . . . . 9
⊢ (𝜑 → (¬
(♯‘𝐴) ∈
ℕ → (♯‘𝐴) = 0)) |
| 22 | 16, 21 | mt3d 148 |
. . . . . . . 8
⊢ (𝜑 → (♯‘𝐴) ∈
ℕ) |
| 23 | | nnuz 12921 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) |
| 24 | 22, 23 | eleqtrdi 2851 |
. . . . . . 7
⊢ (𝜑 → (♯‘𝐴) ∈
(ℤ≥‘1)) |
| 25 | | eluzfz2 13572 |
. . . . . . 7
⊢
((♯‘𝐴)
∈ (ℤ≥‘1) → (♯‘𝐴) ∈ (1...(♯‘𝐴))) |
| 26 | 24, 25 | syl 17 |
. . . . . 6
⊢ (𝜑 → (♯‘𝐴) ∈
(1...(♯‘𝐴))) |
| 27 | 8, 26 | ffvelcdmd 7105 |
. . . . 5
⊢ (𝜑 → (𝐺‘(♯‘𝐴)) ∈ 𝐴) |
| 28 | 3, 27 | sseldd 3984 |
. . . 4
⊢ (𝜑 → (𝐺‘(♯‘𝐴)) ∈ (𝑀...𝑁)) |
| 29 | 2, 28 | sselid 3981 |
. . 3
⊢ (𝜑 → (𝐺‘(♯‘𝐴)) ∈
(ℤ≥‘𝑀)) |
| 30 | | elfzuz3 13561 |
. . . 4
⊢ ((𝐺‘(♯‘𝐴)) ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘(𝐺‘(♯‘𝐴)))) |
| 31 | 28, 30 | syl 17 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝐺‘(♯‘𝐴)))) |
| 32 | | fzss2 13604 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘(𝐺‘(♯‘𝐴))) → (𝑀...(𝐺‘(♯‘𝐴))) ⊆ (𝑀...𝑁)) |
| 33 | 31, 32 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑀...(𝐺‘(♯‘𝐴))) ⊆ (𝑀...𝑁)) |
| 34 | 33 | sselda 3983 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴)))) → 𝑘 ∈ (𝑀...𝑁)) |
| 35 | | seqcoll2.6 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ 𝑆) |
| 36 | 34, 35 | syldan 591 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴)))) → (𝐹‘𝑘) ∈ 𝑆) |
| 37 | | seqcoll2.c |
. . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑆 ∧ 𝑛 ∈ 𝑆)) → (𝑘 + 𝑛) ∈ 𝑆) |
| 38 | 29, 36, 37 | seqcl 14063 |
. . 3
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝐺‘(♯‘𝐴))) ∈ 𝑆) |
| 39 | | peano2uz 12943 |
. . . . . . . 8
⊢ ((𝐺‘(♯‘𝐴)) ∈
(ℤ≥‘𝑀) → ((𝐺‘(♯‘𝐴)) + 1) ∈
(ℤ≥‘𝑀)) |
| 40 | 29, 39 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝐺‘(♯‘𝐴)) + 1) ∈
(ℤ≥‘𝑀)) |
| 41 | | fzss1 13603 |
. . . . . . 7
⊢ (((𝐺‘(♯‘𝐴)) + 1) ∈
(ℤ≥‘𝑀) → (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ⊆ (𝑀...𝑁)) |
| 42 | 40, 41 | syl 17 |
. . . . . 6
⊢ (𝜑 → (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ⊆ (𝑀...𝑁)) |
| 43 | 42 | sselda 3983 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁)) → 𝑘 ∈ (𝑀...𝑁)) |
| 44 | | eluzelre 12889 |
. . . . . . . . 9
⊢ ((𝐺‘(♯‘𝐴)) ∈
(ℤ≥‘𝑀) → (𝐺‘(♯‘𝐴)) ∈ ℝ) |
| 45 | 29, 44 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐺‘(♯‘𝐴)) ∈ ℝ) |
| 46 | 45 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁)) → (𝐺‘(♯‘𝐴)) ∈ ℝ) |
| 47 | | peano2re 11434 |
. . . . . . . 8
⊢ ((𝐺‘(♯‘𝐴)) ∈ ℝ → ((𝐺‘(♯‘𝐴)) + 1) ∈
ℝ) |
| 48 | 46, 47 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁)) → ((𝐺‘(♯‘𝐴)) + 1) ∈ ℝ) |
| 49 | | elfzelz 13564 |
. . . . . . . . 9
⊢ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) → 𝑘 ∈ ℤ) |
| 50 | 49 | zred 12722 |
. . . . . . . 8
⊢ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) → 𝑘 ∈ ℝ) |
| 51 | 50 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁)) → 𝑘 ∈ ℝ) |
| 52 | 46 | ltp1d 12198 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁)) → (𝐺‘(♯‘𝐴)) < ((𝐺‘(♯‘𝐴)) + 1)) |
| 53 | | elfzle1 13567 |
. . . . . . . 8
⊢ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) → ((𝐺‘(♯‘𝐴)) + 1) ≤ 𝑘) |
| 54 | 53 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁)) → ((𝐺‘(♯‘𝐴)) + 1) ≤ 𝑘) |
| 55 | 46, 48, 51, 52, 54 | ltletrd 11421 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁)) → (𝐺‘(♯‘𝐴)) < 𝑘) |
| 56 | 6 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → 𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴) |
| 57 | | f1ocnv 6860 |
. . . . . . . . . . . . . 14
⊢ (𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴 → ◡𝐺:𝐴–1-1-onto→(1...(♯‘𝐴))) |
| 58 | 56, 57 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → ◡𝐺:𝐴–1-1-onto→(1...(♯‘𝐴))) |
| 59 | | f1of 6848 |
. . . . . . . . . . . . 13
⊢ (◡𝐺:𝐴–1-1-onto→(1...(♯‘𝐴)) → ◡𝐺:𝐴⟶(1...(♯‘𝐴))) |
| 60 | 58, 59 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → ◡𝐺:𝐴⟶(1...(♯‘𝐴))) |
| 61 | | simprr 773 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → 𝑘 ∈ 𝐴) |
| 62 | 60, 61 | ffvelcdmd 7105 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → (◡𝐺‘𝑘) ∈ (1...(♯‘𝐴))) |
| 63 | 62 | elfzelzd 13565 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → (◡𝐺‘𝑘) ∈ ℤ) |
| 64 | 63 | zred 12722 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → (◡𝐺‘𝑘) ∈ ℝ) |
| 65 | 18 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → (♯‘𝐴) ∈
ℕ0) |
| 66 | 65 | nn0red 12588 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → (♯‘𝐴) ∈ ℝ) |
| 67 | | elfzle2 13568 |
. . . . . . . . . 10
⊢ ((◡𝐺‘𝑘) ∈ (1...(♯‘𝐴)) → (◡𝐺‘𝑘) ≤ (♯‘𝐴)) |
| 68 | 62, 67 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → (◡𝐺‘𝑘) ≤ (♯‘𝐴)) |
| 69 | 64, 66, 68 | lensymd 11412 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → ¬ (♯‘𝐴) < (◡𝐺‘𝑘)) |
| 70 | 4 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → 𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴)) |
| 71 | 26 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → (♯‘𝐴) ∈ (1...(♯‘𝐴))) |
| 72 | | isorel 7346 |
. . . . . . . . . 10
⊢ ((𝐺 Isom < , <
((1...(♯‘𝐴)),
𝐴) ∧
((♯‘𝐴) ∈
(1...(♯‘𝐴))
∧ (◡𝐺‘𝑘) ∈ (1...(♯‘𝐴)))) →
((♯‘𝐴) <
(◡𝐺‘𝑘) ↔ (𝐺‘(♯‘𝐴)) < (𝐺‘(◡𝐺‘𝑘)))) |
| 73 | 70, 71, 62, 72 | syl12anc 837 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → ((♯‘𝐴) < (◡𝐺‘𝑘) ↔ (𝐺‘(♯‘𝐴)) < (𝐺‘(◡𝐺‘𝑘)))) |
| 74 | | f1ocnvfv2 7297 |
. . . . . . . . . . 11
⊢ ((𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴 ∧ 𝑘 ∈ 𝐴) → (𝐺‘(◡𝐺‘𝑘)) = 𝑘) |
| 75 | 56, 61, 74 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → (𝐺‘(◡𝐺‘𝑘)) = 𝑘) |
| 76 | 75 | breq2d 5155 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → ((𝐺‘(♯‘𝐴)) < (𝐺‘(◡𝐺‘𝑘)) ↔ (𝐺‘(♯‘𝐴)) < 𝑘)) |
| 77 | 73, 76 | bitrd 279 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → ((♯‘𝐴) < (◡𝐺‘𝑘) ↔ (𝐺‘(♯‘𝐴)) < 𝑘)) |
| 78 | 69, 77 | mtbid 324 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘 ∈ 𝐴)) → ¬ (𝐺‘(♯‘𝐴)) < 𝑘) |
| 79 | 78 | expr 456 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁)) → (𝑘 ∈ 𝐴 → ¬ (𝐺‘(♯‘𝐴)) < 𝑘)) |
| 80 | 55, 79 | mt2d 136 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁)) → ¬ 𝑘 ∈ 𝐴) |
| 81 | 43, 80 | eldifd 3962 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁)) → 𝑘 ∈ ((𝑀...𝑁) ∖ 𝐴)) |
| 82 | | seqcoll2.7 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀...𝑁) ∖ 𝐴)) → (𝐹‘𝑘) = 𝑍) |
| 83 | 81, 82 | syldan 591 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁)) → (𝐹‘𝑘) = 𝑍) |
| 84 | 1, 29, 31, 38, 83 | seqid2 14089 |
. 2
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝐺‘(♯‘𝐴))) = (seq𝑀( + , 𝐹)‘𝑁)) |
| 85 | | seqcoll2.1 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → (𝑍 + 𝑘) = 𝑘) |
| 86 | | seqcoll2.a |
. . 3
⊢ (𝜑 → 𝑍 ∈ 𝑆) |
| 87 | 3, 2 | sstrdi 3996 |
. . 3
⊢ (𝜑 → 𝐴 ⊆ (ℤ≥‘𝑀)) |
| 88 | 33 | ssdifd 4145 |
. . . . 5
⊢ (𝜑 → ((𝑀...(𝐺‘(♯‘𝐴))) ∖ 𝐴) ⊆ ((𝑀...𝑁) ∖ 𝐴)) |
| 89 | 88 | sselda 3983 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀...(𝐺‘(♯‘𝐴))) ∖ 𝐴)) → 𝑘 ∈ ((𝑀...𝑁) ∖ 𝐴)) |
| 90 | 89, 82 | syldan 591 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀...(𝐺‘(♯‘𝐴))) ∖ 𝐴)) → (𝐹‘𝑘) = 𝑍) |
| 91 | | seqcoll2.8 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (𝐻‘𝑛) = (𝐹‘(𝐺‘𝑛))) |
| 92 | 85, 1, 37, 86, 4, 26, 87, 36, 90, 91 | seqcoll 14503 |
. 2
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝐺‘(♯‘𝐴))) = (seq1( + , 𝐻)‘(♯‘𝐴))) |
| 93 | 84, 92 | eqtr3d 2779 |
1
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = (seq1( + , 𝐻)‘(♯‘𝐴))) |