Metamath Proof Explorer


Theorem fsumdivc

Description: A finite sum divided by a constant. (Contributed by NM, 2-Jan-2006) (Revised by Mario Carneiro, 24-Apr-2014)

Ref Expression
Hypotheses fsummulc2.1
|- ( ph -> A e. Fin )
fsummulc2.2
|- ( ph -> C e. CC )
fsummulc2.3
|- ( ( ph /\ k e. A ) -> B e. CC )
fsumdivc.4
|- ( ph -> C =/= 0 )
Assertion fsumdivc
|- ( ph -> ( sum_ k e. A B / C ) = sum_ k e. A ( B / C ) )

Proof

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 ) )