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

Theorem seqid2 13170
 Description: The last few partial sums of a sequence that ends with all zeroes (or any element which is a right-identity for +) are all the same. (Contributed by Mario Carneiro, 13-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.)
Hypotheses
Ref Expression
seqid2.1 ((𝜑𝑥𝑆) → (𝑥 + 𝑍) = 𝑥)
seqid2.2 (𝜑𝐾 ∈ (ℤ𝑀))
seqid2.3 (𝜑𝑁 ∈ (ℤ𝐾))
seqid2.4 (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) ∈ 𝑆)
seqid2.5 ((𝜑𝑥 ∈ ((𝐾 + 1)...𝑁)) → (𝐹𝑥) = 𝑍)
Assertion
Ref Expression
seqid2 (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑁))
Distinct variable groups:   𝑥,𝐹   𝑥,𝐾   𝑥,𝑀   𝑥,𝑁   𝜑,𝑥   𝑥,𝑆   𝑥, +   𝑥,𝑍

Proof of Theorem seqid2
Dummy variable 𝑛 is distinct from all other variables.
StepHypRef Expression
1 seqid2.3 . . 3 (𝜑𝑁 ∈ (ℤ𝐾))
2 eluzfz2 12671 . . 3 (𝑁 ∈ (ℤ𝐾) → 𝑁 ∈ (𝐾...𝑁))
31, 2syl 17 . 2 (𝜑𝑁 ∈ (𝐾...𝑁))
4 eleq1 2847 . . . . . 6 (𝑥 = 𝐾 → (𝑥 ∈ (𝐾...𝑁) ↔ 𝐾 ∈ (𝐾...𝑁)))
5 fveq2 6448 . . . . . . 7 (𝑥 = 𝐾 → (seq𝑀( + , 𝐹)‘𝑥) = (seq𝑀( + , 𝐹)‘𝐾))
65eqeq2d 2788 . . . . . 6 (𝑥 = 𝐾 → ((seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑥) ↔ (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝐾)))
74, 6imbi12d 336 . . . . 5 (𝑥 = 𝐾 → ((𝑥 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑥)) ↔ (𝐾 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝐾))))
87imbi2d 332 . . . 4 (𝑥 = 𝐾 → ((𝜑 → (𝑥 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑥))) ↔ (𝜑 → (𝐾 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝐾)))))
9 eleq1 2847 . . . . . 6 (𝑥 = 𝑛 → (𝑥 ∈ (𝐾...𝑁) ↔ 𝑛 ∈ (𝐾...𝑁)))
10 fveq2 6448 . . . . . . 7 (𝑥 = 𝑛 → (seq𝑀( + , 𝐹)‘𝑥) = (seq𝑀( + , 𝐹)‘𝑛))
1110eqeq2d 2788 . . . . . 6 (𝑥 = 𝑛 → ((seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑥) ↔ (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑛)))
129, 11imbi12d 336 . . . . 5 (𝑥 = 𝑛 → ((𝑥 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑥)) ↔ (𝑛 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑛))))
1312imbi2d 332 . . . 4 (𝑥 = 𝑛 → ((𝜑 → (𝑥 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑥))) ↔ (𝜑 → (𝑛 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑛)))))
14 eleq1 2847 . . . . . 6 (𝑥 = (𝑛 + 1) → (𝑥 ∈ (𝐾...𝑁) ↔ (𝑛 + 1) ∈ (𝐾...𝑁)))
15 fveq2 6448 . . . . . . 7 (𝑥 = (𝑛 + 1) → (seq𝑀( + , 𝐹)‘𝑥) = (seq𝑀( + , 𝐹)‘(𝑛 + 1)))
1615eqeq2d 2788 . . . . . 6 (𝑥 = (𝑛 + 1) → ((seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑥) ↔ (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘(𝑛 + 1))))
1714, 16imbi12d 336 . . . . 5 (𝑥 = (𝑛 + 1) → ((𝑥 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑥)) ↔ ((𝑛 + 1) ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘(𝑛 + 1)))))
1817imbi2d 332 . . . 4 (𝑥 = (𝑛 + 1) → ((𝜑 → (𝑥 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑥))) ↔ (𝜑 → ((𝑛 + 1) ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘(𝑛 + 1))))))
19 eleq1 2847 . . . . . 6 (𝑥 = 𝑁 → (𝑥 ∈ (𝐾...𝑁) ↔ 𝑁 ∈ (𝐾...𝑁)))
20 fveq2 6448 . . . . . . 7 (𝑥 = 𝑁 → (seq𝑀( + , 𝐹)‘𝑥) = (seq𝑀( + , 𝐹)‘𝑁))
2120eqeq2d 2788 . . . . . 6 (𝑥 = 𝑁 → ((seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑥) ↔ (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑁)))
2219, 21imbi12d 336 . . . . 5 (𝑥 = 𝑁 → ((𝑥 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑥)) ↔ (𝑁 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑁))))
2322imbi2d 332 . . . 4 (𝑥 = 𝑁 → ((𝜑 → (𝑥 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑥))) ↔ (𝜑 → (𝑁 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑁)))))
24 eqidd 2779 . . . . 5 (𝐾 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝐾))
25242a1i 12 . . . 4 (𝐾 ∈ ℤ → (𝜑 → (𝐾 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝐾))))
26 peano2fzr 12676 . . . . . . . 8 ((𝑛 ∈ (ℤ𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁)) → 𝑛 ∈ (𝐾...𝑁))
2726adantl 475 . . . . . . 7 ((𝜑 ∧ (𝑛 ∈ (ℤ𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → 𝑛 ∈ (𝐾...𝑁))
2827expr 450 . . . . . 6 ((𝜑𝑛 ∈ (ℤ𝐾)) → ((𝑛 + 1) ∈ (𝐾...𝑁) → 𝑛 ∈ (𝐾...𝑁)))
2928imim1d 82 . . . . 5 ((𝜑𝑛 ∈ (ℤ𝐾)) → ((𝑛 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑛)) → ((𝑛 + 1) ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑛))))
30 oveq1 6931 . . . . . 6 ((seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑛) → ((seq𝑀( + , 𝐹)‘𝐾) + (𝐹‘(𝑛 + 1))) = ((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1))))
31 fveqeq2 6457 . . . . . . . . . 10 (𝑥 = (𝑛 + 1) → ((𝐹𝑥) = 𝑍 ↔ (𝐹‘(𝑛 + 1)) = 𝑍))
32 seqid2.5 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐾 + 1)...𝑁)) → (𝐹𝑥) = 𝑍)
3332ralrimiva 3148 . . . . . . . . . . 11 (𝜑 → ∀𝑥 ∈ ((𝐾 + 1)...𝑁)(𝐹𝑥) = 𝑍)
3433adantr 474 . . . . . . . . . 10 ((𝜑 ∧ (𝑛 ∈ (ℤ𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → ∀𝑥 ∈ ((𝐾 + 1)...𝑁)(𝐹𝑥) = 𝑍)
35 eluzp1p1 12023 . . . . . . . . . . . 12 (𝑛 ∈ (ℤ𝐾) → (𝑛 + 1) ∈ (ℤ‘(𝐾 + 1)))
3635ad2antrl 718 . . . . . . . . . . 11 ((𝜑 ∧ (𝑛 ∈ (ℤ𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → (𝑛 + 1) ∈ (ℤ‘(𝐾 + 1)))
37 elfzuz3 12661 . . . . . . . . . . . 12 ((𝑛 + 1) ∈ (𝐾...𝑁) → 𝑁 ∈ (ℤ‘(𝑛 + 1)))
3837ad2antll 719 . . . . . . . . . . 11 ((𝜑 ∧ (𝑛 ∈ (ℤ𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → 𝑁 ∈ (ℤ‘(𝑛 + 1)))
39 elfzuzb 12658 . . . . . . . . . . 11 ((𝑛 + 1) ∈ ((𝐾 + 1)...𝑁) ↔ ((𝑛 + 1) ∈ (ℤ‘(𝐾 + 1)) ∧ 𝑁 ∈ (ℤ‘(𝑛 + 1))))
4036, 38, 39sylanbrc 578 . . . . . . . . . 10 ((𝜑 ∧ (𝑛 ∈ (ℤ𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → (𝑛 + 1) ∈ ((𝐾 + 1)...𝑁))
4131, 34, 40rspcdva 3517 . . . . . . . . 9 ((𝜑 ∧ (𝑛 ∈ (ℤ𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → (𝐹‘(𝑛 + 1)) = 𝑍)
4241oveq2d 6940 . . . . . . . 8 ((𝜑 ∧ (𝑛 ∈ (ℤ𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → ((seq𝑀( + , 𝐹)‘𝐾) + (𝐹‘(𝑛 + 1))) = ((seq𝑀( + , 𝐹)‘𝐾) + 𝑍))
43 oveq1 6931 . . . . . . . . . . 11 (𝑥 = (seq𝑀( + , 𝐹)‘𝐾) → (𝑥 + 𝑍) = ((seq𝑀( + , 𝐹)‘𝐾) + 𝑍))
44 id 22 . . . . . . . . . . 11 (𝑥 = (seq𝑀( + , 𝐹)‘𝐾) → 𝑥 = (seq𝑀( + , 𝐹)‘𝐾))
4543, 44eqeq12d 2793 . . . . . . . . . 10 (𝑥 = (seq𝑀( + , 𝐹)‘𝐾) → ((𝑥 + 𝑍) = 𝑥 ↔ ((seq𝑀( + , 𝐹)‘𝐾) + 𝑍) = (seq𝑀( + , 𝐹)‘𝐾)))
46 seqid2.1 . . . . . . . . . . 11 ((𝜑𝑥𝑆) → (𝑥 + 𝑍) = 𝑥)
4746ralrimiva 3148 . . . . . . . . . 10 (𝜑 → ∀𝑥𝑆 (𝑥 + 𝑍) = 𝑥)
48 seqid2.4 . . . . . . . . . 10 (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) ∈ 𝑆)
4945, 47, 48rspcdva 3517 . . . . . . . . 9 (𝜑 → ((seq𝑀( + , 𝐹)‘𝐾) + 𝑍) = (seq𝑀( + , 𝐹)‘𝐾))
5049adantr 474 . . . . . . . 8 ((𝜑 ∧ (𝑛 ∈ (ℤ𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → ((seq𝑀( + , 𝐹)‘𝐾) + 𝑍) = (seq𝑀( + , 𝐹)‘𝐾))
5142, 50eqtr2d 2815 . . . . . . 7 ((𝜑 ∧ (𝑛 ∈ (ℤ𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → (seq𝑀( + , 𝐹)‘𝐾) = ((seq𝑀( + , 𝐹)‘𝐾) + (𝐹‘(𝑛 + 1))))
52 simprl 761 . . . . . . . . 9 ((𝜑 ∧ (𝑛 ∈ (ℤ𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → 𝑛 ∈ (ℤ𝐾))
53 seqid2.2 . . . . . . . . . 10 (𝜑𝐾 ∈ (ℤ𝑀))
5453adantr 474 . . . . . . . . 9 ((𝜑 ∧ (𝑛 ∈ (ℤ𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → 𝐾 ∈ (ℤ𝑀))
55 uztrn 12014 . . . . . . . . 9 ((𝑛 ∈ (ℤ𝐾) ∧ 𝐾 ∈ (ℤ𝑀)) → 𝑛 ∈ (ℤ𝑀))
5652, 54, 55syl2anc 579 . . . . . . . 8 ((𝜑 ∧ (𝑛 ∈ (ℤ𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → 𝑛 ∈ (ℤ𝑀))
57 seqp1 13139 . . . . . . . 8 (𝑛 ∈ (ℤ𝑀) → (seq𝑀( + , 𝐹)‘(𝑛 + 1)) = ((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1))))
5856, 57syl 17 . . . . . . 7 ((𝜑 ∧ (𝑛 ∈ (ℤ𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → (seq𝑀( + , 𝐹)‘(𝑛 + 1)) = ((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1))))
5951, 58eqeq12d 2793 . . . . . 6 ((𝜑 ∧ (𝑛 ∈ (ℤ𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → ((seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘(𝑛 + 1)) ↔ ((seq𝑀( + , 𝐹)‘𝐾) + (𝐹‘(𝑛 + 1))) = ((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1)))))
6030, 59syl5ibr 238 . . . . 5 ((𝜑 ∧ (𝑛 ∈ (ℤ𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → ((seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑛) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘(𝑛 + 1))))
6129, 60animpimp2impd 835 . . . 4 (𝑛 ∈ (ℤ𝐾) → ((𝜑 → (𝑛 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑛))) → (𝜑 → ((𝑛 + 1) ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘(𝑛 + 1))))))
628, 13, 18, 23, 25, 61uzind4 12057 . . 3 (𝑁 ∈ (ℤ𝐾) → (𝜑 → (𝑁 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑁))))
631, 62mpcom 38 . 2 (𝜑 → (𝑁 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑁)))
643, 63mpd 15 1 (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑁))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 386   = wceq 1601   ∈ wcel 2107  ∀wral 3090  ‘cfv 6137  (class class class)co 6924  1c1 10275   + caddc 10277  ℤcz 11733  ℤ≥cuz 11997  ...cfz 12648  seqcseq 13124 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228  ax-cnex 10330  ax-resscn 10331  ax-1cn 10332  ax-icn 10333  ax-addcl 10334  ax-addrcl 10335  ax-mulcl 10336  ax-mulrcl 10337  ax-mulcom 10338  ax-addass 10339  ax-mulass 10340  ax-distr 10341  ax-i2m1 10342  ax-1ne0 10343  ax-1rid 10344  ax-rnegex 10345  ax-rrecex 10346  ax-cnre 10347  ax-pre-lttri 10348  ax-pre-lttrn 10349  ax-pre-ltadd 10350  ax-pre-mulgt0 10351 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4674  df-iun 4757  df-br 4889  df-opab 4951  df-mpt 4968  df-tr 4990  df-id 5263  df-eprel 5268  df-po 5276  df-so 5277  df-fr 5316  df-we 5318  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-pred 5935  df-ord 5981  df-on 5982  df-lim 5983  df-suc 5984  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-f1 6142  df-fo 6143  df-f1o 6144  df-fv 6145  df-riota 6885  df-ov 6927  df-oprab 6928  df-mpt2 6929  df-om 7346  df-1st 7447  df-2nd 7448  df-wrecs 7691  df-recs 7753  df-rdg 7791  df-er 8028  df-en 8244  df-dom 8245  df-sdom 8246  df-pnf 10415  df-mnf 10416  df-xr 10417  df-ltxr 10418  df-le 10419  df-sub 10610  df-neg 10611  df-nn 11380  df-n0 11648  df-z 11734  df-uz 11998  df-fz 12649  df-seq 13125 This theorem is referenced by:  seqcoll  13568  seqcoll2  13569  fsumcvg  14859  fprodcvg  15072  ovolicc1  23731  lgsdilem2  25521
 Copyright terms: Public domain W3C validator