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∪zB∈ℤ→∑k∈A∪zBmodN∈ℤ

Proof

Step Hyp Ref Expression
1 nfcv ⊢Ⅎ_xBmodN
2 nfcsb1v ⊢Ⅎ_k⦋x/k⦌BmodN
3 csbeq1a ⊢k=x→BmodN=⦋x/k⦌BmodN
4 1 2 3 cbvsumi ⊢∑k∈A∪zBmodN=∑x∈A∪z⦋x/k⦌BmodN
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∪zB∈ℤ→A∪z∈Fin
9 rspcsbela ⊢x∈A∪z∧∀k∈A∪zB∈ℤ→⦋x/k⦌B∈ℤ
10 9 expcom ⊢∀k∈A∪zB∈ℤ→x∈A∪z→⦋x/k⦌B∈ℤ
11 10 3ad2ant3 ⊢A∈Fin∧N∈ℕ∧∀k∈A∪zB∈ℤ→x∈A∪z→⦋x/k⦌B∈ℤ
12 11 imp ⊢A∈Fin∧N∈ℕ∧∀k∈A∪zB∈ℤ∧x∈A∪z→⦋x/k⦌B∈ℤ
13 vex ⊢x∈V
14 csbov1g ⊢x∈V→⦋x/k⦌BmodN=⦋x/k⦌BmodN
15 13 14 ax-mp ⊢⦋x/k⦌BmodN=⦋x/k⦌BmodN
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⦌BmodN∈ℕ0
19 18 nn0zd ⊢N∈ℕ∧⦋x/k⦌B∈ℤ→⦋x/k⦌BmodN∈ℤ
20 15 19 eqeltrid ⊢N∈ℕ∧⦋x/k⦌B∈ℤ→⦋x/k⦌BmodN∈ℤ
21 20 ex ⊢N∈ℕ→⦋x/k⦌B∈ℤ→⦋x/k⦌BmodN∈ℤ
22 21 3ad2ant2 ⊢A∈Fin∧N∈ℕ∧∀k∈A∪zB∈ℤ→⦋x/k⦌B∈ℤ→⦋x/k⦌BmodN∈ℤ
23 22 adantr ⊢A∈Fin∧N∈ℕ∧∀k∈A∪zB∈ℤ∧x∈A∪z→⦋x/k⦌B∈ℤ→⦋x/k⦌BmodN∈ℤ
24 12 23 mpd ⊢A∈Fin∧N∈ℕ∧∀k∈A∪zB∈ℤ∧x∈A∪z→⦋x/k⦌BmodN∈ℤ
25 8 24 fsumzcl ⊢A∈Fin∧N∈ℕ∧∀k∈A∪zB∈ℤ→∑x∈A∪z⦋x/k⦌BmodN∈ℤ
26 4 25 eqeltrid ⊢A∈Fin∧N∈ℕ∧∀k∈A∪zB∈ℤ→∑k∈A∪zBmodN∈ℤ