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	$$⊢\left(A\in \mathrm{Fin}\wedge \forall k\in AB\in \mathbb{Z}\right)\to \sum _{k\in A\setminus \left\{X\right\}}B\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		nfcv	$$⊢\underset{\_}{Ⅎ}xB$$
2		nfcsb1v	$$⊢\underset{\_}{Ⅎ}k⦋x/k⦌B$$
3		csbeq1a	$$⊢k=x\to B=⦋x/k⦌B$$
4	1 2 3	cbvsumi	$$⊢\sum _{k\in A\setminus \left\{X\right\}}B=\sum _{x\in A\setminus \left\{X\right\}}⦋x/k⦌B$$
5		diffi	$$⊢A\in \mathrm{Fin}\to A\setminus \left\{X\right\}\in \mathrm{Fin}$$
6	5	adantr	$$⊢\left(A\in \mathrm{Fin}\wedge \forall k\in AB\in \mathbb{Z}\right)\to A\setminus \left\{X\right\}\in \mathrm{Fin}$$
7		eldifi	$$⊢x\in \left(A\setminus \left\{X\right\}\right)\to x\in A$$
8		rspcsbela	$$⊢\left(x\in A\wedge \forall k\in AB\in \mathbb{Z}\right)\to ⦋x/k⦌B\in \mathbb{Z}$$
9	7 8	sylan	$$⊢\left(x\in \left(A\setminus \left\{X\right\}\right)\wedge \forall k\in AB\in \mathbb{Z}\right)\to ⦋x/k⦌B\in \mathbb{Z}$$
10	9	zred	$$⊢\left(x\in \left(A\setminus \left\{X\right\}\right)\wedge \forall k\in AB\in \mathbb{Z}\right)\to ⦋x/k⦌B\in ℝ$$
11	10	expcom	$$⊢\forall k\in AB\in \mathbb{Z}\to \left(x\in \left(A\setminus \left\{X\right\}\right)\to ⦋x/k⦌B\in ℝ\right)$$
12	11	adantl	$$⊢\left(A\in \mathrm{Fin}\wedge \forall k\in AB\in \mathbb{Z}\right)\to \left(x\in \left(A\setminus \left\{X\right\}\right)\to ⦋x/k⦌B\in ℝ\right)$$
13	12	imp	$$⊢\left(\left(A\in \mathrm{Fin}\wedge \forall k\in AB\in \mathbb{Z}\right)\wedge x\in \left(A\setminus \left\{X\right\}\right)\right)\to ⦋x/k⦌B\in ℝ$$
14	6 13	fsumrecl	$$⊢\left(A\in \mathrm{Fin}\wedge \forall k\in AB\in \mathbb{Z}\right)\to \sum _{x\in A\setminus \left\{X\right\}}⦋x/k⦌B\in ℝ$$
15	4 14	eqeltrid	$$⊢\left(A\in \mathrm{Fin}\wedge \forall k\in AB\in \mathbb{Z}\right)\to \sum _{k\in A\setminus \left\{X\right\}}B\in ℝ$$