ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  seq3id2 GIF version

Theorem seq3id2 10571
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 Jim Kingdon, 12-Nov-2022.)
Hypotheses
Ref Expression
seqid2.1 ((𝜑𝑥𝑆) → (𝑥 + 𝑍) = 𝑥)
seqid2.2 (𝜑𝐾 ∈ (ℤ𝑀))
seqid2.3 (𝜑𝑁 ∈ (ℤ𝐾))
seqid2.4 (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) ∈ 𝑆)
seqid2.5 ((𝜑𝑥 ∈ ((𝐾 + 1)...𝑁)) → (𝐹𝑥) = 𝑍)
seq3id2.f ((𝜑𝑥 ∈ (ℤ𝑀)) → (𝐹𝑥) ∈ 𝑆)
seq3id2.cl ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
Assertion
Ref Expression
seq3id2 (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑁))
Distinct variable groups:   𝑥,𝑦,𝐹   𝑥,𝐾,𝑦   𝑥,𝑀,𝑦   𝑥,𝑁,𝑦   𝜑,𝑥,𝑦   𝑥,𝑆,𝑦   𝑥, + ,𝑦   𝑥,𝑍
Allowed substitution hint:   𝑍(𝑦)

Proof of Theorem seq3id2
Dummy variable 𝑛 is distinct from all other variables.
StepHypRef Expression
1 seqid2.3 . . 3 (𝜑𝑁 ∈ (ℤ𝐾))
2 eluzfz2 10084 . . 3 (𝑁 ∈ (ℤ𝐾) → 𝑁 ∈ (𝐾...𝑁))
31, 2syl 14 . 2 (𝜑𝑁 ∈ (𝐾...𝑁))
4 eleq1 2252 . . . . . 6 (𝑥 = 𝐾 → (𝑥 ∈ (𝐾...𝑁) ↔ 𝐾 ∈ (𝐾...𝑁)))
5 fveq2 5542 . . . . . . 7 (𝑥 = 𝐾 → (seq𝑀( + , 𝐹)‘𝑥) = (seq𝑀( + , 𝐹)‘𝐾))
65eqeq2d 2201 . . . . . 6 (𝑥 = 𝐾 → ((seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑥) ↔ (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝐾)))
74, 6imbi12d 234 . . . . 5 (𝑥 = 𝐾 → ((𝑥 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑥)) ↔ (𝐾 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝐾))))
87imbi2d 230 . . . 4 (𝑥 = 𝐾 → ((𝜑 → (𝑥 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑥))) ↔ (𝜑 → (𝐾 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝐾)))))
9 eleq1 2252 . . . . . 6 (𝑥 = 𝑛 → (𝑥 ∈ (𝐾...𝑁) ↔ 𝑛 ∈ (𝐾...𝑁)))
10 fveq2 5542 . . . . . . 7 (𝑥 = 𝑛 → (seq𝑀( + , 𝐹)‘𝑥) = (seq𝑀( + , 𝐹)‘𝑛))
1110eqeq2d 2201 . . . . . 6 (𝑥 = 𝑛 → ((seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑥) ↔ (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑛)))
129, 11imbi12d 234 . . . . 5 (𝑥 = 𝑛 → ((𝑥 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑥)) ↔ (𝑛 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑛))))
1312imbi2d 230 . . . 4 (𝑥 = 𝑛 → ((𝜑 → (𝑥 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑥))) ↔ (𝜑 → (𝑛 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑛)))))
14 eleq1 2252 . . . . . 6 (𝑥 = (𝑛 + 1) → (𝑥 ∈ (𝐾...𝑁) ↔ (𝑛 + 1) ∈ (𝐾...𝑁)))
15 fveq2 5542 . . . . . . 7 (𝑥 = (𝑛 + 1) → (seq𝑀( + , 𝐹)‘𝑥) = (seq𝑀( + , 𝐹)‘(𝑛 + 1)))
1615eqeq2d 2201 . . . . . 6 (𝑥 = (𝑛 + 1) → ((seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑥) ↔ (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘(𝑛 + 1))))
1714, 16imbi12d 234 . . . . 5 (𝑥 = (𝑛 + 1) → ((𝑥 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑥)) ↔ ((𝑛 + 1) ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘(𝑛 + 1)))))
1817imbi2d 230 . . . 4 (𝑥 = (𝑛 + 1) → ((𝜑 → (𝑥 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑥))) ↔ (𝜑 → ((𝑛 + 1) ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘(𝑛 + 1))))))
19 eleq1 2252 . . . . . 6 (𝑥 = 𝑁 → (𝑥 ∈ (𝐾...𝑁) ↔ 𝑁 ∈ (𝐾...𝑁)))
20 fveq2 5542 . . . . . . 7 (𝑥 = 𝑁 → (seq𝑀( + , 𝐹)‘𝑥) = (seq𝑀( + , 𝐹)‘𝑁))
2120eqeq2d 2201 . . . . . 6 (𝑥 = 𝑁 → ((seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑥) ↔ (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑁)))
2219, 21imbi12d 234 . . . . 5 (𝑥 = 𝑁 → ((𝑥 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑥)) ↔ (𝑁 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑁))))
2322imbi2d 230 . . . 4 (𝑥 = 𝑁 → ((𝜑 → (𝑥 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑥))) ↔ (𝜑 → (𝑁 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑁)))))
24 eqidd 2190 . . . . 5 (𝐾 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝐾))
25242a1i 27 . . . 4 (𝐾 ∈ ℤ → (𝜑 → (𝐾 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝐾))))
26 peano2fzr 10089 . . . . . . . 8 ((𝑛 ∈ (ℤ𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁)) → 𝑛 ∈ (𝐾...𝑁))
2726adantl 277 . . . . . . 7 ((𝜑 ∧ (𝑛 ∈ (ℤ𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → 𝑛 ∈ (𝐾...𝑁))
2827expr 375 . . . . . 6 ((𝜑𝑛 ∈ (ℤ𝐾)) → ((𝑛 + 1) ∈ (𝐾...𝑁) → 𝑛 ∈ (𝐾...𝑁)))
2928imim1d 75 . . . . 5 ((𝜑𝑛 ∈ (ℤ𝐾)) → ((𝑛 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑛)) → ((𝑛 + 1) ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑛))))
30 oveq1 5913 . . . . . 6 ((seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑛) → ((seq𝑀( + , 𝐹)‘𝐾) + (𝐹‘(𝑛 + 1))) = ((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1))))
31 fveqeq2 5551 . . . . . . . . . 10 (𝑥 = (𝑛 + 1) → ((𝐹𝑥) = 𝑍 ↔ (𝐹‘(𝑛 + 1)) = 𝑍))
32 seqid2.5 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐾 + 1)...𝑁)) → (𝐹𝑥) = 𝑍)
3332ralrimiva 2563 . . . . . . . . . . 11 (𝜑 → ∀𝑥 ∈ ((𝐾 + 1)...𝑁)(𝐹𝑥) = 𝑍)
3433adantr 276 . . . . . . . . . 10 ((𝜑 ∧ (𝑛 ∈ (ℤ𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → ∀𝑥 ∈ ((𝐾 + 1)...𝑁)(𝐹𝑥) = 𝑍)
35 eluzp1p1 9604 . . . . . . . . . . . 12 (𝑛 ∈ (ℤ𝐾) → (𝑛 + 1) ∈ (ℤ‘(𝐾 + 1)))
3635ad2antrl 490 . . . . . . . . . . 11 ((𝜑 ∧ (𝑛 ∈ (ℤ𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → (𝑛 + 1) ∈ (ℤ‘(𝐾 + 1)))
37 elfzuz3 10074 . . . . . . . . . . . 12 ((𝑛 + 1) ∈ (𝐾...𝑁) → 𝑁 ∈ (ℤ‘(𝑛 + 1)))
3837ad2antll 491 . . . . . . . . . . 11 ((𝜑 ∧ (𝑛 ∈ (ℤ𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → 𝑁 ∈ (ℤ‘(𝑛 + 1)))
39 elfzuzb 10071 . . . . . . . . . . 11 ((𝑛 + 1) ∈ ((𝐾 + 1)...𝑁) ↔ ((𝑛 + 1) ∈ (ℤ‘(𝐾 + 1)) ∧ 𝑁 ∈ (ℤ‘(𝑛 + 1))))
4036, 38, 39sylanbrc 417 . . . . . . . . . 10 ((𝜑 ∧ (𝑛 ∈ (ℤ𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → (𝑛 + 1) ∈ ((𝐾 + 1)...𝑁))
4131, 34, 40rspcdva 2865 . . . . . . . . 9 ((𝜑 ∧ (𝑛 ∈ (ℤ𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → (𝐹‘(𝑛 + 1)) = 𝑍)
4241oveq2d 5922 . . . . . . . 8 ((𝜑 ∧ (𝑛 ∈ (ℤ𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → ((seq𝑀( + , 𝐹)‘𝐾) + (𝐹‘(𝑛 + 1))) = ((seq𝑀( + , 𝐹)‘𝐾) + 𝑍))
43 oveq1 5913 . . . . . . . . . . 11 (𝑥 = (seq𝑀( + , 𝐹)‘𝐾) → (𝑥 + 𝑍) = ((seq𝑀( + , 𝐹)‘𝐾) + 𝑍))
44 id 19 . . . . . . . . . . 11 (𝑥 = (seq𝑀( + , 𝐹)‘𝐾) → 𝑥 = (seq𝑀( + , 𝐹)‘𝐾))
4543, 44eqeq12d 2204 . . . . . . . . . 10 (𝑥 = (seq𝑀( + , 𝐹)‘𝐾) → ((𝑥 + 𝑍) = 𝑥 ↔ ((seq𝑀( + , 𝐹)‘𝐾) + 𝑍) = (seq𝑀( + , 𝐹)‘𝐾)))
46 seqid2.1 . . . . . . . . . . 11 ((𝜑𝑥𝑆) → (𝑥 + 𝑍) = 𝑥)
4746ralrimiva 2563 . . . . . . . . . 10 (𝜑 → ∀𝑥𝑆 (𝑥 + 𝑍) = 𝑥)
48 seqid2.4 . . . . . . . . . 10 (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) ∈ 𝑆)
4945, 47, 48rspcdva 2865 . . . . . . . . 9 (𝜑 → ((seq𝑀( + , 𝐹)‘𝐾) + 𝑍) = (seq𝑀( + , 𝐹)‘𝐾))
5049adantr 276 . . . . . . . 8 ((𝜑 ∧ (𝑛 ∈ (ℤ𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → ((seq𝑀( + , 𝐹)‘𝐾) + 𝑍) = (seq𝑀( + , 𝐹)‘𝐾))
5142, 50eqtr2d 2223 . . . . . . 7 ((𝜑 ∧ (𝑛 ∈ (ℤ𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → (seq𝑀( + , 𝐹)‘𝐾) = ((seq𝑀( + , 𝐹)‘𝐾) + (𝐹‘(𝑛 + 1))))
52 simprl 529 . . . . . . . . 9 ((𝜑 ∧ (𝑛 ∈ (ℤ𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → 𝑛 ∈ (ℤ𝐾))
53 seqid2.2 . . . . . . . . . 10 (𝜑𝐾 ∈ (ℤ𝑀))
5453adantr 276 . . . . . . . . 9 ((𝜑 ∧ (𝑛 ∈ (ℤ𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → 𝐾 ∈ (ℤ𝑀))
55 uztrn 9595 . . . . . . . . 9 ((𝑛 ∈ (ℤ𝐾) ∧ 𝐾 ∈ (ℤ𝑀)) → 𝑛 ∈ (ℤ𝑀))
5652, 54, 55syl2anc 411 . . . . . . . 8 ((𝜑 ∧ (𝑛 ∈ (ℤ𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → 𝑛 ∈ (ℤ𝑀))
57 seq3id2.f . . . . . . . . 9 ((𝜑𝑥 ∈ (ℤ𝑀)) → (𝐹𝑥) ∈ 𝑆)
5857adantlr 477 . . . . . . . 8 (((𝜑 ∧ (𝑛 ∈ (ℤ𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) ∧ 𝑥 ∈ (ℤ𝑀)) → (𝐹𝑥) ∈ 𝑆)
59 seq3id2.cl . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
6059adantlr 477 . . . . . . . 8 (((𝜑 ∧ (𝑛 ∈ (ℤ𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) ∧ (𝑥𝑆𝑦𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
6156, 58, 60seq3p1 10522 . . . . . . 7 ((𝜑 ∧ (𝑛 ∈ (ℤ𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → (seq𝑀( + , 𝐹)‘(𝑛 + 1)) = ((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1))))
6251, 61eqeq12d 2204 . . . . . 6 ((𝜑 ∧ (𝑛 ∈ (ℤ𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → ((seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘(𝑛 + 1)) ↔ ((seq𝑀( + , 𝐹)‘𝐾) + (𝐹‘(𝑛 + 1))) = ((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1)))))
6330, 62imbitrrid 156 . . . . 5 ((𝜑 ∧ (𝑛 ∈ (ℤ𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → ((seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑛) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘(𝑛 + 1))))
6429, 63animpimp2impd 559 . . . 4 (𝑛 ∈ (ℤ𝐾) → ((𝜑 → (𝑛 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑛))) → (𝜑 → ((𝑛 + 1) ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘(𝑛 + 1))))))
658, 13, 18, 23, 25, 64uzind4 9639 . . 3 (𝑁 ∈ (ℤ𝐾) → (𝜑 → (𝑁 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑁))))
661, 65mpcom 36 . 2 (𝜑 → (𝑁 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑁)))
673, 66mpd 13 1 (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑁))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104   = wceq 1364  wcel 2160  wral 2468  cfv 5242  (class class class)co 5906  1c1 7859   + caddc 7861  cz 9303  cuz 9578  ...cfz 10060  seqcseq 10504
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-coll 4140  ax-sep 4143  ax-nul 4151  ax-pow 4199  ax-pr 4234  ax-un 4458  ax-setind 4561  ax-iinf 4612  ax-cnex 7949  ax-resscn 7950  ax-1cn 7951  ax-1re 7952  ax-icn 7953  ax-addcl 7954  ax-addrcl 7955  ax-mulcl 7956  ax-addcom 7958  ax-addass 7960  ax-distr 7962  ax-i2m1 7963  ax-0lt1 7964  ax-0id 7966  ax-rnegex 7967  ax-cnre 7969  ax-pre-ltirr 7970  ax-pre-ltwlin 7971  ax-pre-lttrn 7972  ax-pre-ltadd 7974
This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-nel 2456  df-ral 2473  df-rex 2474  df-reu 2475  df-rab 2477  df-v 2758  df-sbc 2982  df-csb 3077  df-dif 3151  df-un 3153  df-in 3155  df-ss 3162  df-nul 3443  df-pw 3599  df-sn 3620  df-pr 3621  df-op 3623  df-uni 3832  df-int 3867  df-iun 3910  df-br 4026  df-opab 4087  df-mpt 4088  df-tr 4124  df-id 4318  df-iord 4391  df-on 4393  df-ilim 4394  df-suc 4396  df-iom 4615  df-xp 4657  df-rel 4658  df-cnv 4659  df-co 4660  df-dm 4661  df-rn 4662  df-res 4663  df-ima 4664  df-iota 5203  df-fun 5244  df-fn 5245  df-f 5246  df-f1 5247  df-fo 5248  df-f1o 5249  df-fv 5250  df-riota 5861  df-ov 5909  df-oprab 5910  df-mpo 5911  df-1st 6180  df-2nd 6181  df-recs 6345  df-frec 6431  df-pnf 8042  df-mnf 8043  df-xr 8044  df-ltxr 8045  df-le 8046  df-sub 8178  df-neg 8179  df-inn 8969  df-n0 9227  df-z 9304  df-uz 9579  df-fz 10061  df-seqfrec 10505
This theorem is referenced by:  seq3coll  10887  fsum3cvg  11495  fproddccvg  11689  lgsdilem2  15080
  Copyright terms: Public domain W3C validator