Description: Write a double product as a product over a two-dimensional region. Compare fsum2d . (Contributed by Scott Fenton, 30-Jan-2018)
Ref | Expression | ||
---|---|---|---|
Hypotheses | fprod2d.1 | |
|
fprod2d.2 | |
||
fprod2d.3 | |
||
fprod2d.4 | |
||
Assertion | fprod2d | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fprod2d.1 | |
|
2 | fprod2d.2 | |
|
3 | fprod2d.3 | |
|
4 | fprod2d.4 | |
|
5 | ssid | |
|
6 | sseq1 | |
|
7 | prodeq1 | |
|
8 | iuneq1 | |
|
9 | 0iun | |
|
10 | 8 9 | eqtrdi | |
11 | 10 | prodeq1d | |
12 | 7 11 | eqeq12d | |
13 | 6 12 | imbi12d | |
14 | 13 | imbi2d | |
15 | sseq1 | |
|
16 | prodeq1 | |
|
17 | iuneq1 | |
|
18 | 17 | prodeq1d | |
19 | 16 18 | eqeq12d | |
20 | 15 19 | imbi12d | |
21 | 20 | imbi2d | |
22 | sseq1 | |
|
23 | prodeq1 | |
|
24 | iuneq1 | |
|
25 | 24 | prodeq1d | |
26 | 23 25 | eqeq12d | |
27 | 22 26 | imbi12d | |
28 | 27 | imbi2d | |
29 | sseq1 | |
|
30 | prodeq1 | |
|
31 | iuneq1 | |
|
32 | 31 | prodeq1d | |
33 | 30 32 | eqeq12d | |
34 | 29 33 | imbi12d | |
35 | 34 | imbi2d | |
36 | prod0 | |
|
37 | prod0 | |
|
38 | 36 37 | eqtr4i | |
39 | 38 | 2a1i | |
40 | ssun1 | |
|
41 | sstr | |
|
42 | 40 41 | mpan | |
43 | 42 | imim1i | |
44 | 2 | ad2antrr | |
45 | 3 | ad4ant14 | |
46 | 4 | ad4ant14 | |
47 | simplr | |
|
48 | simpr | |
|
49 | biid | |
|
50 | 1 44 45 46 47 48 49 | fprod2dlem | |
51 | 50 | exp31 | |
52 | 51 | a2d | |
53 | 43 52 | syl5 | |
54 | 53 | expcom | |
55 | 54 | a2d | |
56 | 55 | adantl | |
57 | 14 21 28 35 39 56 | findcard2s | |
58 | 2 57 | mpcom | |
59 | 5 58 | mpi | |