Metamath Proof Explorer

Theorem fsummmodsnunz

Description: A finite sum of summands modulo a positive number with an additional summand is an integer. (Contributed by Alexander van der Vekens, 1-Sep-2018)

Ref Expression
Assertion fsummmodsnunz ⊢ A ∈ Fin ∧ N ∈ ℕ ∧ ∀ k ∈ A ∪ z B ∈ ℤ → ∑ k ∈ A ∪ z 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 ∪ z B mod N = ∑ x ∈ A ∪ z ⦋ x / k⦌ B mod N
5 snfi ⊢ z ∈ Fin
6 unfi ⊢ A ∈ Fin ∧ z ∈ Fin → A ∪ z ∈ Fin
7 5 6 mpan2 ⊢ A ∈ Fin → A ∪ z ∈ Fin
8 7 3ad2ant1 ⊢ A ∈ Fin ∧ N ∈ ℕ ∧ ∀ k ∈ A ∪ z B ∈ ℤ → A ∪ z ∈ Fin
9 rspcsbela ⊢ x ∈ A ∪ z ∧ ∀ k ∈ A ∪ z B ∈ ℤ → ⦋ x / k⦌ B ∈ ℤ
10 9 expcom ⊢ ∀ k ∈ A ∪ z B ∈ ℤ → x ∈ A ∪ z → ⦋ x / k⦌ B ∈ ℤ
11 10 3ad2ant3 ⊢ A ∈ Fin ∧ N ∈ ℕ ∧ ∀ k ∈ A ∪ z B ∈ ℤ → x ∈ A ∪ z → ⦋ x / k⦌ B ∈ ℤ
12 11 imp ⊢ A ∈ Fin ∧ N ∈ ℕ ∧ ∀ k ∈ A ∪ z B ∈ ℤ ∧ x ∈ A ∪ z → ⦋ 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 simpr ⊢ N ∈ ℕ ∧ ⦋ x / k⦌ B ∈ ℤ → ⦋ x / k⦌ B ∈ ℤ
17 simpl ⊢ N ∈ ℕ ∧ ⦋ x / k⦌ B ∈ ℤ → N ∈ ℕ
18 16 17 zmodcld ⊢ N ∈ ℕ ∧ ⦋ x / k⦌ B ∈ ℤ → ⦋ x / k⦌ B mod N ∈ ℕ 0
19 18 nn0zd ⊢ N ∈ ℕ ∧ ⦋ x / k⦌ B ∈ ℤ → ⦋ x / k⦌ B mod N ∈ ℤ
20 15 19 eqeltrid ⊢ N ∈ ℕ ∧ ⦋ x / k⦌ B ∈ ℤ → ⦋ x / k⦌ B mod N ∈ ℤ
21 20 ex ⊢ N ∈ ℕ → ⦋ x / k⦌ B ∈ ℤ → ⦋ x / k⦌ B mod N ∈ ℤ
22 21 3ad2ant2 ⊢ A ∈ Fin ∧ N ∈ ℕ ∧ ∀ k ∈ A ∪ z B ∈ ℤ → ⦋ x / k⦌ B ∈ ℤ → ⦋ x / k⦌ B mod N ∈ ℤ
23 22 adantr ⊢ A ∈ Fin ∧ N ∈ ℕ ∧ ∀ k ∈ A ∪ z B ∈ ℤ ∧ x ∈ A ∪ z → ⦋ x / k⦌ B ∈ ℤ → ⦋ x / k⦌ B mod N ∈ ℤ
24 12 23 mpd ⊢ A ∈ Fin ∧ N ∈ ℕ ∧ ∀ k ∈ A ∪ z B ∈ ℤ ∧ x ∈ A ∪ z → ⦋ x / k⦌ B mod N ∈ ℤ
25 8 24 fsumzcl ⊢ A ∈ Fin ∧ N ∈ ℕ ∧ ∀ k ∈ A ∪ z B ∈ ℤ → ∑ x ∈ A ∪ z ⦋ x / k⦌ B mod N ∈ ℤ
26 4 25 eqeltrid ⊢ A ∈ Fin ∧ N ∈ ℕ ∧ ∀ k ∈ A ∪ z B ∈ ℤ → ∑ k ∈ A ∪ z B mod N ∈ ℤ