Metamath Proof Explorer

Theorem esumdivc

Description: An extended sum divided by a constant. (Contributed by Thierry Arnoux, 6-Jul-2017)

Ref Expression
Hypotheses esumdivc.a 
|- ( ph -> A e. V )
esumdivc.b 
|- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
esumdivc.c 
|- ( ph -> C e. RR+ )
Assertion esumdivc 
|- ( ph -> ( sum* k e. A B /e C ) = sum* k e. A ( B /e C ) )

Proof

Step Hyp Ref Expression
1 esumdivc.a 
 |-  ( ph -> A e. V )
2 esumdivc.b 
 |-  ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
3 esumdivc.c 
 |-  ( ph -> C e. RR+ )
4 1red 
 |-  ( ph -> 1 e. RR )
5 3 rpred 
 |-  ( ph -> C e. RR )
6 3 rpne0d 
 |-  ( ph -> C =/= 0 )
7 rexdiv 
 |-  ( ( 1 e. RR /\ C e. RR /\ C =/= 0 ) -> ( 1 /e C ) = ( 1 / C ) )
8 4 5 6 7 syl3anc 
 |-  ( ph -> ( 1 /e C ) = ( 1 / C ) )
9 ioorp 
 |-  ( 0 (,) +oo ) = RR+
10 ioossico 
 |-  ( 0 (,) +oo ) C_ ( 0 [,) +oo )
11 9 10 eqsstrri 
 |-  RR+ C_ ( 0 [,) +oo )
12 3 rpreccld 
 |-  ( ph -> ( 1 / C ) e. RR+ )
13 11 12 sselid 
 |-  ( ph -> ( 1 / C ) e. ( 0 [,) +oo ) )
14 8 13 eqeltrd 
 |-  ( ph -> ( 1 /e C ) e. ( 0 [,) +oo ) )
15 1 2 14 esummulc1 
 |-  ( ph -> ( sum* k e. A B *e ( 1 /e C ) ) = sum* k e. A ( B *e ( 1 /e C ) ) )
16 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
17 2 ralrimiva 
 |-  ( ph -> A. k e. A B e. ( 0 [,] +oo ) )
18 nfcv 
 |-  F/_ k A
19 18 esumcl 
 |-  ( ( A e. V /\ A. k e. A B e. ( 0 [,] +oo ) ) -> sum* k e. A B e. ( 0 [,] +oo ) )
20 1 17 19 syl2anc 
 |-  ( ph -> sum* k e. A B e. ( 0 [,] +oo ) )
21 16 20 sselid 
 |-  ( ph -> sum* k e. A B e. RR* )
22 xdivrec 
 |-  ( ( sum* k e. A B e. RR* /\ C e. RR /\ C =/= 0 ) -> ( sum* k e. A B /e C ) = ( sum* k e. A B *e ( 1 /e C ) ) )
23 21 5 6 22 syl3anc 
 |-  ( ph -> ( sum* k e. A B /e C ) = ( sum* k e. A B *e ( 1 /e C ) ) )
24 16 2 sselid 
 |-  ( ( ph /\ k e. A ) -> B e. RR* )
25 5 adantr 
 |-  ( ( ph /\ k e. A ) -> C e. RR )
26 6 adantr 
 |-  ( ( ph /\ k e. A ) -> C =/= 0 )
27 xdivrec 
 |-  ( ( B e. RR* /\ C e. RR /\ C =/= 0 ) -> ( B /e C ) = ( B *e ( 1 /e C ) ) )
28 24 25 26 27 syl3anc 
 |-  ( ( ph /\ k e. A ) -> ( B /e C ) = ( B *e ( 1 /e C ) ) )
29 28 esumeq2dv 
 |-  ( ph -> sum* k e. A ( B /e C ) = sum* k e. A ( B *e ( 1 /e C ) ) )
30 15 23 29 3eqtr4d 
 |-  ( ph -> ( sum* k e. A B /e C ) = sum* k e. A ( B /e C ) )