ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sumsnf Unicode version

Theorem sumsnf 10790
Description: A sum of a singleton is the term. A version of sumsn 10792 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
Hypotheses
Ref Expression
sumsnf.1  |-  F/_ k B
sumsnf.2  |-  ( k  =  M  ->  A  =  B )
Assertion
Ref Expression
sumsnf  |-  ( ( M  e.  V  /\  B  e.  CC )  -> 
sum_ k  e.  { M } A  =  B )
Distinct variable groups:    k, M    k, V
Allowed substitution hints:    A( k)    B( k)

Proof of Theorem sumsnf
Dummy variables  m  n  u  v are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfcv 2228 . . . . 5  |-  F/_ m A
2 nfcsb1v 2963 . . . . 5  |-  F/_ k [_ m  /  k ]_ A
3 csbeq1a 2941 . . . . 5  |-  ( k  =  m  ->  A  =  [_ m  /  k ]_ A )
41, 2, 3cbvsumi 10738 . . . 4  |-  sum_ k  e.  { M } A  =  sum_ m  e.  { M } [_ m  / 
k ]_ A
5 csbeq1 2936 . . . . 5  |-  ( m  =  ( { <. 1 ,  M >. } `
 n )  ->  [_ m  /  k ]_ A  =  [_ ( { <. 1 ,  M >. } `  n )  /  k ]_ A
)
6 1nn 8423 . . . . . 6  |-  1  e.  NN
76a1i 9 . . . . 5  |-  ( ( M  e.  V  /\  B  e.  CC )  ->  1  e.  NN )
8 simpl 107 . . . . . . 7  |-  ( ( M  e.  V  /\  B  e.  CC )  ->  M  e.  V )
9 f1osng 5288 . . . . . . 7  |-  ( ( 1  e.  NN  /\  M  e.  V )  ->  { <. 1 ,  M >. } : { 1 } -1-1-onto-> { M } )
106, 8, 9sylancr 405 . . . . . 6  |-  ( ( M  e.  V  /\  B  e.  CC )  ->  { <. 1 ,  M >. } : { 1 } -1-1-onto-> { M } )
11 1z 8766 . . . . . . 7  |-  1  e.  ZZ
12 fzsn 9469 . . . . . . 7  |-  ( 1  e.  ZZ  ->  (
1 ... 1 )  =  { 1 } )
13 f1oeq2 5239 . . . . . . 7  |-  ( ( 1 ... 1 )  =  { 1 }  ->  ( { <. 1 ,  M >. } : ( 1 ... 1 ) -1-1-onto-> { M }  <->  { <. 1 ,  M >. } : {
1 } -1-1-onto-> { M } ) )
1411, 12, 13mp2b 8 . . . . . 6  |-  ( {
<. 1 ,  M >. } : ( 1 ... 1 ) -1-1-onto-> { M } 
<->  { <. 1 ,  M >. } : { 1 } -1-1-onto-> { M } )
1510, 14sylibr 132 . . . . 5  |-  ( ( M  e.  V  /\  B  e.  CC )  ->  { <. 1 ,  M >. } : ( 1 ... 1 ) -1-1-onto-> { M } )
16 elsni 3462 . . . . . . . 8  |-  ( m  e.  { M }  ->  m  =  M )
1716adantl 271 . . . . . . 7  |-  ( ( ( M  e.  V  /\  B  e.  CC )  /\  m  e.  { M } )  ->  m  =  M )
1817csbeq1d 2939 . . . . . 6  |-  ( ( ( M  e.  V  /\  B  e.  CC )  /\  m  e.  { M } )  ->  [_ m  /  k ]_ A  =  [_ M  /  k ]_ A )
19 sumsnf.1 . . . . . . . . . 10  |-  F/_ k B
2019a1i 9 . . . . . . . . 9  |-  ( M  e.  V  ->  F/_ k B )
21 sumsnf.2 . . . . . . . . 9  |-  ( k  =  M  ->  A  =  B )
2220, 21csbiegf 2971 . . . . . . . 8  |-  ( M  e.  V  ->  [_ M  /  k ]_ A  =  B )
2322ad2antrr 472 . . . . . . 7  |-  ( ( ( M  e.  V  /\  B  e.  CC )  /\  m  e.  { M } )  ->  [_ M  /  k ]_ A  =  B )
24 simplr 497 . . . . . . 7  |-  ( ( ( M  e.  V  /\  B  e.  CC )  /\  m  e.  { M } )  ->  B  e.  CC )
2523, 24eqeltrd 2164 . . . . . 6  |-  ( ( ( M  e.  V  /\  B  e.  CC )  /\  m  e.  { M } )  ->  [_ M  /  k ]_ A  e.  CC )
2618, 25eqeltrd 2164 . . . . 5  |-  ( ( ( M  e.  V  /\  B  e.  CC )  /\  m  e.  { M } )  ->  [_ m  /  k ]_ A  e.  CC )
2722ad2antrr 472 . . . . . 6  |-  ( ( ( M  e.  V  /\  B  e.  CC )  /\  n  e.  ( 1 ... 1 ) )  ->  [_ M  / 
k ]_ A  =  B )
28 elfz1eq 9439 . . . . . . . . 9  |-  ( n  e.  ( 1 ... 1 )  ->  n  =  1 )
2928fveq2d 5303 . . . . . . . 8  |-  ( n  e.  ( 1 ... 1 )  ->  ( { <. 1 ,  M >. } `  n )  =  ( { <. 1 ,  M >. } `
 1 ) )
