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

Theorem sumeq1 15725
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 4009 . . . . . 6 (𝐴 = 𝐵 → (𝐴 ⊆ (ℤ𝑚) ↔ 𝐵 ⊆ (ℤ𝑚)))
2 simpl 482 . . . . . . . . . . 11 ((𝐴 = 𝐵𝑛 ∈ ℤ) → 𝐴 = 𝐵)
32eleq2d 2827 . . . . . . . . . 10 ((𝐴 = 𝐵𝑛 ∈ ℤ) → (𝑛𝐴𝑛𝐵))
43ifbid 4549 . . . . . . . . 9 ((𝐴 = 𝐵𝑛 ∈ ℤ) → if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0) = if(𝑛𝐵, 𝑛 / 𝑘𝐶, 0))
54mpteq2dva 5242 . . . . . . . 8 (𝐴 = 𝐵 → (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0)) = (𝑛 ∈ ℤ ↦ if(𝑛𝐵, 𝑛 / 𝑘𝐶, 0)))
65seqeq3d 14050 . . . . . . 7 (𝐴 = 𝐵 → seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) = seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐵, 𝑛 / 𝑘𝐶, 0))))
76breq1d 5153 . . . . . 6 (𝐴 = 𝐵 → (seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥 ↔ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐵, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥))
81, 7anbi12d 632 . . . . 5 (𝐴 = 𝐵 → ((𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥) ↔ (𝐵 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐵, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥)))
98rexbidv 3179 . . . 4 (𝐴 = 𝐵 → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥) ↔ ∃𝑚 ∈ ℤ (𝐵 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐵, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥)))
10 f1oeq3 6838 . . . . . . 7 (𝐴 = 𝐵 → (𝑓:(1...𝑚)–1-1-onto𝐴𝑓:(1...𝑚)–1-1-onto𝐵))
1110anbi1d 631 . . . . . 6 (𝐴 = 𝐵 → ((𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto𝐵𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚))))
1211exbidv 1921 . . . . 5 (𝐴 = 𝐵 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐵𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚))))
1312rexbidv 3179 . . . 4 (𝐴 = 𝐵 → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐵𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚))))
149, 13orbi12d 919 . . 3 (𝐴 = 𝐵 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚))) ↔ (∃𝑚 ∈ ℤ (𝐵 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐵, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐵𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚)))))
1514iotabidv 6545 . 2 (𝐴 = 𝐵 → (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚)))) = (℩𝑥(∃𝑚 ∈ ℤ (𝐵 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐵, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐵𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚)))))
16 df-sum 15723 . 2 Σ𝑘𝐴 𝐶 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚))))
17 df-sum 15723 . 2 Σ𝑘𝐵 𝐶 = (℩𝑥(∃𝑚 ∈ ℤ (𝐵 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐵, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐵𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚))))
1815, 16, 173eqtr4g 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-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-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  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:  sumeq1i  15733  sumeq1d  15736  sumz  15758  fsumadd  15776  fsum2d  15807  fsumrev2  15818  fsummulc2  15820  fsumconst  15826  modfsummods  15829  modfsummod  15830  fsumabs  15837  fsumrelem  15843  fsumrlim  15847  fsumo1  15848  fsumiun  15857  sumeven  16424  sumodd  16425  bitsinv2  16480  bitsf1ocnv  16481  bitsinv  16485  prmreclem5  16958  gsumfsum  21452  fsumcn  24894  ovolfiniun  25536  volfiniun  25582  itgfsum  25862  dvmptfsum  26013  pntrsumbnd2  27611  finsumvtxdg2size  29568  esumpcvgval  34079  esumcvg  34087  rrnval  37834  deg1gprod  42141  mccl  45613  dvmptfprod  45960  dvnprodlem1  45961  dvnprodlem2  45962  dvnprodlem3  45963  dvnprod  45964  sge0rnn0  46383  sge00  46391  fsumlesge0  46392  sge0sn  46394  sge0cl  46396  sge0f1o  46397  sge0resplit  46421  sge0xaddlem1  46448  sge0xaddlem2  46449  sge0reuz  46462
  Copyright terms: Public domain W3C validator