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

Theorem fsumadd 11130
Description: The sum of two finite sums. (Contributed by NM, 14-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.)
Hypotheses
Ref Expression
fsumadd.1  |-  ( ph  ->  A  e.  Fin )
fsumadd.2  |-  ( (
ph  /\  k  e.  A )  ->  B  e.  CC )
fsumadd.3  |-  ( (
ph  /\  k  e.  A )  ->  C  e.  CC )
Assertion
Ref Expression
fsumadd  |-  ( ph  -> 
sum_ k  e.  A  ( B  +  C
)  =  ( sum_ k  e.  A  B  +  sum_ k  e.  A  C ) )
Distinct variable groups:    A, k    ph, k
Allowed substitution hints:    B( k)    C( k)

Proof of Theorem fsumadd
Dummy variables  f  j  n  m are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 00id 7871 . . . . 5  |-  ( 0  +  0 )  =  0
2 sum0 11112 . . . . . 6  |-  sum_ k  e.  (/)  B  =  0
3 sum0 11112 . . . . . 6  |-  sum_ k  e.  (/)  C  =  0
42, 3oveq12i 5754 . . . . 5  |-  ( sum_ k  e.  (/)  B  +  sum_ k  e.  (/)  C )  =  ( 0  +  0 )
5 sum0 11112 . . . . 5  |-  sum_ k  e.  (/)  ( B  +  C )  =  0
61, 4, 53eqtr4ri 2149 . . . 4  |-  sum_ k  e.  (/)  ( B  +  C )  =  (
sum_ k  e.  (/)  B  +  sum_ k  e.  (/)  C )
7 sumeq1 11079 . . . 4  |-  ( A  =  (/)  ->  sum_ k  e.  A  ( B  +  C )  =  sum_ k  e.  (/)  ( B  +  C ) )
8 sumeq1 11079 . . . . 5  |-  ( A  =  (/)  ->  sum_ k  e.  A  B  =  sum_ k  e.  (/)  B )
9 sumeq1 11079 . . . . 5  |-  ( A  =  (/)  ->  sum_ k  e.  A  C  =  sum_ k  e.  (/)  C )
108, 9oveq12d 5760 . . . 4  |-  ( A  =  (/)  ->  ( sum_ k  e.  A  B  +  sum_ k  e.  A  C )  =  (
sum_ k  e.  (/)  B  +  sum_ k  e.  (/)  C ) )
116, 7, 103eqtr4a 2176 . . 3  |-  ( A  =  (/)  ->  sum_ k  e.  A  ( B  +  C )  =  (
sum_ k  e.  A  B  +  sum_ k  e.  A  C ) )
1211a1i 9 . 2  |-  ( ph  ->  ( A  =  (/)  -> 
sum_ k  e.  A  ( B  +  C
)  =  ( sum_ k  e.  A  B  +  sum_ k  e.  A  C ) ) )
13 simprl 505 . . . . . . . . 9  |-  ( (
ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A
) ) -1-1-onto-> A ) )  -> 
( `  A )  e.  NN )
14 nnuz 9317 . . . . . . . . 9  |-  NN  =  ( ZZ>= `  1 )
1513, 14eleqtrdi 2210 . . . . . . . 8  |-  ( (
ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A
) ) -1-1-onto-> A ) )  -> 
( `  A )  e.  ( ZZ>= `  1 )
)
16 eqid 2117 . . . . . . . . . 10  |-  ( j  e.  NN  |->  if ( j  <_  ( `  A
) ,  ( ( ( k  e.  A  |->  B )  o.  f
) `  j ) ,  0 ) )  =  ( j  e.  NN  |->  if ( j  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  B )  o.  f ) `
 j ) ,  0 ) )
17 breq1 3902 . . . . . . . . . . 11  |-  ( j  =  n  ->  (
j  <_  ( `  A
)  <->  n  <_  ( `  A
) ) )
18 fveq2 5389 . . . . . . . . . . 11  |-  ( j  =  n  ->  (
( ( k  e.  A  |->  B )  o.  f ) `  j
)  =  ( ( ( k  e.  A  |->  B )  o.  f
) `  n )
)
1917, 18ifbieq1d 3464 . . . . . . . . . 10  |-  ( j  =  n  ->  if ( j  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  B )  o.  f ) `  j
) ,  0 )  =  if ( n  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  B )  o.  f ) `
 n ) ,  0 ) )
20 elnnuz 9318 . . . . . . . . . . . 12  |-  ( n  e.  NN  <->  n  e.  ( ZZ>= `  1 )
)
2120biimpri 132 . . . . . . . . . . 11  |-  ( n  e.  ( ZZ>= `  1
)  ->  n  e.  NN )
2221adantl 275 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  ->  n  e.  NN )
23 fsumadd.2 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  A )  ->  B  e.  CC )
2423adantlr 468 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  k  e.  A )  ->  B  e.  CC )
2524fmpttd 5543 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A
) ) -1-1-onto-> A ) )  -> 
( k  e.  A  |->  B ) : A --> CC )
26 simprr 506 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A
) ) -1-1-onto-> A ) )  -> 
f : ( 1 ... ( `  A
) ) -1-1-onto-> A )
27 f1of 5335 . . . . . . . . . . . . . . 15  |-  ( f : ( 1 ... ( `  A )
)
-1-1-onto-> A  ->  f : ( 1 ... ( `  A
) ) --> A )
2826, 27syl 14 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A
) ) -1-1-onto-> A ) )  -> 
f : ( 1 ... ( `  A
) ) --> A )
29 fco 5258 . . . . . . . . . . . . . 14  |-  ( ( ( k  e.  A  |->  B ) : A --> CC  /\  f : ( 1 ... ( `  A
) ) --> A )  ->  ( ( k  e.  A  |->  B )  o.  f ) : ( 1 ... ( `  A ) ) --> CC )
3025, 28, 29syl2anc 408 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A
) ) -1-1-onto-> A ) )  -> 
( ( k  e.  A  |->  B )  o.  f ) : ( 1 ... ( `  A
) ) --> CC )
3130ad2antrr 479 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  /\  n  <_  ( `  A ) )  -> 
( ( k  e.  A  |->  B )  o.  f ) : ( 1 ... ( `  A
) ) --> CC )
32 1zzd 9039 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  /\  n  <_  ( `  A ) )  -> 
1  e.  ZZ )
3313ad2antrr 479 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  /\  n  <_  ( `  A ) )  -> 
( `  A )  e.  NN )
3433nnzd 9130 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  /\  n  <_  ( `  A ) )  -> 
( `  A )  e.  ZZ )
35 eluzelz 9291 . . . . . . . . . . . . . . 15  |-  ( n  e.  ( ZZ>= `  1
)  ->  n  e.  ZZ )
3635ad2antlr 480 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  /\  n  <_  ( `  A ) )  ->  n  e.  ZZ )
3732, 34, 363jca 1146 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  /\  n  <_  ( `  A ) )  -> 
( 1  e.  ZZ  /\  ( `  A )  e.  ZZ  /\  n  e.  ZZ ) )
38 eluzle 9294 . . . . . . . . . . . . . . 15  |-  ( n  e.  ( ZZ>= `  1
)  ->  1  <_  n )
3938ad2antlr 480 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  /\  n  <_  ( `  A ) )  -> 
1  <_  n )
40 simpr 109 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  /\  n  <_  ( `  A ) )  ->  n  <_  ( `  A )
)
4139, 40jca 304 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  /\  n  <_  ( `  A ) )  -> 
( 1  <_  n  /\  n  <_  ( `  A
) ) )
42 elfz2 9752 . . . . . . . . . . . . 13  |-  ( n  e.  ( 1 ... ( `  A )
)  <->  ( ( 1  e.  ZZ  /\  ( `  A )  e.  ZZ  /\  n  e.  ZZ )  /\  ( 1  <_  n  /\  n  <_  ( `  A ) ) ) )
4337, 41, 42sylanbrc 413 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  /\  n  <_  ( `  A ) )  ->  n  e.  ( 1 ... ( `  A
) ) )
4431, 43ffvelrnd 5524 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  /\  n  <_  ( `  A ) )  -> 
( ( ( k  e.  A  |->  B )  o.  f ) `  n )  e.  CC )
45 0cnd 7727 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  /\  -.  n  <_  ( `  A )
)  ->  0  e.  CC )
4622nnzd 9130 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  ->  n  e.  ZZ )
4713adantr 274 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  ->  ( `  A
)  e.  NN )
4847nnzd 9130 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  ->  ( `  A
)  e.  ZZ )
49 zdcle 9085 . . . . . . . . . . . 12  |-  ( ( n  e.  ZZ  /\  ( `  A )  e.  ZZ )  -> DECID  n  <_  ( `  A
) )
5046, 48, 49syl2anc 408 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  -> DECID  n  <_  ( `  A
) )
5144, 45, 50ifcldadc 3471 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  ->  if (
n  <_  ( `  A
) ,  ( ( ( k  e.  A  |->  B )  o.  f
) `  n ) ,  0 )  e.  CC )
5216, 19, 22, 51fvmptd3 5482 . . . . . . . . 9  |-  ( ( ( ph  /\  (
( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  ->  ( (
j  e.  NN  |->  if ( j  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  B )  o.  f ) `  j
) ,  0 ) ) `  n )  =  if ( n  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  B )  o.  f ) `
 n ) ,  0 ) )
5352, 51eqeltrd 2194 . . . . . . . 8  |-  ( ( ( ph  /\  (
( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  ->  ( (
j  e.  NN  |->  if ( j  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  B )  o.  f ) `  j
) ,  0 ) ) `  n )  e.  CC )
54 eqid 2117 . . . . . . . . . 10  |-  ( j  e.  NN  |->  if ( j  <_  ( `  A
) ,  ( ( ( k  e.  A  |->  C )  o.  f
) `  j ) ,  0 ) )  =  ( j  e.  NN  |->  if ( j  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  C )  o.  f ) `
 j ) ,  0 ) )
