Description: The product of two infinite products. (Contributed by Scott Fenton, 18-Dec-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | prodfmul.1 | |
|
prodfmul.2 | |
||
prodfmul.3 | |
||
prodfmul.4 | |
||
Assertion | prodfmul | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | prodfmul.1 | |
|
2 | prodfmul.2 | |
|
3 | prodfmul.3 | |
|
4 | prodfmul.4 | |
|
5 | mulcl | |
|
6 | 5 | adantl | |
7 | mulcom | |
|
8 | 7 | adantl | |
9 | mulass | |
|
10 | 9 | adantl | |
11 | 6 8 10 1 2 3 4 | seqcaopr | |