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

Theorem sumeq1 15041
 Description: Equality theorem for a sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)
Assertion
Ref Expression
sumeq1 (𝐴 = 𝐵 → Σ𝑘𝐴 𝐶 = Σ𝑘𝐵 𝐶)

Proof of Theorem sumeq1
Dummy variables 𝑓 𝑚 𝑛 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sseq1 3943 . . . . . 6 (𝐴 = 𝐵 → (𝐴 ⊆ (ℤ𝑚) ↔ 𝐵 ⊆ (ℤ𝑚)))
2 simpl 486 . . . . . . . . . . 11 ((𝐴 = 𝐵𝑛 ∈ ℤ) → 𝐴 = 𝐵)
32eleq2d 2878 . . . . . . . . . 10 ((𝐴 = 𝐵𝑛 ∈ ℤ) → (𝑛𝐴𝑛𝐵))
43ifbid 4450 . . . . . . . . 9 ((𝐴 = 𝐵𝑛 ∈ ℤ) → if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0) = if(𝑛𝐵, 𝑛 / 𝑘𝐶, 0))
54mpteq2dva 5128 . . . . . . . 8 (𝐴 = 𝐵 → (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0)) = (𝑛 ∈ ℤ ↦ if(𝑛𝐵, 𝑛 / 𝑘𝐶, 0)))
65seqeq3d 13376 . . . . . . 7 (𝐴 = 𝐵 → seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) = seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐵, 𝑛 / 𝑘𝐶, 0))))
76breq1d 5043 . . . . . 6 (𝐴 = 𝐵 → (seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥 ↔ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐵, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥))
81, 7anbi12d 633 . . . . 5 (𝐴 = 𝐵 → ((𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥) ↔ (𝐵 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐵, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥)))
98rexbidv 3259 . . . 4 (𝐴 = 𝐵 → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥) ↔ ∃𝑚 ∈ ℤ (𝐵 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐵, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥)))
10 f1oeq3 6585 . . . . . . 7 (𝐴 = 𝐵 → (𝑓:(1...𝑚)–1-1-onto𝐴𝑓:(1...𝑚)–1-1-onto𝐵))
1110anbi1d 632 . . . . . 6 (𝐴 = 𝐵 → ((𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto𝐵𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚))))
1211exbidv 1922 . . . . 5 (𝐴 = 𝐵 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐵𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚))))
1312rexbidv 3259 . . . 4 (𝐴 = 𝐵 → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐵𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚))))
149, 13orbi12d 916 . . 3 (𝐴 = 𝐵 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚))) ↔ (∃𝑚 ∈ ℤ (𝐵 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐵, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐵𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚)))))
1514iotabidv 6312 . 2 (𝐴 = 𝐵 → (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚)))) = (℩𝑥(∃𝑚 ∈ ℤ (𝐵 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐵, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐵𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚)))))
16 df-sum 15039 . 2 Σ𝑘𝐴 𝐶 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚))))
17 df-sum 15039 . 2 Σ𝑘𝐵 𝐶 = (℩𝑥(∃𝑚 ∈ ℤ (𝐵 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐵, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐵𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚))))
1815, 16, 173eqtr4g 2861 1 (𝐴 = 𝐵 → Σ𝑘𝐴 𝐶 = Σ𝑘𝐵 𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∨ wo 844   = wceq 1538  ∃wex 1781   ∈ wcel 2112  ∃wrex 3110  ⦋csb 3831   ⊆ wss 3884  ifcif 4428   class class class wbr 5033   ↦ cmpt 5113  ℩cio 6285  –1-1-onto→wf1o 6327  ‘cfv 6328  (class class class)co 7139  0cc0 10530  1c1 10531   + caddc 10533  ℕcn 11629  ℤcz 11973  ℤ≥cuz 12235  ...cfz 12889  seqcseq 13368   ⇝ cli 14837  Σcsu 15038 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 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ral 3114  df-rex 3115  df-rab 3118  df-v 3446  df-un 3889  df-in 3891  df-ss 3901  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-opab 5096  df-mpt 5114  df-xp 5529  df-cnv 5531  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-iota 6287  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-ov 7142  df-oprab 7143  df-mpo 7144  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-seq 13369  df-sum 15039 This theorem is referenced by:  sumeq1i  15051  sumeq1d  15054  sumz  15075  fsumadd  15092  fsum2d  15122  fsumrev2  15133  fsummulc2  15135  fsumconst  15141  modfsummods  15144  modfsummod  15145  fsumabs  15152  fsumrelem  15158  fsumrlim  15162  fsumo1  15163  fsumiun  15172  sumeven  15732  sumodd  15733  bitsinv2  15786  bitsf1ocnv  15787  bitsinv  15791  prmreclem5  16250  gsumfsum  20162  fsumcn  23479  ovolfiniun  24109  volfiniun  24155  itgfsum  24434  dvmptfsum  24582  pntrsumbnd2  26155  finsumvtxdg2size  27344  esumpcvgval  31451  esumcvg  31459  rrnval  35264  mccl  42237  dvmptfprod  42584  dvnprodlem1  42585  dvnprodlem2  42586  dvnprodlem3  42587  dvnprod  42588  sge0rnn0  43004  sge00  43012  fsumlesge0  43013  sge0sn  43015  sge0cl  43017  sge0f1o  43018  sge0resplit  43042  sge0xaddlem1  43069  sge0xaddlem2  43070  sge0reuz  43083
 Copyright terms: Public domain W3C validator