Proof of Theorem isercolllem3
Step | Hyp | Ref
| Expression |
1 | | addid2 10382 |
. . 3
⊢ (𝑛 ∈ ℂ → (0 +
𝑛) = 𝑛) |
2 | 1 | adantl 473 |
. 2
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑛 ∈ ℂ) → (0 +
𝑛) = 𝑛) |
3 | | addid1 10379 |
. . 3
⊢ (𝑛 ∈ ℂ → (𝑛 + 0) = 𝑛) |
4 | 3 | adantl 473 |
. 2
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑛 ∈ ℂ) → (𝑛 + 0) = 𝑛) |
5 | | addcl 10181 |
. . 3
⊢ ((𝑛 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝑛 + 𝑘) ∈ ℂ) |
6 | 5 | adantl 473 |
. 2
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ (𝑛 ∈ ℂ ∧ 𝑘 ∈ ℂ)) → (𝑛 + 𝑘) ∈ ℂ) |
7 | | 0cnd 10196 |
. 2
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → 0 ∈
ℂ) |
8 | | cnvimass 5631 |
. . . . 5
⊢ (◡𝐺 “ (𝑀...𝑁)) ⊆ dom 𝐺 |
9 | | isercoll.g |
. . . . . . 7
⊢ (𝜑 → 𝐺:ℕ⟶𝑍) |
10 | 9 | adantr 472 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → 𝐺:ℕ⟶𝑍) |
11 | | fdm 6200 |
. . . . . 6
⊢ (𝐺:ℕ⟶𝑍 → dom 𝐺 = ℕ) |
12 | 10, 11 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → dom 𝐺 = ℕ) |
13 | 8, 12 | syl5sseq 3782 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (◡𝐺 “ (𝑀...𝑁)) ⊆ ℕ) |
14 | | isercoll.z |
. . . . 5
⊢ 𝑍 =
(ℤ≥‘𝑀) |
15 | | isercoll.m |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℤ) |
16 | | isercoll.i |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) < (𝐺‘(𝑘 + 1))) |
17 | 14, 15, 9, 16 | isercolllem1 14565 |
. . . 4
⊢ ((𝜑 ∧ (◡𝐺 “ (𝑀...𝑁)) ⊆ ℕ) → (𝐺 ↾ (◡𝐺 “ (𝑀...𝑁))) Isom < , < ((◡𝐺 “ (𝑀...𝑁)), (𝐺 “ (◡𝐺 “ (𝑀...𝑁))))) |
18 | 13, 17 | syldan 488 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝐺 ↾ (◡𝐺 “ (𝑀...𝑁))) Isom < , < ((◡𝐺 “ (𝑀...𝑁)), (𝐺 “ (◡𝐺 “ (𝑀...𝑁))))) |
19 | 14, 15, 9, 16 | isercolllem2 14566 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) →
(1...(♯‘(𝐺
“ (◡𝐺 “ (𝑀...𝑁))))) = (◡𝐺 “ (𝑀...𝑁))) |
20 | | isoeq4 6721 |
. . . 4
⊢
((1...(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑁))))) = (◡𝐺 “ (𝑀...𝑁)) → ((𝐺 ↾ (◡𝐺 “ (𝑀...𝑁))) Isom < , <
((1...(♯‘(𝐺
“ (◡𝐺 “ (𝑀...𝑁))))), (𝐺 “ (◡𝐺 “ (𝑀...𝑁)))) ↔ (𝐺 ↾ (◡𝐺 “ (𝑀...𝑁))) Isom < , < ((◡𝐺 “ (𝑀...𝑁)), (𝐺 “ (◡𝐺 “ (𝑀...𝑁)))))) |
21 | 19, 20 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → ((𝐺 ↾ (◡𝐺 “ (𝑀...𝑁))) Isom < , <
((1...(♯‘(𝐺
“ (◡𝐺 “ (𝑀...𝑁))))), (𝐺 “ (◡𝐺 “ (𝑀...𝑁)))) ↔ (𝐺 ↾ (◡𝐺 “ (𝑀...𝑁))) Isom < , < ((◡𝐺 “ (𝑀...𝑁)), (𝐺 “ (◡𝐺 “ (𝑀...𝑁)))))) |
22 | 18, 21 | mpbird 247 |
. 2
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝐺 ↾ (◡𝐺 “ (𝑀...𝑁))) Isom < , <
((1...(♯‘(𝐺
“ (◡𝐺 “ (𝑀...𝑁))))), (𝐺 “ (◡𝐺 “ (𝑀...𝑁))))) |
23 | 8 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (◡𝐺 “ (𝑀...𝑁)) ⊆ dom 𝐺) |
24 | | sseqin2 3948 |
. . . . 5
⊢ ((◡𝐺 “ (𝑀...𝑁)) ⊆ dom 𝐺 ↔ (dom 𝐺 ∩ (◡𝐺 “ (𝑀...𝑁))) = (◡𝐺 “ (𝑀...𝑁))) |
25 | 23, 24 | sylib 208 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (dom 𝐺 ∩ (◡𝐺 “ (𝑀...𝑁))) = (◡𝐺 “ (𝑀...𝑁))) |
26 | | 1nn 11194 |
. . . . . . 7
⊢ 1 ∈
ℕ |
27 | 26 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → 1 ∈
ℕ) |
28 | | ffvelrn 6508 |
. . . . . . . . . 10
⊢ ((𝐺:ℕ⟶𝑍 ∧ 1 ∈ ℕ) →
(𝐺‘1) ∈ 𝑍) |
29 | 9, 26, 28 | sylancl 697 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺‘1) ∈ 𝑍) |
30 | 29, 14 | syl6eleq 2837 |
. . . . . . . 8
⊢ (𝜑 → (𝐺‘1) ∈
(ℤ≥‘𝑀)) |
31 | 30 | adantr 472 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝐺‘1) ∈
(ℤ≥‘𝑀)) |
32 | | simpr 479 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → 𝑁 ∈
(ℤ≥‘(𝐺‘1))) |
33 | | elfzuzb 12500 |
. . . . . . 7
⊢ ((𝐺‘1) ∈ (𝑀...𝑁) ↔ ((𝐺‘1) ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1)))) |
34 | 31, 32, 33 | sylanbrc 701 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝐺‘1) ∈ (𝑀...𝑁)) |
35 | | ffn 6194 |
. . . . . . 7
⊢ (𝐺:ℕ⟶𝑍 → 𝐺 Fn ℕ) |
36 | | elpreima 6488 |
. . . . . . 7
⊢ (𝐺 Fn ℕ → (1 ∈
(◡𝐺 “ (𝑀...𝑁)) ↔ (1 ∈ ℕ ∧ (𝐺‘1) ∈ (𝑀...𝑁)))) |
37 | 10, 35, 36 | 3syl 18 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (1 ∈
(◡𝐺 “ (𝑀...𝑁)) ↔ (1 ∈ ℕ ∧ (𝐺‘1) ∈ (𝑀...𝑁)))) |
38 | 27, 34, 37 | mpbir2and 995 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → 1 ∈
(◡𝐺 “ (𝑀...𝑁))) |
39 | | ne0i 4052 |
. . . . 5
⊢ (1 ∈
(◡𝐺 “ (𝑀...𝑁)) → (◡𝐺 “ (𝑀...𝑁)) ≠ ∅) |
40 | 38, 39 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (◡𝐺 “ (𝑀...𝑁)) ≠ ∅) |
41 | 25, 40 | eqnetrd 2987 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (dom 𝐺 ∩ (◡𝐺 “ (𝑀...𝑁))) ≠ ∅) |
42 | | imadisj 5630 |
. . . 4
⊢ ((𝐺 “ (◡𝐺 “ (𝑀...𝑁))) = ∅ ↔ (dom 𝐺 ∩ (◡𝐺 “ (𝑀...𝑁))) = ∅) |
43 | 42 | necon3bii 2972 |
. . 3
⊢ ((𝐺 “ (◡𝐺 “ (𝑀...𝑁))) ≠ ∅ ↔ (dom 𝐺 ∩ (◡𝐺 “ (𝑀...𝑁))) ≠ ∅) |
44 | 41, 43 | sylibr 224 |
. 2
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝐺 “ (◡𝐺 “ (𝑀...𝑁))) ≠ ∅) |
45 | | ffun 6197 |
. . . 4
⊢ (𝐺:ℕ⟶𝑍 → Fun 𝐺) |
46 | | funimacnv 6119 |
. . . 4
⊢ (Fun
𝐺 → (𝐺 “ (◡𝐺 “ (𝑀...𝑁))) = ((𝑀...𝑁) ∩ ran 𝐺)) |
47 | 10, 45, 46 | 3syl 18 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝐺 “ (◡𝐺 “ (𝑀...𝑁))) = ((𝑀...𝑁) ∩ ran 𝐺)) |
48 | | inss1 3964 |
. . . 4
⊢ ((𝑀...𝑁) ∩ ran 𝐺) ⊆ (𝑀...𝑁) |
49 | 48 | a1i 11 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → ((𝑀...𝑁) ∩ ran 𝐺) ⊆ (𝑀...𝑁)) |
50 | 47, 49 | eqsstrd 3768 |
. 2
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝐺 “ (◡𝐺 “ (𝑀...𝑁))) ⊆ (𝑀...𝑁)) |
51 | | simpl 474 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → 𝜑) |
52 | | elfzuz 12502 |
. . . 4
⊢ (𝑛 ∈ (𝑀...𝑁) → 𝑛 ∈ (ℤ≥‘𝑀)) |
53 | 52, 14 | syl6eleqr 2838 |
. . 3
⊢ (𝑛 ∈ (𝑀...𝑁) → 𝑛 ∈ 𝑍) |
54 | | isercoll.f |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ ℂ) |
55 | 51, 53, 54 | syl2an 495 |
. 2
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑛 ∈ (𝑀...𝑁)) → (𝐹‘𝑛) ∈ ℂ) |
56 | 47 | difeq2d 3859 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → ((𝑀...𝑁) ∖ (𝐺 “ (◡𝐺 “ (𝑀...𝑁)))) = ((𝑀...𝑁) ∖ ((𝑀...𝑁) ∩ ran 𝐺))) |
57 | | difin 3992 |
. . . . . 6
⊢ ((𝑀...𝑁) ∖ ((𝑀...𝑁) ∩ ran 𝐺)) = ((𝑀...𝑁) ∖ ran 𝐺) |
58 | 56, 57 | syl6eq 2798 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → ((𝑀...𝑁) ∖ (𝐺 “ (◡𝐺 “ (𝑀...𝑁)))) = ((𝑀...𝑁) ∖ ran 𝐺)) |
59 | 53 | ssriv 3736 |
. . . . . 6
⊢ (𝑀...𝑁) ⊆ 𝑍 |
60 | | ssdif 3876 |
. . . . . 6
⊢ ((𝑀...𝑁) ⊆ 𝑍 → ((𝑀...𝑁) ∖ ran 𝐺) ⊆ (𝑍 ∖ ran 𝐺)) |
61 | 59, 60 | mp1i 13 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → ((𝑀...𝑁) ∖ ran 𝐺) ⊆ (𝑍 ∖ ran 𝐺)) |
62 | 58, 61 | eqsstrd 3768 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → ((𝑀...𝑁) ∖ (𝐺 “ (◡𝐺 “ (𝑀...𝑁)))) ⊆ (𝑍 ∖ ran 𝐺)) |
63 | 62 | sselda 3732 |
. . 3
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑛 ∈ ((𝑀...𝑁) ∖ (𝐺 “ (◡𝐺 “ (𝑀...𝑁))))) → 𝑛 ∈ (𝑍 ∖ ran 𝐺)) |
64 | | isercoll.0 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑍 ∖ ran 𝐺)) → (𝐹‘𝑛) = 0) |
65 | 64 | adantlr 753 |
. . 3
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑛 ∈ (𝑍 ∖ ran 𝐺)) → (𝐹‘𝑛) = 0) |
66 | 63, 65 | syldan 488 |
. 2
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑛 ∈ ((𝑀...𝑁) ∖ (𝐺 “ (◡𝐺 “ (𝑀...𝑁))))) → (𝐹‘𝑛) = 0) |
67 | | elfznn 12534 |
. . . 4
⊢ (𝑘 ∈
(1...(♯‘(𝐺
“ (◡𝐺 “ (𝑀...𝑁))))) → 𝑘 ∈ ℕ) |
68 | | isercoll.h |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘𝑘) = (𝐹‘(𝐺‘𝑘))) |
69 | 51, 67, 68 | syl2an 495 |
. . 3
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(1...(♯‘(𝐺
“ (◡𝐺 “ (𝑀...𝑁)))))) → (𝐻‘𝑘) = (𝐹‘(𝐺‘𝑘))) |
70 | 19 | eleq2d 2813 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (𝑘 ∈
(1...(♯‘(𝐺
“ (◡𝐺 “ (𝑀...𝑁))))) ↔ 𝑘 ∈ (◡𝐺 “ (𝑀...𝑁)))) |
71 | 70 | biimpa 502 |
. . . . 5
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(1...(♯‘(𝐺
“ (◡𝐺 “ (𝑀...𝑁)))))) → 𝑘 ∈ (◡𝐺 “ (𝑀...𝑁))) |
72 | | fvres 6356 |
. . . . 5
⊢ (𝑘 ∈ (◡𝐺 “ (𝑀...𝑁)) → ((𝐺 ↾ (◡𝐺 “ (𝑀...𝑁)))‘𝑘) = (𝐺‘𝑘)) |
73 | 71, 72 | syl 17 |
. . . 4
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(1...(♯‘(𝐺
“ (◡𝐺 “ (𝑀...𝑁)))))) → ((𝐺 ↾ (◡𝐺 “ (𝑀...𝑁)))‘𝑘) = (𝐺‘𝑘)) |
74 | 73 | fveq2d 6344 |
. . 3
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(1...(♯‘(𝐺
“ (◡𝐺 “ (𝑀...𝑁)))))) → (𝐹‘((𝐺 ↾ (◡𝐺 “ (𝑀...𝑁)))‘𝑘)) = (𝐹‘(𝐺‘𝑘))) |
75 | 69, 74 | eqtr4d 2785 |
. 2
⊢ (((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(1...(♯‘(𝐺
“ (◡𝐺 “ (𝑀...𝑁)))))) → (𝐻‘𝑘) = (𝐹‘((𝐺 ↾ (◡𝐺 “ (𝑀...𝑁)))‘𝑘))) |
76 | 2, 4, 6, 7, 22, 44, 50, 55, 66, 75 | seqcoll2 13412 |
1
⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘(𝐺‘1))) → (seq𝑀( + , 𝐹)‘𝑁) = (seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑁)))))) |