30 fvsng 5487 . . . . . . . . 9  |-  ( ( 1  e.  NN  /\  M  e.  V )  ->  ( { <. 1 ,  M >. } `  1
)  =  M )
316, 8, 30sylancr 405 . . . . . . . 8  |-  ( ( M  e.  V  /\  B  e.  CC )  ->  ( { <. 1 ,  M >. } `  1
)  =  M )
3229, 31sylan9eqr 2142 . . . . . . 7  |-  ( ( ( M  e.  V  /\  B  e.  CC )  /\  n  e.  ( 1 ... 1 ) )  ->  ( { <. 1 ,  M >. } `
 n )  =  M )
3332csbeq1d 2939 . . . . . 6  |-  ( ( ( M  e.  V  /\  B  e.  CC )  /\  n  e.  ( 1 ... 1 ) )  ->  [_ ( {
<. 1 ,  M >. } `  n )  /  k ]_ A  =  [_ M  /  k ]_ A )
3428fveq2d 5303 . . . . . . 7  |-  ( n  e.  ( 1 ... 1 )  ->  ( { <. 1 ,  B >. } `  n )  =  ( { <. 1 ,  B >. } `
 1 ) )
35 simpr 108 . . . . . . . 8  |-  ( ( M  e.  V  /\  B  e.  CC )  ->  B  e.  CC )
36 fvsng 5487 . . . . . . . 8  |-  ( ( 1  e.  NN  /\  B  e.  CC )  ->  ( { <. 1 ,  B >. } `  1
)  =  B )
376, 35, 36sylancr 405 . . . . . . 7  |-  ( ( M  e.  V  /\  B  e.  CC )  ->  ( { <. 1 ,  B >. } `  1
)  =  B )
3834, 37sylan9eqr 2142 . . . . . 6  |-  ( ( ( M  e.  V  /\  B  e.  CC )  /\  n  e.  ( 1 ... 1 ) )  ->  ( { <. 1 ,  B >. } `
 n )  =  B )
3927, 33, 383eqtr4rd 2131 . . . . 5  |-  ( ( ( M  e.  V  /\  B  e.  CC )  /\  n  e.  ( 1 ... 1 ) )  ->  ( { <. 1 ,  B >. } `
 n )  = 
[_ ( { <. 1 ,  M >. } `
 n )  / 
k ]_ A )
405, 7, 15, 26, 39fisum 10765 . . . 4  |-  ( ( M  e.  V  /\  B  e.  CC )  -> 
sum_ m  e.  { M } [_ m  /  k ]_ A  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  1 ,  ( { <. 1 ,  B >. } `
 n ) ,  0 ) ) ,  CC ) `  1
) )
414, 40syl5eq 2132 . . 3  |-  ( ( M  e.  V  /\  B  e.  CC )  -> 
sum_ k  e.  { M } A  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  1 ,  ( { <. 1 ,  B >. } `  n ) ,  0 ) ) ,  CC ) ` 
1 ) )
42 1zzd 8767 . . . 4  |-  ( ( M  e.  V  /\  B  e.  CC )  ->  1  e.  ZZ )
43 elnnuz 9045 . . . . . . . 8  |-  ( u  e.  NN  <->  u  e.  ( ZZ>= `  1 )
)
4443biimpri 131 . . . . . . 7  |-  ( u  e.  ( ZZ>= `  1
)  ->  u  e.  NN )
4544adantl 271 . . . . . 6  |-  ( ( ( M  e.  V  /\  B  e.  CC )  /\  u  e.  (
ZZ>= `  1 ) )  ->  u  e.  NN )
46 simpr 108 . . . . . . . . . . 11  |-  ( ( ( ( M  e.  V  /\  B  e.  CC )  /\  u  e.  ( ZZ>= `  1 )
)  /\  u  <_  1 )  ->  u  <_  1 )
47 eluzle 9021 . . . . . . . . . . . 12  |-  ( u  e.  ( ZZ>= `  1
)  ->  1  <_  u )
4847ad2antlr 473 . . . . . . . . . . 11  |-  ( ( ( ( M  e.  V  /\  B  e.  CC )  /\  u  e.  ( ZZ>= `  1 )
)  /\  u  <_  1 )  ->  1  <_  u )
49 eluzelre 9019 . . . . . . . . . . . . 13  |-  ( u  e.  ( ZZ>= `  1
)  ->  u  e.  RR )
5049ad2antlr 473 . . . . . . . . . . . 12  |-  ( ( ( ( M  e.  V  /\  B  e.  CC )  /\  u  e.  ( ZZ>= `  1 )
)  /\  u  <_  1 )  ->  u  e.  RR )
51 1red 7493 . . . . . . . . . . . 12  |-  ( ( ( ( M  e.  V  /\  B  e.  CC )  /\  u  e.  ( ZZ>= `  1 )
)  /\  u  <_  1 )  ->  1  e.  RR )
5250, 51letri3d 7590 . . . . . . . . . . 11  |-  ( ( ( ( M  e.  V  /\  B  e.  CC )  /\  u  e.  ( ZZ>= `  1 )
)  /\  u  <_  1 )  ->  ( u  =  1  <->  ( u  <_  1  /\  1  <_  u ) ) )
5346, 48, 52mpbir2and 890 . . . . . . . . . 10  |-  ( ( ( ( M  e.  V  /\  B  e.  CC )  /\  u  e.  ( ZZ>= `  1 )
)  /\  u  <_  1 )  ->  u  = 
1 )
5453fveq2d 5303 . . . . . . . . 9  |-  ( ( ( ( M  e.  V  /\  B  e.  CC )  /\  u  e.  ( ZZ>= `  1 )
)  /\  u  <_  1 )  ->  ( { <. 1 ,  B >. } `
 u )  =  ( { <. 1 ,  B >. } `  1
) )
5537ad2antrr 472 . . . . . . . . 9  |-  ( ( ( ( M  e.  V  /\  B  e.  CC )  /\  u  e.  ( ZZ>= `  1 )
)  /\  u  <_  1 )  ->  ( { <. 1 ,  B >. } `
 1 )  =  B )
5654, 55eqtrd 2120 . . . . . . . 8  |-  ( ( ( ( M  e.  V  /\  B  e.  CC )  /\  u  e.  ( ZZ>= `  1 )
)  /\  u  <_  1 )  ->  ( { <. 1 ,  B >. } `
 u )  =  B )
5735ad2antrr 472 . . . . . . . 8  |-  ( ( ( ( M  e.  V  /\  B  e.  CC )  /\  u  e.  ( ZZ>= `  1 )
)  /\  u  <_  1 )  ->  B  e.  CC )
5856, 57eqeltrd 2164 . . . . . . 7  |-  ( ( ( ( M  e.  V  /\  B  e.  CC )  /\  u  e.  ( ZZ>= `  1 )
)  /\  u  <_  1 )  ->  ( { <. 1 ,  B >. } `
 u )  e.  CC )
59 0cnd 7471 . . . . . . 7  |-  ( ( ( ( M  e.  V  /\  B  e.  CC )  /\  u  e.  ( ZZ>= `  1 )
)  /\  -.  u  <_  1 )  ->  0  e.  CC )
6045nnzd 8857 . . . . . . . 8  |-  ( ( ( M  e.  V  /\  B  e.  CC )  /\  u  e.  (
ZZ>= `  1 ) )  ->  u  e.  ZZ )
61 1zzd 8767 . . . . . . . 8  |-  ( ( ( M  e.  V  /\  B  e.  CC )  /\  u  e.  (
ZZ>= `  1 ) )  ->  1  e.  ZZ )
62 zdcle 8813 . . . . . . . 8  |-  ( ( u  e.  ZZ  /\  1  e.  ZZ )  -> DECID  u  <_  1 )
6360, 61, 62syl2anc 403 . . . . . . 7  |-  ( ( ( M  e.  V  /\  B  e.  CC )  /\  u  e.  (
ZZ>= `  1 ) )  -> DECID 
u  <_  1 )
6458, 59, 63ifcldadc 3418 . . . . . 6  |-  ( ( ( M  e.  V  /\  B  e.  CC )  /\  u  e.  (
ZZ>= `  1 ) )  ->  if ( u  <_  1 ,  ( { <. 1 ,  B >. } `  u ) ,  0 )  e.  CC )
65 breq1 3846 . . . . . . . 8  |-  ( n  =  u  ->  (
n  <_  1  <->  u  <_  1 ) )
66 fveq2 5299 . . . . . . . 8  |-  ( n  =  u  ->  ( { <. 1 ,  B >. } `  n )  =  ( { <. 1 ,  B >. } `
 u ) )
6765, 66ifbieq1d 3411 . . . . . . 7  |-  ( n  =  u  ->  if ( n  <_  1 ,  ( { <. 1 ,  B >. } `  n
) ,  0 )  =  if ( u  <_  1 ,  ( { <. 1 ,  B >. } `  u ) ,  0 ) )
68 eqid 2088 . . . . . . 7  |-  ( n  e.  NN  |->  if ( n  <_  1 , 
( { <. 1 ,  B >. } `  n
) ,  0 ) )  =  ( n  e.  NN  |->  if ( n  <_  1 , 
( { <. 1 ,  B >. } `  n
) ,  0 ) )
6967, 68fvmptg 5374 . . . . . 6  |-  ( ( u  e.  NN  /\  if ( u  <_  1 ,  ( { <. 1 ,  B >. } `
 u ) ,  0 )  e.  CC )  ->  ( ( n  e.  NN  |->  if ( n  <_  1 , 
( { <. 1 ,  B >. } `  n
) ,  0 ) ) `  u )  =  if ( u  <_  1 ,  ( { <. 1 ,  B >. } `  u ) ,  0 ) )
7045, 64, 69syl2anc 403 . . . . 5  |-  ( ( ( M  e.  V  /\  B  e.  CC )  /\  u  e.  (
ZZ>= `  1 ) )  ->  ( ( n  e.  NN  |->  if ( n  <_  1 , 
( { <. 1 ,  B >. } `  n
) ,  0 ) ) `  u )  =  if ( u  <_  1 ,  ( { <. 1 ,  B >. } `  u ) ,  0 ) )
7170, 64eqeltrd 2164 . . . 4  |-  ( ( ( M  e.  V  /\  B  e.  CC )  /\  u  e.  (
ZZ>= `  1 ) )  ->  ( ( n  e.  NN  |->  if ( n  <_  1 , 
( { <. 1 ,  B >. } `  n
) ,  0 ) ) `  u )  e.  CC )
72 addcl 7457 . . . . 5  |-  ( ( u  e.  CC  /\  v  e.  CC )  ->  ( u  +  v )  e.  CC )
7372adantl 271 . . . 4  |-  ( ( ( M  e.  V  /\  B  e.  CC )  /\  ( u  e.  CC  /\  v  e.  CC ) )  -> 
( u  +  v )  e.  CC )
7442, 71, 73iseq1 9863 . . 3  |-  ( ( M  e.  V  /\  B  e.  CC )  ->  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  1 , 
( { <. 1 ,  B >. } `  n
) ,  0 ) ) ,  CC ) `
 1 )  =  ( ( n  e.  NN  |->  if ( n  <_  1 ,  ( { <. 1 ,  B >. } `  n ) ,  0 ) ) `
 1 ) )
7541, 74eqtrd 2120 . 2  |-  ( ( M  e.  V  /\  B  e.  CC )  -> 
sum_ k  e.  { M } A  =  ( ( n  e.  NN  |->  if ( n  <_  1 ,  ( { <. 1 ,  B >. } `
 n ) ,  0 ) ) ` 
1 ) )
76 1le1 8039 . . . . . 6  |-  1  <_  1
7776iftruei 3397 . . . . 5  |-  if ( 1  <_  1 , 
( { <. 1 ,  B >. } `  1
) ,  0 )  =  ( { <. 1 ,  B >. } `
 1 )
7877, 37syl5eq 2132 . . . 4  |-  ( ( M  e.  V  /\  B  e.  CC )  ->  if ( 1  <_ 
1 ,  ( {
<. 1 ,  B >. } `  1 ) ,  0 )  =  B )
7978, 35eqeltrd 2164 . . 3  |-  ( ( M  e.  V  /\  B  e.  CC )  ->  if ( 1  <_ 
1 ,  ( {
<. 1 ,  B >. } `  1 ) ,  0 )  e.  CC )
80 breq1 3846 . . . . 5  |-  ( n  =  1  ->  (
n  <_  1  <->  1  <_  1 ) )
81 fveq2 5299 . . . . 5  |-  ( n  =  1  ->  ( { <. 1 ,  B >. } `  n )  =  ( { <. 1 ,  B >. } `
 1 ) )
8280, 81ifbieq1d 3411 . . . 4  |-  ( n  =  1  ->  if ( n  <_  1 ,  ( { <. 1 ,  B >. } `  n
) ,  0 )  =  if ( 1  <_  1 ,  ( { <. 1 ,  B >. } `  1 ) ,  0 ) )
8382, 68fvmptg 5374 . . 3  |-  ( ( 1  e.  NN  /\  if ( 1  <_  1 ,  ( { <. 1 ,  B >. } `
 1 ) ,  0 )  e.  CC )  ->  ( ( n  e.  NN  |->  if ( n  <_  1 , 
( { <. 1 ,  B >. } `  n
) ,  0 ) ) `  1 )  =  if ( 1  <_  1 ,  ( { <. 1 ,  B >. } `  1 ) ,  0 ) )
846, 79, 83sylancr 405 . 2  |-  ( ( M  e.  V  /\  B  e.  CC )  ->  ( ( n  e.  NN  |->  if ( n  <_  1 ,  ( { <. 1 ,  B >. } `  n ) ,  0 ) ) `
 1 )  =  if ( 1  <_ 
1 ,  ( {
<. 1 ,  B >. } `  1 ) ,  0 ) )
8575, 84, 783eqtrd 2124 1  |-  ( ( M  e.  V  /\  B  e.  CC )  -> 
sum_ k  e.  { M } A  =  B )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 102    <-> wb 103  DECID wdc 780    = wceq 1289    e. wcel 1438   F/_wnfc 2215   [_csb 2933   ifcif 3391   {csn 3444   <.cop 3447   class class class wbr 3843    |-> cmpt 3897   -1-1-onto->wf1o 5009   ` cfv 5010  (class class class)co 5644   CCcc 7338   RRcr 7339   0cc0 7340   1c1 7341    + caddc 7343    <_ cle 7513   NNcn 8412   ZZcz 8740   ZZ>=cuz 9009   ...cfz 9414    seqcseq4 9839   sum_csu 10729
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 579  ax-in2 580  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-13 1449  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-coll 3952  ax-sep 3955  ax-nul 3963  ax-pow 4007  ax-pr 4034  ax-un 4258  ax-setind 4351  ax-iinf 4401  ax-cnex 7426  ax-resscn 7427  ax-1cn 7428  ax-1re 7429  ax-icn 7430  ax-addcl 7431  ax-addrcl 7432  ax-mulcl 7433  ax-mulrcl 7434  ax-addcom 7435  ax-mulcom 7436  ax-addass 7437  ax-mulass 7438  ax-distr 7439  ax-i2m1 7440  ax-0lt1 7441  ax-1rid 7442  ax-0id 7443  ax-rnegex 7444  ax-precex 7445  ax-cnre 7446  ax-pre-ltirr 7447  ax-pre-ltwlin 7448  ax-pre-lttrn 7449  ax-pre-apti 7450  ax-pre-ltadd 7451  ax-pre-mulgt0 7452  ax-pre-mulext 7453  ax-arch 7454  ax-caucvg 7455
This theorem depends on definitions:  df-bi 115  df-dc 781  df-3or 925  df-3an 926  df-tru 1292  df-fal 1295  df-nf 1395  df-sb 1693  df-eu 1951  df-mo 1952  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ne 2256  df-nel 2351  df-ral 2364  df-rex 2365  df-reu 2366  df-rmo 2367  df-rab 2368  df-v 2621  df-sbc 2841  df-csb 2934  df-dif 3001  df-un 3003  df-in 3005  df-ss 3012  df-nul 3287  df-if 3392  df-pw 3429  df-sn 3450  df-pr 3451  df-op 3453  df-uni 3652  df-int 3687  df-iun 3730  df-br 3844  df-opab 3898  df-mpt 3899  df-tr 3935  df-id 4118  df-po 4121  df-iso 4122  df-iord 4191  df-on 4193  df-ilim 4194  df-suc 4196  df-iom 4404  df-xp 4442  df-rel 4443  df-cnv 4444  df-co 4445  df-dm 4446  df-rn 4447  df-res 4448  df-ima 4449  df-iota 4975  df-fun 5012  df-fn 5013  df-f 5014  df-f1 5015  df-fo 5016  df-f1o 5017  df-fv 5018  df-isom 5019  df-riota 5600  df-ov 5647  df-oprab 5648  df-mpt2 5649  df-1st 5903  df-2nd 5904  df-recs 6062  df-irdg 6127  df-frec 6148  df-1o 6173  df-oadd 6177  df-er 6282  df-en 6448  df-dom 6449  df-fin 6450  df-pnf 7514  df-mnf 7515  df-xr 7516  df-ltxr 7517  df-le 7518  df-sub 7645  df-neg 7646  df-reap 8042  df-ap 8049  df-div 8130  df-inn 8413  df-2 8471  df-3 8472  df-4 8473  df-n0 8664  df-z 8741  df-uz 9010  df-q 9095  df-rp 9125  df-fz 9415  df-fzo 9542  df-iseq 9841  df-seq3 9842  df-exp 9943  df-ihash 10172  df-cj 10264  df-re 10265  df-im 10266  df-rsqrt 10419  df-abs 10420  df-clim 10654  df-isum 10730
This theorem is referenced by:  fsumsplitsn  10791  sumsn  10792
  Copyright terms: Public domain W3C validator