Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fprodabs Structured version   Unicode version

Theorem fprodabs 27335
Description: The absolute value of a finite product. (Contributed by Scott Fenton, 25-Dec-2017.)
Hypotheses
Ref Expression
fprodabs.1  |-  Z  =  ( ZZ>= `  M )
fprodabs.2  |-  ( ph  ->  N  e.  Z )
fprodabs.3  |-  ( (
ph  /\  k  e.  Z )  ->  A  e.  CC )
Assertion
Ref Expression
fprodabs  |-  ( ph  ->  ( abs `  prod_ k  e.  ( M ... N ) A )  =  prod_ k  e.  ( M ... N ) ( abs `  A
) )
Distinct variable groups:    ph, k    k, M    k, N    k, Z
Allowed substitution hint:    A( k)

Proof of Theorem fprodabs
Dummy variables  a  n are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fprodabs.2 . . 3  |-  ( ph  ->  N  e.  Z )
2 fprodabs.1 . . 3  |-  Z  =  ( ZZ>= `  M )
31, 2syl6eleq 2527 . 2  |-  ( ph  ->  N  e.  ( ZZ>= `  M ) )
4 oveq2 6092 . . . . . . 7  |-  ( a  =  M  ->  ( M ... a )  =  ( M ... M
) )
54prodeq1d 27285 . . . . . 6  |-  ( a  =  M  ->  prod_ k  e.  ( M ... a ) A  = 
prod_ k  e.  ( M ... M ) A )
65fveq2d 5687 . . . . 5  |-  ( a  =  M  ->  ( abs `  prod_ k  e.  ( M ... a ) A )  =  ( abs `  prod_ k  e.  ( M ... M
) A ) )
74prodeq1d 27285 . . . . 5  |-  ( a  =  M  ->  prod_ k  e.  ( M ... a ) ( abs `  A )  =  prod_ k  e.  ( M ... M ) ( abs `  A ) )
86, 7eqeq12d 2451 . . . 4  |-  ( a  =  M  ->  (
( abs `  prod_ k  e.  ( M ... a ) A )  =  prod_ k  e.  ( M ... a ) ( abs `  A
)  <->  ( abs `  prod_ k  e.  ( M ... M ) A )  =  prod_ k  e.  ( M ... M ) ( abs `  A
) ) )
98imbi2d 316 . . 3  |-  ( a  =  M  ->  (
( ph  ->  ( abs `  prod_ k  e.  ( M ... a ) A )  =  prod_ k  e.  ( M ... a ) ( abs `  A ) )  <->  ( ph  ->  ( abs `  prod_ k  e.  ( M ... M ) A )  =  prod_ k  e.  ( M ... M ) ( abs `  A
) ) ) )
10 oveq2 6092 . . . . . . 7  |-  ( a  =  n  ->  ( M ... a )  =  ( M ... n
) )
1110prodeq1d 27285 . . . . . 6  |-  ( a  =  n  ->  prod_ k  e.  ( M ... a ) A  = 
prod_ k  e.  ( M ... n ) A )
1211fveq2d 5687 . . . . 5  |-  ( a  =  n  ->  ( abs `  prod_ k  e.  ( M ... a ) A )  =  ( abs `  prod_ k  e.  ( M ... n
) A ) )
1310prodeq1d 27285 . . . . 5  |-  ( a  =  n  ->  prod_ k  e.  ( M ... a ) ( abs `  A )  =  prod_ k  e.  ( M ... n ) ( abs `  A ) )
1412, 13eqeq12d 2451 . . . 4  |-  ( a  =  n  ->  (
( abs `  prod_ k  e.  ( M ... a ) A )  =  prod_ k  e.  ( M ... a ) ( abs `  A
)  <->  ( abs `  prod_ k  e.  ( M ... n ) A )  =  prod_ k  e.  ( M ... n ) ( abs `  A
) ) )
1514imbi2d 316 . . 3  |-  ( a  =  n  ->  (
( ph  ->  ( abs `  prod_ k  e.  ( M ... a ) A )  =  prod_ k  e.  ( M ... a ) ( abs `  A ) )  <->  ( ph  ->  ( abs `  prod_ k  e.  ( M ... n ) A )  =  prod_ k  e.  ( M ... n ) ( abs `  A
) ) ) )
16 oveq2 6092 . . . . . . 7  |-  ( a  =  ( n  + 
1 )  ->  ( M ... a )  =  ( M ... (
n  +  1 ) ) )
1716prodeq1d 27285 . . . . . 6  |-  ( a  =  ( n  + 
1 )  ->  prod_ k  e.  ( M ... a ) A  = 
prod_ k  e.  ( M ... ( n  + 
1 ) ) A )
1817fveq2d 5687 . . . . 5  |-  ( a  =  ( n  + 
1 )  ->  ( abs `  prod_ k  e.  ( M ... a ) A )  =  ( abs `  prod_ k  e.  ( M ... (
n  +  1 ) ) A ) )
1916prodeq1d 27285 . . . . 5  |-  ( a  =  ( n  + 
1 )  ->  prod_ k  e.  ( M ... a ) ( abs `  A )  =  prod_ k  e.  ( M ... ( n  +  1
) ) ( abs `  A ) )
2018, 19eqeq12d 2451 . . . 4  |-  ( a  =  ( n  + 
1 )  ->  (
( abs `  prod_ k  e.  ( M ... a ) A )  =  prod_ k  e.  ( M ... a ) ( abs `  A
)  <->  ( abs `  prod_ k  e.  ( M ... ( n  +  1
) ) A )  =  prod_ k  e.  ( M ... ( n  +  1 ) ) ( abs `  A
) ) )
2120imbi2d 316 . . 3  |-  ( a  =  ( n  + 
1 )  ->  (
( ph  ->  ( abs `  prod_ k  e.  ( M ... a ) A )  =  prod_ k  e.  ( M ... a ) ( abs `  A ) )  <->  ( ph  ->  ( abs `  prod_ k  e.  ( M ... ( n  +  1
) ) A )  =  prod_ k  e.  ( M ... ( n  +  1 ) ) ( abs `  A
) ) ) )
22 oveq2 6092 . . . . . . 7  |-  ( a  =  N  ->  ( M ... a )  =  ( M ... N
) )
2322prodeq1d 27285 . . . . . 6  |-  ( a  =  N  ->  prod_ k  e.  ( M ... a ) A  = 
prod_ k  e.  ( M ... N ) A )
2423fveq2d 5687 . . . . 5  |-  ( a  =  N  ->  ( abs `  prod_ k  e.  ( M ... a ) A )  =  ( abs `  prod_ k  e.  ( M ... N
) A ) )
2522prodeq1d 27285 . . . . 5  |-  ( a  =  N  ->  prod_ k  e.  ( M ... a ) ( abs `  A )  =  prod_ k  e.  ( M ... N ) ( abs `  A ) )
2624, 25eqeq12d 2451 . . . 4  |-  ( a  =  N  ->  (
( abs `  prod_ k  e.  ( M ... a ) A )  =  prod_ k  e.  ( M ... a ) ( abs `  A
)  <->  ( abs `  prod_ k  e.  ( M ... N ) A )  =  prod_ k  e.  ( M ... N ) ( abs `  A
) ) )
2726imbi2d 316 . . 3  |-  ( a  =  N  ->  (
( ph  ->  ( abs `  prod_ k  e.  ( M ... a ) A )  =  prod_ k  e.  ( M ... a ) ( abs `  A ) )  <->  ( ph  ->  ( abs `  prod_ k  e.  ( M ... N ) A )  =  prod_ k  e.  ( M ... N ) ( abs `  A
) ) ) )
28 csbfv2g 5719 . . . . . 6  |-  ( M  e.  ZZ  ->  [_ M  /  k ]_ ( abs `  A )  =  ( abs `  [_ M  /  k ]_ A
) )
2928adantl 463 . . . . 5  |-  ( (
ph  /\  M  e.  ZZ )  ->  [_ M  /  k ]_ ( abs `  A )  =  ( abs `  [_ M  /  k ]_ A
) )
30 fzsn 11491 . . . . . . . 8  |-  ( M  e.  ZZ  ->  ( M ... M )  =  { M } )
3130adantl 463 . . . . . . 7  |-  ( (
ph  /\  M  e.  ZZ )  ->  ( M ... M )  =  { M } )
3231prodeq1d 27285 . . . . . 6  |-  ( (
ph  /\  M  e.  ZZ )  ->  prod_ k  e.  ( M ... M
) ( abs `  A
)  =  prod_ k  e.  { M }  ( abs `  A ) )
33 simpr 458 . . . . . . 7  |-  ( (
ph  /\  M  e.  ZZ )  ->  M  e.  ZZ )
34 uzid 10867 . . . . . . . . . . . 12  |-  ( M  e.  ZZ  ->  M  e.  ( ZZ>= `  M )
)
3534, 2syl6eleqr 2528 . . . . . . . . . . 11  |-  ( M  e.  ZZ  ->  M  e.  Z )
36 fprodabs.3 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  Z )  ->  A  e.  CC )
3736ralrimiva 2793 . . . . . . . . . . . 12  |-  ( ph  ->  A. k  e.  Z  A  e.  CC )
38 nfcsb1v 3296 . . . . . . . . . . . . . 14  |-  F/_ k [_ M  /  k ]_ A
3938nfel1 2583 . . . . . . . . . . . . 13  |-  F/ k
[_ M  /  k ]_ A  e.  CC
40 csbeq1a 3289 . . . . . . . . . . . . . 14  |-  ( k  =  M  ->  A  =  [_ M  /  k ]_ A )
4140eleq1d 2503 . . . . . . . . . . . . 13  |-  ( k  =  M  ->  ( A  e.  CC  <->  [_ M  / 
k ]_ A  e.  CC ) )
4239, 41rspc 3060 . . . . . . . . . . . 12  |-  ( M  e.  Z  ->  ( A. k  e.  Z  A  e.  CC  ->  [_ M  /  k ]_ A  e.  CC )
)
4337, 42mpan9 466 . . . . . . . . . . 11  |-  ( (
ph  /\  M  e.  Z )  ->  [_ M  /  k ]_ A  e.  CC )
4435, 43sylan2 471 . . . . . . . . . 10  |-  ( (
ph  /\  M  e.  ZZ )  ->  [_ M  /  k ]_ A  e.  CC )
4544abscld 12910 . . . . . . . . 9  |-  ( (
ph  /\  M  e.  ZZ )  ->  ( abs `  [_ M  /  k ]_ A )  e.  RR )
4645recnd 9404 . . . . . . . 8  |-  ( (
ph  /\  M  e.  ZZ )  ->  ( abs `  [_ M  /  k ]_ A )  e.  CC )
4729, 46eqeltrd 2511 . . . . . . 7  |-  ( (
ph  /\  M  e.  ZZ )  ->  [_ M  /  k ]_ ( abs `  A )  e.  CC )
48 prodsns 27333 . . . . . . 7  |-  ( ( M  e.  ZZ  /\  [_ M  /  k ]_ ( abs `  A )  e.  CC )  ->  prod_ k  e.  { M }  ( abs `  A
)  =  [_ M  /  k ]_ ( abs `  A ) )
4933, 47, 48syl2anc 656 . . . . . 6  |-  ( (
ph  /\  M  e.  ZZ )  ->  prod_ k  e.  { M }  ( abs `  A )  = 
[_ M  /  k ]_ ( abs `  A
) )
5032, 49eqtrd 2469 . . . . 5  |-  ( (
ph  /\  M  e.  ZZ )  ->  prod_ k  e.  ( M ... M
) ( abs `  A
)  =  [_ M  /  k ]_ ( abs `  A ) )
5130prodeq1d 27285 . . . . . . . 8  |-  ( M  e.  ZZ  ->  prod_ k  e.  ( M ... M ) A  = 
prod_ k  e.  { M } A )
5251adantl 463 . . . . . . 7  |-  ( (
ph  /\  M  e.  ZZ )  ->  prod_ k  e.  ( M ... M
) A  =  prod_ k  e.  { M } A )
53 prodsns 27333 . . . . . . . 8  |-  ( ( M  e.  ZZ  /\  [_ M  /  k ]_ A  e.  CC )  ->  prod_ k  e.  { M } A  =  [_ M  /  k ]_ A
)
5433, 44, 53syl2anc 656 . . . . . . 7  |-  ( (
ph  /\  M  e.  ZZ )  ->  prod_ k  e.  { M } A  =  [_ M  /  k ]_ A )
5552, 54eqtrd 2469 . . . . . 6  |-  ( (
ph  /\  M  e.  ZZ )  ->  prod_ k  e.  ( M ... M
) A  =  [_ M  /  k ]_ A
)
5655fveq2d 5687 . . . . 5  |-  ( (
ph  /\  M  e.  ZZ )  ->  ( abs `  prod_ k  e.  ( M ... M ) A )  =  ( abs `  [_ M  /  k ]_ A
) )
5729, 50, 563eqtr4rd 2480 . . . 4  |-  ( (
ph  /\  M  e.  ZZ )  ->  ( abs `  prod_ k  e.  ( M ... M ) A )  =  prod_ k  e.  ( M ... M ) ( abs `  A ) )
5857expcom 435 . . 3  |-  ( M  e.  ZZ  ->  ( ph  ->  ( abs `  prod_ k  e.  ( M ... M ) A )  =  prod_ k  e.  ( M ... M ) ( abs `  A
) ) )
59 simp3 985 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( ZZ>= `  M )  /\  ( abs `  prod_ k  e.  ( M ... n ) A )  =  prod_ k  e.  ( M ... n ) ( abs `  A
) )  ->  ( abs `  prod_ k  e.  ( M ... n ) A )  =  prod_ k  e.  ( M ... n ) ( abs `  A ) )
60 ovex 6109 . . . . . . . . . . 11  |-  ( n  +  1 )  e. 
_V
61 csbfv2g 5719 . . . . . . . . . . 11  |-  ( ( n  +  1 )  e.  _V  ->  [_ (
n  +  1 )  /  k ]_ ( abs `  A )  =  ( abs `  [_ (
n  +  1 )  /  k ]_ A
) )
6260, 61ax-mp 5 . . . . . . . . . 10  |-  [_ (
n  +  1 )  /  k ]_ ( abs `  A )  =  ( abs `  [_ (
n  +  1 )  /  k ]_ A
)
6362eqcomi 2441 . . . . . . . . 9  |-  ( abs `  [_ ( n  + 
1 )  /  k ]_ A )  =  [_ ( n  +  1
)  /  k ]_ ( abs `  A )
6463a1i 11 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( ZZ>= `  M )  /\  ( abs `  prod_ k  e.  ( M ... n ) A )  =  prod_ k  e.  ( M ... n ) ( abs `  A
) )  ->  ( abs `  [_ ( n  +  1 )  / 
k ]_ A )  = 
[_ ( n  + 
1 )  /  k ]_ ( abs `  A
) )
6559, 64oveq12d 6102 . . . . . . 7  |-  ( (
ph  /\  n  e.  ( ZZ>= `  M )  /\  ( abs `  prod_ k  e.  ( M ... n ) A )  =  prod_ k  e.  ( M ... n ) ( abs `  A
) )  ->  (
( abs `  prod_ k  e.  ( M ... n ) A )  x.  ( abs `  [_ (
n  +  1 )  /  k ]_ A
) )  =  (
prod_ k  e.  ( M ... n ) ( abs `  A )  x.  [_ ( n  +  1 )  / 
k ]_ ( abs `  A
) ) )
66 simpr 458 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( ZZ>= `  M )
)  ->  n  e.  ( ZZ>= `  M )
)
67 elfzuz 11440 . . . . . . . . . . . . . 14  |-  ( k  e.  ( M ... ( n  +  1
) )  ->  k  e.  ( ZZ>= `  M )
)
6867, 2syl6eleqr 2528 . . . . . . . . . . . . 13  |-  ( k  e.  ( M ... ( n  +  1
) )  ->  k  e.  Z )
6968, 36sylan2 471 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( M ... ( n  +  1 ) ) )  ->  A  e.  CC )
7069adantlr 709 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  ( ZZ>= `  M )
)  /\  k  e.  ( M ... ( n  +  1 ) ) )  ->  A  e.  CC )
7166, 70fprodp1s 27332 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( ZZ>= `  M )
)  ->  prod_ k  e.  ( M ... (
n  +  1 ) ) A  =  (
prod_ k  e.  ( M ... n ) A  x.  [_ ( n  +  1 )  / 
k ]_ A ) )
7271fveq2d 5687 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( ZZ>= `  M )
)  ->  ( abs ` 
prod_ k  e.  ( M ... ( n  + 
1 ) ) A )  =  ( abs `  ( prod_ k  e.  ( M ... n ) A  x.  [_ (
n  +  1 )  /  k ]_ A
) ) )
73 fzfid 11783 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( ZZ>= `  M )
)  ->  ( M ... n )  e.  Fin )
74 elfzuz 11440 . . . . . . . . . . . . . 14  |-  ( k  e.  ( M ... n )  ->  k  e.  ( ZZ>= `  M )
)
7574, 2syl6eleqr 2528 . . . . . . . . . . . . 13  |-  ( k  e.  ( M ... n )  ->  k  e.  Z )
7675, 36sylan2 471 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( M ... n ) )  ->  A  e.  CC )
7776adantlr 709 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  ( ZZ>= `  M )
)  /\  k  e.  ( M ... n ) )  ->  A  e.  CC )
7873, 77fprodcl 27316 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( ZZ>= `  M )
)  ->  prod_ k  e.  ( M ... n
) A  e.  CC )
79 peano2uz 10900 . . . . . . . . . . . 12  |-  ( n  e.  ( ZZ>= `  M
)  ->  ( n  +  1 )  e.  ( ZZ>= `  M )
)
8079, 2syl6eleqr 2528 . . . . . . . . . . 11  |-  ( n  e.  ( ZZ>= `  M
)  ->  ( n  +  1 )  e.  Z )
81 nfcsb1v 3296 . . . . . . . . . . . . . 14  |-  F/_ k [_ ( n  +  1 )  /  k ]_ A
8281nfel1 2583 . . . . . . . . . . . . 13  |-  F/ k
[_ ( n  + 
1 )  /  k ]_ A  e.  CC
83 csbeq1a 3289 . . . . . . . . . . . . . 14  |-  ( k  =  ( n  + 
1 )  ->  A  =  [_ ( n  + 
1 )  /  k ]_ A )
8483eleq1d 2503 . . . . . . . . . . . . 13  |-  ( k  =  ( n  + 
1 )  ->  ( A  e.  CC  <->  [_ ( n  +  1 )  / 
k ]_ A  e.  CC ) )
8582, 84rspc 3060 . . . . . . . . . . . 12  |-  ( ( n  +  1 )  e.  Z  ->  ( A. k  e.  Z  A  e.  CC  ->  [_ ( n  +  1 )  /  k ]_ A  e.  CC )
)
8637, 85mpan9 466 . . . . . . . . . . 11  |-  ( (
ph  /\  ( n  +  1 )  e.  Z )  ->  [_ (
n  +  1 )  /  k ]_ A  e.  CC )
8780, 86sylan2 471 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( ZZ>= `  M )
)  ->  [_ ( n  +  1 )  / 
k ]_ A  e.  CC )
8878, 87absmuld 12928 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( ZZ>= `  M )
)  ->  ( abs `  ( prod_ k  e.  ( M ... n ) A  x.  [_ (
n  +  1 )  /  k ]_ A
) )  =  ( ( abs `  prod_ k  e.  ( M ... n ) A )  x.  ( abs `  [_ (
n  +  1 )  /  k ]_ A
) ) )
8972, 88eqtrd 2469 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( ZZ>= `  M )
)  ->  ( abs ` 
prod_ k  e.  ( M ... ( n  + 
1 ) ) A )  =  ( ( abs `  prod_ k  e.  ( M ... n
) A )  x.  ( abs `  [_ (
n  +  1 )  /  k ]_ A
) ) )
90893adant3 1003 . . . . . . 7  |-  ( (
ph  /\  n  e.  ( ZZ>= `  M )  /\  ( abs `  prod_ k  e.  ( M ... n ) A )  =  prod_ k  e.  ( M ... n ) ( abs `  A
) )  ->  ( abs `  prod_ k  e.  ( M ... ( n  +  1 ) ) A )  =  ( ( abs `  prod_ k  e.  ( M ... n ) A )  x.  ( abs `  [_ (
n  +  1 )  /  k ]_ A
) ) )
9170abscld 12910 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  ( ZZ>= `  M )
)  /\  k  e.  ( M ... ( n  +  1 ) ) )  ->  ( abs `  A )  e.  RR )
9291recnd 9404 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  ( ZZ>= `  M )
)  /\  k  e.  ( M ... ( n  +  1 ) ) )  ->  ( abs `  A )  e.  CC )
9366, 92fprodp1s 27332 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( ZZ>= `  M )
)  ->  prod_ k  e.  ( M ... (
n  +  1 ) ) ( abs `  A
)  =  ( prod_
k  e.  ( M ... n ) ( abs `  A )  x.  [_ ( n  +  1 )  / 
k ]_ ( abs `  A
) ) )
94933adant3 1003 . . . . . . 7  |-  ( (
ph  /\  n  e.  ( ZZ>= `  M )  /\  ( abs `  prod_ k  e.  ( M ... n ) A )  =  prod_ k  e.  ( M ... n ) ( abs `  A
) )  ->  prod_ k  e.  ( M ... ( n  +  1
) ) ( abs `  A )  =  (
prod_ k  e.  ( M ... n ) ( abs `  A )  x.  [_ ( n  +  1 )  / 
k ]_ ( abs `  A
) ) )
9565, 90, 943eqtr4d 2479 . . . . . 6  |-  ( (
ph  /\  n  e.  ( ZZ>= `  M )  /\  ( abs `  prod_ k  e.  ( M ... n ) A )  =  prod_ k  e.  ( M ... n ) ( abs `  A
) )  ->  ( abs `  prod_ k  e.  ( M ... ( n  +  1 ) ) A )  =  prod_ k  e.  ( M ... ( n  +  1
) ) ( abs `  A ) )
96953exp 1181 . . . . 5  |-  ( ph  ->  ( n  e.  (
ZZ>= `  M )  -> 
( ( abs `  prod_ k  e.  ( M ... n ) A )  =  prod_ k  e.  ( M ... n ) ( abs `  A
)  ->  ( abs ` 
prod_ k  e.  ( M ... ( n  + 
1 ) ) A )  =  prod_ k  e.  ( M ... (
n  +  1 ) ) ( abs `  A
) ) ) )
9796com12 31 . . . 4  |-  ( n  e.  ( ZZ>= `  M
)  ->  ( ph  ->  ( ( abs `  prod_ k  e.  ( M ... n ) A )  =  prod_ k  e.  ( M ... n ) ( abs `  A
)  ->  ( abs ` 
prod_ k  e.  ( M ... ( n  + 
1 ) ) A )  =  prod_ k  e.  ( M ... (
n  +  1 ) ) ( abs `  A
) ) ) )
9897a2d 26 . . 3  |-  ( n  e.  ( ZZ>= `  M
)  ->  ( ( ph  ->  ( abs `  prod_ k  e.  ( M ... n ) A )  =  prod_ k  e.  ( M ... n ) ( abs `  A
) )  ->  ( ph  ->  ( abs `  prod_ k  e.  ( M ... ( n  +  1
) ) A )  =  prod_ k  e.  ( M ... ( n  +  1 ) ) ( abs `  A
) ) ) )
999, 15, 21, 27, 58, 98uzind4 10904 . 2  |-  ( N  e.  ( ZZ>= `  M
)  ->  ( ph  ->  ( abs `  prod_ k  e.  ( M ... N ) A )  =  prod_ k  e.  ( M ... N ) ( abs `  A
) ) )
1003, 99mpcom 36 1  |-  ( ph  ->  ( abs `  prod_ k  e.  ( M ... N ) A )  =  prod_ k  e.  ( M ... N ) ( abs `  A
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 960    = wceq 1364    e. wcel 1757   A.wral 2709   _Vcvv 2966   [_csb 3280   {csn 3869   ` cfv 5410  (class class class)co 6084   CCcc 9272   1c1 9275    + caddc 9277    x. cmul 9279   ZZcz 10638   ZZ>=cuz 10853   ...cfz 11428   abscabs 12711   prod_cprod 27269
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2418  ax-rep 4395  ax-sep 4405  ax-nul 4413  ax-pow 4462  ax-pr 4523  ax-un 6365  ax-inf2 7839  ax-cnex 9330  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-mulcom 9338  ax-addass 9339  ax-mulass 9340  ax-distr 9341  ax-i2m1 9342  ax-1ne0 9343  ax-1rid 9344  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349  ax-pre-ltadd 9350  ax-pre-mulgt0 9351  ax-pre-sup 9352
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-fal 1370  df-ex 1592  df-nf 1595  df-sb 1702  df-eu 2260  df-mo 2261  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-nel 2603  df-ral 2714  df-rex 2715  df-reu 2716  df-rmo 2717  df-rab 2718  df-v 2968  df-sbc 3180  df-csb 3281  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-pss 3336  df-nul 3630  df-if 3784  df-pw 3854  df-sn 3870  df-pr 3872  df-tp 3874  df-op 3876  df-uni 4084  df-int 4121  df-iun 4165  df-br 4285  df-opab 4343  df-mpt 4344  df-tr 4378  df-eprel 4623  df-id 4627  df-po 4632  df-so 4633  df-fr 4670  df-se 4671  df-we 4672  df-ord 4713  df-on 4714  df-lim 4715  df-suc 4716  df-xp 4837  df-rel 4838  df-cnv 4839  df-co 4840  df-dm 4841  df-rn 4842  df-res 4843  df-ima 4844  df-iota 5373  df-fun 5412  df-fn 5413  df-f 5414  df-f1 5415  df-fo 5416  df-f1o 5417  df-fv 5418  df-isom 5419  df-riota 6043  df-ov 6087  df-oprab 6088  df-mpt2 6089  df-om 6470  df-1st 6570  df-2nd 6571  df-recs 6822  df-rdg 6856  df-1o 6912  df-oadd 6916  df-er 7093  df-en 7303  df-dom 7304  df-sdom 7305  df-fin 7306  df-sup 7683  df-oi 7716  df-card 8101  df-pnf 9412  df-mnf 9413  df-xr 9414  df-ltxr 9415  df-le 9416  df-sub 9589  df-neg 9590  df-div 9986  df-nn 10315  df-2 10372  df-3 10373  df-n0 10572  df-z 10639  df-uz 10854  df-rp 10984  df-fz 11429  df-fzo 11537  df-seq 11795  df-exp 11854  df-hash 12092  df-cj 12576  df-re 12577  df-im 12578  df-sqr 12712  df-abs 12713  df-clim 12954  df-prod 27270
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator