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

Theorem seqz 13423
 Description: If the operation + has an absorbing element 𝑍 (a.k.a. zero element), then any sequence containing a 𝑍 evaluates to 𝑍. (Contributed by Mario Carneiro, 27-May-2014.)
Hypotheses
Ref Expression
seqhomo.1 ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
seqhomo.2 ((𝜑𝑥 ∈ (𝑀...𝑁)) → (𝐹𝑥) ∈ 𝑆)
seqz.3 ((𝜑𝑥𝑆) → (𝑍 + 𝑥) = 𝑍)
seqz.4 ((𝜑𝑥𝑆) → (𝑥 + 𝑍) = 𝑍)
seqz.5 (𝜑𝐾 ∈ (𝑀...𝑁))
seqz.6 (𝜑𝑁𝑉)
seqz.7 (𝜑 → (𝐹𝐾) = 𝑍)
Assertion
Ref Expression
seqz (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = 𝑍)
Distinct variable groups:   𝑥,𝑦,𝐹   𝑥,𝑀,𝑦   𝑥,𝑁,𝑦   𝜑,𝑥,𝑦   𝑥,𝐾,𝑦   𝑥, + ,𝑦   𝑥,𝑆,𝑦   𝑥,𝑍,𝑦
Allowed substitution hints:   𝑉(𝑥,𝑦)