55 fveq2 5389 . . . . . . . . . . 11  |-  ( j  =  n  ->  (
( ( k  e.  A  |->  C )  o.  f ) `  j
)  =  ( ( ( k  e.  A  |->  C )  o.  f
) `  n )
)
5617, 55ifbieq1d 3464 . . . . . . . . . 10  |-  ( j  =  n  ->  if ( j  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  C )  o.  f ) `  j
) ,  0 )  =  if ( n  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  C )  o.  f ) `
 n ) ,  0 ) )
57 fsumadd.3 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  A )  ->  C  e.  CC )
5857adantlr 468 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  k  e.  A )  ->  C  e.  CC )
5958fmpttd 5543 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A
) ) -1-1-onto-> A ) )  -> 
( k  e.  A  |->  C ) : A --> CC )
6059ad2antrr 479 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  /\  n  <_  ( `  A ) )  -> 
( k  e.  A  |->  C ) : A --> CC )
6128ad2antrr 479 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  /\  n  <_  ( `  A ) )  -> 
f : ( 1 ... ( `  A
) ) --> A )
62 fco 5258 . . . . . . . . . . . . 13  |-  ( ( ( k  e.  A  |->  C ) : A --> CC  /\  f : ( 1 ... ( `  A
) ) --> A )  ->  ( ( k  e.  A  |->  C )  o.  f ) : ( 1 ... ( `  A ) ) --> CC )
6360, 61, 62syl2anc 408 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  /\  n  <_  ( `  A ) )  -> 
( ( k  e.  A  |->  C )  o.  f ) : ( 1 ... ( `  A
) ) --> CC )
6463, 43ffvelrnd 5524 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  /\  n  <_  ( `  A ) )  -> 
( ( ( k  e.  A  |->  C )  o.  f ) `  n )  e.  CC )
6564, 45, 50ifcldadc 3471 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  ->  if (
n  <_  ( `  A
) ,  ( ( ( k  e.  A  |->  C )  o.  f
) `  n ) ,  0 )  e.  CC )
6654, 56, 22, 65fvmptd3 5482 . . . . . . . . 9  |-  ( ( ( ph  /\  (
( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  ->  ( (
j  e.  NN  |->  if ( j  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  C )  o.  f ) `  j
) ,  0 ) ) `  n )  =  if ( n  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  C )  o.  f ) `
 n ) ,  0 ) )
