This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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