Metamath Proof Explorer

Theorem fprodabs

Description: The absolute value of a finite product. (Contributed by Scott Fenton, 25-Dec-2017)

Ref Expression
Hypotheses fprodabs.1 
|- Z = ( ZZ>= ` M )
fprodabs.2 
|- ( ph -> N e. Z )
fprodabs.3 
|- ( ( ph /\ k e. Z ) -> A e. CC )
Assertion fprodabs 
|- ( ph -> ( abs ` prod_ k e. ( M ... N ) A ) = prod_ k e. ( M ... N ) ( abs ` A ) )

Proof

Step Hyp Ref Expression
1 fprodabs.1 
 |-  Z = ( ZZ>= ` M )
2 fprodabs.2 
 |-  ( ph -> N e. Z )
3 fprodabs.3 
 |-  ( ( ph /\ k e. Z ) -> A e. CC )
4 2 1 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
5 oveq2 
 |-  ( a = M -> ( M ... a ) = ( M ... M ) )
6 5 prodeq1d 
 |-  ( a = M -> prod_ k e. ( M ... a ) A = prod_ k e. ( M ... M ) A )
7 6 fveq2d 
 |-  ( a = M -> ( abs ` prod_ k e. ( M ... a ) A ) = ( abs ` prod_ k e. ( M ... M ) A ) )
8 5 prodeq1d 
 |-  ( a = M -> prod_ k e. ( M ... a ) ( abs ` A ) = prod_ k e. ( M ... M ) ( abs ` A ) )
9 7 8 eqeq12d 
 |-  ( 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 ) ) )
10 9 imbi2d 
 |-  ( 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 ) ) ) )
11 oveq2 
 |-  ( a = n -> ( M ... a ) = ( M ... n ) )
12 11 prodeq1d 
 |-  ( a = n -> prod_ k e. ( M ... a ) A = prod_ k e. ( M ... n ) A )
13 12 fveq2d 
 |-  ( a = n -> ( abs ` prod_ k e. ( M ... a ) A ) = ( abs ` prod_ k e. ( M ... n ) A ) )
14 11 prodeq1d 
 |-  ( a = n -> prod_ k e. ( M ... a ) ( abs ` A ) = prod_ k e. ( M ... n ) ( abs ` A ) )
15 13 14 eqeq12d 
 |-  ( 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 ) ) )
16 15 imbi2d 
 |-  ( 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 ) ) ) )
17 oveq2 
 |-  ( a = ( n + 1 ) -> ( M ... a ) = ( M ... ( n + 1 ) ) )
18 17 prodeq1d 
 |-  ( a = ( n + 1 ) -> prod_ k e. ( M ... a ) A = prod_ k e. ( M ... ( n + 1 ) ) A )
19 18 fveq2d 
 |-  ( a = ( n + 1 ) -> ( abs ` prod_ k e. ( M ... a ) A ) = ( abs ` prod_ k e. ( M ... ( n + 1 ) ) A ) )
20 17 prodeq1d 
 |-  ( a = ( n + 1 ) -> prod_ k e. ( M ... a ) ( abs ` A ) = prod_ k e. ( M ... ( n + 1 ) ) ( abs ` A ) )
21 19 20 eqeq12d 
 |-  ( 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 ) ) )
22 21 imbi2d 
 |-  ( 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 ) ) ) )
23 oveq2 
 |-  ( a = N -> ( M ... a ) = ( M ... N ) )
24 23 prodeq1d 
 |-  ( a = N -> prod_ k e. ( M ... a ) A = prod_ k e. ( M ... N ) A )
25 24 fveq2d 
 |-  ( a = N -> ( abs ` prod_ k e. ( M ... a ) A ) = ( abs ` prod_ k e. ( M ... N ) A ) )
26 23 prodeq1d 
 |-  ( a = N -> prod_ k e. ( M ... a ) ( abs ` A ) = prod_ k e. ( M ... N ) ( abs ` A ) )
27 25 26 eqeq12d 
 |-  ( 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 ) ) )
28 27 imbi2d 
 |-  ( 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 ) ) ) )
29 csbfv2g 
 |-  ( M e. ZZ -> [_ M / k ]_ ( abs ` A ) = ( abs ` [_ M / k ]_ A ) )
30 29 adantl 
 |-  ( ( ph /\ M e. ZZ ) -> [_ M / k ]_ ( abs ` A ) = ( abs ` [_ M / k ]_ A ) )