6766, 65eqeltrd 2194 . . . . . . . 8  |-  ( ( ( ph  /\  (
( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  ->  ( (
j  e.  NN  |->  if ( j  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  C )  o.  f ) `  j
) ,  0 ) ) `  n )  e.  CC )
68 simpll 503 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  /\  n  <_  ( `  A ) )  -> 
( ph  /\  (
( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) ) )
6928ffvelrnda 5523 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( 1 ... ( `  A ) ) )  ->  ( f `  n )  e.  A
)
70 simpr 109 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  A )  ->  k  e.  A )
7123, 57addcld 7753 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  A )  ->  ( B  +  C )  e.  CC )
72 eqid 2117 . . . . . . . . . . . . . . . . . . 19  |-  ( k  e.  A  |->  ( B  +  C ) )  =  ( k  e.  A  |->  ( B  +  C ) )
7372fvmpt2 5472 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  A  /\  ( B  +  C
)  e.  CC )  ->  ( ( k  e.  A  |->  ( B  +  C ) ) `
 k )  =  ( B  +  C
) )
7470, 71, 73syl2anc 408 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  A )  ->  (
( k  e.  A  |->  ( B  +  C
) ) `  k
)  =  ( B  +  C ) )
75 eqid 2117 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  e.  A  |->  B )  =  ( k  e.  A  |->  B )
7675fvmpt2 5472 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  A  /\  B  e.  CC )  ->  ( ( k  e.  A  |->  B ) `  k )  =  B )
7770, 23, 76syl2anc 408 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  A )  ->  (
( k  e.  A  |->  B ) `  k
)  =  B )
78 eqid 2117 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  e.  A  |->  C )  =  ( k  e.  A  |->  C )
7978fvmpt2 5472 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  A  /\  C  e.  CC )  ->  ( ( k  e.  A  |->  C ) `  k )  =  C )
8070, 57, 79syl2anc 408 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  A )  ->  (
( k  e.  A  |->  C ) `  k
)  =  C )
8177, 80oveq12d 5760 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  A )  ->  (
( ( k  e.  A  |->  B ) `  k )  +  ( ( k  e.  A  |->  C ) `  k
) )  =  ( B  +  C ) )
8274, 81eqtr4d 2153 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  A )  ->  (
( k  e.  A  |->  ( B  +  C
) ) `  k
)  =  ( ( ( k  e.  A  |->  B ) `  k
)  +  ( ( k  e.  A  |->  C ) `  k ) ) )
8382ralrimiva 2482 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A. k  e.  A  ( ( k  e.  A  |->  ( B  +  C ) ) `  k )  =  ( ( ( k  e.  A  |->  B ) `  k )  +  ( ( k  e.  A  |->  C ) `  k
) ) )
8483ad2antrr 479 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( 1 ... ( `  A ) ) )  ->  A. k  e.  A  ( ( k  e.  A  |->  ( B  +  C ) ) `  k )  =  ( ( ( k  e.  A  |->  B ) `  k )  +  ( ( k  e.  A  |->  C ) `  k
) ) )
85 nffvmpt1 5400 . . . . . . . . . . . . . . . 16  |-  F/_ k
( ( k  e.  A  |->  ( B  +  C ) ) `  ( f `  n
) )
86 nffvmpt1 5400 . . . . . . . . . . . . . . . . 17  |-  F/_ k
( ( k  e.  A  |->  B ) `  ( f `  n
) )
87 nfcv 2258 . . . . . . . . . . . . . . . . 17  |-  F/_ k  +
88 nffvmpt1 5400 . . . . . . . . . . . . . . . . 17  |-  F/_ k
( ( k  e.  A  |->  C ) `  ( f `  n
) )
8986, 87, 88nfov 5769 . . . . . . . . . . . . . . . 16  |-  F/_ k
( ( ( k  e.  A  |->  B ) `
 ( f `  n ) )  +  ( ( k  e.  A  |->  C ) `  ( f `  n
) ) )
9085, 89nfeq 2266 . . . . . . . . . . . . . . 15  |-  F/ k ( ( k  e.  A  |->  ( B  +  C ) ) `  ( f `  n
) )  =  ( ( ( k  e.  A  |->  B ) `  ( f `  n
) )  +  ( ( k  e.  A  |->  C ) `  (
f `  n )
) )
91 fveq2 5389 . . . . . . . . . . . . . . . 16  |-  ( k  =  ( f `  n )  ->  (
( k  e.  A  |->  ( B  +  C
) ) `  k
)  =  ( ( k  e.  A  |->  ( B  +  C ) ) `  ( f `
 n ) ) )
92 fveq2 5389 . . . . . . . . . . . . . . . . 17  |-  ( k  =  ( f `  n )  ->  (
( k  e.  A  |->  B ) `  k
)  =  ( ( k  e.  A  |->  B ) `  ( f `
 n ) ) )
93 fveq2 5389 . . . . . . . . . . . . . . . . 17  |-  ( k  =  ( f `  n )  ->  (
( k  e.  A  |->  C ) `  k
)  =  ( ( k  e.  A  |->  C ) `  ( f `
 n ) ) )
9492, 93oveq12d 5760 . . . . . . . . . . . . . . . 16  |-  ( k  =  ( f `  n )  ->  (
( ( k  e.  A  |->  B ) `  k )  +  ( ( k  e.  A  |->  C ) `  k
) )  =  ( ( ( k  e.  A  |->  B ) `  ( f `  n
) )  +  ( ( k  e.  A  |->  C ) `  (
f `  n )
) ) )
9591, 94eqeq12d 2132 . . . . . . . . . . . . . . 15  |-  ( k  =  ( f `  n )  ->  (
( ( k  e.  A  |->  ( B  +  C ) ) `  k )  =  ( ( ( k  e.  A  |->  B ) `  k )  +  ( ( k  e.  A  |->  C ) `  k
) )  <->  ( (
k  e.  A  |->  ( B  +  C ) ) `  ( f `
 n ) )  =  ( ( ( k  e.  A  |->  B ) `  ( f `
 n ) )  +  ( ( k  e.  A  |->  C ) `
 ( f `  n ) ) ) ) )
9690, 95rspc 2757 . . . . . . . . . . . . . 14  |-  ( ( f `  n )  e.  A  ->  ( A. k  e.  A  ( ( k  e.  A  |->  ( B  +  C ) ) `  k )  =  ( ( ( k  e.  A  |->  B ) `  k )  +  ( ( k  e.  A  |->  C ) `  k
) )  ->  (
( k  e.  A  |->  ( B  +  C
) ) `  (
f `  n )
)  =  ( ( ( k  e.  A  |->  B ) `  (
f `  n )
)  +  ( ( k  e.  A  |->  C ) `  ( f `
 n ) ) ) ) )
