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 ∈ Fin ∧ ∀ k ∈ A B ∈ ℤ → ∑ k ∈ A ∖ X B ∈ ℝ

Proof

Step Hyp Ref Expression
1 nfcv ⊢ Ⅎ _ x B
2 nfcsb1v ⊢ Ⅎ _ k ⦋ x / k⦌ B
3 csbeq1a ⊢ k = x → B = ⦋ x / k⦌ B
4 1 2 3 cbvsumi ⊢ ∑ k ∈ A ∖ X B = ∑ x ∈ A ∖ X ⦋ x / k⦌ B
5 diffi ⊢ A ∈ Fin → A ∖ X ∈ Fin
6 5 adantr ⊢ A ∈ Fin ∧ ∀ 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 zred ⊢ x ∈ A ∖ X ∧ ∀ k ∈ A B ∈ ℤ → ⦋ x / k⦌ B ∈ ℝ
11 10 expcom ⊢ ∀ k ∈ A B ∈ ℤ → x ∈ A ∖ X → ⦋ x / k⦌ B ∈ ℝ
12 11 adantl ⊢ A ∈ Fin ∧ ∀ k ∈ A B ∈ ℤ → x ∈ A ∖ X → ⦋ x / k⦌ B ∈ ℝ
13 12 imp ⊢ A ∈ Fin ∧ ∀ k ∈ A B ∈ ℤ ∧ x ∈ A ∖ X → ⦋ x / k⦌ B ∈ ℝ
14 6 13 fsumrecl ⊢ A ∈ Fin ∧ ∀ k ∈ A B ∈ ℤ → ∑ x ∈ A ∖ X ⦋ x / k⦌ B ∈ ℝ
15 4 14 eqeltrid ⊢ A ∈ Fin ∧ ∀ k ∈ A B ∈ ℤ → ∑ k ∈ A ∖ X B ∈ ℝ