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

Theorem sumeq2sdv 15739
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 3906 . . . . . . . . . 10 (𝜑𝑛 / 𝑘𝐵 = 𝑛 / 𝑘𝐶)
32ifeq1d 4545 . . . . . . . . 9 (𝜑 → if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0) = if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))
43mpteq2dv 5244 . . . . . . . 8 (𝜑 → (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)) = (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0)))
54seqeq3d 14050 . . . . . . 7 (𝜑 → seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) = seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))))
65breq1d 5153 . . . . . 6 (𝜑 → (seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥 ↔ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥))
76anbi2d 630 . . . . 5 (𝜑 → ((𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ↔ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥)))
87rexbidv 3179 . . . 4 (𝜑 → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ↔ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥)))
91csbeq2dv 3906 . . . . . . . . . . 11 (𝜑(𝑓𝑛) / 𝑘𝐵 = (𝑓𝑛) / 𝑘𝐶)
109mpteq2dv 5244 . . . . . . . . . 10 (𝜑 → (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵) = (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))
1110seqeq3d 14050 . . . . . . . . 9 (𝜑 → seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵)) = seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶)))
1211fveq1d 6908 . . . . . . . 8 (𝜑 → (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚))
1312eqeq2d 2748 . . . . . . 7 (𝜑 → (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚) ↔ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚)))
1413anbi2d 630 . . . . . 6 (𝜑 → ((𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚))))
1514exbidv 1921 . . . . 5 (𝜑 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚))))
1615rexbidv 3179 . . . 4 (𝜑 → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚))))
178, 16orbi12d 919 . . 3 (𝜑 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))) ↔ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚)))))
1817iotabidv 6545 . 2 (𝜑 → (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)))) = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚)))))
19 df-sum 15723 . 2 Σ𝑘𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))))
20 df-sum 15723 . 2 Σ𝑘𝐴 𝐶 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚))))
2118, 19, 203eqtr4g 2802 1 (𝜑 → Σ𝑘𝐴 𝐵 = Σ𝑘𝐴 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wo 848   = wceq 1540  wex 1779  wcel 2108  wrex 3070  csb 3899  wss 3951  ifcif 4525   class class class wbr 5143  cmpt 5225  cio 6512  1-1-ontowf1o 6560  cfv 6561  (class class class)co 7431  0cc0 11155  1c1 11156   + caddc 11158  cn 12266  cz 12613  cuz 12878  ...cfz 13547  seqcseq 14042  cli 15520  Σcsu 15722
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-xp 5691  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-iota 6514  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-seq 14043  df-sum 15723
This theorem is referenced by:  sumsplit  15804  fsumrlim  15847  hash2iun1dif1  15860  incexclem  15872  bpolylem  16084  bpolyval  16085  efval  16115  rpnnen2lem12  16261  pcfac  16937  ramcl  17067  cshwshashnsame  17141  fsumcn  24894  fsum2cn  24895  lebnumlem3  24995  rrxdsfival  25447  uniioombllem6  25623  itg1climres  25749  itgeq1f  25806  itgeq1fOLD  25807  itgeq1  25808  cbvitgv  25812  itgeq2  25813  dvmptfsum  26013  elplyr  26240  plyeq0lem  26249  plyadd  26256  plymul  26257  coeeu  26264  coelem  26265  coeeq  26266  coeidlem  26276  coeid  26277  coeid2  26278  plyco  26280  plycjlem  26316  aareccl  26368  taylply2  26409  taylply2OLD  26410  pserdvlem2  26472  pserdv  26473  abelthlem6  26480  abelthlem9  26484  logtayl  26702  leibpi  26985  basellem3  27126  dchrvmasum2if  27541  dchrvmaeq0  27548  rpvmasum2  27556  dchrisum0re  27557  brcgr  28915  axsegcon  28942  dipfval  30721  ipval  30722  fsumiunle  32831  itgeq12dv  34328  eulerpartleme  34365  eulerpartlemr  34376  eulerpartlemn  34383  reprsum  34628  reprsuc  34630  reprpmtf1o  34641  vtsval  34652  iprodgam  35742  fwddifnval  36164  sumeq12sdv  36218  itgeq12sdv  36220  cbvitgdavw  36282  cbvitgdavw2  36298  knoppndvlem6  36518  knoppf  36536  rrnmval  37835  fsumshftd  38953  fsumcnf  45026  mccl  45613  dvnmul  45958  dvmptfprod  45960  dvnprodlem1  45961  dvnprodlem3  45963  dvnprod  45964  stoweidlem17  46032  stoweidlem26  46041  stoweidlem30  46045  stoweidlem32  46047  dirkertrigeq  46116  dirkeritg  46117  fourierdlem83  46204  fourierdlem103  46224  etransclem11  46260  etransclem24  46273  etransclem26  46275  etransclem27  46276  etransclem28  46277  etransclem31  46280  etransclem35  46284  etransclem46  46295  etransclem47  46296  rrndistlt  46305  ioorrnopn  46320  sge0val  46381  hoiqssbllem2  46638  nnsum3primes4  47775  nnsum4primesodd  47783  nnsum4primesoddALTV  47784  nnsum4primesevenALTV  47788  nn0sumshdiglemB  48541  nn0sumshdiglem1  48542  aacllem  49320
  Copyright terms: Public domain W3C validator