9769, 84, 96sylc 62 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( 1 ... ( `  A ) ) )  ->  ( ( k  e.  A  |->  ( B  +  C ) ) `
 ( f `  n ) )  =  ( ( ( k  e.  A  |->  B ) `
 ( f `  n ) )  +  ( ( k  e.  A  |->  C ) `  ( f `  n
) ) ) )
98 fvco3 5460 . . . . . . . . . . . . . 14  |-  ( ( f : ( 1 ... ( `  A
) ) --> A  /\  n  e.  ( 1 ... ( `  A
) ) )  -> 
( ( ( k  e.  A  |->  ( B  +  C ) )  o.  f ) `  n )  =  ( ( k  e.  A  |->  ( B  +  C
) ) `  (
f `  n )
) )
9928, 98sylan 281 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( 1 ... ( `  A ) ) )  ->  ( ( ( k  e.  A  |->  ( B  +  C ) )  o.  f ) `
 n )  =  ( ( k  e.  A  |->  ( B  +  C ) ) `  ( f `  n
) ) )
100 fvco3 5460 . . . . . . . . . . . . . . 15  |-  ( ( f : ( 1 ... ( `  A
) ) --> A  /\  n  e.  ( 1 ... ( `  A
) ) )  -> 
( ( ( k  e.  A  |->  B )  o.  f ) `  n )  =  ( ( k  e.  A  |->  B ) `  (
f `  n )
) )
10128, 100sylan 281 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( 1 ... ( `  A ) ) )  ->  ( ( ( k  e.  A  |->  B )  o.  f ) `
 n )  =  ( ( k  e.  A  |->  B ) `  ( f `  n
) ) )
102 fvco3 5460 . . . . . . . . . . . . . . 15  |-  ( ( f : ( 1 ... ( `  A
) ) --> A  /\  n  e.  ( 1 ... ( `  A
) ) )  -> 
( ( ( k  e.  A  |->  C )  o.  f ) `  n )  =  ( ( k  e.  A  |->  C ) `  (
f `  n )
) )
10328, 102sylan 281 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( 1 ... ( `  A ) ) )  ->  ( ( ( k  e.  A  |->  C )  o.  f ) `
 n )  =  ( ( k  e.  A  |->  C ) `  ( f `  n
) ) )
104101, 103oveq12d 5760 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( 1 ... ( `  A ) ) )  ->  ( ( ( ( k  e.  A  |->  B )  o.  f
) `  n )  +  ( ( ( k  e.  A  |->  C )  o.  f ) `
 n ) )  =  ( ( ( k  e.  A  |->  B ) `  ( f `
 n ) )  +  ( ( k  e.  A  |->  C ) `
 ( f `  n ) ) ) )
10597, 99, 1043eqtr4d 2160 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( 1 ... ( `  A ) ) )  ->  ( ( ( k  e.  A  |->  ( B  +  C ) )  o.  f ) `
 n )  =  ( ( ( ( k  e.  A  |->  B )  o.  f ) `
 n )  +  ( ( ( k  e.  A  |->  C )  o.  f ) `  n ) ) )
10668, 43, 105syl2anc 408 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  /\  n  <_  ( `  A ) )  -> 
( ( ( k  e.  A  |->  ( B  +  C ) )  o.  f ) `  n )  =  ( ( ( ( k  e.  A  |->  B )  o.  f ) `  n )  +  ( ( ( k  e.  A  |->  C )  o.  f ) `  n
) ) )
10740iftrued 3451 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  /\  n  <_  ( `  A ) )  ->  if ( n  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  ( B  +  C ) )  o.  f ) `  n
) ,  0 )  =  ( ( ( k  e.  A  |->  ( B  +  C ) )  o.  f ) `
 n ) )
10840iftrued 3451 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  /\  n  <_  ( `  A ) )  ->  if ( n  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  B )  o.  f ) `  n
) ,  0 )  =  ( ( ( k  e.  A  |->  B )  o.  f ) `
 n ) )
10940iftrued 3451 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  /\  n  <_  ( `  A ) )  ->  if ( n  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  C )  o.  f ) `  n
) ,  0 )  =  ( ( ( k  e.  A  |->  C )  o.  f ) `
 n ) )
110108, 109oveq12d 5760 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  /\  n  <_  ( `  A ) )  -> 
( if ( n  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  B )  o.  f ) `
 n ) ,  0 )  +  if ( n  <_  ( `  A
) ,  ( ( ( k  e.  A  |->  C )  o.  f
) `  n ) ,  0 ) )  =  ( ( ( ( k  e.  A  |->  B )  o.  f
) `  n )  +  ( ( ( k  e.  A  |->  C )  o.  f ) `
 n ) ) )