31 fzsn 
 |-  ( M e. ZZ -> ( M ... M ) = { M } )
32 31 adantl 
 |-  ( ( ph /\ M e. ZZ ) -> ( M ... M ) = { M } )
33 32 prodeq1d 
 |-  ( ( ph /\ M e. ZZ ) -> prod_ k e. ( M ... M ) ( abs ` A ) = prod_ k e. { M } ( abs ` A ) )
34 simpr 
 |-  ( ( ph /\ M e. ZZ ) -> M e. ZZ )
35 uzid 
 |-  ( M e. ZZ -> M e. ( ZZ>= ` M ) )
36 35 1 eleqtrrdi 
 |-  ( M e. ZZ -> M e. Z )
37 3 ralrimiva 
 |-  ( ph -> A. k e. Z A e. CC )
38 nfcsb1v 
 |-  F/_ k [_ M / k ]_ A
39 38 nfel1 
 |-  F/ k [_ M / k ]_ A e. CC
40 csbeq1a 
 |-  ( k = M -> A = [_ M / k ]_ A )
41 40 eleq1d 
 |-  ( k = M -> ( A e. CC <-> [_ M / k ]_ A e. CC ) )
42 39 41 rspc 
 |-  ( M e. Z -> ( A. k e. Z A e. CC -> [_ M / k ]_ A e. CC ) )
43 37 42 mpan9 
 |-  ( ( ph /\ M e. Z ) -> [_ M / k ]_ A e. CC )
44 36 43 sylan2 
 |-  ( ( ph /\ M e. ZZ ) -> [_ M / k ]_ A e. CC )
45 44 abscld 
 |-  ( ( ph /\ M e. ZZ ) -> ( abs ` [_ M / k ]_ A ) e. RR )
46 45 recnd 
 |-  ( ( ph /\ M e. ZZ ) -> ( abs ` [_ M / k ]_ A ) e. CC )
47 30 46 eqeltrd 
 |-  ( ( ph /\ M e. ZZ ) -> [_ M / k ]_ ( abs ` A ) e. CC )
48 prodsns 
 |-  ( ( M e. ZZ /\ [_ M / k ]_ ( abs ` A ) e. CC ) -> prod_ k e. { M } ( abs ` A ) = [_ M / k ]_ ( abs ` A ) )
49 34 47 48 syl2anc 
 |-  ( ( ph /\ M e. ZZ ) -> prod_ k e. { M } ( abs ` A ) = [_ M / k ]_ ( abs ` A ) )
50 33 49 eqtrd 
 |-  ( ( ph /\ M e. ZZ ) -> prod_ k e. ( M ... M ) ( abs ` A ) = [_ M / k ]_ ( abs ` A ) )
51 31 prodeq1d 
 |-  ( M e. ZZ -> prod_ k e. ( M ... M ) A = prod_ k e. { M } A )
52 51 adantl 
 |-  ( ( ph /\ M e. ZZ ) -> prod_ k e. ( M ... M ) A = prod_ k e. { M } A )
53 prodsns 
 |-  ( ( M e. ZZ /\ [_ M / k ]_ A e. CC ) -> prod_ k e. { M } A = [_ M / k ]_ A )
54 34 44 53 syl2anc 
 |-  ( ( ph /\ M e. ZZ ) -> prod_ k e. { M } A = [_ M / k ]_ A )
55 52 54 eqtrd 
 |-  ( ( ph /\ M e. ZZ ) -> prod_ k e. ( M ... M ) A = [_ M / k ]_ A )
56 55 fveq2d 
 |-  ( ( ph /\ M e. ZZ ) -> ( abs ` prod_ k e. ( M ... M ) A ) = ( abs ` [_ M / k ]_ A ) )
57 30 50 56 3eqtr4rd 
 |-  ( ( ph /\ M e. ZZ ) -> ( abs ` prod_ k e. ( M ... M ) A ) = prod_ k e. ( M ... M ) ( abs ` A ) )
58 57 expcom 
 |-  ( M e. ZZ -> ( ph -> ( abs ` prod_ k e. ( M ... M ) A ) = prod_ k e. ( M ... M ) ( abs ` A ) ) )
59 simp3 
 |-  ( ( 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 
 |-  ( n + 1 ) e. _V
61 csbfv2g 
 |-  ( ( n + 1 ) e. _V -> [_ ( n + 1 ) / k ]_ ( abs ` A ) = ( abs ` [_ ( n + 1 ) / k ]_ A ) )
62 60 61 ax-mp 
 |-  [_ ( n + 1 ) / k ]_ ( abs ` A ) = ( abs ` [_ ( n + 1 ) / k ]_ A )
63 62 eqcomi 
 |-  ( abs ` [_ ( n + 1 ) / k ]_ A ) = [_ ( n + 1 ) / k ]_ ( abs ` A )
64 63 a1i 
 |-  ( ( 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 ) )
65 59 64 oveq12d 
 |-  ( ( 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 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> n e. ( ZZ>= ` M ) )
67 elfzuz 
 |-  ( k e. ( M ... ( n + 1 ) ) -> k e. ( ZZ>= ` M ) )
68 67 1 eleqtrrdi 
 |-  ( k e. ( M ... ( n + 1 ) ) -> k e. Z )
69 68 3 sylan2 
 |-  ( ( ph /\ k e. ( M ... ( n + 1 ) ) ) -> A e. CC )
70 69 adantlr 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` M ) ) /\ k e. ( M ... ( n + 1 ) ) ) -> A e. CC )
71 66 70 fprodp1s 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> prod_ k e. ( M ... ( n + 1 ) ) A = ( prod_ k e. ( M ... n ) A x. [_ ( n + 1 ) / k ]_ A ) )
72 71 fveq2d 
 |-  ( ( 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 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( M ... n ) e. Fin )
74 elfzuz 
 |-  ( k e. ( M ... n ) -> k e. ( ZZ>= ` M ) )
75 74 1 eleqtrrdi 
 |-  ( k e. ( M ... n ) -> k e. Z )
76 75 3 sylan2 
 |-  ( ( ph /\ k e. ( M ... n ) ) -> A e. CC )
77 76 adantlr 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` M ) ) /\ k e. ( M ... n ) ) -> A e. CC )
78 73 77 fprodcl 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> prod_ k e. ( M ... n ) A e. CC )
79 peano2uz 
 |-  ( n e. ( ZZ>= ` M ) -> ( n + 1 ) e. ( ZZ>= ` M ) )
