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

Theorem cbvsum 15743
Description: Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)
Hypotheses
Ref Expression
cbvsum.1 (𝑗 = 𝑘𝐵 = 𝐶)
cbvsum.2 𝑘𝐵
cbvsum.3 𝑗𝐶
Assertion
Ref Expression
cbvsum Σ𝑗𝐴 𝐵 = Σ𝑘𝐴 𝐶
Distinct variable group:   𝑗,𝑘
Allowed substitution hints:   𝐴(𝑗,𝑘)   𝐵(𝑗,𝑘)   𝐶(𝑗,𝑘)

Proof of Theorem cbvsum
Dummy variables 𝑓 𝑚 𝑛 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cbvsum.2 . . . . . . . . . . . . 13 𝑘𝐵
2 cbvsum.3 . . . . . . . . . . . . 13 𝑗𝐶
3 cbvsum.1 . . . . . . . . . . . . 13 (𝑗 = 𝑘𝐵 = 𝐶)
41, 2, 3cbvcsbw 3931 . . . . . . . . . . . 12 𝑛 / 𝑗𝐵 = 𝑛 / 𝑘𝐶
54a1i 11 . . . . . . . . . . 11 (⊤ → 𝑛 / 𝑗𝐵 = 𝑛 / 𝑘𝐶)
65ifeq1d 4567 . . . . . . . . . 10 (⊤ → if(𝑛𝐴, 𝑛 / 𝑗𝐵, 0) = if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))
76mpteq2dv 5268 . . . . . . . . 9 (⊤ → (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑗𝐵, 0)) = (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0)))
87seqeq3d 14060 . . . . . . . 8 (⊤ → seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑗𝐵, 0))) = seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))))
98mptru 1544 . . . . . . 7 seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑗𝐵, 0))) = seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0)))
109breq1i 5173 . . . . . 6 (seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑗𝐵, 0))) ⇝ 𝑥 ↔ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥)
1110anbi2i 622 . . . . 5 ((𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑗𝐵, 0))) ⇝ 𝑥) ↔ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥))
1211rexbii 3100 . . . 4 (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑗𝐵, 0))) ⇝ 𝑥) ↔ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥))
131, 2, 3cbvcsbw 3931 . . . . . . . . . . . . 13 (𝑓𝑛) / 𝑗𝐵 = (𝑓𝑛) / 𝑘𝐶
1413a1i 11 . . . . . . . . . . . 12 (⊤ → (𝑓𝑛) / 𝑗𝐵 = (𝑓𝑛) / 𝑘𝐶)
1514mpteq2dv 5268 . . . . . . . . . . 11 (⊤ → (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑗𝐵) = (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))
1615seqeq3d 14060 . . . . . . . . . 10 (⊤ → seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑗𝐵)) = seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶)))
1716mptru 1544 . . . . . . . . 9 seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑗𝐵)) = seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))
1817fveq1i 6921 . . . . . . . 8 (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑗𝐵))‘𝑚) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚)
1918eqeq2i 2753 . . . . . . 7 (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑗𝐵))‘𝑚) ↔ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚))
2019anbi2i 622 . . . . . 6 ((𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑗𝐵))‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚)))
2120exbii 1846 . . . . 5 (∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑗𝐵))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚)))
2221rexbii 3100 . . . 4 (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑗𝐵))‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚)))
2312, 22orbi12i 913 . . 3 ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑗𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑗𝐵))‘𝑚))) ↔ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚))))
2423iotabii 6558 . 2 (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑗𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑗𝐵))‘𝑚)))) = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚))))
25 df-sum 15735 . 2 Σ𝑗𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑗𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑗𝐵))‘𝑚))))
26 df-sum 15735 . 2 Σ𝑘𝐴 𝐶 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚))))
2724, 25, 263eqtr4i 2778 1 Σ𝑗𝐴 𝐵 = Σ𝑘𝐴 𝐶
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wo 846   = wceq 1537  wtru 1538  wex 1777  wcel 2108  wnfc 2893  wrex 3076  csb 3921  wss 3976  ifcif 4548   class class class wbr 5166  cmpt 5249  cio 6523  1-1-ontowf1o 6572  cfv 6573  (class class class)co 7448  0cc0 11184  1c1 11185   + caddc 11187  cn 12293  cz 12639  cuz 12903  ...cfz 13567  seqcseq 14052  cli 15530  Σcsu 15734
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-11 2158  ax-12 2178  ax-ext 2711
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-xp 5706  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-iota 6525  df-fv 6581  df-ov 7451  df-oprab 7452  df-mpo 7453  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-seq 14053  df-sum 15735
This theorem is referenced by:  sumfc  15757  sumss2  15774  fsumclf  15786  fsumzcl2  15787  fsumsplitf  15790  sumsnf  15791  sumsns  15798  fsummsnunz  15802  fsumsplitsnun  15803  fsum2dlem  15818  fsumcom2  15822  fsumshftm  15829  fsumrlim  15859  fsumo1  15860  o1fsum  15861  fsumiun  15869  ovolfiniun  25555  ovoliun2  25560  volfiniun  25601  itgfsum  25882  elplyd  26261  coeeq2  26301  fsumdvdscom  27246  fsumdvdsmul  27256  fsumdvdsmulOLD  27258  fsumvma  27275  fsumiunle  32833  esumpfinvalf  34040  fsumshftd  38908  sticksstones8  42110  sticksstones10  42112  sticksstones12a  42114  sticksstones12  42115  aks6d1c7lem3  42139  binomcxplemdvsum  44324  sumsnd  44926  fsummulc1f  45492  fsumf1of  45495  fsumiunss  45496  fsumreclf  45497  fsumlessf  45498  fsumsermpt  45500  dvnmul  45864  fourierdlem115  46142  sge0revalmpt  46299  sge0fsummpt  46311  sge0iunmptlemfi  46334  sge0iunmptlemre  46336  sge0ltfirpmpt2  46347  sge0isummpt2  46353  sge0xaddlem2  46355  sge0fsummptf  46357  fsummsndifre  47246  fsumsplitsndif  47247  fsummmodsndifre  47248  fsummmodsnunz  47249
  Copyright terms: Public domain W3C validator