111106, 107, 1103eqtr4d 2160 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  /\  n  <_  ( `  A ) )  ->  if ( n  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  ( B  +  C ) )  o.  f ) `  n
) ,  0 )  =  ( if ( n  <_  ( `  A
) ,  ( ( ( k  e.  A  |->  B )  o.  f
) `  n ) ,  0 )  +  if ( n  <_ 
( `  A ) ,  ( ( ( k  e.  A  |->  C )  o.  f ) `  n ) ,  0 ) ) )
1121eqcomi 2121 . . . . . . . . . . 11  |-  0  =  ( 0  +  0 )
113 simpr 109 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  /\  -.  n  <_  ( `  A )
)  ->  -.  n  <_  ( `  A )
)
114113iffalsed 3454 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  /\  -.  n  <_  ( `  A )
)  ->  if (
n  <_  ( `  A
) ,  ( ( ( k  e.  A  |->  ( B  +  C
) )  o.  f
) `  n ) ,  0 )  =  0 )
115113iffalsed 3454 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  /\  -.  n  <_  ( `  A )
)  ->  if (
n  <_  ( `  A
) ,  ( ( ( k  e.  A  |->  B )  o.  f
) `  n ) ,  0 )  =  0 )
116113iffalsed 3454 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  /\  -.  n  <_  ( `  A )
)  ->  if (
n  <_  ( `  A
) ,  ( ( ( k  e.  A  |->  C )  o.  f
) `  n ) ,  0 )  =  0 )
117115, 116oveq12d 5760 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  /\  -.  n  <_  ( `  A )
)  ->  ( if ( n  <_  ( `  A
) ,  ( ( ( k  e.  A  |->  B )  o.  f
) `  n ) ,  0 )  +  if ( n  <_ 
( `  A ) ,  ( ( ( k  e.  A  |->  C )  o.  f ) `  n ) ,  0 ) )  =  ( 0  +  0 ) )
118112, 114, 1173eqtr4a 2176 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  /\  -.  n  <_  ( `  A )
)  ->  if (
n  <_  ( `  A
) ,  ( ( ( k  e.  A  |->  ( B  +  C
) )  o.  f
) `  n ) ,  0 )  =  ( if ( n  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  B )  o.  f ) `
 n ) ,  0 )  +  if ( n  <_  ( `  A
) ,  ( ( ( k  e.  A  |->  C )  o.  f
) `  n ) ,  0 ) ) )
119 exmiddc 806 . . . . . . . . . . 11  |-  (DECID  n  <_ 
( `  A )  -> 
( n  <_  ( `  A )  \/  -.  n  <_  ( `  A )
) )
12050, 119syl 14 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  ->  ( n  <_  ( `  A )  \/  -.  n  <_  ( `  A ) ) )
121111, 118, 120mpjaodan 772 . . . . . . . . 9  |-  ( ( ( ph  /\  (
( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  ->  if (
n  <_  ( `  A
) ,  ( ( ( k  e.  A  |->  ( B  +  C
) )  o.  f
) `  n ) ,  0 )  =  ( if ( n  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  B )  o.  f ) `
 n ) ,  0 )  +  if ( n  <_  ( `  A
) ,  ( ( ( k  e.  A  |->  C )  o.  f
) `  n ) ,  0 ) ) )
122 eqid 2117 . . . . . . . . . 10  |-  ( j  e.  NN  |->  if ( j  <_  ( `  A
) ,  ( ( ( k  e.  A  |->  ( B  +  C
) )  o.  f
) `  j ) ,  0 ) )  =  ( j  e.  NN  |->  if ( j  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  ( B  +  C ) )  o.  f ) `
 j ) ,  0 ) )
123 fveq2 5389 . . . . . . . . . . 11  |-  ( j  =  n  ->  (
( ( k  e.  A  |->  ( B  +  C ) )  o.  f ) `  j
)  =  ( ( ( k  e.  A  |->  ( B  +  C
) )  o.  f
) `  n )
)
12417, 123ifbieq1d 3464 . . . . . . . . . 10  |-  ( j  =  n  ->  if ( j  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  ( B  +  C ) )  o.  f ) `  j
) ,  0 )  =  if ( n  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  ( B  +  C ) )  o.  f ) `
 n ) ,  0 ) )
12571fmpttd 5543 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( k  e.  A  |->  ( B  +  C
) ) : A --> CC )
126125ad3antrrr 483 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  /\  n  <_  ( `  A ) )  -> 
( k  e.  A  |->  ( B  +  C
) ) : A --> CC )
127 fco 5258 . . . . . . . . . . . . 13  |-  ( ( ( k  e.  A  |->  ( B  +  C
) ) : A --> CC  /\  f : ( 1 ... ( `  A
) ) --> A )  ->  ( ( k  e.  A  |->  ( B  +  C ) )  o.  f ) : ( 1 ... ( `  A ) ) --> CC )
128126, 61, 127syl2anc 408 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  /\  n  <_  ( `  A ) )  -> 
( ( k  e.  A  |->  ( B  +  C ) )  o.  f ) : ( 1 ... ( `  A
) ) --> CC )
129128, 43ffvelrnd 5524 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  /\  n  <_  ( `  A ) )  -> 
( ( ( k  e.  A  |->  ( B  +  C ) )  o.  f ) `  n )  e.  CC )
130129, 45, 50ifcldadc 3471 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  ->  if (
n  <_  ( `  A
) ,  ( ( ( k  e.  A  |->  ( B  +  C
) )  o.  f
) `  n ) ,  0 )  e.  CC )
131122, 124, 22, 130fvmptd3 5482 . . . . . . . . 9  |-  ( ( ( ph  /\  (
( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  ->  ( (
j  e.  NN  |->  if ( j  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  ( B  +  C ) )  o.  f ) `  j
) ,  0 ) ) `  n )  =  if ( n  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  ( B  +  C ) )  o.  f ) `
 n ) ,  0 ) )
13252, 66oveq12d 5760 . . . . . . . . 9  |-  ( ( ( ph  /\  (
( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  ->  ( (
( j  e.  NN  |->  if ( j  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  B )  o.  f ) `  j
) ,  0 ) ) `  n )  +  ( ( j  e.  NN  |->  if ( j  <_  ( `  A
) ,  ( ( ( k  e.  A  |->  C )  o.  f
) `  j ) ,  0 ) ) `
 n ) )  =  ( if ( n  <_  ( `  A
) ,  ( ( ( k  e.  A  |->  B )  o.  f
) `  n ) ,  0 )  +  if ( n  <_ 
( `  A ) ,  ( ( ( k  e.  A  |->  C )  o.  f ) `  n ) ,  0 ) ) )
133121, 131, 1323eqtr4d 2160 . . . . . . . 8  |-  ( ( ( ph  /\  (
( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  n  e.  ( ZZ>= `  1 )
)  ->  ( (
j  e.  NN  |->  if ( j  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  ( B  +  C ) )  o.  f ) `  j
) ,  0 ) ) `  n )  =  ( ( ( j  e.  NN  |->  if ( j  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  B )  o.  f ) `  j
) ,  0 ) ) `  n )  +  ( ( j  e.  NN  |->  if ( j  <_  ( `  A
) ,  ( ( ( k  e.  A  |->  C )  o.  f
) `  j ) ,  0 ) ) `
 n ) ) )
13415, 53, 67, 133ser3add 10233 . . . . . . 7  |-  ( (
ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A
) ) -1-1-onto-> A ) )  -> 
(  seq 1 (  +  ,  ( j  e.  NN  |->  if ( j  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  ( B  +  C ) )  o.  f ) `
 j ) ,  0 ) ) ) `
 ( `  A
) )  =  ( (  seq 1 (  +  ,  ( j  e.  NN  |->  if ( j  <_  ( `  A
) ,  ( ( ( k  e.  A  |->  B )  o.  f
) `  j ) ,  0 ) ) ) `  ( `  A
) )  +  (  seq 1 (  +  ,  ( j  e.  NN  |->  if ( j  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  C )  o.  f ) `
 j ) ,  0 ) ) ) `
 ( `  A
) ) ) )
135 fveq2 5389 . . . . . . . . 9  |-  ( m  =  ( f `  n )  ->  (
( k  e.  A  |->  ( B  +  C
) ) `  m
)  =  ( ( k  e.  A  |->  ( B  +  C ) ) `  ( f `
 n ) ) )
13624, 58addcld 7753 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  k  e.  A )  ->  ( B  +  C )  e.  CC )
137136fmpttd 5543 . . . . . . . . . 10  |-  ( (
ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A
) ) -1-1-onto-> A ) )  -> 
( k  e.  A  |->  ( B  +  C
) ) : A --> CC )
138137ffvelrnda 5523 . . . . . . . . 9  |-  ( ( ( ph  /\  (
( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  m  e.  A )  ->  (
( k  e.  A  |->  ( B  +  C
) ) `  m
)  e.  CC )
139135, 13, 26, 138, 99fsum3 11111 . . . . . . . 8  |-  ( (
ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A
) ) -1-1-onto-> A ) )  ->  sum_ m  e.  A  ( ( k  e.  A  |->  ( B  +  C
) ) `  m
)  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  ( B  +  C ) )  o.  f ) `  n
) ,  0 ) ) ) `  ( `  A ) ) )
140 breq1 3902 . . . . . . . . . . . 12  |-  ( n  =  j  ->  (
n  <_  ( `  A
)  <->  j  <_  ( `  A ) ) )
141 fveq2 5389 . . . . . . . . . . . 12  |-  ( n  =  j  ->  (
( ( k  e.  A  |->  ( B  +  C ) )  o.  f ) `  n
)  =  ( ( ( k  e.  A  |->  ( B  +  C
) )  o.  f
) `  j )
)
142140, 141ifbieq1d 3464 . . . . . . . . . . 11  |-  ( n  =  j  ->  if ( n  <_  ( `  A
) ,  ( ( ( k  e.  A  |->  ( B  +  C
) )  o.  f
) `  n ) ,  0 )  =  if ( j  <_ 
( `  A ) ,  ( ( ( k  e.  A  |->  ( B  +  C ) )  o.  f ) `  j ) ,  0 ) )
143142cbvmptv 3994 . . . . . . . . . 10  |-  ( n  e.  NN  |->  if ( n  <_  ( `  A
) ,  ( ( ( k  e.  A  |->  ( B  +  C
) )  o.  f
) `  n ) ,  0 ) )  =  ( j  e.  NN  |->  if ( j  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  ( B  +  C ) )  o.  f ) `
 j ) ,  0 ) )
