Description: Split a finite product into two parts. (Contributed by Scott Fenton, 16-Dec-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | fprodsplit.1 | |
|
fprodsplit.2 | |
||
fprodsplit.3 | |
||
fprodsplit.4 | |
||
Assertion | fprodsplit | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fprodsplit.1 | |
|
2 | fprodsplit.2 | |
|
3 | fprodsplit.3 | |
|
4 | fprodsplit.4 | |
|
5 | iftrue | |
|
6 | 5 | prodeq2i | |
7 | ssun1 | |
|
8 | 7 2 | sseqtrrid | |
9 | 5 | adantl | |
10 | 8 | sselda | |
11 | 10 4 | syldan | |
12 | 9 11 | eqeltrd | |
13 | eldifn | |
|
14 | 13 | iffalsed | |
15 | 14 | adantl | |
16 | 8 12 15 3 | fprodss | |
17 | 6 16 | eqtr3id | |
18 | iftrue | |
|
19 | 18 | prodeq2i | |
20 | ssun2 | |
|
21 | 20 2 | sseqtrrid | |
22 | 18 | adantl | |
23 | 21 | sselda | |
24 | 23 4 | syldan | |
25 | 22 24 | eqeltrd | |
26 | eldifn | |
|
27 | 26 | iffalsed | |
28 | 27 | adantl | |
29 | 21 25 28 3 | fprodss | |
30 | 19 29 | eqtr3id | |
31 | 17 30 | oveq12d | |
32 | ax-1cn | |
|
33 | ifcl | |
|
34 | 4 32 33 | sylancl | |
35 | ifcl | |
|
36 | 4 32 35 | sylancl | |
37 | 3 34 36 | fprodmul | |
38 | 2 | eleq2d | |
39 | elun | |
|
40 | 38 39 | bitrdi | |
41 | 40 | biimpa | |
42 | disjel | |
|
43 | 1 42 | sylan | |
44 | 43 | iffalsed | |
45 | 9 44 | oveq12d | |
46 | 11 | mulid1d | |
47 | 45 46 | eqtrd | |
48 | 43 | ex | |
49 | 48 | con2d | |
50 | 49 | imp | |
51 | 50 | iffalsed | |
52 | 51 22 | oveq12d | |
53 | 24 | mulid2d | |
54 | 52 53 | eqtrd | |
55 | 47 54 | jaodan | |
56 | 41 55 | syldan | |
57 | 56 | prodeq2dv | |
58 | 31 37 57 | 3eqtr2rd | |