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 Fin N k A B k A X B mod N

Proof

Step Hyp Ref Expression
1 nfcv _ x B mod N
2 nfcsb1v _ k x / k B mod N
3 csbeq1a k = x B mod N = x / k B mod N
4 1 2 3 cbvsumi k A X B mod N = x A X x / k B mod N
5 diffi A Fin A X Fin
6 5 3ad2ant1 A Fin N k A B A X Fin
7 eldifi x A X x A
8 rspcsbela x A k A B x / k B
9 7 8 sylan x A X k A B x / k B
10 9 expcom k A B x A X x / k B
11 10 3ad2ant3 A Fin N k A B x A X x / k B
12 11 imp A Fin N k A B x A X x / k B
13 vex x V
14 csbov1g x 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 x / k B
17 16 adantl N x / k B x / k B
18 nnrp N N +
19 18 adantr N x / k B N +
20 17 19 modcld N x / k B x / k B mod N
21 15 20 eqeltrid N x / k B x / k B mod N
22 21 ex N x / k B x / k B mod N
23 22 3ad2ant2 A Fin N k A B x / k B x / k B mod N
24 23 adantr A Fin N k A B x A X x / k B x / k B mod N
25 12 24 mpd A Fin N k A B x A X x / k B mod N
26 6 25 fsumrecl A Fin N k A B x A X x / k B mod N
27 4 26 eqeltrid A Fin N k A B k A X B mod N