80 79 1 eleqtrrdi 
 |-  ( n e. ( ZZ>= ` M ) -> ( n + 1 ) e. Z )
81 nfcsb1v 
 |-  F/_ k [_ ( n + 1 ) / k ]_ A
82 81 nfel1 
 |-  F/ k [_ ( n + 1 ) / k ]_ A e. CC
83 csbeq1a 
 |-  ( k = ( n + 1 ) -> A = [_ ( n + 1 ) / k ]_ A )
84 83 eleq1d 
 |-  ( k = ( n + 1 ) -> ( A e. CC <-> [_ ( n + 1 ) / k ]_ A e. CC ) )
85 82 84 rspc 
 |-  ( ( n + 1 ) e. Z -> ( A. k e. Z A e. CC -> [_ ( n + 1 ) / k ]_ A e. CC ) )
86 37 85 mpan9 
 |-  ( ( ph /\ ( n + 1 ) e. Z ) -> [_ ( n + 1 ) / k ]_ A e. CC )
87 80 86 sylan2 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> [_ ( n + 1 ) / k ]_ A e. CC )
88 78 87 absmuld 
 |-  ( ( 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 ) ) )
89 72 88 eqtrd 
 |-  ( ( 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 ) ) )
90 89 3adant3 
 |-  ( ( 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 ) ) )
91 70 abscld 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` M ) ) /\ k e. ( M ... ( n + 1 ) ) ) -> ( abs ` A ) e. RR )
92 91 recnd 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` M ) ) /\ k e. ( M ... ( n + 1 ) ) ) -> ( abs ` A ) e. CC )
93 66 92 fprodp1s 
 |-  ( ( 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 ) ) )
94 93 3adant3 
 |-  ( ( 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 ) ) )
95 65 90 94 3eqtr4d 
 |-  ( ( 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 ) )
96 95 3exp 
 |-  ( 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 ) ) ) )
97 96 com12 
 |-  ( 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 ) ) ) )
98 97 a2d 
 |-  ( 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 ) ) ) )
99 10 16 22 28 58 98 uzind4 
 |-  ( N e. ( ZZ>= ` M ) -> ( ph -> ( abs ` prod_ k e. ( M ... N ) A ) = prod_ k e. ( M ... N ) ( abs ` A ) ) )
100 4 99 mpcom 
 |-  ( ph -> ( abs ` prod_ k e. ( M ... N ) A ) = prod_ k e. ( M ... N ) ( abs ` A ) )