Proof of Theorem isercolllem3
Step | Hyp | Ref
| Expression |
1 | | addid2 10098 |
. . 3
⊢ (𝑛 ∈ ℂ → (0 +
𝑛) = 𝑛) |
2 | 1 | adantl 481 |
. 2
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑛 ∈ ℂ) → (0 +
𝑛) = 𝑛) |
3 | | addid1 10095 |
. . 3
⊢ (𝑛 ∈ ℂ → (𝑛 + 0) = 𝑛) |
4 | 3 | adantl 481 |
. 2
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑛 ∈ ℂ) → (𝑛 + 0) = 𝑛) |
5 | | addcl 9897 |
. . 3
⊢ ((𝑛 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝑛 + 𝑘) ∈ ℂ) |
6 | 5 | adantl 481 |
. 2
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ (𝑛 ∈ ℂ ∧ 𝑘 ∈ ℂ)) → (𝑛 + 𝑘) ∈ ℂ) |
7 | | 0cnd 9912 |
. 2
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → 0 ∈
ℂ) |
8 | | cnvimass 5404 |
. . . . 5
⊢ (◡𝐺 “ (𝑀...𝑁)) ⊆ dom 𝐺 |
9 | | isercoll.g |
. . . . . . 7
⊢ (𝜑 → 𝐺:ℕ⟶𝑍) |
10 | 9 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → 𝐺:ℕ⟶𝑍) |
11 | | fdm 5964 |
. . . . . 6
⊢ (𝐺:ℕ⟶𝑍 → dom 𝐺 = ℕ) |
12 | 10, 11 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → dom 𝐺 = ℕ) |
13 | 8, 12 | syl5sseq 3616 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (◡𝐺 “ (𝑀...𝑁)) ⊆ ℕ) |
14 | | isercoll.z |
. . . . 5
⊢ 𝑍 =
(ℤ≥‘𝑀) |
15 | | isercoll.m |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℤ) |
16 | | isercoll.i |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) < (𝐺‘(𝑘 + 1))) |
17 | 14, 15, 9, 16 | isercolllem1 14243 |
. . . 4
⊢ ((𝜑 ∧ (◡𝐺 “ (𝑀...𝑁)) ⊆ ℕ) → (𝐺 ↾ (◡𝐺 “ (𝑀...𝑁))) Isom < , < ((◡𝐺 “ (𝑀...𝑁)), (𝐺 “ (◡𝐺 “ (𝑀...𝑁))))) |
18 | 13, 17 | syldan 486 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝐺 ↾ (◡𝐺 “ (𝑀...𝑁))) Isom < , < ((◡𝐺 “ (𝑀...𝑁)), (𝐺 “ (◡𝐺 “ (𝑀...𝑁))))) |
19 | 14, 15, 9, 16 | isercolllem2 14244 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) →
(1...(#‘(𝐺 “
(◡𝐺 “ (𝑀...𝑁))))) = (◡𝐺 “ (𝑀...𝑁))) |
20 | | isoeq4 6470 |
. . . 4
⊢
((1...(#‘(𝐺
“ (◡𝐺 “ (𝑀...𝑁))))) = (◡𝐺 “ (𝑀...𝑁)) → ((𝐺 ↾ (◡𝐺 “ (𝑀...𝑁))) Isom < , < ((1...(#‘(𝐺 “ (◡𝐺 “ (𝑀...𝑁))))), (𝐺 “ (◡𝐺 “ (𝑀...𝑁)))) ↔ (𝐺 ↾ (◡𝐺 “ (𝑀...𝑁))) Isom < , < ((◡𝐺 “ (𝑀...𝑁)), (𝐺 “ (◡𝐺 “ (𝑀...𝑁)))))) |
21 | 19, 20 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → ((𝐺 ↾ (◡𝐺 “ (𝑀...𝑁))) Isom < , < ((1...(#‘(𝐺 “ (◡𝐺 “ (𝑀...𝑁))))), (𝐺 “ (◡𝐺 “ (𝑀...𝑁)))) ↔ (𝐺 ↾ (◡𝐺 “ (𝑀...𝑁))) Isom < , < ((◡𝐺 “ (𝑀...𝑁)), (𝐺 “ (◡𝐺 “ (𝑀...𝑁)))))) |
22 | 18, 21 | mpbird 246 |
. 2
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝐺 ↾ (◡𝐺 “ (𝑀...𝑁))) Isom < , < ((1...(#‘(𝐺 “ (◡𝐺 “ (𝑀...𝑁))))), (𝐺 “ (◡𝐺 “ (𝑀...𝑁))))) |
23 | 8 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (◡𝐺 “ (𝑀...𝑁)) ⊆ dom 𝐺) |
24 | | sseqin2 3779 |
. . . . 5
⊢ ((◡𝐺 “ (𝑀...𝑁)) ⊆ dom 𝐺 ↔ (dom 𝐺 ∩ (◡𝐺 “ (𝑀...𝑁))) = (◡𝐺 “ (𝑀...𝑁))) |
25 | 23, 24 | sylib 207 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (dom 𝐺 ∩ (◡𝐺 “ (𝑀...𝑁))) = (◡𝐺 “ (𝑀...𝑁))) |
26 | | 1nn 10908 |
. . . . . . 7
⊢ 1 ∈
ℕ |
27 | 26 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → 1 ∈
ℕ) |
28 | | ffvelrn 6265 |
. . . . . . . . . 10
⊢ ((𝐺:ℕ⟶𝑍 ∧ 1 ∈ ℕ) →
(𝐺‘1) ∈ 𝑍) |
29 | 9, 26, 28 | sylancl 693 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺‘1) ∈ 𝑍) |
30 | 29, 14 | syl6eleq 2698 |
. . . . . . . 8
⊢ (𝜑 → (𝐺‘1) ∈
(ℤ≥‘𝑀)) |
31 | 30 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝐺‘1) ∈
(ℤ≥‘𝑀)) |
32 | | simpr 476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → 𝑁 ∈
(ℤ≥‘(𝐺‘1))) |
33 | | elfzuzb 12207 |
. . . . . . 7
⊢ ((𝐺‘1) ∈ (𝑀...𝑁) ↔ ((𝐺‘1) ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1)))) |
34 | 31, 32, 33 | sylanbrc 695 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝐺‘1) ∈ (𝑀...𝑁)) |
35 | | ffn 5958 |
. . . . . . 7
⊢ (𝐺:ℕ⟶𝑍 → 𝐺 Fn ℕ) |
36 | | elpreima 6245 |
. . . . . . 7
⊢ (𝐺 Fn ℕ → (1 ∈
(◡𝐺 “ (𝑀...𝑁)) ↔ (1 ∈ ℕ ∧ (𝐺‘1) ∈ (𝑀...𝑁)))) |
37 | 10, 35, 36 | 3syl 18 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (1 ∈
(◡𝐺 “ (𝑀...𝑁)) ↔ (1 ∈ ℕ ∧ (𝐺‘1) ∈ (𝑀...𝑁)))) |
38 | 27, 34, 37 | mpbir2and 959 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → 1 ∈
(◡𝐺 “ (𝑀...𝑁))) |
39 | | ne0i 3880 |
. . . . 5
⊢ (1 ∈
(◡𝐺 “ (𝑀...𝑁)) → (◡𝐺 “ (𝑀...𝑁)) ≠ ∅) |
40 | 38, 39 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (◡𝐺 “ (𝑀...𝑁)) ≠ ∅) |
41 | 25, 40 | eqnetrd 2849 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (dom 𝐺 ∩ (◡𝐺 “ (𝑀...𝑁))) ≠ ∅) |
42 | | imadisj 5403 |
. . . 4
⊢ ((𝐺 “ (◡𝐺 “ (𝑀...𝑁))) = ∅ ↔ (dom 𝐺 ∩ (◡𝐺 “ (𝑀...𝑁))) = ∅) |
43 | 42 | necon3bii 2834 |
. . 3
⊢ ((𝐺 “ (◡𝐺 “ (𝑀...𝑁))) ≠ ∅ ↔ (dom 𝐺 ∩ (◡𝐺 “ (𝑀...𝑁))) ≠ ∅) |
44 | 41, 43 | sylibr 223 |
. 2
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝐺 “ (◡𝐺 “ (𝑀...𝑁))) ≠ ∅) |
45 | | ffun 5961 |
. . . 4
⊢ (𝐺:ℕ⟶𝑍 → Fun 𝐺) |
46 | | funimacnv 5884 |
. . . 4
⊢ (Fun
𝐺 → (𝐺 “ (◡𝐺 “ (𝑀...𝑁))) = ((𝑀...𝑁) ∩ ran 𝐺)) |
47 | 10, 45, 46 | 3syl 18 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝐺 “ (◡𝐺 “ (𝑀...𝑁))) = ((𝑀...𝑁) ∩ ran 𝐺)) |
48 | | inss1 3795 |
. . . 4
⊢ ((𝑀...𝑁) ∩ ran 𝐺) ⊆ (𝑀...𝑁) |
49 | 48 | a1i 11 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → ((𝑀...𝑁) ∩ ran 𝐺) ⊆ (𝑀...𝑁)) |
50 | 47, 49 | eqsstrd 3602 |
. 2
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝐺 “ (◡𝐺 “ (𝑀...𝑁))) ⊆ (𝑀...𝑁)) |
51 | | simpl 472 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → 𝜑) |
52 | | elfzuz 12209 |
. . . 4
⊢ (𝑛 ∈ (𝑀...𝑁) → 𝑛 ∈ (ℤ≥‘𝑀)) |
53 | 52, 14 | syl6eleqr 2699 |
. . 3
⊢ (𝑛 ∈ (𝑀...𝑁) → 𝑛 ∈ 𝑍) |
54 | | isercoll.f |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ ℂ) |
55 | 51, 53, 54 | syl2an 493 |
. 2
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑛 ∈ (𝑀...𝑁)) → (𝐹‘𝑛) ∈ ℂ) |
56 | 47 | difeq2d 3690 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → ((𝑀...𝑁) ∖ (𝐺 “ (◡𝐺 “ (𝑀...𝑁)))) = ((𝑀...𝑁) ∖ ((𝑀...𝑁) ∩ ran 𝐺))) |
57 | | difin 3823 |
. . . . . 6
⊢ ((𝑀...𝑁) ∖ ((𝑀...𝑁) ∩ ran 𝐺)) = ((𝑀...𝑁) ∖ ran 𝐺) |
58 | 56, 57 | syl6eq 2660 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → ((𝑀...𝑁) ∖ (𝐺 “ (◡𝐺 “ (𝑀...𝑁)))) = ((𝑀...𝑁) ∖ ran 𝐺)) |
59 | 53 | ssriv 3572 |
. . . . . 6
⊢ (𝑀...𝑁) ⊆ 𝑍 |
60 | | ssdif 3707 |
. . . . . 6
⊢ ((𝑀...𝑁) ⊆ 𝑍 → ((𝑀...𝑁) ∖ ran 𝐺) ⊆ (𝑍 ∖ ran 𝐺)) |
61 | 59, 60 | mp1i 13 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → ((𝑀...𝑁) ∖ ran 𝐺) ⊆ (𝑍 ∖ ran 𝐺)) |
62 | 58, 61 | eqsstrd 3602 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → ((𝑀...𝑁) ∖ (𝐺 “ (◡𝐺 “ (𝑀...𝑁)))) ⊆ (𝑍 ∖ ran 𝐺)) |
63 | 62 | sselda 3568 |
. . 3
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑛 ∈ ((𝑀...𝑁) ∖ (𝐺 “ (◡𝐺 “ (𝑀...𝑁))))) → 𝑛 ∈ (𝑍 ∖ ran 𝐺)) |
64 | | isercoll.0 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑍 ∖ ran 𝐺)) → (𝐹‘𝑛) = 0) |
65 | 64 | adantlr 747 |
. . 3
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑛 ∈ (𝑍 ∖ ran 𝐺)) → (𝐹‘𝑛) = 0) |
66 | 63, 65 | syldan 486 |
. 2
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑛 ∈ ((𝑀...𝑁) ∖ (𝐺 “ (◡𝐺 “ (𝑀...𝑁))))) → (𝐹‘𝑛) = 0) |
67 | | elfznn 12241 |
. . . 4
⊢ (𝑘 ∈ (1...(#‘(𝐺 “ (◡𝐺 “ (𝑀...𝑁))))) → 𝑘 ∈ ℕ) |
68 | | isercoll.h |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘𝑘) = (𝐹‘(𝐺‘𝑘))) |
69 | 51, 67, 68 | syl2an 493 |
. . 3
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈ (1...(#‘(𝐺 “ (◡𝐺 “ (𝑀...𝑁)))))) → (𝐻‘𝑘) = (𝐹‘(𝐺‘𝑘))) |
70 | 19 | eleq2d 2673 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝑘 ∈ (1...(#‘(𝐺 “ (◡𝐺 “ (𝑀...𝑁))))) ↔ 𝑘 ∈ (◡𝐺 “ (𝑀...𝑁)))) |
71 | 70 | biimpa 500 |
. . . . 5
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈ (1...(#‘(𝐺 “ (◡𝐺 “ (𝑀...𝑁)))))) → 𝑘 ∈ (◡𝐺 “ (𝑀...𝑁))) |
72 | | fvres 6117 |
. . . . 5
⊢ (𝑘 ∈ (◡𝐺 “ (𝑀...𝑁)) → ((𝐺 ↾ (◡𝐺 “ (𝑀...𝑁)))‘𝑘) = (𝐺‘𝑘)) |
73 | 71, 72 | syl 17 |
. . . 4
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈ (1...(#‘(𝐺 “ (◡𝐺 “ (𝑀...𝑁)))))) → ((𝐺 ↾ (◡𝐺 “ (𝑀...𝑁)))‘𝑘) = (𝐺‘𝑘)) |
74 | 73 | fveq2d 6107 |
. . 3
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈ (1...(#‘(𝐺 “ (◡𝐺 “ (𝑀...𝑁)))))) → (𝐹‘((𝐺 ↾ (◡𝐺 “ (𝑀...𝑁)))‘𝑘)) = (𝐹‘(𝐺‘𝑘))) |
75 | 69, 74 | eqtr4d 2647 |
. 2
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈ (1...(#‘(𝐺 “ (◡𝐺 “ (𝑀...𝑁)))))) → (𝐻‘𝑘) = (𝐹‘((𝐺 ↾ (◡𝐺 “ (𝑀...𝑁)))‘𝑘))) |
76 | 2, 4, 6, 7, 22, 44, 50, 55, 66, 75 | seqcoll2 13106 |
1
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (seq𝑀( + , 𝐹)‘𝑁) = (seq1( + , 𝐻)‘(#‘(𝐺 “ (◡𝐺 “ (𝑀...𝑁)))))) |