Metamath Proof Explorer

Definition df-prod

Description: Define the product of a series with an index set of integers A . This definition takes most of the aspects of df-sum and adapts them for multiplication instead of addition. However, we insist that in the infinite case, there is a nonzero tail of the sequence. This ensures that the convergence criteria match those of infinite sums. (Contributed by Scott Fenton, 4-Dec-2017)

Ref Expression
Assertion df-prod 
|- prod_ k e. A B = ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 vk 
 |-  k
1 cA 
 |-  A
2 cB 
 |-  B
3 1 2 0 cprod 
 |-  prod_ k e. A B
4 vx 
 |-  x
5 vm 
 |-  m
6 cz 
 |-  ZZ
7 cuz 
 |-  ZZ>=
8 5 cv 
 |-  m
9 8 7 cfv 
 |-  ( ZZ>= ` m )
10 1 9 wss 
 |-  A C_ ( ZZ>= ` m )
11 vn 
 |-  n
12 vy 
 |-  y
13 12 cv 
 |-  y
14 cc0 
 |-  0
15 13 14 wne 
 |-  y =/= 0
16 11 cv 
 |-  n
17 cmul 
 |-  x.
18 0 cv 
 |-  k
19 18 1 wcel 
 |-  k e. A
20 c1 
 |-  1
21 19 2 20 cif 
 |-  if ( k e. A , B , 1 )
22 0 6 21 cmpt 
 |-  ( k e. ZZ |-> if ( k e. A , B , 1 ) )
23 17 22 16 cseq 
 |-  seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) )
24 cli 
 |-  ~~>
25 23 13 24 wbr 
 |-  seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y
26 15 25 wa 
 |-  ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y )
27 26 12 wex 
 |-  E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y )
28 27 11 9 wrex 
 |-  E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y )
29 17 22 8 cseq 
 |-  seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) )
30 4 cv 
 |-  x
31 29 30 24 wbr 
 |-  seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x
32 10 28 31 w3a 
 |-  ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x )
33 32 5 6 wrex 
 |-  E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x )
34 cn 
 |-  NN
35 vf 
 |-  f
36 35 cv 
 |-  f
37 cfz 
 |-  ...
38 20 8 37 co 
 |-  ( 1 ... m )
39 38 1 36 wf1o 
 |-  f : ( 1 ... m ) -1-1-onto-> A
40 16 36 cfv 
 |-  ( f ` n )
41 0 40 2 csb 
 |-  [_ ( f ` n ) / k ]_ B
42 11 34 41 cmpt 
 |-  ( n e. NN |-> [_ ( f ` n ) / k ]_ B )
43 17 42 20 cseq 
 |-  seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) )
44 8 43 cfv 
 |-  ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m )
45 30 44 wceq 
 |-  x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m )
46 39 45 wa 
 |-  ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) )
47 46 35 wex 
 |-  E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) )
48 47 5 34 wrex 
 |-  E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) )
49 33 48 wo 
 |-  ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) )
50 49 4 cio 
 |-  ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) )
51 3 50 wceq 
 |-  prod_ k e. A B = ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) )