Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  isercoll2 Structured version   Visualization version   GIF version

Theorem isercoll2 14519
 Description: Generalize isercoll 14518 so that both sequences have arbitrary starting point. (Contributed by Mario Carneiro, 6-Apr-2015.)
Hypotheses
Ref Expression
isercoll2.z 𝑍 = (ℤ𝑀)
isercoll2.w 𝑊 = (ℤ𝑁)
isercoll2.m (𝜑𝑀 ∈ ℤ)
isercoll2.n (𝜑𝑁 ∈ ℤ)
isercoll2.g (𝜑𝐺:𝑍𝑊)
isercoll2.i ((𝜑𝑘𝑍) → (𝐺𝑘) < (𝐺‘(𝑘 + 1)))
isercoll2.0 ((𝜑𝑛 ∈ (𝑊 ∖ ran 𝐺)) → (𝐹𝑛) = 0)
isercoll2.f ((𝜑𝑛𝑊) → (𝐹𝑛) ∈ ℂ)
isercoll2.h ((𝜑𝑘𝑍) → (𝐻𝑘) = (𝐹‘(𝐺𝑘)))
Assertion
Ref Expression
isercoll2 (𝜑 → (seq𝑀( + , 𝐻) ⇝ 𝐴 ↔ seq𝑁( + , 𝐹) ⇝ 𝐴))
Distinct variable groups:   𝑘,𝑛,𝐴   𝑘,𝐹,𝑛   𝑘,𝐺,𝑛   𝑘,𝐻,𝑛   𝑛,𝑁   𝑘,𝑀,𝑛   𝜑,𝑘,𝑛   𝑛,𝑊   𝑘,𝑍
Allowed substitution hints:   𝑁(𝑘)   𝑊(𝑘)   𝑍(𝑛)