144 seqeq3 10178 . . . . . . . . . 10  |-  ( ( n  e.  NN  |->  if ( n  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  ( B  +  C ) )  o.  f ) `  n
) ,  0 ) )  =  ( j  e.  NN  |->  if ( j  <_  ( `  A
) ,  ( ( ( k  e.  A  |->  ( B  +  C
) )  o.  f
) `  j ) ,  0 ) )  ->  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  ( B  +  C ) )  o.  f ) `
 n ) ,  0 ) ) )  =  seq 1 (  +  ,  ( j  e.  NN  |->  if ( j  <_  ( `  A
) ,  ( ( ( k  e.  A  |->  ( B  +  C
) )  o.  f
) `  j ) ,  0 ) ) ) )
145143, 144ax-mp 5 . . . . . . . . 9  |-  seq 1
(  +  ,  ( n  e.  NN  |->  if ( n  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  ( B  +  C ) )  o.  f ) `  n
) ,  0 ) ) )  =  seq 1 (  +  , 
( j  e.  NN  |->  if ( j  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  ( B  +  C ) )  o.  f ) `  j
) ,  0 ) ) )
146145fveq1i 5390 . . . . . . . 8  |-  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  ( B  +  C ) )  o.  f ) `  n
) ,  0 ) ) ) `  ( `  A ) )  =  (  seq 1 (  +  ,  ( j  e.  NN  |->  if ( j  <_  ( `  A
) ,  ( ( ( k  e.  A  |->  ( B  +  C
) )  o.  f
) `  j ) ,  0 ) ) ) `  ( `  A
) )
147139, 146syl6eq 2166 . . . . . . 7  |-  ( (
ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A
) ) -1-1-onto-> A ) )  ->  sum_ m  e.  A  ( ( k  e.  A  |->  ( B  +  C
) ) `  m
)  =  (  seq 1 (  +  , 
( j  e.  NN  |->  if ( j  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  ( B  +  C ) )  o.  f ) `  j
) ,  0 ) ) ) `  ( `  A ) ) )
148 fveq2 5389 . . . . . . . . . 10  |-  ( m  =  ( f `  n )  ->  (
( k  e.  A  |->  B ) `  m
)  =  ( ( k  e.  A  |->  B ) `  ( f `
 n ) ) )
14925ffvelrnda 5523 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  m  e.  A )  ->  (
( k  e.  A  |->  B ) `  m
)  e.  CC )
150148, 13, 26, 149, 101fsum3 11111 . . . . . . . . 9  |-  ( (
ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A
) ) -1-1-onto-> A ) )  ->  sum_ m  e.  A  ( ( k  e.  A  |->  B ) `  m
)  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  B )  o.  f ) `  n
) ,  0 ) ) ) `  ( `  A ) ) )
151 fveq2 5389 . . . . . . . . . . . . 13  |-  ( n  =  j  ->  (
( ( k  e.  A  |->  B )  o.  f ) `  n
)  =  ( ( ( k  e.  A  |->  B )  o.  f
) `  j )
)
152140, 151ifbieq1d 3464 . . . . . . . . . . . 12  |-  ( n  =  j  ->  if ( n  <_  ( `  A
) ,  ( ( ( k  e.  A  |->  B )  o.  f
) `  n ) ,  0 )  =  if ( j  <_ 
( `  A ) ,  ( ( ( k  e.  A  |->  B )  o.  f ) `  j ) ,  0 ) )
153152cbvmptv 3994 . . . . . . . . . . 11  |-  ( n  e.  NN  |->  if ( n  <_  ( `  A
) ,  ( ( ( k  e.  A  |->  B )  o.  f
) `  n ) ,  0 ) )  =  ( j  e.  NN  |->  if ( j  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  B )  o.  f ) `
 j ) ,  0 ) )
154 seqeq3 10178 . . . . . . . . . . 11  |-  ( ( n  e.  NN  |->  if ( n  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  B )  o.  f ) `  n
) ,  0 ) )  =  ( j  e.  NN  |->  if ( j  <_  ( `  A
) ,  ( ( ( k  e.  A  |->  B )  o.  f
) `  j ) ,  0 ) )  ->  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  B )  o.  f ) `
 n ) ,  0 ) ) )  =  seq 1 (  +  ,  ( j  e.  NN  |->  if ( j  <_  ( `  A
) ,  ( ( ( k  e.  A  |->  B )  o.  f
) `  j ) ,  0 ) ) ) )
155153, 154ax-mp 5 . . . . . . . . . 10  |-  seq 1
(  +  ,  ( n  e.  NN  |->  if ( n  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  B )  o.  f ) `  n
) ,  0 ) ) )  =  seq 1 (  +  , 
( j  e.  NN  |->  if ( j  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  B )  o.  f ) `  j
) ,  0 ) ) )
156155fveq1i 5390 . . . . . . . . 9  |-  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  B )  o.  f ) `  n
) ,  0 ) ) ) `  ( `  A ) )  =  (  seq 1 (  +  ,  ( j  e.  NN  |->  if ( j  <_  ( `  A
) ,  ( ( ( k  e.  A  |->  B )  o.  f
) `  j ) ,  0 ) ) ) `  ( `  A
) )
157150, 156syl6eq 2166 . . . . . . . 8  |-  ( (
ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A
) ) -1-1-onto-> A ) )  ->  sum_ m  e.  A  ( ( k  e.  A  |->  B ) `  m
)  =  (  seq 1 (  +  , 
( j  e.  NN  |->  if ( j  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  B )  o.  f ) `  j
) ,  0 ) ) ) `  ( `  A ) ) )
158 fveq2 5389 . . . . . . . . . 10  |-  ( m  =  ( f `  n )  ->  (
( k  e.  A  |->  C ) `  m
)  =  ( ( k  e.  A  |->  C ) `  ( f `
 n ) ) )
