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

Theorem sumeq1 13803
Description: Equality theorem for a sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)
Assertion
Ref Expression
sumeq1  |-  ( A  =  B  ->  sum_ k  e.  A  C  =  sum_ k  e.  B  C
)

Proof of Theorem sumeq1
Dummy variables  f  m  n  x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sseq1 3464 . . . . . 6  |-  ( A  =  B  ->  ( A  C_  ( ZZ>= `  m
)  <->  B  C_  ( ZZ>= `  m ) ) )
2 simpl 463 . . . . . . . . . . 11  |-  ( ( A  =  B  /\  n  e.  ZZ )  ->  A  =  B )
32eleq2d 2524 . . . . . . . . . 10  |-  ( ( A  =  B  /\  n  e.  ZZ )  ->  ( n  e.  A  <->  n  e.  B ) )
43ifbid 3914 . . . . . . . . 9  |-  ( ( A  =  B  /\  n  e.  ZZ )  ->  if ( n  e.  A ,  [_ n  /  k ]_ C ,  0 )  =  if ( n  e.  B ,  [_ n  /  k ]_ C ,  0 ) )
54mpteq2dva 4502 . . . . . . . 8  |-  ( A  =  B  ->  (
n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ C ,  0 ) )  =  ( n  e.  ZZ  |->  if ( n  e.  B ,  [_ n  /  k ]_ C ,  0 ) ) )
65seqeq3d 12252 . . . . . . 7  |-  ( A  =  B  ->  seq m (  +  , 
( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ C ,  0 ) ) )  =  seq m (  +  , 
( n  e.  ZZ  |->  if ( n  e.  B ,  [_ n  /  k ]_ C ,  0 ) ) ) )
76breq1d 4425 . . . . . 6  |-  ( A  =  B  ->  (  seq m (  +  , 
( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ C ,  0 ) ) )  ~~>  x  <->  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  B ,  [_ n  /  k ]_ C ,  0 ) ) )  ~~>  x ) )
81, 7anbi12d 722 . . . . 5  |-  ( A  =  B  ->  (
( A  C_  ( ZZ>=
`  m )  /\  seq m (  +  , 
( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ C ,  0 ) ) )  ~~>  x )  <-> 
( B  C_  ( ZZ>=
`  m )  /\  seq m (  +  , 
( n  e.  ZZ  |->  if ( n  e.  B ,  [_ n  /  k ]_ C ,  0 ) ) )  ~~>  x ) ) )
98rexbidv 2912 . . . 4  |-  ( A  =  B  ->  ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m )  /\  seq m (  +  , 
( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ C ,  0 ) ) )  ~~>  x )  <->  E. m  e.  ZZ  ( B  C_  ( ZZ>= `  m )  /\  seq m (  +  , 
( n  e.  ZZ  |->  if ( n  e.  B ,  [_ n  /  k ]_ C ,  0 ) ) )  ~~>  x ) ) )
10 f1oeq3 5829 . . . . . . 7  |-  ( A  =  B  ->  (
f : ( 1 ... m ) -1-1-onto-> A  <->  f :
( 1 ... m
)
-1-1-onto-> B ) )
1110anbi1d 716 . . . . . 6  |-  ( A  =  B  ->  (
( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  [_ ( f `  n )  /  k ]_ C ) ) `  m ) )  <->  ( f : ( 1 ... m ) -1-1-onto-> B  /\  x  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  [_ (
f `  n )  /  k ]_ C
) ) `  m
) ) ) )
1211exbidv 1778 . . . . 5  |-  ( A  =  B  ->  ( E. f ( f : ( 1 ... m
)
-1-1-onto-> A  /\  x  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  [_ ( f `  n )  /  k ]_ C ) ) `  m ) )  <->  E. f
( f : ( 1 ... m ) -1-1-onto-> B  /\  x  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  [_ ( f `  n )  /  k ]_ C ) ) `  m ) ) ) )
1312rexbidv 2912 . . . 4  |-  ( A  =  B  ->  ( E. m  e.  NN  E. f ( f : ( 1 ... m
)
-1-1-onto-> A  /\  x  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  [_ ( f `  n )  /  k ]_ C ) ) `  m ) )  <->  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> B  /\  x  =  (  seq 1 (  +  , 
( n  e.  NN  |->  [_ ( f `  n
)  /  k ]_ C ) ) `  m ) ) ) )
149, 13orbi12d 721 . . 3  |-  ( A  =  B  ->  (
( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m )  /\  seq m (  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ C ,  0 ) ) )  ~~>  x )  \/ 
E. m  e.  NN  E. f ( f : ( 1 ... m
)
-1-1-onto-> A  /\  x  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  [_ ( f `  n )  /  k ]_ C ) ) `  m ) ) )  <-> 
( E. m  e.  ZZ  ( B  C_  ( ZZ>= `  m )  /\  seq m (  +  ,  ( n  e.  ZZ  |->  if ( n  e.  B ,  [_ n  /  k ]_ C ,  0 ) ) )  ~~>  x )  \/ 
E. m  e.  NN  E. f ( f : ( 1 ... m
)
-1-1-onto-> B  /\  x  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  [_ ( f `  n )  /  k ]_ C ) ) `  m ) ) ) ) )
1514iotabidv 5585 . 2  |-  ( A  =  B  ->  ( iota x ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m )  /\  seq m (  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ C ,  0 ) ) )  ~~>  x )  \/ 
E. m  e.  NN  E. f ( f : ( 1 ... m
)
-1-1-onto-> A  /\  x  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  [_ ( f `  n )  /  k ]_ C ) ) `  m ) ) ) )  =  ( iota
x ( E. m  e.  ZZ  ( B  C_  ( ZZ>= `  m )  /\  seq m (  +  ,  ( n  e.  ZZ  |->  if ( n  e.  B ,  [_ n  /  k ]_ C ,  0 ) ) )  ~~>  x )  \/ 
E. m  e.  NN  E. f ( f : ( 1 ... m
)
-1-1-onto-> B  /\  x  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  [_ ( f `  n )  /  k ]_ C ) ) `  m ) ) ) ) )
16 df-sum 13801 . 2  |-  sum_ k  e.  A  C  =  ( iota x ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m
)  /\  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ C ,  0 ) ) )  ~~>  x )  \/  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  , 
( n  e.  NN  |->  [_ ( f `  n
)  /  k ]_ C ) ) `  m ) ) ) )
17 df-sum 13801 . 2  |-  sum_ k  e.  B  C  =  ( iota x ( E. m  e.  ZZ  ( B  C_  ( ZZ>= `  m
)  /\  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  B ,  [_ n  /  k ]_ C ,  0 ) ) )  ~~>  x )  \/  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> B  /\  x  =  (  seq 1 (  +  , 
( n  e.  NN  |->  [_ ( f `  n
)  /  k ]_ C ) ) `  m ) ) ) )
1815, 16, 173eqtr4g 2520 1  |-  ( A  =  B  ->  sum_ k  e.  A  C  =  sum_ k  e.  B  C
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ wo 374    /\ wa 375    = wceq 1454   E.wex 1673    e. wcel 1897   E.wrex 2749   [_csb 3374    C_ wss 3415   ifcif 3892   class class class wbr 4415    |-> cmpt 4474   iotacio 5562   -1-1-onto->wf1o 5599   ` cfv 5600  (class class class)co 6314   0cc0 9564   1c1 9565    + caddc 9567   NNcn 10636   ZZcz 10965   ZZ>=cuz 11187   ...cfz 11812    seqcseq 12244    ~~> cli 13596   sum_csu 13800
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ral 2753  df-rex 2754  df-rab 2757  df-v 3058  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-sn 3980  df-pr 3982  df-op 3986  df-uni 4212  df-br 4416  df-opab 4475  df-mpt 4476  df-xp 4858  df-cnv 4860  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-pred 5398  df-iota 5564  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608  df-ov 6317  df-oprab 6318  df-mpt2 6319  df-wrecs 7053  df-recs 7115  df-rdg 7153  df-seq 12245  df-sum 13801
This theorem is referenced by:  sumeq1i  13812  sumeq1d  13815  sumz  13836  fsumadd  13853  fsum2d  13880  fsumrev2  13891  fsummulc2  13893  fsumconst  13899  modfsummods  13901  modfsummod  13902  fsumabs  13909  fsumrelem  13915  fsumrlim  13919  fsumo1  13920  fsumiun  13929  bitsinv2  14465  bitsf1ocnv  14466  bitsinv  14470  prmreclem5  14912  gsumfsum  19082  fsumcn  21950  ovolfiniun  22502  volfiniun  22548  itgfsum  22832  dvmptfsum  22975  pntrsumbnd2  24453  esumpcvgval  28947  esumcvg  28955  rrnval  32203  mccl  37715  dvmptfprod  37857  dvnprodlem1  37858  dvnprodlem2  37859  dvnprodlem3  37860  dvnprod  37861  sge0rnn0  38247  sge00  38255  fsumlesge0  38256  sge0sn  38258  sge0cl  38260  sge0f1o  38261  sge0resplit  38285  sge0xaddlem1  38312  sge0xaddlem2  38313
  Copyright terms: Public domain W3C validator