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

Theorem seqz 13056
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 12545 . . . 4 (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ𝑀))
31, 2syl 17 . . 3 (𝜑𝐾 ∈ (ℤ𝑀))
4 eluzelz 11896 . . . . . . . . 9 (𝐾 ∈ (ℤ𝑀) → 𝐾 ∈ ℤ)
53, 4syl 17 . . . . . . . 8 (𝜑𝐾 ∈ ℤ)
6 seq1 13021 . . . . . . . 8 (𝐾 ∈ ℤ → (seq𝐾( + , 𝐹)‘𝐾) = (𝐹𝐾))
75, 6syl 17 . . . . . . 7 (𝜑 → (seq𝐾( + , 𝐹)‘𝐾) = (𝐹𝐾))
8 seqz.7 . . . . . . 7 (𝜑 → (𝐹𝐾) = 𝑍)
97, 8eqtrd 2799 . . . . . 6 (𝜑 → (seq𝐾( + , 𝐹)‘𝐾) = 𝑍)
10 seqeq1 13011 . . . . . . . 8 (𝐾 = 𝑀 → seq𝐾( + , 𝐹) = seq𝑀( + , 𝐹))
1110fveq1d 6377 . . . . . . 7 (𝐾 = 𝑀 → (seq𝐾( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝐾))
1211eqeq1d 2767 . . . . . 6 (𝐾 = 𝑀 → ((seq𝐾( + , 𝐹)‘𝐾) = 𝑍 ↔ (seq𝑀( + , 𝐹)‘𝐾) = 𝑍))
139, 12syl5ibcom 236 . . . . 5 (𝜑 → (𝐾 = 𝑀 → (seq𝑀( + , 𝐹)‘𝐾) = 𝑍))
14 eluzel2 11891 . . . . . . . . 9 (𝐾 ∈ (ℤ𝑀) → 𝑀 ∈ ℤ)
153, 14syl 17 . . . . . . . 8 (𝜑𝑀 ∈ ℤ)
16 seqm1 13025 . . . . . . . 8 ((𝑀 ∈ ℤ ∧ 𝐾 ∈ (ℤ‘(𝑀 + 1))) → (seq𝑀( + , 𝐹)‘𝐾) = ((seq𝑀( + , 𝐹)‘(𝐾 − 1)) + (𝐹𝐾)))
1715, 16sylan 575 . . . . . . 7 ((𝜑𝐾 ∈ (ℤ‘(𝑀 + 1))) → (seq𝑀( + , 𝐹)‘𝐾) = ((seq𝑀( + , 𝐹)‘(𝐾 − 1)) + (𝐹𝐾)))
188adantr 472 . . . . . . . . 9 ((𝜑𝐾 ∈ (ℤ‘(𝑀 + 1))) → (𝐹𝐾) = 𝑍)
1918oveq2d 6858 . . . . . . . 8 ((𝜑𝐾 ∈ (ℤ‘(𝑀 + 1))) → ((seq𝑀( + , 𝐹)‘(𝐾 − 1)) + (𝐹𝐾)) = ((seq𝑀( + , 𝐹)‘(𝐾 − 1)) + 𝑍))
20 oveq1 6849 . . . . . . . . . 10 (𝑥 = (seq𝑀( + , 𝐹)‘(𝐾 − 1)) → (𝑥 + 𝑍) = ((seq𝑀( + , 𝐹)‘(𝐾 − 1)) + 𝑍))
2120eqeq1d 2767 . . . . . . . . 9 (𝑥 = (seq𝑀( + , 𝐹)‘(𝐾 − 1)) → ((𝑥 + 𝑍) = 𝑍 ↔ ((seq𝑀( + , 𝐹)‘(𝐾 − 1)) + 𝑍) = 𝑍))
22 seqz.4 . . . . . . . . . . 11 ((𝜑𝑥𝑆) → (𝑥 + 𝑍) = 𝑍)
2322ralrimiva 3113 . . . . . . . . . 10 (𝜑 → ∀𝑥𝑆 (𝑥 + 𝑍) = 𝑍)
2423adantr 472 . . . . . . . . 9 ((𝜑𝐾 ∈ (ℤ‘(𝑀 + 1))) → ∀𝑥𝑆 (𝑥 + 𝑍) = 𝑍)
25 eluzp1m1 11910 . . . . . . . . . . 11 ((𝑀 ∈ ℤ ∧ 𝐾 ∈ (ℤ‘(𝑀 + 1))) → (𝐾 − 1) ∈ (ℤ𝑀))
2615, 25sylan 575 . . . . . . . . . 10 ((𝜑𝐾 ∈ (ℤ‘(𝑀 + 1))) → (𝐾 − 1) ∈ (ℤ𝑀))
27 fzssp1 12591 . . . . . . . . . . . . . . 15 (𝑀...(𝐾 − 1)) ⊆ (𝑀...((𝐾 − 1) + 1))
285zcnd 11730 . . . . . . . . . . . . . . . . 17 (𝜑𝐾 ∈ ℂ)
29 ax-1cn 10247 . . . . . . . . . . . . . . . . 17 1 ∈ ℂ
30 npcan 10544 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐾 − 1) + 1) = 𝐾)
3128, 29, 30sylancl 580 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐾 − 1) + 1) = 𝐾)
3231oveq2d 6858 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀...((𝐾 − 1) + 1)) = (𝑀...𝐾))
3327, 32syl5sseq 3813 . . . . . . . . . . . . . 14 (𝜑 → (𝑀...(𝐾 − 1)) ⊆ (𝑀...𝐾))
34 elfzuz3 12546 . . . . . . . . . . . . . . . 16 (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ𝐾))
351, 34syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑁 ∈ (ℤ𝐾))
36 fzss2 12588 . . . . . . . . . . . . . . 15 (𝑁 ∈ (ℤ𝐾) → (𝑀...𝐾) ⊆ (𝑀...𝑁))
3735, 36syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑀...𝐾) ⊆ (𝑀...𝑁))
3833, 37sstrd 3771 . . . . . . . . . . . . 13 (𝜑 → (𝑀...(𝐾 − 1)) ⊆ (𝑀...𝑁))
3938adantr 472 . . . . . . . . . . . 12 ((𝜑𝐾 ∈ (ℤ‘(𝑀 + 1))) → (𝑀...(𝐾 − 1)) ⊆ (𝑀...𝑁))
4039sselda 3761 . . . . . . . . . . 11 (((𝜑𝐾 ∈ (ℤ‘(𝑀 + 1))) ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → 𝑥 ∈ (𝑀...𝑁))
41 seqhomo.2 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝑀...𝑁)) → (𝐹𝑥) ∈ 𝑆)
4241adantlr 706 . . . . . . . . . . 11 (((𝜑𝐾 ∈ (ℤ‘(𝑀 + 1))) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹𝑥) ∈ 𝑆)
4340, 42syldan 585 . . . . . . . . . 10 (((𝜑𝐾 ∈ (ℤ‘(𝑀 + 1))) ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → (𝐹𝑥) ∈ 𝑆)
44 seqhomo.1 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
4544adantlr 706 . . . . . . . . . 10 (((𝜑𝐾 ∈ (ℤ‘(𝑀 + 1))) ∧ (𝑥𝑆𝑦𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
4626, 43, 45seqcl 13028 . . . . . . . . 9 ((𝜑𝐾 ∈ (ℤ‘(𝑀 + 1))) → (seq𝑀( + , 𝐹)‘(𝐾 − 1)) ∈ 𝑆)
4721, 24, 46rspcdva 3467 . . . . . . . 8 ((𝜑𝐾 ∈ (ℤ‘(𝑀 + 1))) → ((seq𝑀( + , 𝐹)‘(𝐾 − 1)) + 𝑍) = 𝑍)
4819, 47eqtrd 2799 . . . . . . 7 ((𝜑𝐾 ∈ (ℤ‘(𝑀 + 1))) → ((seq𝑀( + , 𝐹)‘(𝐾 − 1)) + (𝐹𝐾)) = 𝑍)
4917, 48eqtrd 2799 . . . . . 6 ((𝜑𝐾 ∈ (ℤ‘(𝑀 + 1))) → (seq𝑀( + , 𝐹)‘𝐾) = 𝑍)
5049ex 401 . . . . 5 (𝜑 → (𝐾 ∈ (ℤ‘(𝑀 + 1)) → (seq𝑀( + , 𝐹)‘𝐾) = 𝑍))
51 uzp1 11921 . . . . . 6 (𝐾 ∈ (ℤ𝑀) → (𝐾 = 𝑀𝐾 ∈ (ℤ‘(𝑀 + 1))))
523, 51syl 17 . . . . 5 (𝜑 → (𝐾 = 𝑀𝐾 ∈ (ℤ‘(𝑀 + 1))))
5313, 50, 52mpjaod 886 . . . 4 (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) = 𝑍)
5453, 8eqtr4d 2802 . . 3 (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) = (𝐹𝐾))
55 eqidd 2766 . . 3 ((𝜑𝑥 ∈ ((𝐾 + 1)...𝑁)) → (𝐹𝑥) = (𝐹𝑥))
563, 54, 35, 55seqfveq2 13030 . 2 (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = (seq𝐾( + , 𝐹)‘𝑁))
57 fvex 6388 . . . . . 6 (𝐹𝐾) ∈ V
5857elsn 4349 . . . . 5 ((𝐹𝐾) ∈ {𝑍} ↔ (𝐹𝐾) = 𝑍)
598, 58sylibr 225 . . . 4 (𝜑 → (𝐹𝐾) ∈ {𝑍})
60 simprl 787 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ {𝑍} ∧ 𝑦𝑆)) → 𝑥 ∈ {𝑍})
61 velsn 4350 . . . . . . . 8 (𝑥 ∈ {𝑍} ↔ 𝑥 = 𝑍)
6260, 61sylib 209 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ {𝑍} ∧ 𝑦𝑆)) → 𝑥 = 𝑍)
6362oveq1d 6857 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ {𝑍} ∧ 𝑦𝑆)) → (𝑥 + 𝑦) = (𝑍 + 𝑦))
64 oveq2 6850 . . . . . . . 8 (𝑥 = 𝑦 → (𝑍 + 𝑥) = (𝑍 + 𝑦))
6564eqeq1d 2767 . . . . . . 7 (𝑥 = 𝑦 → ((𝑍 + 𝑥) = 𝑍 ↔ (𝑍 + 𝑦) = 𝑍))
66 seqz.3 . . . . . . . . 9 ((𝜑𝑥𝑆) → (𝑍 + 𝑥) = 𝑍)
6766ralrimiva 3113 . . . . . . . 8 (𝜑 → ∀𝑥𝑆 (𝑍 + 𝑥) = 𝑍)
6867adantr 472 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ {𝑍} ∧ 𝑦𝑆)) → ∀𝑥𝑆 (𝑍 + 𝑥) = 𝑍)
69 simprr 789 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ {𝑍} ∧ 𝑦𝑆)) → 𝑦𝑆)
7065, 68, 69rspcdva 3467 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ {𝑍} ∧ 𝑦𝑆)) → (𝑍 + 𝑦) = 𝑍)
7163, 70eqtrd 2799 . . . . 5 ((𝜑 ∧ (𝑥 ∈ {𝑍} ∧ 𝑦𝑆)) → (𝑥 + 𝑦) = 𝑍)
72 ovex 6874 . . . . . 6 (𝑥 + 𝑦) ∈ V
7372elsn 4349 . . . . 5 ((𝑥 + 𝑦) ∈ {𝑍} ↔ (𝑥 + 𝑦) = 𝑍)
7471, 73sylibr 225 . . . 4 ((𝜑 ∧ (𝑥 ∈ {𝑍} ∧ 𝑦𝑆)) → (𝑥 + 𝑦) ∈ {𝑍})
75 peano2uz 11941 . . . . . . . 8 (𝐾 ∈ (ℤ𝑀) → (𝐾 + 1) ∈ (ℤ𝑀))
763, 75syl 17 . . . . . . 7 (𝜑 → (𝐾 + 1) ∈ (ℤ𝑀))
77 fzss1 12587 . . . . . . 7 ((𝐾 + 1) ∈ (ℤ𝑀) → ((𝐾 + 1)...𝑁) ⊆ (𝑀...𝑁))
7876, 77syl 17 . . . . . 6 (𝜑 → ((𝐾 + 1)...𝑁) ⊆ (𝑀...𝑁))
7978sselda 3761 . . . . 5 ((𝜑𝑥 ∈ ((𝐾 + 1)...𝑁)) → 𝑥 ∈ (𝑀...𝑁))
8079, 41syldan 585 . . . 4 ((𝜑𝑥 ∈ ((𝐾 + 1)...𝑁)) → (𝐹𝑥) ∈ 𝑆)
8159, 74, 35, 80seqcl2 13026 . . 3 (𝜑 → (seq𝐾( + , 𝐹)‘𝑁) ∈ {𝑍})
82 elsni 4351 . . 3 ((seq𝐾( + , 𝐹)‘𝑁) ∈ {𝑍} → (seq𝐾( + , 𝐹)‘𝑁) = 𝑍)
8381, 82syl 17 . 2 (𝜑 → (seq𝐾( + , 𝐹)‘𝑁) = 𝑍)
8456, 83eqtrd 2799 1 (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = 𝑍)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wo 873   = wceq 1652  wcel 2155  wral 3055  wss 3732  {csn 4334  cfv 6068  (class class class)co 6842  cc 10187  1c1 10190   + caddc 10192  cmin 10520  cz 11624  cuz 11886  ...cfz 12533  seqcseq 13008
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-1st 7366  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-er 7947  df-en 8161  df-dom 8162  df-sdom 8163  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-nn 11275  df-n0 11539  df-z 11625  df-uz 11887  df-fz 12534  df-seq 13009
This theorem is referenced by:  bcval5  13309  elqaalem2  24366  lgsne0  25351
  Copyright terms: Public domain W3C validator