15959ffvelrnda 5523 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
( `  A )  e.  NN  /\  f : ( 1 ... ( `  A ) ) -1-1-onto-> A ) )  /\  m  e.  A )  ->  (
( k  e.  A  |->  C ) `  m
)  e.  CC )
160158, 13, 26, 159, 103fsum3 11111 . . . . . . . . 9  |-  ( (
ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A
) ) -1-1-onto-> A ) )  ->  sum_ m  e.  A  ( ( k  e.  A  |->  C ) `  m
)  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  C )  o.  f ) `  n
) ,  0 ) ) ) `  ( `  A ) ) )
161 fveq2 5389 . . . . . . . . . . . . 13  |-  ( n  =  j  ->  (
( ( k  e.  A  |->  C )  o.  f ) `  n
)  =  ( ( ( k  e.  A  |->  C )  o.  f
) `  j )
)
162140, 161ifbieq1d 3464 . . . . . . . . . . . 12  |-  ( n  =  j  ->  if ( n  <_  ( `  A
) ,  ( ( ( k  e.  A  |->  C )  o.  f
) `  n ) ,  0 )  =  if ( j  <_ 
( `  A ) ,  ( ( ( k  e.  A  |->  C )  o.  f ) `  j ) ,  0 ) )
163162cbvmptv 3994 . . . . . . . . . . 11  |-  ( n  e.  NN  |->  if ( n  <_  ( `  A
) ,  ( ( ( k  e.  A  |->  C )  o.  f
) `  n ) ,  0 ) )  =  ( j  e.  NN  |->  if ( j  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  C )  o.  f ) `
 j ) ,  0 ) )
164 seqeq3 10178 . . . . . . . . . . 11  |-  ( ( n  e.  NN  |->  if ( n  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  C )  o.  f ) `  n
) ,  0 ) )  =  ( j  e.  NN  |->  if ( j  <_  ( `  A
) ,  ( ( ( k  e.  A  |->  C )  o.  f
) `  j ) ,  0 ) )  ->  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  C )  o.  f ) `
 n ) ,  0 ) ) )  =  seq 1 (  +  ,  ( j  e.  NN  |->  if ( j  <_  ( `  A
) ,  ( ( ( k  e.  A  |->  C )  o.  f
) `  j ) ,  0 ) ) ) )
165163, 164ax-mp 5 . . . . . . . . . 10  |-  seq 1
(  +  ,  ( n  e.  NN  |->  if ( n  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  C )  o.  f ) `  n
) ,  0 ) ) )  =  seq 1 (  +  , 
( j  e.  NN  |->  if ( j  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  C )  o.  f ) `  j
) ,  0 ) ) )
166165fveq1i 5390 . . . . . . . . 9  |-  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  C )  o.  f ) `  n
) ,  0 ) ) ) `  ( `  A ) )  =  (  seq 1 (  +  ,  ( j  e.  NN  |->  if ( j  <_  ( `  A
) ,  ( ( ( k  e.  A  |->  C )  o.  f
) `  j ) ,  0 ) ) ) `  ( `  A
) )
167160, 166syl6eq 2166 . . . . . . . 8  |-  ( (
ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A
) ) -1-1-onto-> A ) )  ->  sum_ m  e.  A  ( ( k  e.  A  |->  C ) `  m
)  =  (  seq 1 (  +  , 
( j  e.  NN  |->  if ( j  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  C )  o.  f ) `  j
) ,  0 ) ) ) `  ( `  A ) ) )
168157, 167oveq12d 5760 . . . . . . 7  |-  ( (
ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A
) ) -1-1-onto-> A ) )  -> 
( sum_ m  e.  A  ( ( k  e.  A  |->  B ) `  m )  +  sum_ m  e.  A  ( ( k  e.  A  |->  C ) `  m ) )  =  ( (  seq 1 (  +  ,  ( j  e.  NN  |->  if ( j  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  B )  o.  f ) `
 j ) ,  0 ) ) ) `
 ( `  A
) )  +  (  seq 1 (  +  ,  ( j  e.  NN  |->  if ( j  <_  ( `  A ) ,  ( ( ( k  e.  A  |->  C )  o.  f ) `
 j ) ,  0 ) ) ) `
 ( `  A
) ) ) )
169134, 147, 1683eqtr4d 2160 . . . . . 6  |-  ( (
ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A
) ) -1-1-onto-> A ) )  ->  sum_ m  e.  A  ( ( k  e.  A  |->  ( B  +  C
) ) `  m
)  =  ( sum_ m  e.  A  ( ( k  e.  A  |->  B ) `  m )  +  sum_ m  e.  A  ( ( k  e.  A  |->  C ) `  m ) ) )
17071ralrimiva 2482 . . . . . . . 8  |-  ( ph  ->  A. k  e.  A  ( B  +  C
)  e.  CC )
171 sumfct 11098 . . . . . . . 8  |-  ( A. k  e.  A  ( B  +  C )  e.  CC  ->  sum_ m  e.  A  ( ( k  e.  A  |->  ( B  +  C ) ) `
 m )  = 
