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

Theorem sumss2 15092
 Description: Change the index set of a sum by adding zeroes. (Contributed by Mario Carneiro, 15-Jul-2013.) (Revised by Mario Carneiro, 20-Apr-2014.)
Assertion
Ref Expression
sumss2 (((𝐴𝐵 ∧ ∀𝑘𝐴 𝐶 ∈ ℂ) ∧ (𝐵 ⊆ (ℤ𝑀) ∨ 𝐵 ∈ Fin)) → Σ𝑘𝐴 𝐶 = Σ𝑘𝐵 if(𝑘𝐴, 𝐶, 0))
Distinct variable groups:   𝐴,𝑘   𝐵,𝑘
Allowed substitution hints:   𝐶(𝑘)   𝑀(𝑘)

Proof of Theorem sumss2
Dummy variable 𝑚 is distinct from all other variables.
StepHypRef Expression
1 simpll 766 . . . 4 (((𝐴𝐵 ∧ ∀𝑘𝐴 𝐶 ∈ ℂ) ∧ 𝐵 ⊆ (ℤ𝑀)) → 𝐴𝐵)
2 iftrue 4433 . . . . . . 7 (𝑚𝐴 → if(𝑚𝐴, 𝑚 / 𝑘𝐶, 0) = 𝑚 / 𝑘𝐶)
32adantl 485 . . . . . 6 ((∀𝑘𝐴 𝐶 ∈ ℂ ∧ 𝑚𝐴) → if(𝑚𝐴, 𝑚 / 𝑘𝐶, 0) = 𝑚 / 𝑘𝐶)
4 nfcsb1v 3853 . . . . . . . . 9 𝑘𝑚 / 𝑘𝐶
54nfel1 2971 . . . . . . . 8 𝑘𝑚 / 𝑘𝐶 ∈ ℂ
6 csbeq1a 3843 . . . . . . . . 9 (𝑘 = 𝑚𝐶 = 𝑚 / 𝑘𝐶)
76eleq1d 2874 . . . . . . . 8 (𝑘 = 𝑚 → (𝐶 ∈ ℂ ↔ 𝑚 / 𝑘𝐶 ∈ ℂ))
85, 7rspc 3559 . . . . . . 7 (𝑚𝐴 → (∀𝑘𝐴 𝐶 ∈ ℂ → 𝑚 / 𝑘𝐶 ∈ ℂ))
98impcom 411 . . . . . 6 ((∀𝑘𝐴 𝐶 ∈ ℂ ∧ 𝑚𝐴) → 𝑚 / 𝑘𝐶 ∈ ℂ)
103, 9eqeltrd 2890 . . . . 5 ((∀𝑘𝐴 𝐶 ∈ ℂ ∧ 𝑚𝐴) → if(𝑚𝐴, 𝑚 / 𝑘𝐶, 0) ∈ ℂ)
1110ad4ant24 753 . . . 4 ((((𝐴𝐵 ∧ ∀𝑘𝐴 𝐶 ∈ ℂ) ∧ 𝐵 ⊆ (ℤ𝑀)) ∧ 𝑚𝐴) → if(𝑚𝐴, 𝑚 / 𝑘𝐶, 0) ∈ ℂ)
12 eldifn 4057 . . . . . 6 (𝑚 ∈ (𝐵𝐴) → ¬ 𝑚𝐴)
1312iffalsed 4438 . . . . 5 (𝑚 ∈ (𝐵𝐴) → if(𝑚𝐴, 𝑚 / 𝑘𝐶, 0) = 0)
1413adantl 485 . . . 4 ((((𝐴𝐵 ∧ ∀𝑘𝐴 𝐶 ∈ ℂ) ∧ 𝐵 ⊆ (ℤ𝑀)) ∧ 𝑚 ∈ (𝐵𝐴)) → if(𝑚𝐴, 𝑚 / 𝑘𝐶, 0) = 0)
15 simpr 488 . . . 4 (((𝐴𝐵 ∧ ∀𝑘𝐴 𝐶 ∈ ℂ) ∧ 𝐵 ⊆ (ℤ𝑀)) → 𝐵 ⊆ (ℤ𝑀))
161, 11, 14, 15sumss 15090 . . 3 (((𝐴𝐵 ∧ ∀𝑘𝐴 𝐶 ∈ ℂ) ∧ 𝐵 ⊆ (ℤ𝑀)) → Σ𝑚𝐴 if(𝑚𝐴, 𝑚 / 𝑘𝐶, 0) = Σ𝑚𝐵 if(𝑚𝐴, 𝑚 / 𝑘𝐶, 0))
17 simpll 766 . . . 4 (((𝐴𝐵 ∧ ∀𝑘𝐴 𝐶 ∈ ℂ) ∧ 𝐵 ∈ Fin) → 𝐴𝐵)
1810ad4ant24 753 . . . 4 ((((𝐴𝐵 ∧ ∀𝑘𝐴 𝐶 ∈ ℂ) ∧ 𝐵 ∈ Fin) ∧ 𝑚𝐴) → if(𝑚𝐴, 𝑚 / 𝑘𝐶, 0) ∈ ℂ)
1913adantl 485 . . . 4 ((((𝐴𝐵 ∧ ∀𝑘𝐴 𝐶 ∈ ℂ) ∧ 𝐵 ∈ Fin) ∧ 𝑚 ∈ (𝐵𝐴)) → if(𝑚𝐴, 𝑚 / 𝑘𝐶, 0) = 0)
20 simpr 488 . . . 4 (((𝐴𝐵 ∧ ∀𝑘𝐴 𝐶 ∈ ℂ) ∧ 𝐵 ∈ Fin) → 𝐵 ∈ Fin)
2117, 18, 19, 20fsumss 15091 . . 3 (((𝐴𝐵 ∧ ∀𝑘𝐴 𝐶 ∈ ℂ) ∧ 𝐵 ∈ Fin) → Σ𝑚𝐴 if(𝑚𝐴, 𝑚 / 𝑘𝐶, 0) = Σ𝑚𝐵 if(𝑚𝐴, 𝑚 / 𝑘𝐶, 0))
2216, 21jaodan 955 . 2 (((𝐴𝐵 ∧ ∀𝑘𝐴 𝐶 ∈ ℂ) ∧ (𝐵 ⊆ (ℤ𝑀) ∨ 𝐵 ∈ Fin)) → Σ𝑚𝐴 if(𝑚𝐴, 𝑚 / 𝑘𝐶, 0) = Σ𝑚𝐵 if(𝑚𝐴, 𝑚 / 𝑘𝐶, 0))
23 iftrue 4433 . . . 4 (𝑘𝐴 → if(𝑘𝐴, 𝐶, 0) = 𝐶)
2423sumeq2i 15065 . . 3 Σ𝑘𝐴 if(𝑘𝐴, 𝐶, 0) = Σ𝑘𝐴 𝐶
25 nfcv 2955 . . . 4 𝑚if(𝑘𝐴, 𝐶, 0)
26 nfv 1915 . . . . 5 𝑘 𝑚𝐴
27 nfcv 2955 . . . . 5 𝑘0
2826, 4, 27nfif 4456 . . . 4 𝑘if(𝑚𝐴, 𝑚 / 𝑘𝐶, 0)
29 eleq1w 2872 . . . . 5 (𝑘 = 𝑚 → (𝑘𝐴𝑚𝐴))
3029, 6ifbieq1d 4450 . . . 4 (𝑘 = 𝑚 → if(𝑘𝐴, 𝐶, 0) = if(𝑚𝐴, 𝑚 / 𝑘𝐶, 0))
3125, 28, 30cbvsumi 15063 . . 3 Σ𝑘𝐴 if(𝑘𝐴, 𝐶, 0) = Σ𝑚𝐴 if(𝑚𝐴, 𝑚 / 𝑘𝐶, 0)
3224, 31eqtr3i 2823 . 2 Σ𝑘𝐴 𝐶 = Σ𝑚𝐴 if(𝑚𝐴, 𝑚 / 𝑘𝐶, 0)
3325, 28, 30cbvsumi 15063 . 2 Σ𝑘𝐵 if(𝑘𝐴, 𝐶, 0) = Σ𝑚𝐵 if(𝑚𝐴, 𝑚 / 𝑘𝐶, 0)
3422, 32, 333eqtr4g 2858 1 (((𝐴𝐵 ∧ ∀𝑘𝐴 𝐶 ∈ ℂ) ∧ (𝐵 ⊆ (ℤ𝑀) ∨ 𝐵 ∈ Fin)) → Σ𝑘𝐴 𝐶 = Σ𝑘𝐵 if(𝑘𝐴, 𝐶, 0))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∨ wo 844   = wceq 1538   ∈ wcel 2111  ∀wral 3106  ⦋csb 3829   ∖ cdif 3879   ⊆ wss 3882  ifcif 4427  ‘cfv 6329  Fincfn 8507  ℂcc 10539  0cc0 10541  ℤ≥cuz 12248  Σcsu 15051 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7451  ax-inf2 9103  ax-cnex 10597  ax-resscn 10598  ax-1cn 10599  ax-icn 10600  ax-addcl 10601  ax-addrcl 10602  ax-mulcl 10603  ax-mulrcl 10604  ax-mulcom 10605  ax-addass 10606  ax-mulass 10607  ax-distr 10608  ax-i2m1 10609  ax-1ne0 10610  ax-1rid 10611  ax-rnegex 10612  ax-rrecex 10613  ax-cnre 10614  ax-pre-lttri 10615  ax-pre-lttrn 10616  ax-pre-ltadd 10617  ax-pre-mulgt0 10618  ax-pre-sup 10619 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3722  df-csb 3830  df-dif 3885  df-un 3887  df-in 3889  df-ss 3899  df-pss 3901  df-nul 4246  df-if 4428  df-pw 4501  df-sn 4528  df-pr 4530  df-tp 4532  df-op 4534  df-uni 4804  df-int 4842  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5441  df-so 5442  df-fr 5481  df-se 5482  df-we 5483  df-xp 5528  df-rel 5529  df-cnv 5530  df-co 5531  df-dm 5532  df-rn 5533  df-res 5534  df-ima 5535  df-pred 6121  df-ord 6167  df-on 6168  df-lim 6169  df-suc 6170  df-iota 6288  df-fun 6331  df-fn 6332  df-f 6333  df-f1 6334  df-fo 6335  df-f1o 6336  df-fv 6337  df-isom 6338  df-riota 7100  df-ov 7145  df-oprab 7146  df-mpo 7147  df-om 7571  df-1st 7681  df-2nd 7682  df-wrecs 7945  df-recs 8006  df-rdg 8044  df-1o 8100  df-oadd 8104  df-er 8287  df-en 8508  df-dom 8509  df-sdom 8510  df-fin 8511  df-sup 8905  df-oi 8973  df-card 9367  df-pnf 10681  df-mnf 10682  df-xr 10683  df-ltxr 10684  df-le 10685  df-sub 10876  df-neg 10877  df-div 11302  df-nn 11641  df-2 11703  df-3 11704  df-n0 11901  df-z 11987  df-uz 12249  df-rp 12395  df-fz 12903  df-fzo 13046  df-seq 13382  df-exp 13443  df-hash 13704  df-cj 14467  df-re 14468  df-im 14469  df-sqrt 14603  df-abs 14604  df-clim 14854  df-sum 15052 This theorem is referenced by:  fsumsplit  15106  sumsplit  15132  isumless  15209  rpnnen2lem11  15586  sumhash  16239  prmrec  16265  plyeq0lem  24848  prmorcht  25804  musumsum  25818  pclogsum  25840  dchrhash  25896  rpvmasum2  26137  pntlemj  26228  plymulx0  31990  hashreprin  32064  circlemeth  32084
 Copyright terms: Public domain W3C validator