Metamath Proof Explorer

Theorem fsummsndifre

Description: A finite sum with one of its integer summands removed is a real number. (Contributed by Alexander van der Vekens, 31-Aug-2018)

Ref Expression
Assertion fsummsndifre 
|- ( ( A e. Fin /\ A. k e. A B e. ZZ ) -> sum_ k e. ( A \ { X } ) B e. RR )

Proof

Step Hyp Ref Expression
1 nfcv 
 |-  F/_ x B
2 nfcsb1v 
 |-  F/_ k [_ x / k ]_ B
3 csbeq1a 
 |-  ( k = x -> B = [_ x / k ]_ B )
4 1 2 3 cbvsumi 
 |-  sum_ k e. ( A \ { X } ) B = sum_ x e. ( A \ { X } ) [_ x / k ]_ B
5 diffi 
 |-  ( A e. Fin -> ( A \ { X } ) e. Fin )
6 5 adantr 
 |-  ( ( A e. Fin /\ A. k e. A B e. ZZ ) -> ( A \ { X } ) e. Fin )
7 eldifi 
 |-  ( x e. ( A \ { X } ) -> x e. A )
8 rspcsbela 
 |-  ( ( x e. A /\ A. k e. A B e. ZZ ) -> [_ x / k ]_ B e. ZZ )
9 7 8 sylan 
 |-  ( ( x e. ( A \ { X } ) /\ A. k e. A B e. ZZ ) -> [_ x / k ]_ B e. ZZ )
10 9 zred 
 |-  ( ( x e. ( A \ { X } ) /\ A. k e. A B e. ZZ ) -> [_ x / k ]_ B e. RR )
11 10 expcom 
 |-  ( A. k e. A B e. ZZ -> ( x e. ( A \ { X } ) -> [_ x / k ]_ B e. RR ) )
12 11 adantl 
 |-  ( ( A e. Fin /\ A. k e. A B e. ZZ ) -> ( x e. ( A \ { X } ) -> [_ x / k ]_ B e. RR ) )
13 12 imp 
 |-  ( ( ( A e. Fin /\ A. k e. A B e. ZZ ) /\ x e. ( A \ { X } ) ) -> [_ x / k ]_ B e. RR )
14 6 13 fsumrecl 
 |-  ( ( A e. Fin /\ A. k e. A B e. ZZ ) -> sum_ x e. ( A \ { X } ) [_ x / k ]_ B e. RR )
15 4 14 eqeltrid 
 |-  ( ( A e. Fin /\ A. k e. A B e. ZZ ) -> sum_ k e. ( A \ { X } ) B e. RR )