Metamath Proof Explorer

Theorem fsummmodsndifre

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

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

Proof

Step Hyp Ref Expression
1 nfcv 
 |-  F/_ x ( B mod N )
2 nfcsb1v 
 |-  F/_ k [_ x / k ]_ ( B mod N )
3 csbeq1a 
 |-  ( k = x -> ( B mod N ) = [_ x / k ]_ ( B mod N ) )
4 1 2 3 cbvsumi 
 |-  sum_ k e. ( A \ { X } ) ( B mod N ) = sum_ x e. ( A \ { X } ) [_ x / k ]_ ( B mod N )
5 diffi 
 |-  ( A e. Fin -> ( A \ { X } ) e. Fin )
6 5 3ad2ant1 
 |-  ( ( A e. Fin /\ N e. NN /\ 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 expcom 
 |-  ( A. k e. A B e. ZZ -> ( x e. ( A \ { X } ) -> [_ x / k ]_ B e. ZZ ) )
11 10 3ad2ant3 
 |-  ( ( A e. Fin /\ N e. NN /\ A. k e. A B e. ZZ ) -> ( x e. ( A \ { X } ) -> [_ x / k ]_ B e. ZZ ) )
12 11 imp 
 |-  ( ( ( A e. Fin /\ N e. NN /\ A. k e. A B e. ZZ ) /\ x e. ( A \ { X } ) ) -> [_ x / k ]_ B e. ZZ )
13 vex 
 |-  x e. _V
14 csbov1g 
 |-  ( x e. _V -> [_ x / k ]_ ( B mod N ) = ( [_ x / k ]_ B mod N ) )
15 13 14 ax-mp 
 |-  [_ x / k ]_ ( B mod N ) = ( [_ x / k ]_ B mod N )
16 zre 
 |-  ( [_ x / k ]_ B e. ZZ -> [_ x / k ]_ B e. RR )
17 16 adantl 
 |-  ( ( N e. NN /\ [_ x / k ]_ B e. ZZ ) -> [_ x / k ]_ B e. RR )
18 nnrp 
 |-  ( N e. NN -> N e. RR+ )
19 18 adantr 
 |-  ( ( N e. NN /\ [_ x / k ]_ B e. ZZ ) -> N e. RR+ )
20 17 19 modcld 
 |-  ( ( N e. NN /\ [_ x / k ]_ B e. ZZ ) -> ( [_ x / k ]_ B mod N ) e. RR )
21 15 20 eqeltrid 
 |-  ( ( N e. NN /\ [_ x / k ]_ B e. ZZ ) -> [_ x / k ]_ ( B mod N ) e. RR )
22 21 ex 
 |-  ( N e. NN -> ( [_ x / k ]_ B e. ZZ -> [_ x / k ]_ ( B mod N ) e. RR ) )
23 22 3ad2ant2 
 |-  ( ( A e. Fin /\ N e. NN /\ A. k e. A B e. ZZ ) -> ( [_ x / k ]_ B e. ZZ -> [_ x / k ]_ ( B mod N ) e. RR ) )
24 23 adantr 
 |-  ( ( ( A e. Fin /\ N e. NN /\ A. k e. A B e. ZZ ) /\ x e. ( A \ { X } ) ) -> ( [_ x / k ]_ B e. ZZ -> [_ x / k ]_ ( B mod N ) e. RR ) )
25 12 24 mpd 
 |-  ( ( ( A e. Fin /\ N e. NN /\ A. k e. A B e. ZZ ) /\ x e. ( A \ { X } ) ) -> [_ x / k ]_ ( B mod N ) e. RR )
26 6 25 fsumrecl 
 |-  ( ( A e. Fin /\ N e. NN /\ A. k e. A B e. ZZ ) -> sum_ x e. ( A \ { X } ) [_ x / k ]_ ( B mod N ) e. RR )
27 4 26 eqeltrid 
 |-  ( ( A e. Fin /\ N e. NN /\ A. k e. A B e. ZZ ) -> sum_ k e. ( A \ { X } ) ( B mod N ) e. RR )