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

Theorem sumeq1 13596
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 3510 . . . . . 6  |-  ( A  =  B  ->  ( A  C_  ( ZZ>= `  m
)  <->  B  C_  ( ZZ>= `  m ) ) )
2 simpl 455 . . . . . . . . . . 11  |-  ( ( A  =  B  /\  n  e.  ZZ )  ->  A  =  B )
32eleq2d 2524 . . . . . . . . . 10  |-  ( ( A  =  B  /\  n  e.  ZZ )  ->  ( n  e.  A  <->  n  e.  B ) )
43ifbid 3951 . . . . . . . . 9  |-  ( ( A  =  B  /\  n  e.  ZZ )  ->  if ( n  e.  A ,  [_ n  /  k ]_ C ,  0 )  =  if ( n  e.  B ,  [_ n  /  k ]_ C ,  0 ) )
54mpteq2dva 4525 . . . . . . . 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 12100 . . . . . . 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 4449 . . . . . 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 708 . . . . 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 2965 . . . 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 5791 . . . . . . 7  |-  ( A  =  B  ->  (
f : ( 1 ... m ) -1-1-onto-> A  <->  f :
( 1 ... m
)
-1-1-onto-> B ) )
1110anbi1d 702 . . . . . 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 1719 . . . . 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 2965 . . . 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 707 . . 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 5555 . 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 13594 . 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 13594 . 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 366    /\ wa 367    = wceq 1398   E.wex 1617    e. wcel 1823   E.wrex 2805   [_csb 3420    C_ wss 3461   ifcif 3929   class class class wbr 4439    |-> cmpt 4497   iotacio 5532   -1-1-onto->wf1o 5569   ` cfv 5570  (class class class)co 6270   0cc0 9481   1c1 9482    + caddc 9484   NNcn 10531   ZZcz 10860   ZZ>=cuz 11082   ...cfz 11675    seqcseq 12092    ~~> cli 13392   sum_csu 13593
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-mpt 4499  df-cnv 4996  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-ov 6273  df-oprab 6274  df-mpt2 6275  df-recs 7034  df-rdg 7068  df-seq 12093  df-sum 13594
This theorem is referenced by:  sumeq1i  13605  sumeq1d  13608  sumz  13629  fsumadd  13646  fsum2d  13671  fsumrev2  13682  fsummulc2  13684  fsumconst  13690  modfsummods  13692  modfsummod  13693  fsumabs  13700  fsumrelem  13706  fsumrlim  13710  fsumo1  13711  fsumiun  13720  bitsinv2  14180  bitsf1ocnv  14181  bitsinv  14185  prmreclem5  14525  gsumfsum  18682  fsumcn  21543  ovolfiniun  22081  volfiniun  22126  itgfsum  22402  dvmptfsum  22545  pntrsumbnd2  23953  esumpcvgval  28310  esumcvg  28318  rrnval  30566  mccl  31848  dvmptfprod  31984  dvnprodlem1  31985  dvnprodlem2  31986  dvnprodlem3  31987  dvnprod  31988
  Copyright terms: Public domain W3C validator