Step |
Hyp |
Ref |
Expression |
1 |
|
fsummulc2.1 |
|- ( ph -> A e. Fin ) |
2 |
|
fsummulc2.2 |
|- ( ph -> C e. CC ) |
3 |
|
fsummulc2.3 |
|- ( ( ph /\ k e. A ) -> B e. CC ) |
4 |
|
fsumdivc.4 |
|- ( ph -> C =/= 0 ) |
5 |
2 4
|
reccld |
|- ( ph -> ( 1 / C ) e. CC ) |
6 |
1 5 3
|
fsummulc1 |
|- ( ph -> ( sum_ k e. A B x. ( 1 / C ) ) = sum_ k e. A ( B x. ( 1 / C ) ) ) |
7 |
1 3
|
fsumcl |
|- ( ph -> sum_ k e. A B e. CC ) |
8 |
7 2 4
|
divrecd |
|- ( ph -> ( sum_ k e. A B / C ) = ( sum_ k e. A B x. ( 1 / C ) ) ) |
9 |
2
|
adantr |
|- ( ( ph /\ k e. A ) -> C e. CC ) |
10 |
4
|
adantr |
|- ( ( ph /\ k e. A ) -> C =/= 0 ) |
11 |
3 9 10
|
divrecd |
|- ( ( ph /\ k e. A ) -> ( B / C ) = ( B x. ( 1 / C ) ) ) |
12 |
11
|
sumeq2dv |
|- ( ph -> sum_ k e. A ( B / C ) = sum_ k e. A ( B x. ( 1 / C ) ) ) |
13 |
6 8 12
|
3eqtr4d |
|- ( ph -> ( sum_ k e. A B / C ) = sum_ k e. A ( B / C ) ) |