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 csbeq1a ⊢ k = x → B mod N = ⦋ x / k⦌ B mod N
2 nfcv ⊢ Ⅎ _ x B mod N
3 nfcsb1v ⊢ Ⅎ _ k ⦋ x / k⦌ B mod N
4 1 2 3 cbvsum ⊢ ∑ 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 ∈ ℝ