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

Theorem isercoll2 15232
Description: Generalize isercoll 15231 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 12207 . . . 4 1 ∈ ℤ
4 zsubcl 12219 . . . 4 ((1 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (1 − 𝑀) ∈ ℤ)
53, 2, 4sylancr 590 . . 3 (𝜑 → (1 − 𝑀) ∈ ℤ)
6 seqex 13576 . . . 4 seq𝑀( + , 𝐻) ∈ V
76a1i 11 . . 3 (𝜑 → seq𝑀( + , 𝐻) ∈ V)
8 seqex 13576 . . . 4 seq1( + , (𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1))))) ∈ V
98a1i 11 . . 3 (𝜑 → seq1( + , (𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1))))) ∈ V)
10 simpr 488 . . . . . 6 ((𝜑𝑘𝑍) → 𝑘𝑍)
1110, 1eleqtrdi 2848 . . . . 5 ((𝜑𝑘𝑍) → 𝑘 ∈ (ℤ𝑀))
125adantr 484 . . . . 5 ((𝜑𝑘𝑍) → (1 − 𝑀) ∈ ℤ)
13 simpl 486 . . . . . 6 ((𝜑𝑘𝑍) → 𝜑)
14 elfzuz 13108 . . . . . . 7 (𝑗 ∈ (𝑀...𝑘) → 𝑗 ∈ (ℤ𝑀))
1514, 1eleqtrrdi 2849 . . . . . 6 (𝑗 ∈ (𝑀...𝑘) → 𝑗𝑍)
16 simpr 488 . . . . . . . . . . . . 13 ((𝜑𝑗𝑍) → 𝑗𝑍)
1716, 1eleqtrdi 2848 . . . . . . . . . . . 12 ((𝜑𝑗𝑍) → 𝑗 ∈ (ℤ𝑀))
18 eluzelz 12448 . . . . . . . . . . . 12 (𝑗 ∈ (ℤ𝑀) → 𝑗 ∈ ℤ)
1917, 18syl 17 . . . . . . . . . . 11 ((𝜑𝑗𝑍) → 𝑗 ∈ ℤ)
2019zcnd 12283 . . . . . . . . . 10 ((𝜑𝑗𝑍) → 𝑗 ∈ ℂ)
212zcnd 12283 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℂ)
2221adantr 484 . . . . . . . . . 10 ((𝜑𝑗𝑍) → 𝑀 ∈ ℂ)
23 1cnd 10828 . . . . . . . . . 10 ((𝜑𝑗𝑍) → 1 ∈ ℂ)
2420, 22, 23subadd23d 11211 . . . . . . . . 9 ((𝜑𝑗𝑍) → ((𝑗𝑀) + 1) = (𝑗 + (1 − 𝑀)))
25 uznn0sub 12473 . . . . . . . . . . 11 (𝑗 ∈ (ℤ𝑀) → (𝑗𝑀) ∈ ℕ0)
2617, 25syl 17 . . . . . . . . . 10 ((𝜑𝑗𝑍) → (𝑗𝑀) ∈ ℕ0)
27 nn0p1nn 12129 . . . . . . . . . 10 ((𝑗𝑀) ∈ ℕ0 → ((𝑗𝑀) + 1) ∈ ℕ)
2826, 27syl 17 . . . . . . . . 9 ((𝜑𝑗𝑍) → ((𝑗𝑀) + 1) ∈ ℕ)
2924, 28eqeltrrd 2839 . . . . . . . 8 ((𝜑𝑗𝑍) → (𝑗 + (1 − 𝑀)) ∈ ℕ)
30 oveq1 7220 . . . . . . . . . . 11 (𝑥 = (𝑗 + (1 − 𝑀)) → (𝑥 − 1) = ((𝑗 + (1 − 𝑀)) − 1))
3130oveq2d 7229 . . . . . . . . . 10 (𝑥 = (𝑗 + (1 − 𝑀)) → (𝑀 + (𝑥 − 1)) = (𝑀 + ((𝑗 + (1 − 𝑀)) − 1)))
3231fveq2d 6721 . . . . . . . . 9 (𝑥 = (𝑗 + (1 − 𝑀)) → (𝐻‘(𝑀 + (𝑥 − 1))) = (𝐻‘(𝑀 + ((𝑗 + (1 − 𝑀)) − 1))))
33 eqid 2737 . . . . . . . . 9 (𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1)))) = (𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1))))
34 fvex 6730 . . . . . . . . 9 (𝐻‘(𝑀 + ((𝑗 + (1 − 𝑀)) − 1))) ∈ V
3532, 33, 34fvmpt 6818 . . . . . . . 8 ((𝑗 + (1 − 𝑀)) ∈ ℕ → ((𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1))))‘(𝑗 + (1 − 𝑀))) = (𝐻‘(𝑀 + ((𝑗 + (1 − 𝑀)) − 1))))
3629, 35syl 17 . . . . . . 7 ((𝜑𝑗𝑍) → ((𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1))))‘(𝑗 + (1 − 𝑀))) = (𝐻‘(𝑀 + ((𝑗 + (1 − 𝑀)) − 1))))
3724oveq1d 7228 . . . . . . . . . . 11 ((𝜑𝑗𝑍) → (((𝑗𝑀) + 1) − 1) = ((𝑗 + (1 − 𝑀)) − 1))
3826nn0cnd 12152 . . . . . . . . . . . 12 ((𝜑𝑗𝑍) → (𝑗𝑀) ∈ ℂ)
39 ax-1cn 10787 . . . . . . . . . . . 12 1 ∈ ℂ
40 pncan 11084 . . . . . . . . . . . 12 (((𝑗𝑀) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑗𝑀) + 1) − 1) = (𝑗𝑀))
4138, 39, 40sylancl 589 . . . . . . . . . . 11 ((𝜑𝑗𝑍) → (((𝑗𝑀) + 1) − 1) = (𝑗𝑀))
4237, 41eqtr3d 2779 . . . . . . . . . 10 ((𝜑𝑗𝑍) → ((𝑗 + (1 − 𝑀)) − 1) = (𝑗𝑀))
4342oveq2d 7229 . . . . . . . . 9 ((𝜑𝑗𝑍) → (𝑀 + ((𝑗 + (1 − 𝑀)) − 1)) = (𝑀 + (𝑗𝑀)))
4422, 20pncan3d 11192 . . . . . . . . 9 ((𝜑𝑗𝑍) → (𝑀 + (𝑗𝑀)) = 𝑗)
4543, 44eqtrd 2777 . . . . . . . 8 ((𝜑𝑗𝑍) → (𝑀 + ((𝑗 + (1 − 𝑀)) − 1)) = 𝑗)
4645fveq2d 6721 . . . . . . 7 ((𝜑𝑗𝑍) → (𝐻‘(𝑀 + ((𝑗 + (1 − 𝑀)) − 1))) = (𝐻𝑗))
4736, 46eqtr2d 2778 . . . . . 6 ((𝜑𝑗𝑍) → (𝐻𝑗) = ((𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1))))‘(𝑗 + (1 − 𝑀))))
4813, 15, 47syl2an 599 . . . . 5 (((𝜑𝑘𝑍) ∧ 𝑗 ∈ (𝑀...𝑘)) → (𝐻𝑗) = ((𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1))))‘(𝑗 + (1 − 𝑀))))
4911, 12, 48seqshft2 13602 . . . 4 ((𝜑𝑘𝑍) → (seq𝑀( + , 𝐻)‘𝑘) = (seq(𝑀 + (1 − 𝑀))( + , (𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1)))))‘(𝑘 + (1 − 𝑀))))
5021adantr 484 . . . . . . 7 ((𝜑𝑘𝑍) → 𝑀 ∈ ℂ)
51 pncan3 11086 . . . . . . 7 ((𝑀 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑀 + (1 − 𝑀)) = 1)
5250, 39, 51sylancl 589 . . . . . 6 ((𝜑𝑘𝑍) → (𝑀 + (1 − 𝑀)) = 1)
5352seqeq1d 13580 . . . . 5 ((𝜑𝑘𝑍) → seq(𝑀 + (1 − 𝑀))( + , (𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1))))) = seq1( + , (𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1))))))
5453fveq1d 6719 . . . 4 ((𝜑𝑘𝑍) → (seq(𝑀 + (1 − 𝑀))( + , (𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1)))))‘(𝑘 + (1 − 𝑀))) = (seq1( + , (𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1)))))‘(𝑘 + (1 − 𝑀))))
5549, 54eqtr2d 2778 . . 3 ((𝜑𝑘𝑍) → (seq1( + , (𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1)))))‘(𝑘 + (1 − 𝑀))) = (seq𝑀( + , 𝐻)‘𝑘))
561, 2, 5, 7, 9, 55climshft2 15143 . 2 (𝜑 → (seq𝑀( + , 𝐻) ⇝ 𝐴 ↔ seq1( + , (𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1))))) ⇝ 𝐴))
57 isercoll2.w . . 3 𝑊 = (ℤ𝑁)
58 isercoll2.n . . 3 (𝜑𝑁 ∈ ℤ)
59 isercoll2.g . . . . . 6 (𝜑𝐺:𝑍𝑊)
6059adantr 484 . . . . 5 ((𝜑𝑥 ∈ ℕ) → 𝐺:𝑍𝑊)
61 uzid 12453 . . . . . . . 8 (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ𝑀))
622, 61syl 17 . . . . . . 7 (𝜑𝑀 ∈ (ℤ𝑀))
63 nnm1nn0 12131 . . . . . . 7 (𝑥 ∈ ℕ → (𝑥 − 1) ∈ ℕ0)
64 uzaddcl 12500 . . . . . . 7 ((𝑀 ∈ (ℤ𝑀) ∧ (𝑥 − 1) ∈ ℕ0) → (𝑀 + (𝑥 − 1)) ∈ (ℤ𝑀))
6562, 63, 64syl2an 599 . . . . . 6 ((𝜑𝑥 ∈ ℕ) → (𝑀 + (𝑥 − 1)) ∈ (ℤ𝑀))
6665, 1eleqtrrdi 2849 . . . . 5 ((𝜑𝑥 ∈ ℕ) → (𝑀 + (𝑥 − 1)) ∈ 𝑍)
6760, 66ffvelrnd 6905 . . . 4 ((𝜑𝑥 ∈ ℕ) → (𝐺‘(𝑀 + (𝑥 − 1))) ∈ 𝑊)
6867fmpttd 6932 . . 3 (𝜑 → (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1)))):ℕ⟶𝑊)
69 fveq2 6717 . . . . . . 7 (𝑘 = (𝑀 + (𝑗 − 1)) → (𝐺𝑘) = (𝐺‘(𝑀 + (𝑗 − 1))))
70 fvoveq1 7236 . . . . . . 7 (𝑘 = (𝑀 + (𝑗 − 1)) → (𝐺‘(𝑘 + 1)) = (𝐺‘((𝑀 + (𝑗 − 1)) + 1)))
7169, 70breq12d 5066 . . . . . 6 (𝑘 = (𝑀 + (𝑗 − 1)) → ((𝐺𝑘) < (𝐺‘(𝑘 + 1)) ↔ (𝐺‘(𝑀 + (𝑗 − 1))) < (𝐺‘((𝑀 + (𝑗 − 1)) + 1))))
72 isercoll2.i . . . . . . . 8 ((𝜑𝑘𝑍) → (𝐺𝑘) < (𝐺‘(𝑘 + 1)))
7372ralrimiva 3105 . . . . . . 7 (𝜑 → ∀𝑘𝑍 (𝐺𝑘) < (𝐺‘(𝑘 + 1)))
7473adantr 484 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → ∀𝑘𝑍 (𝐺𝑘) < (𝐺‘(𝑘 + 1)))
75 nnm1nn0 12131 . . . . . . . 8 (𝑗 ∈ ℕ → (𝑗 − 1) ∈ ℕ0)
76 uzaddcl 12500 . . . . . . . 8 ((𝑀 ∈ (ℤ𝑀) ∧ (𝑗 − 1) ∈ ℕ0) → (𝑀 + (𝑗 − 1)) ∈ (ℤ𝑀))
7762, 75, 76syl2an 599 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → (𝑀 + (𝑗 − 1)) ∈ (ℤ𝑀))
7877, 1eleqtrrdi 2849 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → (𝑀 + (𝑗 − 1)) ∈ 𝑍)
7971, 74, 78rspcdva 3539 . . . . 5 ((𝜑𝑗 ∈ ℕ) → (𝐺‘(𝑀 + (𝑗 − 1))) < (𝐺‘((𝑀 + (𝑗 − 1)) + 1)))
80 nncn 11838 . . . . . . . . . 10 (𝑗 ∈ ℕ → 𝑗 ∈ ℂ)
8180adantl 485 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → 𝑗 ∈ ℂ)
82 1cnd 10828 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → 1 ∈ ℂ)
8381, 82, 82addsubd 11210 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → ((𝑗 + 1) − 1) = ((𝑗 − 1) + 1))
8483oveq2d 7229 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → (𝑀 + ((𝑗 + 1) − 1)) = (𝑀 + ((𝑗 − 1) + 1)))
8521adantr 484 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → 𝑀 ∈ ℂ)
8675adantl 485 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (𝑗 − 1) ∈ ℕ0)
8786nn0cnd 12152 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (𝑗 − 1) ∈ ℂ)
8885, 87, 82addassd 10855 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → ((𝑀 + (𝑗 − 1)) + 1) = (𝑀 + ((𝑗 − 1) + 1)))
8984, 88eqtr4d 2780 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → (𝑀 + ((𝑗 + 1) − 1)) = ((𝑀 + (𝑗 − 1)) + 1))
9089fveq2d 6721 . . . . 5 ((𝜑𝑗 ∈ ℕ) → (𝐺‘(𝑀 + ((𝑗 + 1) − 1))) = (𝐺‘((𝑀 + (𝑗 − 1)) + 1)))
9179, 90breqtrrd 5081 . . . 4 ((𝜑𝑗 ∈ ℕ) → (𝐺‘(𝑀 + (𝑗 − 1))) < (𝐺‘(𝑀 + ((𝑗 + 1) − 1))))
92 oveq1 7220 . . . . . . . 8 (𝑥 = 𝑗 → (𝑥 − 1) = (𝑗 − 1))
9392oveq2d 7229 . . . . . . 7 (𝑥 = 𝑗 → (𝑀 + (𝑥 − 1)) = (𝑀 + (𝑗 − 1)))
9493fveq2d 6721 . . . . . 6 (𝑥 = 𝑗 → (𝐺‘(𝑀 + (𝑥 − 1))) = (𝐺‘(𝑀 + (𝑗 − 1))))
95 eqid 2737 . . . . . 6 (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1)))) = (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1))))
96 fvex 6730 . . . . . 6 (𝐺‘(𝑀 + (𝑗 − 1))) ∈ V
9794, 95, 96fvmpt 6818 . . . . 5 (𝑗 ∈ ℕ → ((𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1))))‘𝑗) = (𝐺‘(𝑀 + (𝑗 − 1))))
9897adantl 485 . . . 4 ((𝜑𝑗 ∈ ℕ) → ((𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1))))‘𝑗) = (𝐺‘(𝑀 + (𝑗 − 1))))
99 peano2nn 11842 . . . . . 6 (𝑗 ∈ ℕ → (𝑗 + 1) ∈ ℕ)
10099adantl 485 . . . . 5 ((𝜑𝑗 ∈ ℕ) → (𝑗 + 1) ∈ ℕ)
101 oveq1 7220 . . . . . . . 8 (𝑥 = (𝑗 + 1) → (𝑥 − 1) = ((𝑗 + 1) − 1))
102101oveq2d 7229 . . . . . . 7 (𝑥 = (𝑗 + 1) → (𝑀 + (𝑥 − 1)) = (𝑀 + ((𝑗 + 1) − 1)))
103102fveq2d 6721 . . . . . 6 (𝑥 = (𝑗 + 1) → (𝐺‘(𝑀 + (𝑥 − 1))) = (𝐺‘(𝑀 + ((𝑗 + 1) − 1))))
104 fvex 6730 . . . . . 6 (𝐺‘(𝑀 + ((𝑗 + 1) − 1))) ∈ V
105103, 95, 104fvmpt 6818 . . . . 5 ((𝑗 + 1) ∈ ℕ → ((𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1))))‘(𝑗 + 1)) = (𝐺‘(𝑀 + ((𝑗 + 1) − 1))))
106100, 105syl 17 . . . 4 ((𝜑𝑗 ∈ ℕ) → ((𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1))))‘(𝑗 + 1)) = (𝐺‘(𝑀 + ((𝑗 + 1) − 1))))
10791, 98, 1063brtr4d 5085 . . 3 ((𝜑𝑗 ∈ ℕ) → ((𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1))))‘𝑗) < ((𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1))))‘(𝑗 + 1)))
10859ffnd 6546 . . . . . . . 8 (𝜑𝐺 Fn 𝑍)
109 uznn0sub 12473 . . . . . . . . . . . . 13 (𝑘 ∈ (ℤ𝑀) → (𝑘𝑀) ∈ ℕ0)
11011, 109syl 17 . . . . . . . . . . . 12 ((𝜑𝑘𝑍) → (𝑘𝑀) ∈ ℕ0)
111 nn0p1nn 12129 . . . . . . . . . . . 12 ((𝑘𝑀) ∈ ℕ0 → ((𝑘𝑀) + 1) ∈ ℕ)
112110, 111syl 17 . . . . . . . . . . 11 ((𝜑𝑘𝑍) → ((𝑘𝑀) + 1) ∈ ℕ)
113110nn0cnd 12152 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝑍) → (𝑘𝑀) ∈ ℂ)
114 pncan 11084 . . . . . . . . . . . . . . 15 (((𝑘𝑀) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑘𝑀) + 1) − 1) = (𝑘𝑀))
115113, 39, 114sylancl 589 . . . . . . . . . . . . . 14 ((𝜑𝑘𝑍) → (((𝑘𝑀) + 1) − 1) = (𝑘𝑀))
116115oveq2d 7229 . . . . . . . . . . . . 13 ((𝜑𝑘𝑍) → (𝑀 + (((𝑘𝑀) + 1) − 1)) = (𝑀 + (𝑘𝑀)))
117 eluzelz 12448 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (ℤ𝑀) → 𝑘 ∈ ℤ)
118117, 1eleq2s 2856 . . . . . . . . . . . . . . 15 (𝑘𝑍𝑘 ∈ ℤ)
119118zcnd 12283 . . . . . . . . . . . . . 14 (𝑘𝑍𝑘 ∈ ℂ)
120 pncan3 11086 . . . . . . . . . . . . . 14 ((𝑀 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝑀 + (𝑘𝑀)) = 𝑘)
12121, 119, 120syl2an 599 . . . . . . . . . . . . 13 ((𝜑𝑘𝑍) → (𝑀 + (𝑘𝑀)) = 𝑘)
122116, 121eqtr2d 2778 . . . . . . . . . . . 12 ((𝜑𝑘𝑍) → 𝑘 = (𝑀 + (((𝑘𝑀) + 1) − 1)))
123122fveq2d 6721 . . . . . . . . . . 11 ((𝜑𝑘𝑍) → (𝐺𝑘) = (𝐺‘(𝑀 + (((𝑘𝑀) + 1) − 1))))
124 oveq1 7220 . . . . . . . . . . . . . 14 (𝑥 = ((𝑘𝑀) + 1) → (𝑥 − 1) = (((𝑘𝑀) + 1) − 1))
125124oveq2d 7229 . . . . . . . . . . . . 13 (𝑥 = ((𝑘𝑀) + 1) → (𝑀 + (𝑥 − 1)) = (𝑀 + (((𝑘𝑀) + 1) − 1)))
126125fveq2d 6721 . . . . . . . . . . . 12 (𝑥 = ((𝑘𝑀) + 1) → (𝐺‘(𝑀 + (𝑥 − 1))) = (𝐺‘(𝑀 + (((𝑘𝑀) + 1) − 1))))
127126rspceeqv 3552 . . . . . . . . . . 11 ((((𝑘𝑀) + 1) ∈ ℕ ∧ (𝐺𝑘) = (𝐺‘(𝑀 + (((𝑘𝑀) + 1) − 1)))) → ∃𝑥 ∈ ℕ (𝐺𝑘) = (𝐺‘(𝑀 + (𝑥 − 1))))
128112, 123, 127syl2anc 587 . . . . . . . . . 10 ((𝜑𝑘𝑍) → ∃𝑥 ∈ ℕ (𝐺𝑘) = (𝐺‘(𝑀 + (𝑥 − 1))))
129 fvex 6730 . . . . . . . . . . 11 (𝐺𝑘) ∈ V
13095elrnmpt 5825 . . . . . . . . . . 11 ((𝐺𝑘) ∈ V → ((𝐺𝑘) ∈ ran (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1)))) ↔ ∃𝑥 ∈ ℕ (𝐺𝑘) = (𝐺‘(𝑀 + (𝑥 − 1)))))
131129, 130ax-mp 5 . . . . . . . . . 10 ((𝐺𝑘) ∈ ran (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1)))) ↔ ∃𝑥 ∈ ℕ (𝐺𝑘) = (𝐺‘(𝑀 + (𝑥 − 1))))
132128, 131sylibr 237 . . . . . . . . 9 ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ ran (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1)))))
133132ralrimiva 3105 . . . . . . . 8 (𝜑 → ∀𝑘𝑍 (𝐺𝑘) ∈ ran (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1)))))
134 ffnfv 6935 . . . . . . . 8 (𝐺:𝑍⟶ran (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1)))) ↔ (𝐺 Fn 𝑍 ∧ ∀𝑘𝑍 (𝐺𝑘) ∈ ran (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1))))))
135108, 133, 134sylanbrc 586 . . . . . . 7 (𝜑𝐺:𝑍⟶ran (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1)))))
136135frnd 6553 . . . . . 6 (𝜑 → ran 𝐺 ⊆ ran (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1)))))
137136sscond 4056 . . . . 5 (𝜑 → (𝑊 ∖ ran (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1))))) ⊆ (𝑊 ∖ ran 𝐺))
138137sselda 3901 . . . 4 ((𝜑𝑛 ∈ (𝑊 ∖ ran (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1)))))) → 𝑛 ∈ (𝑊 ∖ ran 𝐺))
139 isercoll2.0 . . . 4 ((𝜑𝑛 ∈ (𝑊 ∖ ran 𝐺)) → (𝐹𝑛) = 0)
140138, 139syldan 594 . . 3 ((𝜑𝑛 ∈ (𝑊 ∖ ran (𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1)))))) → (𝐹𝑛) = 0)
141 isercoll2.f . . 3 ((𝜑𝑛𝑊) → (𝐹𝑛) ∈ ℂ)
142 fveq2 6717 . . . . . 6 (𝑘 = (𝑀 + (𝑗 − 1)) → (𝐻𝑘) = (𝐻‘(𝑀 + (𝑗 − 1))))
14369fveq2d 6721 . . . . . 6 (𝑘 = (𝑀 + (𝑗 − 1)) → (𝐹‘(𝐺𝑘)) = (𝐹‘(𝐺‘(𝑀 + (𝑗 − 1)))))
144142, 143eqeq12d 2753 . . . . 5 (𝑘 = (𝑀 + (𝑗 − 1)) → ((𝐻𝑘) = (𝐹‘(𝐺𝑘)) ↔ (𝐻‘(𝑀 + (𝑗 − 1))) = (𝐹‘(𝐺‘(𝑀 + (𝑗 − 1))))))
145 isercoll2.h . . . . . . 7 ((𝜑𝑘𝑍) → (𝐻𝑘) = (𝐹‘(𝐺𝑘)))
146145ralrimiva 3105 . . . . . 6 (𝜑 → ∀𝑘𝑍 (𝐻𝑘) = (𝐹‘(𝐺𝑘)))
147146adantr 484 . . . . 5 ((𝜑𝑗 ∈ ℕ) → ∀𝑘𝑍 (𝐻𝑘) = (𝐹‘(𝐺𝑘)))
148144, 147, 78rspcdva 3539 . . . 4 ((𝜑𝑗 ∈ ℕ) → (𝐻‘(𝑀 + (𝑗 − 1))) = (𝐹‘(𝐺‘(𝑀 + (𝑗 − 1)))))
14993fveq2d 6721 . . . . . 6 (𝑥 = 𝑗 → (𝐻‘(𝑀 + (𝑥 − 1))) = (𝐻‘(𝑀 + (𝑗 − 1))))
150 fvex 6730 . . . . . 6 (𝐻‘(𝑀 + (𝑗 − 1))) ∈ V
151149, 33, 150fvmpt 6818 . . . . 5 (𝑗 ∈ ℕ → ((𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1))))‘𝑗) = (𝐻‘(𝑀 + (𝑗 − 1))))
152151adantl 485 . . . 4 ((𝜑𝑗 ∈ ℕ) → ((𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1))))‘𝑗) = (𝐻‘(𝑀 + (𝑗 − 1))))
15398fveq2d 6721 . . . 4 ((𝜑𝑗 ∈ ℕ) → (𝐹‘((𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1))))‘𝑗)) = (𝐹‘(𝐺‘(𝑀 + (𝑗 − 1)))))
154148, 152, 1533eqtr4d 2787 . . 3 ((𝜑𝑗 ∈ ℕ) → ((𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1))))‘𝑗) = (𝐹‘((𝑥 ∈ ℕ ↦ (𝐺‘(𝑀 + (𝑥 − 1))))‘𝑗)))
15557, 58, 68, 107, 140, 141, 154isercoll 15231 . 2 (𝜑 → (seq1( + , (𝑥 ∈ ℕ ↦ (𝐻‘(𝑀 + (𝑥 − 1))))) ⇝ 𝐴 ↔ seq𝑁( + , 𝐹) ⇝ 𝐴))
15656, 155bitrd 282 1 (𝜑 → (seq𝑀( + , 𝐻) ⇝ 𝐴 ↔ seq𝑁( + , 𝐹) ⇝ 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1543  wcel 2110  wral 3061  wrex 3062  Vcvv 3408  cdif 3863   class class class wbr 5053  cmpt 5135  ran crn 5552   Fn wfn 6375  wf 6376  cfv 6380  (class class class)co 7213  cc 10727  0cc0 10729  1c1 10730   + caddc 10732   < clt 10867  cmin 11062  cn 11830  0cn0 12090  cz 12176  cuz 12438  ...cfz 13095  seqcseq 13574  cli 15045
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5179  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-inf2 9256  ax-cnex 10785  ax-resscn 10786  ax-1cn 10787  ax-icn 10788  ax-addcl 10789  ax-addrcl 10790  ax-mulcl 10791  ax-mulrcl 10792  ax-mulcom 10793  ax-addass 10794  ax-mulass 10795  ax-distr 10796  ax-i2m1 10797  ax-1ne0 10798  ax-1rid 10799  ax-rnegex 10800  ax-rrecex 10801  ax-cnre 10802  ax-pre-lttri 10803  ax-pre-lttrn 10804  ax-pre-ltadd 10805  ax-pre-mulgt0 10806  ax-pre-sup 10807
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-int 4860  df-iun 4906  df-br 5054  df-opab 5116  df-mpt 5136  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-pred 6160  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-isom 6389  df-riota 7170  df-ov 7216  df-oprab 7217  df-mpo 7218  df-om 7645  df-1st 7761  df-2nd 7762  df-wrecs 8047  df-recs 8108  df-rdg 8146  df-1o 8202  df-oadd 8206  df-er 8391  df-en 8627  df-dom 8628  df-sdom 8629  df-fin 8630  df-sup 9058  df-card 9555  df-pnf 10869  df-mnf 10870  df-xr 10871  df-ltxr 10872  df-le 10873  df-sub 11064  df-neg 11065  df-nn 11831  df-n0 12091  df-xnn0 12163  df-z 12177  df-uz 12439  df-fz 13096  df-seq 13575  df-hash 13897  df-shft 14630  df-clim 15049
This theorem is referenced by:  iserodd  16388  stirlinglem5  43294
  Copyright terms: Public domain W3C validator