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

Theorem sumeq2sdv 15735
Description: Equality deduction for sum. (Contributed by NM, 3-Jan-2006.) (Proof shortened by Glauco Siliprandi, 5-Apr-2020.) Avoid axioms. (Revised by GG, 14-Aug-2025.)
Hypothesis
Ref Expression
sumeq2sdv.1 (𝜑𝐵 = 𝐶)
Assertion
Ref Expression
sumeq2sdv (𝜑 → Σ𝑘𝐴 𝐵 = Σ𝑘𝐴 𝐶)
Distinct variable group:   𝜑,𝑘
Allowed substitution hints:   𝐴(𝑘)   𝐵(𝑘)   𝐶(𝑘)

Proof of Theorem sumeq2sdv
Dummy variables 𝑥 𝑚 𝑛 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sumeq2sdv.1 . . . . . . . . . . 11 (𝜑𝐵 = 𝐶)
21csbeq2dv 3914 . . . . . . . . . 10 (𝜑𝑛 / 𝑘𝐵 = 𝑛 / 𝑘𝐶)
32ifeq1d 4549 . . . . . . . . 9 (𝜑 → if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0) = if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))
43mpteq2dv 5249 . . . . . . . 8 (𝜑 → (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)) = (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0)))
54seqeq3d 14046 . . . . . . 7 (𝜑 → seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) = seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))))
65breq1d 5157 . . . . . 6 (𝜑 → (seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥 ↔ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥))
76anbi2d 630 . . . . 5 (𝜑 → ((𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ↔ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥)))
87rexbidv 3176 . . . 4 (𝜑 → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ↔ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥)))
91csbeq2dv 3914 . . . . . . . . . . 11 (𝜑(𝑓𝑛) / 𝑘𝐵 = (𝑓𝑛) / 𝑘𝐶)
109mpteq2dv 5249 . . . . . . . . . 10 (𝜑 → (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵) = (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))
1110seqeq3d 14046 . . . . . . . . 9 (𝜑 → seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵)) = seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶)))
1211fveq1d 6908 . . . . . . . 8 (𝜑 → (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚))
1312eqeq2d 2745 . . . . . . 7 (𝜑 → (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚) ↔ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚)))
1413anbi2d 630 . . . . . 6 (𝜑 → ((𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚))))
1514exbidv 1918 . . . . 5 (𝜑 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚))))
1615rexbidv 3176 . . . 4 (𝜑 → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚))))
178, 16orbi12d 918 . . 3 (𝜑 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))) ↔ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚)))))
1817iotabidv 6546 . 2 (𝜑 → (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)))) = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚)))))
19 df-sum 15719 . 2 Σ𝑘𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))))
20 df-sum 15719 . 2 Σ𝑘𝐴 𝐶 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚))))
2118, 19, 203eqtr4g 2799 1 (𝜑 → Σ𝑘𝐴 𝐵 = Σ𝑘𝐴 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wo 847   = wceq 1536  wex 1775  wcel 2105  wrex 3067  csb 3907  wss 3962  ifcif 4530   class class class wbr 5147  cmpt 5230  cio 6513  1-1-ontowf1o 6561  cfv 6562  (class class class)co 7430  0cc0 11152  1c1 11153   + caddc 11155  cn 12263  cz 12610  cuz 12875  ...cfz 13543  seqcseq 14038  cli 15516  Σcsu 15718
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-xp 5694  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-iota 6515  df-fv 6570  df-ov 7433  df-oprab 7434  df-mpo 7435  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-seq 14039  df-sum 15719
This theorem is referenced by:  sumsplit  15800  fsumrlim  15843  hash2iun1dif1  15856  incexclem  15868  bpolylem  16080  bpolyval  16081  efval  16111  rpnnen2lem12  16257  pcfac  16932  ramcl  17062  cshwshashnsame  17137  fsumcn  24907  fsum2cn  24908  lebnumlem3  25008  rrxdsfival  25460  uniioombllem6  25636  itg1climres  25763  itgeq1f  25820  itgeq1fOLD  25821  itgeq1  25822  cbvitgv  25826  itgeq2  25827  dvmptfsum  26027  elplyr  26254  plyeq0lem  26263  plyadd  26270  plymul  26271  coeeu  26278  coelem  26279  coeeq  26280  coeidlem  26290  coeid  26291  coeid2  26292  plyco  26294  plycjlem  26330  aareccl  26382  taylply2  26423  taylply2OLD  26424  pserdvlem2  26486  pserdv  26487  abelthlem6  26494  abelthlem9  26498  logtayl  26716  leibpi  26999  basellem3  27140  dchrvmasum2if  27555  dchrvmaeq0  27562  rpvmasum2  27570  dchrisum0re  27571  brcgr  28929  axsegcon  28956  dipfval  30730  ipval  30731  fsumiunle  32835  itgeq12dv  34307  eulerpartleme  34344  eulerpartlemr  34355  eulerpartlemn  34362  reprsum  34606  reprsuc  34608  reprpmtf1o  34619  vtsval  34630  iprodgam  35721  fwddifnval  36144  sumeq12sdv  36199  itgeq12sdv  36201  cbvitgdavw  36263  cbvitgdavw2  36279  knoppndvlem6  36499  knoppf  36517  rrnmval  37814  fsumshftd  38933  fsumcnf  44958  mccl  45553  dvnmul  45898  dvmptfprod  45900  dvnprodlem1  45901  dvnprodlem3  45903  dvnprod  45904  stoweidlem17  45972  stoweidlem26  45981  stoweidlem30  45985  stoweidlem32  45987  dirkertrigeq  46056  dirkeritg  46057  fourierdlem83  46144  fourierdlem103  46164  etransclem11  46200  etransclem24  46213  etransclem26  46215  etransclem27  46216  etransclem28  46217  etransclem31  46220  etransclem35  46224  etransclem46  46235  etransclem47  46236  rrndistlt  46245  ioorrnopn  46260  sge0val  46321  hoiqssbllem2  46578  nnsum3primes4  47712  nnsum4primesodd  47720  nnsum4primesoddALTV  47721  nnsum4primesevenALTV  47725  nn0sumshdiglemB  48469  nn0sumshdiglem1  48470  aacllem  49031
  Copyright terms: Public domain W3C validator