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

Theorem sumeq1 15668
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 4005 . . . . . 6 (𝐴 = 𝐵 → (𝐴 ⊆ (ℤ𝑚) ↔ 𝐵 ⊆ (ℤ𝑚)))
2 simpl 482 . . . . . . . . . . 11 ((𝐴 = 𝐵𝑛 ∈ ℤ) → 𝐴 = 𝐵)
32eleq2d 2815 . . . . . . . . . 10 ((𝐴 = 𝐵𝑛 ∈ ℤ) → (𝑛𝐴𝑛𝐵))
43ifbid 4552 . . . . . . . . 9 ((𝐴 = 𝐵𝑛 ∈ ℤ) → if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0) = if(𝑛𝐵, 𝑛 / 𝑘𝐶, 0))
54mpteq2dva 5248 . . . . . . . 8 (𝐴 = 𝐵 → (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0)) = (𝑛 ∈ ℤ ↦ if(𝑛𝐵, 𝑛 / 𝑘𝐶, 0)))
65seqeq3d 14007 . . . . . . 7 (𝐴 = 𝐵 → seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) = seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐵, 𝑛 / 𝑘𝐶, 0))))
76breq1d 5158 . . . . . 6 (𝐴 = 𝐵 → (seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥 ↔ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐵, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥))
81, 7anbi12d 631 . . . . 5 (𝐴 = 𝐵 → ((𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥) ↔ (𝐵 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐵, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥)))
98rexbidv 3175 . . . 4 (𝐴 = 𝐵 → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥) ↔ ∃𝑚 ∈ ℤ (𝐵 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐵, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥)))
10 f1oeq3 6829 . . . . . . 7 (𝐴 = 𝐵 → (𝑓:(1...𝑚)–1-1-onto𝐴𝑓:(1...𝑚)–1-1-onto𝐵))
1110anbi1d 630 . . . . . 6 (𝐴 = 𝐵 → ((𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto𝐵𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚))))
1211exbidv 1917 . . . . 5 (𝐴 = 𝐵 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐵𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚))))
1312rexbidv 3175 . . . 4 (𝐴 = 𝐵 → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐵𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚))))
149, 13orbi12d 917 . . 3 (𝐴 = 𝐵 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚))) ↔ (∃𝑚 ∈ ℤ (𝐵 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐵, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐵𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚)))))
1514iotabidv 6532 . 2 (𝐴 = 𝐵 → (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚)))) = (℩𝑥(∃𝑚 ∈ ℤ (𝐵 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐵, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐵𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚)))))
16 df-sum 15666 . 2 Σ𝑘𝐴 𝐶 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚))))
17 df-sum 15666 . 2 Σ𝑘𝐵 𝐶 = (℩𝑥(∃𝑚 ∈ ℤ (𝐵 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐵, 𝑛 / 𝑘𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐵𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐶))‘𝑚))))
1815, 16, 173eqtr4g 2793 1 (𝐴 = 𝐵 → Σ𝑘𝐴 𝐶 = Σ𝑘𝐵 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wo 846   = wceq 1534  wex 1774  wcel 2099  wrex 3067  csb 3892  wss 3947  ifcif 4529   class class class wbr 5148  cmpt 5231  cio 6498  1-1-ontowf1o 6547  cfv 6548  (class class class)co 7420  0cc0 11139  1c1 11140   + caddc 11142  cn 12243  cz 12589  cuz 12853  ...cfz 13517  seqcseq 13999  cli 15461  Σcsu 15665
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-ral 3059  df-rex 3068  df-rab 3430  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-xp 5684  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6305  df-iota 6500  df-f 6552  df-f1 6553  df-fo 6554  df-f1o 6555  df-fv 6556  df-ov 7423  df-oprab 7424  df-mpo 7425  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-seq 14000  df-sum 15666
This theorem is referenced by:  sumeq1i  15677  sumeq1d  15680  sumz  15701  fsumadd  15719  fsum2d  15750  fsumrev2  15761  fsummulc2  15763  fsumconst  15769  modfsummods  15772  modfsummod  15773  fsumabs  15780  fsumrelem  15786  fsumrlim  15790  fsumo1  15791  fsumiun  15800  sumeven  16364  sumodd  16365  bitsinv2  16418  bitsf1ocnv  16419  bitsinv  16423  prmreclem5  16889  gsumfsum  21367  fsumcn  24801  ovolfiniun  25443  volfiniun  25489  itgfsum  25769  dvmptfsum  25920  pntrsumbnd2  27513  finsumvtxdg2size  29377  esumpcvgval  33697  esumcvg  33705  rrnval  37300  deg1gprod  41612  mccl  44986  dvmptfprod  45333  dvnprodlem1  45334  dvnprodlem2  45335  dvnprodlem3  45336  dvnprod  45337  sge0rnn0  45756  sge00  45764  fsumlesge0  45765  sge0sn  45767  sge0cl  45769  sge0f1o  45770  sge0resplit  45794  sge0xaddlem1  45821  sge0xaddlem2  45822  sge0reuz  45835
  Copyright terms: Public domain W3C validator