Proof of Theorem isercoll2
Dummy variables 𝑗 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isercoll2.z . . 3 𝑍 = (ℤ𝑀)
2 isercoll2.m . . 3 (𝜑𝑀 ∈ ℤ)
3 1z 11520 . . . 4 1 ∈ ℤ
4 zsubcl 11532 . . . 4 ((1 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (1 − 𝑀) ∈ ℤ)
53, 2, 4sylancr 698 . . 3 (𝜑 → (1 − 𝑀) ∈ ℤ)
6 seqex 12918 . . . 4 seq𝑀( + , 𝐻) ∈ V
76a1i 11 . . 3 (𝜑 → seq𝑀( + , 𝐻) ∈ V)
8 seqex 12918 . . . 4 seq1( + , (𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1))))) ∈ V
98a1i 11 . . 3 (𝜑 → seq1( + , (𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1))))) ∈ V)
10 simpr 479 . . . . . 6 ((𝜑𝑘𝑍) → 𝑘𝑍)
1110, 1syl6eleq 2813 . . . . 5 ((𝜑𝑘𝑍) → 𝑘 ∈ (ℤ𝑀))
125adantr 472 . . . . 5 ((𝜑𝑘𝑍) → (1 − 𝑀) ∈ ℤ)
13 simpl 474 . . . . . 6 ((𝜑𝑘𝑍) → 𝜑)
14 elfzuz 12452 . . . . . . 7 (𝑗 ∈ (𝑀...𝑘) → 𝑗 ∈ (ℤ𝑀))
1514, 1syl6eleqr 2814 . . . . . 6 (𝑗 ∈ (𝑀...𝑘) → 𝑗𝑍)
16 simpr 479 . . . . . . . . . . . . 13 ((𝜑𝑗𝑍) → 𝑗𝑍)
1716, 1syl6eleq 2813 . . . . . . . . . . . 12 ((𝜑𝑗𝑍) → 𝑗 ∈ (ℤ𝑀))
18 eluzelz 11810 . . . . . . . . . . . 12 (𝑗 ∈ (ℤ𝑀) → 𝑗 ∈ ℤ)
1917, 18syl 17 . . . . . . . . . . 11 ((𝜑𝑗𝑍) → 𝑗 ∈ ℤ)
2019zcnd 11596 . . . . . . . . . 10 ((𝜑𝑗𝑍) → 𝑗 ∈ ℂ)
212zcnd 11596 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℂ)
2221adantr 472 . . . . . . . . . 10 ((𝜑𝑗𝑍) → 𝑀 ∈ ℂ)
23 1cnd 10169 . . . . . . . . . 10 ((𝜑𝑗𝑍) → 1 ∈ ℂ)
2420, 22, 23subadd23d 10527 . . . . . . . . 9 ((𝜑𝑗𝑍) → ((𝑗𝑀) + 1) = (𝑗 + (1 − 𝑀)))
25 uznn0sub 11833 . . . . . . . . . . 11 (𝑗 ∈ (ℤ𝑀) → (𝑗𝑀) ∈ ℕ0)
2617, 25syl 17 . . . . . . . . . 10 ((𝜑𝑗𝑍) → (𝑗𝑀) ∈ ℕ0)
27 nn0p1nn 11445 . . . . . . . . . 10 ((𝑗𝑀) ∈ ℕ0 → ((𝑗𝑀) + 1) ∈ ℕ)
2826, 27syl 17 . . . . . . . . 9 ((𝜑𝑗𝑍) → ((𝑗𝑀) + 1) ∈ ℕ)
2924, 28eqeltrrd 2804 . . . . . . . 8 ((𝜑𝑗𝑍) → (𝑗 + (1 − 𝑀)) ∈ ℕ)
30 oveq1 6772 . . . . . . . . . . 11 (𝑥 = (𝑗 + (1 − 𝑀)) → (𝑥 − 1) = ((𝑗 + (1 − 𝑀)) − 1))
3130oveq2d 6781 . . . . . . . . . 10 (𝑥 = (𝑗 + (1 − 𝑀)) → (𝑀 + (𝑥 − 1)) = (𝑀 + ((𝑗 + (1 − 𝑀)) − 1)))
3231fveq2d 6308 . . . . . . . . 9 (𝑥 = (𝑗 + (1 − 𝑀)) → (𝐻‘(𝑀 + (𝑥 − 1))) = (𝐻‘(𝑀 + ((𝑗 + (1 − 𝑀)) − 1))))
33 eqid 2724 . . . . . . . . 9 (𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1)))) = (𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1))))
34 fvex 6314 . . . . . . . . 9 (𝐻‘(𝑀 + ((𝑗 + (1 − 𝑀)) − 1))) ∈ V
3532, 33, 34fvmpt 6396 . . . . . . . 8 ((𝑗 + (1 − 𝑀)) ∈ ℕ → ((𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1))))‘(𝑗 + (1 − 𝑀))) = (𝐻‘(𝑀 + ((𝑗 + (1 − 𝑀)) − 1))))
3629, 35syl 17 . . . . . . 7 ((𝜑𝑗𝑍) → ((𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1))))‘(𝑗 + (1 − 𝑀))) = (𝐻‘(𝑀 + ((𝑗 + (1 − 𝑀)) − 1))))
3724oveq1d 6780 . . . . . . . . . . 11 ((𝜑𝑗𝑍) → (((𝑗𝑀) + 1) − 1) = ((𝑗 + (1 − 𝑀)) − 1))
3826nn0cnd 11466 . . . . . . . . . . . 12 ((𝜑𝑗𝑍) → (𝑗𝑀) ∈ ℂ)
39 ax-1cn 10107 . . . . . . . . . . . 12 1 ∈ ℂ
40 pncan 10400 . . . . . . . . . . . 12 (((𝑗𝑀) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑗𝑀) + 1) − 1) = (𝑗𝑀))
4138, 39, 40sylancl 697 . . . . . . . . . . 11 ((𝜑𝑗𝑍) → (((𝑗𝑀) + 1) − 1) = (𝑗𝑀))
4237, 41eqtr3d 2760 . . . . . . . . . 10 ((𝜑𝑗𝑍) → ((𝑗 + (1 − 𝑀)) − 1) = (𝑗𝑀))
4342oveq2d 6781 . . . . . . . . 9 ((𝜑𝑗𝑍) → (𝑀 + ((𝑗 + (1 − 𝑀)) − 1)) = (𝑀 + (𝑗𝑀)))
4422, 20pncan3d 10508 . . . . . . . . 9 ((𝜑𝑗𝑍) → (𝑀 + (𝑗𝑀)) = 𝑗)
4543, 44eqtrd 2758 . . . . . . . 8 ((𝜑𝑗𝑍) → (𝑀 + ((𝑗 + (1 − 𝑀)) − 1)) = 𝑗)
4645fveq2d 6308 . . . . . . 7 ((𝜑𝑗𝑍) → (𝐻‘(𝑀 + ((𝑗 + (1 − 𝑀)) − 1))) = (𝐻𝑗))
4736, 46eqtr2d 2759 . . . . . 6 ((𝜑𝑗𝑍) → (𝐻𝑗) = ((𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1))))‘(𝑗 + (1 − 𝑀))))
4813, 15, 47syl2an 495 . . . . 5 (((𝜑𝑘𝑍) ∧ 𝑗 ∈ (𝑀...𝑘)) → (𝐻𝑗) = ((𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1))))‘(𝑗 + (1 − 𝑀))))
4911, 12, 48seqshft2 12942 . . . 4 ((𝜑𝑘𝑍) → (seq𝑀( + , 𝐻)‘𝑘) = (seq(𝑀 + (1 − 𝑀))( + , (𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1)))))‘(𝑘 + (1 − 𝑀))))
5021adantr 472 . . . . . . 7 ((𝜑𝑘𝑍) → 𝑀 ∈ ℂ)
51 pncan3 10402 . . . . . . 7 ((𝑀 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑀 + (1 − 𝑀)) = 1)
5250, 39, 51sylancl 697 . . . . . 6 ((𝜑𝑘𝑍) → (𝑀 + (1 − 𝑀)) = 1)
5352seqeq1d 12922 . . . . 5 ((𝜑𝑘𝑍) → seq(𝑀 + (1 − 𝑀))( + , (𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1))))) = seq1( + , (𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1))))))
5453fveq1d 6306 . . . 4 ((𝜑𝑘𝑍) → (seq(𝑀 + (1 − 𝑀))( + , (𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1)))))‘(𝑘 + (1 − 𝑀))) = (seq1( + , (𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1)))))‘(𝑘 + (1 − 𝑀))))
5549, 54eqtr2d 2759 . . 3 ((𝜑𝑘𝑍) → (seq1( + , (𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1)))))‘(𝑘 + (1 − 𝑀))) = (seq𝑀( + , 𝐻)‘𝑘))
561, 2, 5, 7, 9, 55climshft2 14433 . 2 (𝜑 → (seq𝑀( + , 𝐻) ⇝ 𝐴 ↔ seq1( + , (𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1))))) ⇝ 𝐴))
57 isercoll2.w . . 3 𝑊 = (ℤ𝑁)
58 isercoll2.n . . 3 (𝜑𝑁 ∈ ℤ)
59 isercoll2.g . . . . . 6 (𝜑𝐺:𝑍𝑊)
6059adantr 472 . . . . 5 ((𝜑𝑥 ∈ ℕ) → 𝐺:𝑍𝑊)
61 uzid 11815 . . . . . . . 8 (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ𝑀))
622, 61syl 17 . . . . . . 7 (𝜑𝑀 ∈ (ℤ𝑀))
63 nnm1nn0 11447 . . . . . . 7 (𝑥 ∈ ℕ → (𝑥 − 1) ∈ ℕ0)
64 uzaddcl 11858 . . . . . . 7 ((𝑀 ∈ (ℤ𝑀) ∧ (𝑥 − 1) ∈ ℕ0) → (𝑀 + (𝑥 − 1)) ∈ (ℤ𝑀))
6562, 63, 64syl2an 495 . . . . . 6 ((𝜑𝑥 ∈ ℕ) → (𝑀 + (𝑥 − 1)) ∈ (ℤ𝑀))
6665, 1syl6eleqr 2814 . . . . 5 ((𝜑𝑥 ∈ ℕ) → (𝑀 + (𝑥 − 1)) ∈ 𝑍)
6760, 66ffvelrnd 6475 . . . 4 ((𝜑𝑥 ∈ ℕ) → (𝐺‘(𝑀 + (𝑥 − 1))) ∈ 𝑊)
68 eqid 2724 . . . 4 (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1)))) = (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1))))
6967, 68fmptd 6500 . . 3 (𝜑 → (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1)))):ℕ⟶𝑊)
70 nnm1nn0 11447 . . . . . . . 8 (𝑗 ∈ ℕ → (𝑗 − 1) ∈ ℕ0)
71 uzaddcl 11858 . . . . . . . 8 ((𝑀 ∈ (ℤ𝑀) ∧ (𝑗 − 1) ∈ ℕ0) → (𝑀 + (𝑗 − 1)) ∈ (ℤ𝑀))
7262, 70, 71syl2an 495 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → (𝑀 + (𝑗 − 1)) ∈ (ℤ𝑀))
7372, 1syl6eleqr 2814 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → (𝑀 + (𝑗 − 1)) ∈ 𝑍)
74 isercoll2.i . . . . . . . 8 ((𝜑𝑘𝑍) → (𝐺𝑘) < (𝐺‘(𝑘 + 1)))
7574ralrimiva 3068 . . . . . . 7 (𝜑 → ∀𝑘𝑍 (𝐺𝑘) < (𝐺‘(𝑘 + 1)))
7675adantr 472 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → ∀𝑘𝑍 (𝐺𝑘) < (𝐺‘(𝑘 + 1)))
77 fveq2 6304 . . . . . . . 8 (𝑘 = (𝑀 + (𝑗 − 1)) → (𝐺𝑘) = (𝐺‘(𝑀 + (𝑗 − 1))))
78 oveq1 6772 . . . . . . . . 9 (𝑘 = (𝑀 + (𝑗 − 1)) → (𝑘 + 1) = ((𝑀 + (𝑗 − 1)) + 1))
7978fveq2d 6308 . . . . . . . 8 (𝑘 = (𝑀 + (𝑗 − 1)) → (𝐺‘(𝑘 + 1)) = (𝐺‘((𝑀 + (𝑗 − 1)) + 1)))
8077, 79breq12d 4773 . . . . . . 7 (𝑘 = (𝑀 + (𝑗 − 1)) → ((𝐺𝑘) < (𝐺‘(𝑘 + 1)) ↔ (𝐺‘(𝑀 + (𝑗 − 1))) < (𝐺‘((𝑀 + (𝑗 − 1)) + 1))))
8180rspcv 3409 . . . . . 6 ((𝑀 + (𝑗 − 1)) ∈ 𝑍 → (∀𝑘𝑍 (𝐺𝑘) < (𝐺‘(𝑘 + 1)) → (𝐺‘(𝑀 + (𝑗 − 1))) < (𝐺‘((𝑀 + (𝑗 − 1)) + 1))))
8273, 76, 81sylc 65 . . . . 5 ((𝜑𝑗 ∈ ℕ) → (𝐺‘(𝑀 + (𝑗 − 1))) < (𝐺‘((𝑀 + (𝑗 − 1)) + 1)))
83 nncn 11141 . . . . . . . . . 10 (𝑗 ∈ ℕ → 𝑗 ∈ ℂ)
8483adantl 473 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → 𝑗 ∈ ℂ)
85 1cnd 10169 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → 1 ∈ ℂ)
8684, 85, 85addsubd 10526 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → ((𝑗 + 1) − 1) = ((𝑗 − 1) + 1))
8786oveq2d 6781 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → (𝑀 + ((𝑗 + 1) − 1)) = (𝑀 + ((𝑗 − 1) + 1)))
8821adantr 472 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → 𝑀 ∈ ℂ)
8970adantl 473 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (𝑗 − 1) ∈ ℕ0)
9089nn0cnd 11466 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (𝑗 − 1) ∈ ℂ)
9188, 90, 85addassd 10175 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → ((𝑀 + (𝑗 − 1)) + 1) = (𝑀 + ((𝑗 − 1) + 1)))
9287, 91eqtr4d 2761 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → (𝑀 + ((𝑗 + 1) − 1)) = ((𝑀 + (𝑗 − 1)) + 1))
9392fveq2d 6308 . . . . 5 ((𝜑𝑗 ∈ ℕ) → (𝐺‘(𝑀 + ((𝑗 + 1) − 1))) = (𝐺‘((𝑀 + (𝑗 − 1)) + 1)))
9482, 93breqtrrd 4788 . . . 4 ((𝜑𝑗 ∈ ℕ) → (𝐺‘(𝑀 + (𝑗 − 1))) < (𝐺‘(𝑀 + ((𝑗 + 1) − 1))))
95 oveq1 6772 . . . . . . . 8 (𝑥 = 𝑗 → (𝑥 − 1) = (𝑗 − 1))
9695oveq2d 6781 . . . . . . 7 (𝑥 = 𝑗 → (𝑀 + (𝑥 − 1)) = (𝑀 + (𝑗 − 1)))
9796fveq2d 6308 . . . . . 6 (𝑥 = 𝑗 → (𝐺‘(𝑀 + (𝑥 − 1))) = (𝐺‘(𝑀 + (𝑗 − 1))))
98 fvex 6314 . . . . . 6 (𝐺‘(𝑀 + (𝑗 − 1))) ∈ V
9997, 68, 98fvmpt 6396 . . . . 5 (𝑗 ∈ ℕ → ((𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1))))‘𝑗) = (𝐺‘(𝑀 + (𝑗 − 1))))
10099adantl 473 . . . 4 ((𝜑𝑗 ∈ ℕ) → ((𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1))))‘𝑗) = (𝐺‘(𝑀 + (𝑗 − 1))))
101 peano2nn 11145 . . . . . 6 (𝑗 ∈ ℕ → (𝑗 + 1) ∈ ℕ)
102101adantl 473 . . . . 5 ((𝜑𝑗 ∈ ℕ) → (𝑗 + 1) ∈ ℕ)
103 oveq1 6772 . . . . . . . 8 (𝑥 = (𝑗 + 1) → (𝑥 − 1) = ((𝑗 + 1) − 1))
104103oveq2d 6781 . . . . . . 7 (𝑥 = (𝑗 + 1) → (𝑀 + (𝑥 − 1)) = (𝑀 + ((𝑗 + 1) − 1)))
105104fveq2d 6308 . . . . . 6 (𝑥 = (𝑗 + 1) → (𝐺‘(𝑀 + (𝑥 − 1))) = (𝐺‘(𝑀 + ((𝑗 + 1) − 1))))
106 fvex 6314 . . . . . 6 (𝐺‘(𝑀 + ((𝑗 + 1) − 1))) ∈ V
107105, 68, 106fvmpt 6396 . . . . 5 ((𝑗 + 1) ∈ ℕ → ((𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1))))‘(𝑗 + 1)) = (𝐺‘(𝑀 + ((𝑗 + 1) − 1))))
108102, 107syl 17 . . . 4 ((𝜑𝑗 ∈ ℕ) → ((𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1))))‘(𝑗 + 1)) = (𝐺‘(𝑀 + ((𝑗 + 1) − 1))))
10994, 100, 1083brtr4d 4792 . . 3 ((𝜑𝑗 ∈ ℕ) → ((𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1))))‘𝑗) < ((𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1))))‘(𝑗 + 1)))
110 ffn 6158 . . . . . . . . 9 (𝐺:𝑍𝑊𝐺 Fn 𝑍)
11159, 110syl 17 . . . . . . . 8 (𝜑𝐺 Fn 𝑍)
112 uznn0sub 11833 . . . . . . . . . . . . 13 (𝑘 ∈ (ℤ𝑀) → (𝑘𝑀) ∈ ℕ0)
11311, 112syl 17 . . . . . . . . . . . 12 ((𝜑𝑘𝑍) → (𝑘𝑀) ∈ ℕ0)
114 nn0p1nn 11445 . . . . . . . . . . . 12 ((𝑘𝑀) ∈ ℕ0 → ((𝑘𝑀) + 1) ∈ ℕ)
115113, 114syl 17 . . . . . . . . . . 11 ((𝜑𝑘𝑍) → ((𝑘𝑀) + 1) ∈ ℕ)
116113nn0cnd 11466 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝑍) → (𝑘𝑀) ∈ ℂ)
117 pncan 10400 . . . . . . . . . . . . . . 15 (((𝑘𝑀) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑘𝑀) + 1) − 1) = (𝑘𝑀))
118116, 39, 117sylancl 697 . . . . . . . . . . . . . 14 ((𝜑𝑘𝑍) → (((𝑘𝑀) + 1) − 1) = (𝑘𝑀))
119118oveq2d 6781 . . . . . . . . . . . . 13 ((𝜑𝑘𝑍) → (𝑀 + (((𝑘𝑀) + 1) − 1)) = (𝑀 + (𝑘𝑀)))
120 eluzelz 11810 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (ℤ𝑀) → 𝑘 ∈ ℤ)
121120, 1eleq2s 2821 . . . . . . . . . . . . . . 15 (𝑘𝑍𝑘 ∈ ℤ)
122121zcnd 11596 . . . . . . . . . . . . . 14 (𝑘𝑍𝑘 ∈ ℂ)
123 pncan3 10402 . . . . . . . . . . . . . 14 ((𝑀 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝑀 + (𝑘𝑀)) = 𝑘)
12421, 122, 123syl2an 495 . . . . . . . . . . . . 13 ((𝜑𝑘𝑍) → (𝑀 + (𝑘𝑀)) = 𝑘)
125119, 124eqtr2d 2759 . . . . . . . . . . . 12 ((𝜑𝑘𝑍) → 𝑘 = (𝑀 + (((𝑘𝑀) + 1) − 1)))
126125fveq2d 6308 . . . . . . . . . . 11 ((𝜑𝑘𝑍) → (𝐺𝑘) = (𝐺‘(𝑀 + (((𝑘𝑀) + 1) − 1))))
127 oveq1 6772 . . . . . . . . . . . . . . 15 (𝑥 = ((𝑘𝑀) + 1) → (𝑥 − 1) = (((𝑘𝑀) + 1) − 1))
128127oveq2d 6781 . . . . . . . . . . . . . 14 (𝑥 = ((𝑘𝑀) + 1) → (𝑀 + (𝑥 − 1)) = (𝑀 + (((𝑘𝑀) + 1) − 1)))
129128fveq2d 6308 . . . . . . . . . . . . 13 (𝑥 = ((𝑘𝑀) + 1) → (𝐺‘(𝑀 + (𝑥 − 1))) = (𝐺‘(𝑀 + (((𝑘𝑀) + 1) − 1))))
130129eqeq2d 2734 . . . . . . . . . . . 12 (𝑥 = ((𝑘𝑀) + 1) → ((𝐺𝑘) = (𝐺‘(𝑀 + (𝑥 − 1))) ↔ (𝐺𝑘) = (𝐺‘(𝑀 + (((𝑘𝑀) + 1) − 1)))))
131130rspcev 3413 . . . . . . . . . . 11 ((((𝑘𝑀) + 1) ∈ ℕ ∧ (𝐺𝑘) = (𝐺‘(𝑀 + (((𝑘𝑀) + 1) − 1)))) → ∃𝑥 ∈ ℕ (𝐺𝑘) = (𝐺‘(𝑀 + (𝑥 − 1))))
132115, 126, 131syl2anc 696 . . . . . . . . . 10 ((𝜑𝑘𝑍) → ∃𝑥 ∈ ℕ (𝐺𝑘) = (𝐺‘(𝑀 + (𝑥 − 1))))
133 fvex 6314 . . . . . . . . . . 11 (𝐺𝑘) ∈ V
13468elrnmpt 5479 . . . . . . . . . . 11 ((𝐺𝑘) ∈ V → ((𝐺𝑘) ∈ ran (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1)))) ↔ ∃𝑥 ∈ ℕ (𝐺𝑘) = (𝐺‘(𝑀 + (𝑥 − 1)))))
135133, 134ax-mp 5 . . . . . . . . . 10 ((𝐺𝑘) ∈ ran (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1)))) ↔ ∃𝑥 ∈ ℕ (𝐺𝑘) = (𝐺‘(𝑀 + (𝑥 − 1))))
136132, 135sylibr 224 . . . . . . . . 9 ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ ran (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1)))))
137136ralrimiva 3068 . . . . . . . 8 (𝜑 → ∀𝑘𝑍 (𝐺𝑘) ∈ ran (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1)))))
138 ffnfv 6503 . . . . . . . 8 (𝐺:𝑍⟶ran (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1)))) ↔ (𝐺 Fn 𝑍 ∧ ∀𝑘𝑍 (𝐺𝑘) ∈ ran (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1))))))
139111, 137, 138sylanbrc 701 . . . . . . 7 (𝜑𝐺:𝑍⟶ran (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1)))))
140 frn 6166 . . . . . . 7 (𝐺:𝑍⟶ran (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1)))) → ran 𝐺 ⊆ ran (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1)))))
141139, 140syl 17 . . . . . 6 (𝜑 → ran 𝐺 ⊆ ran (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1)))))
142141sscond 3855 . . . . 5 (𝜑 → (𝑊 ∖ ran (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1))))) ⊆ (𝑊 ∖ ran 𝐺))
143142sselda 3709 . . . 4 ((𝜑𝑛 ∈ (𝑊 ∖ ran (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1)))))) → 𝑛 ∈ (𝑊 ∖ ran 𝐺))
144 isercoll2.0 . . . 4 ((𝜑𝑛 ∈ (𝑊 ∖ ran 𝐺)) → (𝐹𝑛) = 0)
145143, 144syldan 488 . . 3 ((𝜑𝑛 ∈ (𝑊 ∖ ran (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1)))))) → (𝐹𝑛) = 0)
146 isercoll2.f . . 3 ((𝜑𝑛𝑊) → (𝐹𝑛) ∈ ℂ)
147 isercoll2.h . . . . . . 7 ((𝜑𝑘𝑍) → (𝐻𝑘) = (𝐹‘(𝐺𝑘)))
148147ralrimiva 3068 . . . . . 6 (𝜑 → ∀𝑘𝑍 (𝐻𝑘) = (𝐹‘(𝐺𝑘)))
149148adantr 472 . . . . 5 ((𝜑𝑗 ∈ ℕ) → ∀𝑘𝑍 (𝐻𝑘) = (𝐹‘(𝐺𝑘)))
150 fveq2 6304 . . . . . . 7 (𝑘 = (𝑀 + (𝑗 − 1)) → (𝐻𝑘) = (𝐻‘(𝑀 + (𝑗 − 1))))
15177fveq2d 6308 . . . . . . 7 (𝑘 = (𝑀 + (𝑗 − 1)) → (𝐹‘(𝐺𝑘)) = (𝐹‘(𝐺‘(𝑀 + (𝑗 − 1)))))
152150, 151eqeq12d 2739 . . . . . 6 (𝑘 = (𝑀 + (𝑗 − 1)) → ((𝐻𝑘) = (𝐹‘(𝐺𝑘)) ↔ (𝐻‘(𝑀 + (𝑗 − 1))) = (𝐹‘(𝐺‘(𝑀 + (𝑗 − 1))))))
153152rspcv 3409 . . . . 5 ((𝑀 + (𝑗 − 1)) ∈ 𝑍 → (∀𝑘𝑍 (𝐻𝑘) = (𝐹‘(𝐺𝑘)) → (𝐻‘(𝑀 + (𝑗 − 1))) = (𝐹‘(𝐺‘(𝑀 + (𝑗 − 1))))))
15473, 149, 153sylc 65 . . . 4 ((𝜑𝑗 ∈ ℕ) → (𝐻‘(𝑀 + (𝑗 − 1))) = (𝐹‘(𝐺‘(𝑀 + (𝑗 − 1)))))
15596fveq2d 6308 . . . . . 6 (𝑥 = 𝑗 → (𝐻‘(𝑀 + (𝑥 − 1))) = (𝐻‘(𝑀 + (𝑗 − 1))))
156 fvex 6314 . . . . . 6 (𝐻‘(𝑀 + (𝑗 − 1))) ∈ V
157155, 33, 156fvmpt 6396 . . . . 5 (𝑗 ∈ ℕ → ((𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1))))‘𝑗) = (𝐻‘(𝑀 + (𝑗 − 1))))
158157adantl 473 . . . 4 ((𝜑𝑗 ∈ ℕ) → ((𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1))))‘𝑗) = (𝐻‘(𝑀 + (𝑗 − 1))))
159100fveq2d 6308 . . . 4 ((𝜑𝑗 ∈ ℕ) → (𝐹‘((𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1))))‘𝑗)) = (𝐹‘(𝐺‘(𝑀 + (𝑗 − 1)))))
160154, 158, 1593eqtr4d 2768 . . 3 ((𝜑𝑗 ∈ ℕ) → ((𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1))))‘𝑗) = (𝐹‘((𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1))))‘𝑗)))
16157, 58, 69, 109, 145, 146, 160isercoll 14518 . 2 (𝜑 → (seq1( + , (𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1))))) ⇝ 𝐴 ↔ seq𝑁( + , 𝐹) ⇝ 𝐴))
16256, 161bitrd 268 1 (𝜑 → (seq𝑀( + , 𝐻) ⇝ 𝐴 ↔ seq𝑁( + , 𝐹) ⇝ 𝐴))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1596   ∈ wcel 2103  ∀wral 3014  ∃wrex 3015  Vcvv 3304   ∖ cdif 3677   ⊆ wss 3680   class class class wbr 4760   ↦ cmpt 4837  ran crn 5219   Fn wfn 5996  ⟶wf 5997  ‘cfv 6001  (class class class)co 6765  ℂcc 10047  0cc0 10049  1c1 10050   + caddc 10052   < clt 10187   − cmin 10379  ℕcn 11133  ℕ0cn0 11405  ℤcz 11490  ℤ≥cuz 11800  ...cfz 12440  seqcseq 12916   ⇝ cli 14335 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-rep 4879  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011  ax-un 7066  ax-inf2 8651  ax-cnex 10105  ax-resscn 10106  ax-1cn 10107  ax-icn 10108  ax-addcl 10109  ax-addrcl 10110  ax-mulcl 10111  ax-mulrcl 10112  ax-mulcom 10113  ax-addass 10114  ax-mulass 10115  ax-distr 10116  ax-i2m1 10117  ax-1ne0 10118  ax-1rid 10119  ax-rnegex 10120  ax-rrecex 10121  ax-cnre 10122  ax-pre-lttri 10123  ax-pre-lttrn 10124  ax-pre-ltadd 10125  ax-pre-mulgt0 10126  ax-pre-sup 10127 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-nel 3000  df-ral 3019  df-rex 3020  df-reu 3021  df-rmo 3022  df-rab 3023  df-v 3306  df-sbc 3542  df-csb 3640  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-pss 3696  df-nul 4024  df-if 4195  df-pw 4268  df-sn 4286  df-pr 4288  df-tp 4290  df-op 4292  df-uni 4545  df-int 4584  df-iun 4630  df-br 4761  df-opab 4821  df-mpt 4838  df-tr 4861  df-id 5128  df-eprel 5133  df-po 5139  df-so 5140  df-fr 5177  df-we 5179  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-pred 5793  df-ord 5839  df-on 5840  df-lim 5841  df-suc 5842  df-iota 5964  df-fun 6003  df-fn 6004  df-f 6005  df-f1 6006  df-fo 6007  df-f1o 6008  df-fv 6009  df-isom 6010  df-riota 6726  df-ov 6768  df-oprab 6769  df-mpt2 6770  df-om 7183  df-1st 7285  df-2nd 7286  df-wrecs 7527  df-recs 7588  df-rdg 7626  df-1o 7680  df-oadd 7684  df-er 7862  df-en 8073  df-dom 8074  df-sdom 8075  df-fin 8076  df-sup 8464  df-card 8878  df-pnf 10189  df-mnf 10190  df-xr 10191  df-ltxr 10192  df-le 10193  df-sub 10381  df-neg 10382  df-nn 11134  df-n0 11406  df-xnn0 11477  df-z 11491  df-uz 11801  df-fz 12441  df-seq 12917  df-hash 13233  df-shft 13927  df-clim 14339 This theorem is referenced by:  iserodd  15663  stirlinglem5  40715
 Copyright terms: Public domain W3C validator