Step | Hyp | Ref
| Expression |
1 | | isercoll2.z |
. . 3
⊢ 𝑍 =
(ℤ≥‘𝑀) |
2 | | isercoll2.m |
. . 3
⊢ (𝜑 → 𝑀 ∈ ℤ) |
3 | | 1z 11407 |
. . . 4
⊢ 1 ∈
ℤ |
4 | | zsubcl 11419 |
. . . 4
⊢ ((1
∈ ℤ ∧ 𝑀
∈ ℤ) → (1 − 𝑀) ∈ ℤ) |
5 | 3, 2, 4 | sylancr 695 |
. . 3
⊢ (𝜑 → (1 − 𝑀) ∈
ℤ) |
6 | | seqex 12803 |
. . . 4
⊢ seq𝑀( + , 𝐻) ∈ V |
7 | 6 | a1i 11 |
. . 3
⊢ (𝜑 → seq𝑀( + , 𝐻) ∈ V) |
8 | | seqex 12803 |
. . . 4
⊢ seq1( + ,
(𝑥 ∈ ℕ ↦
(𝐻‘(𝑀 + (𝑥 − 1))))) ∈ V |
9 | 8 | a1i 11 |
. . 3
⊢ (𝜑 → seq1( + , (𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1))))) ∈ V) |
10 | | simpr 477 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ 𝑍) |
11 | 10, 1 | syl6eleq 2711 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ (ℤ≥‘𝑀)) |
12 | 5 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (1 − 𝑀) ∈ ℤ) |
13 | | simpl 473 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝜑) |
14 | | elfzuz 12338 |
. . . . . . 7
⊢ (𝑗 ∈ (𝑀...𝑘) → 𝑗 ∈ (ℤ≥‘𝑀)) |
15 | 14, 1 | syl6eleqr 2712 |
. . . . . 6
⊢ (𝑗 ∈ (𝑀...𝑘) → 𝑗 ∈ 𝑍) |
16 | | simpr 477 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ 𝑍) |
17 | 16, 1 | syl6eleq 2711 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ (ℤ≥‘𝑀)) |
18 | | eluzelz 11697 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → 𝑗 ∈ ℤ) |
19 | 17, 18 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ ℤ) |
20 | 19 | zcnd 11483 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ ℂ) |
21 | 2 | zcnd 11483 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℂ) |
22 | 21 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑀 ∈ ℂ) |
23 | | 1cnd 10056 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 1 ∈ ℂ) |
24 | 20, 22, 23 | subadd23d 10414 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → ((𝑗 − 𝑀) + 1) = (𝑗 + (1 − 𝑀))) |
25 | | uznn0sub 11719 |
. . . . . . . . . . 11
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → (𝑗 − 𝑀) ∈
ℕ0) |
26 | 17, 25 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝑗 − 𝑀) ∈
ℕ0) |
27 | | nn0p1nn 11332 |
. . . . . . . . . 10
⊢ ((𝑗 − 𝑀) ∈ ℕ0 → ((𝑗 − 𝑀) + 1) ∈ ℕ) |
28 | 26, 27 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → ((𝑗 − 𝑀) + 1) ∈ ℕ) |
29 | 24, 28 | eqeltrrd 2702 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝑗 + (1 − 𝑀)) ∈ ℕ) |
30 | | oveq1 6657 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑗 + (1 − 𝑀)) → (𝑥 − 1) = ((𝑗 + (1 − 𝑀)) − 1)) |
31 | 30 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑗 + (1 − 𝑀)) → (𝑀 + (𝑥 − 1)) = (𝑀 + ((𝑗 + (1 − 𝑀)) − 1))) |
32 | 31 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑥 = (𝑗 + (1 − 𝑀)) → (𝐻‘(𝑀 + (𝑥 − 1))) = (𝐻‘(𝑀 + ((𝑗 + (1 − 𝑀)) − 1)))) |
33 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1)))) = (𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1)))) |
34 | | fvex 6201 |
. . . . . . . . 9
⊢ (𝐻‘(𝑀 + ((𝑗 + (1 − 𝑀)) − 1))) ∈ V |
35 | 32, 33, 34 | fvmpt 6282 |
. . . . . . . 8
⊢ ((𝑗 + (1 − 𝑀)) ∈ ℕ → ((𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1))))‘(𝑗 + (1 − 𝑀))) = (𝐻‘(𝑀 + ((𝑗 + (1 − 𝑀)) − 1)))) |
36 | 29, 35 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → ((𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1))))‘(𝑗 + (1 − 𝑀))) = (𝐻‘(𝑀 + ((𝑗 + (1 − 𝑀)) − 1)))) |
37 | 24 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (((𝑗 − 𝑀) + 1) − 1) = ((𝑗 + (1 − 𝑀)) − 1)) |
38 | 26 | nn0cnd 11353 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝑗 − 𝑀) ∈ ℂ) |
39 | | ax-1cn 9994 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℂ |
40 | | pncan 10287 |
. . . . . . . . . . . 12
⊢ (((𝑗 − 𝑀) ∈ ℂ ∧ 1 ∈ ℂ)
→ (((𝑗 − 𝑀) + 1) − 1) = (𝑗 − 𝑀)) |
41 | 38, 39, 40 | sylancl 694 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (((𝑗 − 𝑀) + 1) − 1) = (𝑗 − 𝑀)) |
42 | 37, 41 | eqtr3d 2658 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → ((𝑗 + (1 − 𝑀)) − 1) = (𝑗 − 𝑀)) |
43 | 42 | oveq2d 6666 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝑀 + ((𝑗 + (1 − 𝑀)) − 1)) = (𝑀 + (𝑗 − 𝑀))) |
44 | 22, 20 | pncan3d 10395 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝑀 + (𝑗 − 𝑀)) = 𝑗) |
45 | 43, 44 | eqtrd 2656 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝑀 + ((𝑗 + (1 − 𝑀)) − 1)) = 𝑗) |
46 | 45 | fveq2d 6195 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐻‘(𝑀 + ((𝑗 + (1 − 𝑀)) − 1))) = (𝐻‘𝑗)) |
47 | 36, 46 | eqtr2d 2657 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐻‘𝑗) = ((𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1))))‘(𝑗 + (1 − 𝑀)))) |
48 | 13, 15, 47 | syl2an 494 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑗 ∈ (𝑀...𝑘)) → (𝐻‘𝑗) = ((𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1))))‘(𝑗 + (1 − 𝑀)))) |
49 | 11, 12, 48 | seqshft2 12827 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (seq𝑀( + , 𝐻)‘𝑘) = (seq(𝑀 + (1 − 𝑀))( + , (𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1)))))‘(𝑘 + (1 − 𝑀)))) |
50 | 21 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑀 ∈ ℂ) |
51 | | pncan3 10289 |
. . . . . . 7
⊢ ((𝑀 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑀 + (1
− 𝑀)) =
1) |
52 | 50, 39, 51 | sylancl 694 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑀 + (1 − 𝑀)) = 1) |
53 | 52 | seqeq1d 12807 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → seq(𝑀 + (1 − 𝑀))( + , (𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1))))) = seq1( + , (𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1)))))) |
54 | 53 | fveq1d 6193 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (seq(𝑀 + (1 − 𝑀))( + , (𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1)))))‘(𝑘 + (1 − 𝑀))) = (seq1( + , (𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1)))))‘(𝑘 + (1 − 𝑀)))) |
55 | 49, 54 | eqtr2d 2657 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (seq1( + , (𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1)))))‘(𝑘 + (1 − 𝑀))) = (seq𝑀( + , 𝐻)‘𝑘)) |
56 | 1, 2, 5, 7, 9, 55 | climshft2 14313 |
. 2
⊢ (𝜑 → (seq𝑀( + , 𝐻) ⇝ 𝐴 ↔ seq1( + , (𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1))))) ⇝ 𝐴)) |
57 | | isercoll2.w |
. . 3
⊢ 𝑊 =
(ℤ≥‘𝑁) |
58 | | isercoll2.n |
. . 3
⊢ (𝜑 → 𝑁 ∈ ℤ) |
59 | | isercoll2.g |
. . . . . 6
⊢ (𝜑 → 𝐺:𝑍⟶𝑊) |
60 | 59 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → 𝐺:𝑍⟶𝑊) |
61 | | uzid 11702 |
. . . . . . . 8
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
(ℤ≥‘𝑀)) |
62 | 2, 61 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑀)) |
63 | | nnm1nn0 11334 |
. . . . . . 7
⊢ (𝑥 ∈ ℕ → (𝑥 − 1) ∈
ℕ0) |
64 | | uzaddcl 11744 |
. . . . . . 7
⊢ ((𝑀 ∈
(ℤ≥‘𝑀) ∧ (𝑥 − 1) ∈ ℕ0)
→ (𝑀 + (𝑥 − 1)) ∈
(ℤ≥‘𝑀)) |
65 | 62, 63, 64 | syl2an 494 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝑀 + (𝑥 − 1)) ∈
(ℤ≥‘𝑀)) |
66 | 65, 1 | syl6eleqr 2712 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝑀 + (𝑥 − 1)) ∈ 𝑍) |
67 | 60, 66 | ffvelrnd 6360 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝐺‘(𝑀 + (𝑥 − 1))) ∈ 𝑊) |
68 | | eqid 2622 |
. . . 4
⊢ (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1)))) = (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1)))) |
69 | 67, 68 | fmptd 6385 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1)))):ℕ⟶𝑊) |
70 | | nnm1nn0 11334 |
. . . . . . . 8
⊢ (𝑗 ∈ ℕ → (𝑗 − 1) ∈
ℕ0) |
71 | | uzaddcl 11744 |
. . . . . . . 8
⊢ ((𝑀 ∈
(ℤ≥‘𝑀) ∧ (𝑗 − 1) ∈ ℕ0)
→ (𝑀 + (𝑗 − 1)) ∈
(ℤ≥‘𝑀)) |
72 | 62, 70, 71 | syl2an 494 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑀 + (𝑗 − 1)) ∈
(ℤ≥‘𝑀)) |
73 | 72, 1 | syl6eleqr 2712 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑀 + (𝑗 − 1)) ∈ 𝑍) |
74 | | isercoll2.i |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) < (𝐺‘(𝑘 + 1))) |
75 | 74 | ralrimiva 2966 |
. . . . . . 7
⊢ (𝜑 → ∀𝑘 ∈ 𝑍 (𝐺‘𝑘) < (𝐺‘(𝑘 + 1))) |
76 | 75 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∀𝑘 ∈ 𝑍 (𝐺‘𝑘) < (𝐺‘(𝑘 + 1))) |
77 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑘 = (𝑀 + (𝑗 − 1)) → (𝐺‘𝑘) = (𝐺‘(𝑀 + (𝑗 − 1)))) |
78 | | oveq1 6657 |
. . . . . . . . 9
⊢ (𝑘 = (𝑀 + (𝑗 − 1)) → (𝑘 + 1) = ((𝑀 + (𝑗 − 1)) + 1)) |
79 | 78 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑘 = (𝑀 + (𝑗 − 1)) → (𝐺‘(𝑘 + 1)) = (𝐺‘((𝑀 + (𝑗 − 1)) + 1))) |
80 | 77, 79 | breq12d 4666 |
. . . . . . 7
⊢ (𝑘 = (𝑀 + (𝑗 − 1)) → ((𝐺‘𝑘) < (𝐺‘(𝑘 + 1)) ↔ (𝐺‘(𝑀 + (𝑗 − 1))) < (𝐺‘((𝑀 + (𝑗 − 1)) + 1)))) |
81 | 80 | rspcv 3305 |
. . . . . 6
⊢ ((𝑀 + (𝑗 − 1)) ∈ 𝑍 → (∀𝑘 ∈ 𝑍 (𝐺‘𝑘) < (𝐺‘(𝑘 + 1)) → (𝐺‘(𝑀 + (𝑗 − 1))) < (𝐺‘((𝑀 + (𝑗 − 1)) + 1)))) |
82 | 73, 76, 81 | sylc 65 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐺‘(𝑀 + (𝑗 − 1))) < (𝐺‘((𝑀 + (𝑗 − 1)) + 1))) |
83 | | nncn 11028 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℂ) |
84 | 83 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℂ) |
85 | | 1cnd 10056 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 1 ∈
ℂ) |
86 | 84, 85, 85 | addsubd 10413 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑗 + 1) − 1) = ((𝑗 − 1) + 1)) |
87 | 86 | oveq2d 6666 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑀 + ((𝑗 + 1) − 1)) = (𝑀 + ((𝑗 − 1) + 1))) |
88 | 21 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑀 ∈ ℂ) |
89 | 70 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑗 − 1) ∈
ℕ0) |
90 | 89 | nn0cnd 11353 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑗 − 1) ∈ ℂ) |
91 | 88, 90, 85 | addassd 10062 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑀 + (𝑗 − 1)) + 1) = (𝑀 + ((𝑗 − 1) + 1))) |
92 | 87, 91 | eqtr4d 2659 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑀 + ((𝑗 + 1) − 1)) = ((𝑀 + (𝑗 − 1)) + 1)) |
93 | 92 | fveq2d 6195 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐺‘(𝑀 + ((𝑗 + 1) − 1))) = (𝐺‘((𝑀 + (𝑗 − 1)) + 1))) |
94 | 82, 93 | breqtrrd 4681 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐺‘(𝑀 + (𝑗 − 1))) < (𝐺‘(𝑀 + ((𝑗 + 1) − 1)))) |
95 | | oveq1 6657 |
. . . . . . . 8
⊢ (𝑥 = 𝑗 → (𝑥 − 1) = (𝑗 − 1)) |
96 | 95 | oveq2d 6666 |
. . . . . . 7
⊢ (𝑥 = 𝑗 → (𝑀 + (𝑥 − 1)) = (𝑀 + (𝑗 − 1))) |
97 | 96 | fveq2d 6195 |
. . . . . 6
⊢ (𝑥 = 𝑗 → (𝐺‘(𝑀 + (𝑥 − 1))) = (𝐺‘(𝑀 + (𝑗 − 1)))) |
98 | | fvex 6201 |
. . . . . 6
⊢ (𝐺‘(𝑀 + (𝑗 − 1))) ∈ V |
99 | 97, 68, 98 | fvmpt 6282 |
. . . . 5
⊢ (𝑗 ∈ ℕ → ((𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1))))‘𝑗) = (𝐺‘(𝑀 + (𝑗 − 1)))) |
100 | 99 | adantl 482 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1))))‘𝑗) = (𝐺‘(𝑀 + (𝑗 − 1)))) |
101 | | peano2nn 11032 |
. . . . . 6
⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ∈
ℕ) |
102 | 101 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ∈ ℕ) |
103 | | oveq1 6657 |
. . . . . . . 8
⊢ (𝑥 = (𝑗 + 1) → (𝑥 − 1) = ((𝑗 + 1) − 1)) |
104 | 103 | oveq2d 6666 |
. . . . . . 7
⊢ (𝑥 = (𝑗 + 1) → (𝑀 + (𝑥 − 1)) = (𝑀 + ((𝑗 + 1) − 1))) |
105 | 104 | fveq2d 6195 |
. . . . . 6
⊢ (𝑥 = (𝑗 + 1) → (𝐺‘(𝑀 + (𝑥 − 1))) = (𝐺‘(𝑀 + ((𝑗 + 1) − 1)))) |
106 | | fvex 6201 |
. . . . . 6
⊢ (𝐺‘(𝑀 + ((𝑗 + 1) − 1))) ∈ V |
107 | 105, 68, 106 | fvmpt 6282 |
. . . . 5
⊢ ((𝑗 + 1) ∈ ℕ →
((𝑥 ∈ ℕ ↦
(𝐺‘(𝑀 + (𝑥 − 1))))‘(𝑗 + 1)) = (𝐺‘(𝑀 + ((𝑗 + 1) − 1)))) |
108 | 102, 107 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1))))‘(𝑗 + 1)) = (𝐺‘(𝑀 + ((𝑗 + 1) − 1)))) |
109 | 94, 100, 108 | 3brtr4d 4685 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1))))‘𝑗) < ((𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1))))‘(𝑗 + 1))) |
110 | | ffn 6045 |
. . . . . . . . 9
⊢ (𝐺:𝑍⟶𝑊 → 𝐺 Fn 𝑍) |
111 | 59, 110 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 Fn 𝑍) |
112 | | uznn0sub 11719 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈
(ℤ≥‘𝑀) → (𝑘 − 𝑀) ∈
ℕ0) |
113 | 11, 112 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑘 − 𝑀) ∈
ℕ0) |
114 | | nn0p1nn 11332 |
. . . . . . . . . . . 12
⊢ ((𝑘 − 𝑀) ∈ ℕ0 → ((𝑘 − 𝑀) + 1) ∈ ℕ) |
115 | 113, 114 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝑘 − 𝑀) + 1) ∈ ℕ) |
116 | 113 | nn0cnd 11353 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑘 − 𝑀) ∈ ℂ) |
117 | | pncan 10287 |
. . . . . . . . . . . . . . 15
⊢ (((𝑘 − 𝑀) ∈ ℂ ∧ 1 ∈ ℂ)
→ (((𝑘 − 𝑀) + 1) − 1) = (𝑘 − 𝑀)) |
118 | 116, 39, 117 | sylancl 694 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (((𝑘 − 𝑀) + 1) − 1) = (𝑘 − 𝑀)) |
119 | 118 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑀 + (((𝑘 − 𝑀) + 1) − 1)) = (𝑀 + (𝑘 − 𝑀))) |
120 | | eluzelz 11697 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈
(ℤ≥‘𝑀) → 𝑘 ∈ ℤ) |
121 | 120, 1 | eleq2s 2719 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ ℤ) |
122 | 121 | zcnd 11483 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ ℂ) |
123 | | pncan3 10289 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝑀 + (𝑘 − 𝑀)) = 𝑘) |
124 | 21, 122, 123 | syl2an 494 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑀 + (𝑘 − 𝑀)) = 𝑘) |
125 | 119, 124 | eqtr2d 2657 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 = (𝑀 + (((𝑘 − 𝑀) + 1) − 1))) |
126 | 125 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = (𝐺‘(𝑀 + (((𝑘 − 𝑀) + 1) − 1)))) |
127 | | oveq1 6657 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = ((𝑘 − 𝑀) + 1) → (𝑥 − 1) = (((𝑘 − 𝑀) + 1) − 1)) |
128 | 127 | oveq2d 6666 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = ((𝑘 − 𝑀) + 1) → (𝑀 + (𝑥 − 1)) = (𝑀 + (((𝑘 − 𝑀) + 1) − 1))) |
129 | 128 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ((𝑘 − 𝑀) + 1) → (𝐺‘(𝑀 + (𝑥 − 1))) = (𝐺‘(𝑀 + (((𝑘 − 𝑀) + 1) − 1)))) |
130 | 129 | eqeq2d 2632 |
. . . . . . . . . . . 12
⊢ (𝑥 = ((𝑘 − 𝑀) + 1) → ((𝐺‘𝑘) = (𝐺‘(𝑀 + (𝑥 − 1))) ↔ (𝐺‘𝑘) = (𝐺‘(𝑀 + (((𝑘 − 𝑀) + 1) − 1))))) |
131 | 130 | rspcev 3309 |
. . . . . . . . . . 11
⊢ ((((𝑘 − 𝑀) + 1) ∈ ℕ ∧ (𝐺‘𝑘) = (𝐺‘(𝑀 + (((𝑘 − 𝑀) + 1) − 1)))) → ∃𝑥 ∈ ℕ (𝐺‘𝑘) = (𝐺‘(𝑀 + (𝑥 − 1)))) |
132 | 115, 126,
131 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ∃𝑥 ∈ ℕ (𝐺‘𝑘) = (𝐺‘(𝑀 + (𝑥 − 1)))) |
133 | | fvex 6201 |
. . . . . . . . . . 11
⊢ (𝐺‘𝑘) ∈ V |
134 | 68 | elrnmpt 5372 |
. . . . . . . . . . 11
⊢ ((𝐺‘𝑘) ∈ V → ((𝐺‘𝑘) ∈ ran (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1)))) ↔ ∃𝑥 ∈ ℕ (𝐺‘𝑘) = (𝐺‘(𝑀 + (𝑥 − 1))))) |
135 | 133, 134 | ax-mp 5 |
. . . . . . . . . 10
⊢ ((𝐺‘𝑘) ∈ ran (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1)))) ↔ ∃𝑥 ∈ ℕ (𝐺‘𝑘) = (𝐺‘(𝑀 + (𝑥 − 1)))) |
136 | 132, 135 | sylibr 224 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ran (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1))))) |
137 | 136 | ralrimiva 2966 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑘 ∈ 𝑍 (𝐺‘𝑘) ∈ ran (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1))))) |
138 | | ffnfv 6388 |
. . . . . . . 8
⊢ (𝐺:𝑍⟶ran (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1)))) ↔ (𝐺 Fn 𝑍 ∧ ∀𝑘 ∈ 𝑍 (𝐺‘𝑘) ∈ ran (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1)))))) |
139 | 111, 137,
138 | sylanbrc 698 |
. . . . . . 7
⊢ (𝜑 → 𝐺:𝑍⟶ran (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1))))) |
140 | | frn 6053 |
. . . . . . 7
⊢ (𝐺:𝑍⟶ran (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1)))) → ran 𝐺 ⊆ ran (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1))))) |
141 | 139, 140 | syl 17 |
. . . . . 6
⊢ (𝜑 → ran 𝐺 ⊆ ran (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1))))) |
142 | 141 | sscond 3747 |
. . . . 5
⊢ (𝜑 → (𝑊 ∖ ran (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1))))) ⊆ (𝑊 ∖ ran 𝐺)) |
143 | 142 | sselda 3603 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑊 ∖ ran (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1)))))) → 𝑛 ∈ (𝑊 ∖ ran 𝐺)) |
144 | | isercoll2.0 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑊 ∖ ran 𝐺)) → (𝐹‘𝑛) = 0) |
145 | 143, 144 | syldan 487 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑊 ∖ ran (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1)))))) → (𝐹‘𝑛) = 0) |
146 | | isercoll2.f |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑊) → (𝐹‘𝑛) ∈ ℂ) |
147 | | isercoll2.h |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = (𝐹‘(𝐺‘𝑘))) |
148 | 147 | ralrimiva 2966 |
. . . . . 6
⊢ (𝜑 → ∀𝑘 ∈ 𝑍 (𝐻‘𝑘) = (𝐹‘(𝐺‘𝑘))) |
149 | 148 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∀𝑘 ∈ 𝑍 (𝐻‘𝑘) = (𝐹‘(𝐺‘𝑘))) |
150 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑘 = (𝑀 + (𝑗 − 1)) → (𝐻‘𝑘) = (𝐻‘(𝑀 + (𝑗 − 1)))) |
151 | 77 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑘 = (𝑀 + (𝑗 − 1)) → (𝐹‘(𝐺‘𝑘)) = (𝐹‘(𝐺‘(𝑀 + (𝑗 − 1))))) |
152 | 150, 151 | eqeq12d 2637 |
. . . . . 6
⊢ (𝑘 = (𝑀 + (𝑗 − 1)) → ((𝐻‘𝑘) = (𝐹‘(𝐺‘𝑘)) ↔ (𝐻‘(𝑀 + (𝑗 − 1))) = (𝐹‘(𝐺‘(𝑀 + (𝑗 − 1)))))) |
153 | 152 | rspcv 3305 |
. . . . 5
⊢ ((𝑀 + (𝑗 − 1)) ∈ 𝑍 → (∀𝑘 ∈ 𝑍 (𝐻‘𝑘) = (𝐹‘(𝐺‘𝑘)) → (𝐻‘(𝑀 + (𝑗 − 1))) = (𝐹‘(𝐺‘(𝑀 + (𝑗 − 1)))))) |
154 | 73, 149, 153 | sylc 65 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐻‘(𝑀 + (𝑗 − 1))) = (𝐹‘(𝐺‘(𝑀 + (𝑗 − 1))))) |
155 | 96 | fveq2d 6195 |
. . . . . 6
⊢ (𝑥 = 𝑗 → (𝐻‘(𝑀 + (𝑥 − 1))) = (𝐻‘(𝑀 + (𝑗 − 1)))) |
156 | | fvex 6201 |
. . . . . 6
⊢ (𝐻‘(𝑀 + (𝑗 − 1))) ∈ V |
157 | 155, 33, 156 | fvmpt 6282 |
. . . . 5
⊢ (𝑗 ∈ ℕ → ((𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1))))‘𝑗) = (𝐻‘(𝑀 + (𝑗 − 1)))) |
158 | 157 | adantl 482 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1))))‘𝑗) = (𝐻‘(𝑀 + (𝑗 − 1)))) |
159 | 100 | fveq2d 6195 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘((𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1))))‘𝑗)) = (𝐹‘(𝐺‘(𝑀 + (𝑗 − 1))))) |
160 | 154, 158,
159 | 3eqtr4d 2666 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1))))‘𝑗) = (𝐹‘((𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1))))‘𝑗))) |
161 | 57, 58, 69, 109, 145, 146, 160 | isercoll 14398 |
. 2
⊢ (𝜑 → (seq1( + , (𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1))))) ⇝ 𝐴 ↔ seq𝑁( + , 𝐹) ⇝ 𝐴)) |
162 | 56, 161 | bitrd 268 |
1
⊢ (𝜑 → (seq𝑀( + , 𝐻) ⇝ 𝐴 ↔ seq𝑁( + , 𝐹) ⇝ 𝐴)) |