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

Theorem cbvsum 15638
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 𝑗𝐴
cbvsum.4 𝑘𝐵
cbvsum.5 𝑗𝐶
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.4 . . . . . . . . . . . . 13 𝑘𝐵
2 cbvsum.5 . . . . . . . . . . . . 13 𝑗𝐶
3 cbvsum.1 . . . . . . . . . . . . 13 (𝑗 = 𝑘𝐵 = 𝐶)
41, 2, 3cbvcsbw 3903 . . . . . . . . . . . 12 𝑛 / 𝑗𝐵 = 𝑛 / 𝑘𝐶
54a1i 11 . . . . . . . . . . 11 (⊤ → 𝑛 / 𝑗𝐵 = 𝑛 / 𝑘𝐶)
65ifeq1d 4547 . . . . . . . . . 10 (⊤ → if(𝑛𝐴, 𝑛 / 𝑗𝐵, 0) = if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))
76mpteq2dv 5250 . . . . . . . . 9 (⊤ → (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑗𝐵, 0)) = (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0)))
87seqeq3d 13971 . . . . . . . 8 (⊤ → seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑗𝐵, 0))) = seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))))
98mptru 1549 . . . . . . 7 seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑗𝐵, 0))) = seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0)))
109breq1i 5155 . . . . . 6 (seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑗𝐵, 0))) ⇝ 𝑥 ↔ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥)
1110anbi2i 624 . . . . 5 ((𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑗𝐵, 0))) ⇝ 𝑥) ↔ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥))
1211rexbii 3095 . . . 4 (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑗𝐵, 0))) ⇝ 𝑥) ↔ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥))
131, 2, 3cbvcsbw 3903 . . . . . . . . . . . . 13 (𝑓𝑛) / 𝑗𝐵 = (𝑓𝑛) / 𝑘𝐶
1413a1i 11 . . . . . . . . . . . 12 (⊤ → (𝑓𝑛) / 𝑗𝐵 = (𝑓𝑛) / 𝑘𝐶)
1514mpteq2dv 5250 . . . . . . . . . . 11 (⊤ → (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑗𝐵) = (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))
1615seqeq3d 13971 . . . . . . . . . 10 (⊤ → seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑗𝐵)) = seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶)))
1716mptru 1549 . . . . . . . . 9 seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑗𝐵)) = seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))
1817fveq1i 6890 . . . . . . . 8 (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑗𝐵))‘𝑚) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚)
1918eqeq2i 2746 . . . . . . 7 (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑗𝐵))‘𝑚) ↔ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚))
2019anbi2i 624 . . . . . 6 ((𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑗𝐵))‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚)))
2120exbii 1851 . . . . 5 (∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑗𝐵))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚)))
2221rexbii 3095 . . . 4 (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑗𝐵))‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚)))
2312, 22orbi12i 914 . . 3 ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑗𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑗𝐵))‘𝑚))) ↔ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚))))
2423iotabii 6526 . 2 (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑗𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑗𝐵))‘𝑚)))) = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚))))
25 df-sum 15630 . 2 Σ𝑗𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑗𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑗𝐵))‘𝑚))))
26 df-sum 15630 . 2 Σ𝑘𝐴 𝐶 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚))))
2724, 25, 263eqtr4i 2771 1 Σ𝑗𝐴 𝐵 = Σ𝑘𝐴 𝐶
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wo 846   = wceq 1542  wtru 1543  wex 1782  wcel 2107  wnfc 2884  wrex 3071  csb 3893  wss 3948  ifcif 4528   class class class wbr 5148  cmpt 5231  cio 6491  1-1-ontowf1o 6540  cfv 6541  (class class class)co 7406  0cc0 11107  1c1 11108   + caddc 11110  cn 12209  cz 12555  cuz 12819  ...cfz 13481  seqcseq 13963  cli 15425  Σcsu 15629
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-11 2155  ax-12 2172  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-xp 5682  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-iota 6493  df-fv 6549  df-ov 7409  df-oprab 7410  df-mpo 7411  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-seq 13964  df-sum 15630
This theorem is referenced by:  cbvsumv  15639  cbvsumi  15640  fsumclf  15681  fsumiunle  32023  esumpfinvalf  33063  sticksstones8  40958  sticksstones10  40960  sticksstones12a  40962  sticksstones12  40963  fsummulc1f  44274  fsumf1of  44277  fsumiunss  44278  fsumreclf  44279  fsumlessf  44280  fsumsermpt  44282  dvnmul  44646  sge0revalmpt  45081  sge0fsummpt  45093  sge0iunmptlemfi  45116  sge0iunmptlemre  45118  sge0ltfirpmpt2  45129  sge0isummpt2  45135  sge0xaddlem2  45137  sge0fsummptf  45139
  Copyright terms: Public domain W3C validator