sum_ k  e.  A  ( B  +  C
) )
172170, 171syl 14 . . . . . . 7  |-  ( ph  -> 
sum_ m  e.  A  ( ( k  e.  A  |->  ( B  +  C ) ) `  m )  =  sum_ k  e.  A  ( B  +  C )
)
173172adantr 274 . . . . . 6  |-  ( (
ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A
) ) -1-1-onto-> A ) )  ->  sum_ m  e.  A  ( ( k  e.  A  |->  ( B  +  C
) ) `  m
)  =  sum_ k  e.  A  ( B  +  C ) )
17423ralrimiva 2482 . . . . . . . . 9  |-  ( ph  ->  A. k  e.  A  B  e.  CC )
175 sumfct 11098 . . . . . . . . 9  |-  ( A. k  e.  A  B  e.  CC  ->  sum_ m  e.  A  ( ( k  e.  A  |->  B ) `
 m )  = 
sum_ k  e.  A  B )
176174, 175syl 14 . . . . . . . 8  |-  ( ph  -> 
sum_ m  e.  A  ( ( k  e.  A  |->  B ) `  m )  =  sum_ k  e.  A  B
)
17757ralrimiva 2482 . . . . . . . . 9  |-  ( ph  ->  A. k  e.  A  C  e.  CC )
178 sumfct 11098 . . . . . . . . 9  |-  ( A. k  e.  A  C  e.  CC  ->  sum_ m  e.  A  ( ( k  e.  A  |->  C ) `
 m )  = 
sum_ k  e.  A  C )
179177, 178syl 14 . . . . . . . 8  |-  ( ph  -> 
sum_ m  e.  A  ( ( k  e.  A  |->  C ) `  m )  =  sum_ k  e.  A  C
)
180176, 179oveq12d 5760 . . . . . . 7  |-  ( ph  ->  ( sum_ m  e.  A  ( ( k  e.  A  |->  B ) `  m )  +  sum_ m  e.  A  ( ( k  e.  A  |->  C ) `  m ) )  =  ( sum_ k  e.  A  B  +  sum_ k  e.  A  C ) )
181180adantr 274 . . . . . 6  |-  ( (
ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A
) ) -1-1-onto-> A ) )  -> 
( sum_ m  e.  A  ( ( k  e.  A  |->  B ) `  m )  +  sum_ m  e.  A  ( ( k  e.  A  |->  C ) `  m ) )  =  ( sum_ k  e.  A  B  +  sum_ k  e.  A  C ) )
182169, 173, 1813eqtr3d 2158 . . . . 5  |-  ( (
ph  /\  ( ( `  A )  e.  NN  /\  f : ( 1 ... ( `  A
) ) -1-1-onto-> A ) )  ->  sum_ k  e.  A  ( B  +  C )  =  ( sum_ k  e.  A  B  +  sum_ k  e.  A  C
) )
183182expr 372 . . . 4  |-  ( (
ph  /\  ( `  A
)  e.  NN )  ->  ( f : ( 1 ... ( `  A ) ) -1-1-onto-> A  ->  sum_ k  e.  A  ( B  +  C )  =  ( sum_ k  e.  A  B  +  sum_ k  e.  A  C
) ) )
184183exlimdv 1775 . . 3  |-  ( (
ph  /\  ( `  A
)  e.  NN )  ->  ( E. f 
f : ( 1 ... ( `  A
) ) -1-1-onto-> A  ->  sum_ k  e.  A  ( B  +  C )  =  (
sum_ k  e.  A  B  +  sum_ k  e.  A  C ) ) )
185184expimpd 360 . 2  |-  ( ph  ->  ( ( ( `  A
)  e.  NN  /\  E. f  f : ( 1 ... ( `  A
) ) -1-1-onto-> A )  ->  sum_ k  e.  A  ( B  +  C )  =  (
sum_ k  e.  A  B  +  sum_ k  e.  A  C ) ) )
186 fsumadd.1 . . 3  |-  ( ph  ->  A  e.  Fin )
187 fz1f1o 11099 . . 3  |-  ( A  e.  Fin  ->  ( A  =  (/)  \/  (
( `  A )  e.  NN  /\  E. f 
f : ( 1 ... ( `  A
) ) -1-1-onto-> A ) ) )
188186, 187syl 14 . 2  |-  ( ph  ->  ( A  =  (/)  \/  ( ( `  A
)  e.  NN  /\  E. f  f : ( 1 ... ( `  A
) ) -1-1-onto-> A ) ) )
18912, 185, 188mpjaod 692 1  |-  ( ph  -> 
sum_ k  e.  A  ( B  +  C
)  =  ( sum_ k  e.  A  B  +  sum_ k  e.  A  C ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 103    \/ wo 682  DECID wdc 804    /\ w3a 947    = wceq 1316   E.wex 1453    e. wcel 1465   A.wral 2393   (/)c0 3333   ifcif 3444   class class class wbr 3899    |-> cmpt 3959    o. ccom 4513   -->wf 5089   -1-1-onto->wf1o 5092   ` cfv 5093  (class class class)co 5742   Fincfn 6602   CCcc 7586   0cc0 7588   1c1 7589    + caddc 7591    <_ cle 7769   NNcn 8684   ZZcz 9012   ZZ>=cuz 9282   ...cfz 9745    seqcseq 10173  ♯chash 10476   sum_csu 11077
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 588  ax-in2 589  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-13 1476  ax-14 1477  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099  ax-coll 4013  ax-sep 4016  ax-nul 4024  ax-pow 4068  ax-pr 4101  ax-un 4325  ax-setind 4422  ax-iinf 4472  ax-cnex 7679  ax-resscn 7680  ax-1cn 7681  ax-1re 7682  ax-icn 7683  ax-addcl 7684  ax-addrcl 7685  ax-mulcl 7686  ax-mulrcl 7687  ax-addcom 7688  ax-mulcom 7689  ax-addass 7690  ax-mulass 7691  ax-distr 7692  ax-i2m1 7693  ax-0lt1 7694  ax-1rid 7695  ax-0id 7696  ax-rnegex 7697  ax-precex 7698  ax-cnre 7699  ax-pre-ltirr 7700  ax-pre-ltwlin 7701  ax-pre-lttrn 7702  ax-pre-apti 7703  ax-pre-ltadd 7704  ax-pre-mulgt0 7705  ax-pre-mulext 7706  ax-arch 7707  ax-caucvg 7708
This theorem depends on definitions:  df-bi 116  df-dc 805  df-3or 948  df-3an 949  df-tru 1319  df-fal 1322  df-nf 1422  df-sb 1721  df-eu 1980  df-mo 1981  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-ne 2286  df-nel 2381  df-ral 2398  df-rex 2399  df-reu 2400  df-rmo 2401  df-rab 2402  df-v 2662  df-sbc 2883  df-csb 2976  df-dif 3043  df-un 3045  df-in 3047  df-ss 3054  df-nul 3334  df-if 3445  df-pw 3482  df-sn 3503  df-pr 3504  df-op 3506  df-uni 3707  df-int 3742  df-iun 3785  df-br 3900  df-opab 3960  df-mpt 3961  df-tr 3997  df-id 4185  df-po 4188  df-iso 4189  df-iord 4258  df-on 4260  df-ilim 4261  df-suc 4263  df-iom 4475  df-xp 4515  df-rel 4516  df-cnv 4517  df-co 4518  df-dm 4519  df-rn 4520  df-res 4521  df-ima 4522  df-iota 5058  df-fun 5095  df-fn 5096  df-f 5097  df-f1 5098  df-fo 5099  df-f1o 5100  df-fv 5101  df-isom 5102  df-riota 5698  df-ov 5745  df-oprab 5746  df-mpo 5747  df-1st 6006  df-2nd 6007  df-recs 6170  df-irdg 6235  df-frec 6256  df-1o 6281  df-oadd 6285  df-er 6397  df-en 6603  df-dom 6604  df-fin 6605  df-pnf 7770  df-mnf 7771  df-xr 7772  df-ltxr 7773  df-le 7774  df-sub 7903  df-neg 7904  df-reap 8304  df-ap 8311  df-div 8400  df-inn 8685  df-2 8743  df-3 8744  df-4 8745  df-n0 8936  df-z 9013  df-uz 9283  df-q 9368  df-rp 9398  df-fz 9746  df-fzo 9875  df-seqfrec 10174  df-exp 10248  df-ihash 10477  df-cj 10569  df-re 10570  df-im 10571  df-rsqrt 10725  df-abs 10726  df-clim 11003  df-sumdc 11078
This theorem is referenced by:  fsumsplit  11131  fsumsub  11176  binomlem  11207
  Copyright terms: Public domain W3C validator