Proof of Theorem seqz
StepHypRef Expression
1 seqz.5 . . . 4 (𝜑𝐾 ∈ (𝑀...𝑁))
2 elfzuz 12907 . . . 4 (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ𝑀))
31, 2syl 17 . . 3 (𝜑𝐾 ∈ (ℤ𝑀))
4 eluzelz 12250 . . . . . . . . 9 (𝐾 ∈ (ℤ𝑀) → 𝐾 ∈ ℤ)
53, 4syl 17 . . . . . . . 8 (𝜑𝐾 ∈ ℤ)
6 seq1 13386 . . . . . . . 8 (𝐾 ∈ ℤ → (seq𝐾( + , 𝐹)‘𝐾) = (𝐹𝐾))
75, 6syl 17 . . . . . . 7 (𝜑 → (seq𝐾( + , 𝐹)‘𝐾) = (𝐹𝐾))
8 seqz.7 . . . . . . 7 (𝜑 → (𝐹𝐾) = 𝑍)
97, 8eqtrd 2859 . . . . . 6 (𝜑 → (seq𝐾( + , 𝐹)‘𝐾) = 𝑍)
10 seqeq1 13376 . . . . . . . 8 (𝐾 = 𝑀 → seq𝐾( + , 𝐹) = seq𝑀( + , 𝐹))
1110fveq1d 6663 . . . . . . 7 (𝐾 = 𝑀 → (seq𝐾( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝐾))
1211eqeq1d 2826 . . . . . 6 (𝐾 = 𝑀 → ((seq𝐾( + , 𝐹)‘𝐾) = 𝑍 ↔ (seq𝑀( + , 𝐹)‘𝐾) = 𝑍))
139, 12syl5ibcom 248 . . . . 5 (𝜑 → (𝐾 = 𝑀 → (seq𝑀( + , 𝐹)‘𝐾) = 𝑍))
14 eluzel2 12245 . . . . . . . . 9 (𝐾 ∈ (ℤ𝑀) → 𝑀 ∈ ℤ)
153, 14syl 17 . . . . . . . 8 (𝜑𝑀 ∈ ℤ)
16 seqm1 13392 . . . . . . . 8 ((𝑀 ∈ ℤ ∧ 𝐾 ∈ (ℤ‘(𝑀 + 1))) → (seq𝑀( + , 𝐹)‘𝐾) = ((seq𝑀( + , 𝐹)‘(𝐾 − 1)) + (𝐹𝐾)))
1715, 16sylan 583 . . . . . . 7 ((𝜑𝐾 ∈ (ℤ‘(𝑀 + 1))) → (seq𝑀( + , 𝐹)‘𝐾) = ((seq𝑀( + , 𝐹)‘(𝐾 − 1)) + (𝐹𝐾)))
188adantr 484 . . . . . . . . 9 ((𝜑𝐾 ∈ (ℤ‘(𝑀 + 1))) → (𝐹𝐾) = 𝑍)
1918oveq2d 7165 . . . . . . . 8 ((𝜑𝐾 ∈ (ℤ‘(𝑀 + 1))) → ((seq𝑀( + , 𝐹)‘(𝐾 − 1)) + (𝐹𝐾)) = ((seq𝑀( + , 𝐹)‘(𝐾 − 1)) + 𝑍))
20 oveq1 7156 . . . . . . . . . 10 (𝑥 = (seq𝑀( + , 𝐹)‘(𝐾 − 1)) → (𝑥 + 𝑍) = ((seq𝑀( + , 𝐹)‘(𝐾 − 1)) + 𝑍))
2120eqeq1d 2826 . . . . . . . . 9 (𝑥 = (seq𝑀( + , 𝐹)‘(𝐾 − 1)) → ((𝑥 + 𝑍) = 𝑍 ↔ ((seq𝑀( + , 𝐹)‘(𝐾 − 1)) + 𝑍) = 𝑍))
22 seqz.4 . . . . . . . . . . 11 ((𝜑𝑥𝑆) → (𝑥 + 𝑍) = 𝑍)
2322ralrimiva 3177 . . . . . . . . . 10 (𝜑 → ∀𝑥𝑆 (𝑥 + 𝑍) = 𝑍)
2423adantr 484 . . . . . . . . 9 ((𝜑𝐾 ∈ (ℤ‘(𝑀 + 1))) → ∀𝑥𝑆 (𝑥 + 𝑍) = 𝑍)
25 eluzp1m1 12265 . . . . . . . . . . 11 ((𝑀 ∈ ℤ ∧ 𝐾 ∈ (ℤ‘(𝑀 + 1))) → (𝐾 − 1) ∈ (ℤ𝑀))
2615, 25sylan 583 . . . . . . . . . 10 ((𝜑𝐾 ∈ (ℤ‘(𝑀 + 1))) → (𝐾 − 1) ∈ (ℤ𝑀))
27 fzssp1 12954 . . . . . . . . . . . . . . 15 (𝑀...(𝐾 − 1)) ⊆ (𝑀...((𝐾 − 1) + 1))
285zcnd 12085 . . . . . . . . . . . . . . . . 17 (𝜑𝐾 ∈ ℂ)
29 ax-1cn 10593 . . . . . . . . . . . . . . . . 17 1 ∈ ℂ
30 npcan 10893 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐾 − 1) + 1) = 𝐾)
3128, 29, 30sylancl 589 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐾 − 1) + 1) = 𝐾)
3231oveq2d 7165 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀...((𝐾 − 1) + 1)) = (𝑀...𝐾))
3327, 32sseqtrid 4005 . . . . . . . . . . . . . 14 (𝜑 → (𝑀...(𝐾 − 1)) ⊆ (𝑀...𝐾))
34 elfzuz3 12908 . . . . . . . . . . . . . . . 16 (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ𝐾))
351, 34syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑁 ∈ (ℤ𝐾))
36 fzss2 12951 . . . . . . . . . . . . . . 15 (𝑁 ∈ (ℤ𝐾) → (𝑀...𝐾) ⊆ (𝑀...𝑁))
3735, 36syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑀...𝐾) ⊆ (𝑀...𝑁))
3833, 37sstrd 3963 . . . . . . . . . . . . 13 (𝜑 → (𝑀...(𝐾 − 1)) ⊆ (𝑀...𝑁))
3938adantr 484 . . . . . . . . . . . 12 ((𝜑𝐾 ∈ (ℤ‘(𝑀 + 1))) → (𝑀...(𝐾 − 1)) ⊆ (𝑀...𝑁))
4039sselda 3953 . . . . . . . . . . 11 (((𝜑𝐾 ∈ (ℤ‘(𝑀 + 1))) ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → 𝑥 ∈ (𝑀...𝑁))
41 seqhomo.2 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝑀...𝑁)) → (𝐹𝑥) ∈ 𝑆)
4241adantlr 714 . . . . . . . . . . 11 (((𝜑𝐾 ∈ (ℤ‘(𝑀 + 1))) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹𝑥) ∈ 𝑆)
4340, 42syldan 594 . . . . . . . . . 10 (((𝜑𝐾 ∈ (ℤ‘(𝑀 + 1))) ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → (𝐹𝑥) ∈ 𝑆)
44 seqhomo.1 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
4544adantlr 714 . . . . . . . . . 10 (((𝜑𝐾 ∈ (ℤ‘(𝑀 + 1))) ∧ (𝑥𝑆𝑦𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
4626, 43, 45seqcl 13395 . . . . . . . . 9 ((𝜑𝐾 ∈ (ℤ‘(𝑀 + 1))) → (seq𝑀( + , 𝐹)‘(𝐾 − 1)) ∈ 𝑆)
4721, 24, 46rspcdva 3611 . . . . . . . 8 ((𝜑𝐾 ∈ (ℤ‘(𝑀 + 1))) → ((seq𝑀( + , 𝐹)‘(𝐾 − 1)) + 𝑍) = 𝑍)
4819, 47eqtrd 2859 . . . . . . 7 ((𝜑𝐾 ∈ (ℤ‘(𝑀 + 1))) → ((seq𝑀( + , 𝐹)‘(𝐾 − 1)) + (𝐹𝐾)) = 𝑍)
4917, 48eqtrd 2859 . . . . . 6 ((𝜑𝐾 ∈ (ℤ‘(𝑀 + 1))) → (seq𝑀( + , 𝐹)‘𝐾) = 𝑍)
5049ex 416 . . . . 5 (𝜑 → (𝐾 ∈ (ℤ‘(𝑀 + 1)) → (seq𝑀( + , 𝐹)‘𝐾) = 𝑍))
51 uzp1 12276 . . . . . 6 (𝐾 ∈ (ℤ𝑀) → (𝐾 = 𝑀𝐾 ∈ (ℤ‘(𝑀 + 1))))
523, 51syl 17 . . . . 5 (𝜑 → (𝐾 = 𝑀𝐾 ∈ (ℤ‘(𝑀 + 1))))
5313, 50, 52mpjaod 857 . . . 4 (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) = 𝑍)
5453, 8eqtr4d 2862 . . 3 (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) = (𝐹𝐾))
55 eqidd 2825 . . 3 ((𝜑𝑥 ∈ ((𝐾 + 1)...𝑁)) → (𝐹𝑥) = (𝐹𝑥))
563, 54, 35, 55seqfveq2 13397 . 2 (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = (seq𝐾( + , 𝐹)‘𝑁))
57 fvex 6674 . . . . . 6 (𝐹𝐾) ∈ V
5857elsn 4565 . . . . 5 ((𝐹𝐾) ∈ {𝑍} ↔ (𝐹𝐾) = 𝑍)
598, 58sylibr 237 . . . 4 (𝜑 → (𝐹𝐾) ∈ {𝑍})
60 simprl 770 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ {𝑍} ∧ 𝑦𝑆)) → 𝑥 ∈ {𝑍})
61 velsn 4566 . . . . . . . 8 (𝑥 ∈ {𝑍} ↔ 𝑥 = 𝑍)
6260, 61sylib 221 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ {𝑍} ∧ 𝑦𝑆)) → 𝑥 = 𝑍)
6362oveq1d 7164 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ {𝑍} ∧ 𝑦𝑆)) → (𝑥 + 𝑦) = (𝑍 + 𝑦))
64 oveq2 7157 . . . . . . . 8 (𝑥 = 𝑦 → (𝑍 + 𝑥) = (𝑍 + 𝑦))
6564eqeq1d 2826 . . . . . . 7 (𝑥 = 𝑦 → ((𝑍 + 𝑥) = 𝑍 ↔ (𝑍 + 𝑦) = 𝑍))
66 seqz.3 . . . . . . . . 9 ((𝜑𝑥𝑆) → (𝑍 + 𝑥) = 𝑍)
6766ralrimiva 3177 . . . . . . . 8 (𝜑 → ∀𝑥𝑆 (𝑍 + 𝑥) = 𝑍)
6867adantr 484 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ {𝑍} ∧ 𝑦𝑆)) → ∀𝑥𝑆 (𝑍 + 𝑥) = 𝑍)
69 simprr 772 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ {𝑍} ∧ 𝑦𝑆)) → 𝑦𝑆)
7065, 68, 69rspcdva 3611 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ {𝑍} ∧ 𝑦𝑆)) → (𝑍 + 𝑦) = 𝑍)
7163, 70eqtrd 2859 . . . . 5 ((𝜑 ∧ (𝑥 ∈ {𝑍} ∧ 𝑦𝑆)) → (𝑥 + 𝑦) = 𝑍)
72 ovex 7182 . . . . . 6 (𝑥 + 𝑦) ∈ V
7372elsn 4565 . . . . 5 ((𝑥 + 𝑦) ∈ {𝑍} ↔ (𝑥 + 𝑦) = 𝑍)
7471, 73sylibr 237 . . . 4 ((𝜑 ∧ (𝑥 ∈ {𝑍} ∧ 𝑦𝑆)) → (𝑥 + 𝑦) ∈ {𝑍})
75 peano2uz 12298 . . . . . . . 8 (𝐾 ∈ (ℤ𝑀) → (𝐾 + 1) ∈ (ℤ𝑀))
763, 75syl 17 . . . . . . 7 (𝜑 → (𝐾 + 1) ∈ (ℤ𝑀))
77 fzss1 12950 . . . . . . 7 ((𝐾 + 1) ∈ (ℤ𝑀) → ((𝐾 + 1)...𝑁) ⊆ (𝑀...𝑁))
7876, 77syl 17 . . . . . 6 (𝜑 → ((𝐾 + 1)...𝑁) ⊆ (𝑀...𝑁))
7978sselda 3953 . . . . 5 ((𝜑𝑥 ∈ ((𝐾 + 1)...𝑁)) → 𝑥 ∈ (𝑀...𝑁))
8079, 41syldan 594 . . . 4 ((𝜑𝑥 ∈ ((𝐾 + 1)...𝑁)) → (𝐹𝑥) ∈ 𝑆)
8159, 74, 35, 80seqcl2 13393 . . 3 (𝜑 → (seq𝐾( + , 𝐹)‘𝑁) ∈ {𝑍})
82 elsni 4567 . . 3 ((seq𝐾( + , 𝐹)‘𝑁) ∈ {𝑍} → (seq𝐾( + , 𝐹)‘𝑁) = 𝑍)
8381, 82syl 17 . 2 (𝜑 → (seq𝐾( + , 𝐹)‘𝑁) = 𝑍)
8456, 83eqtrd 2859 1 (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = 𝑍)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∨ wo 844   = wceq 1538   ∈ wcel 2115  ∀wral 3133   ⊆ wss 3919  {csn 4550  ‘cfv 6343  (class class class)co 7149  ℂcc 10533  1c1 10536   + caddc 10538   − cmin 10868  ℤcz 11978  ℤ≥cuz 12240  ...cfz 12894  seqcseq 13373 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7455  ax-cnex 10591  ax-resscn 10592  ax-1cn 10593  ax-icn 10594  ax-addcl 10595  ax-addrcl 10596  ax-mulcl 10597  ax-mulrcl 10598  ax-mulcom 10599  ax-addass 10600  ax-mulass 10601  ax-distr 10602  ax-i2m1 10603  ax-1ne0 10604  ax-1rid 10605  ax-rnegex 10606  ax-rrecex 10607  ax-cnre 10608  ax-pre-lttri 10609  ax-pre-lttrn 10610  ax-pre-ltadd 10611  ax-pre-mulgt0 10612 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4825  df-iun 4907  df-br 5053  df-opab 5115  df-mpt 5133  df-tr 5159  df-id 5447  df-eprel 5452  df-po 5461  df-so 5462  df-fr 5501  df-we 5503  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-pred 6135  df-ord 6181  df-on 6182  df-lim 6183  df-suc 6184  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-riota 7107  df-ov 7152  df-oprab 7153  df-mpo 7154  df-om 7575  df-1st 7684  df-2nd 7685  df-wrecs 7943  df-recs 8004  df-rdg 8042  df-er 8285  df-en 8506  df-dom 8507  df-sdom 8508  df-pnf 10675  df-mnf 10676  df-xr 10677  df-ltxr 10678  df-le 10679  df-sub 10870  df-neg 10871  df-nn 11635  df-n0 11895  df-z 11979  df-uz 12241  df-fz 12895  df-seq 13374 This theorem is referenced by:  bcval5  13683  elqaalem2  24919  lgsne0  25922
 Copyright terms: Public domain W3C validator