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 ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) → Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) ∈ ℤ )

Proof

Step Hyp Ref Expression
1 csbeq1a ⊢ ( 𝑘 = 𝑥 → ( 𝐵 mod 𝑁 ) = ⦋ 𝑥 / 𝑘 ⦌ ( 𝐵 mod 𝑁 ) )
2 nfcv ⊢ Ⅎ 𝑥 ( 𝐵 mod 𝑁 )
3 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑥 / 𝑘 ⦌ ( 𝐵 mod 𝑁 )
4 1 2 3 cbvsum ⊢ Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) = Σ 𝑥 ∈ ( 𝐴 ∪ { 𝑧 } ) ⦋ 𝑥 / 𝑘 ⦌ ( 𝐵 mod 𝑁 )
5 snfi ⊢ { 𝑧 } ∈ Fin
6 unfi ⊢ ( ( 𝐴 ∈ Fin ∧ { 𝑧 } ∈ Fin ) → ( 𝐴 ∪ { 𝑧 } ) ∈ Fin )
7 5 6 mpan2 ⊢ ( 𝐴 ∈ Fin → ( 𝐴 ∪ { 𝑧 } ) ∈ Fin )
8 7 3ad2ant1 ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) → ( 𝐴 ∪ { 𝑧 } ) ∈ Fin )
9 rspcsbela ⊢ ( ( 𝑥 ∈ ( 𝐴 ∪ { 𝑧 } ) ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) → ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ ℤ )
10 9 expcom ⊢ ( ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ → ( 𝑥 ∈ ( 𝐴 ∪ { 𝑧 } ) → ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ ℤ ) )
11 10 3ad2ant3 ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) → ( 𝑥 ∈ ( 𝐴 ∪ { 𝑧 } ) → ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ ℤ ) )
12 11 imp ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) ∧ 𝑥 ∈ ( 𝐴 ∪ { 𝑧 } ) ) → ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ ℤ )
13 vex ⊢ 𝑥 ∈ V
14 csbov1g ⊢ ( 𝑥 ∈ V → ⦋ 𝑥 / 𝑘 ⦌ ( 𝐵 mod 𝑁 ) = ( ⦋ 𝑥 / 𝑘 ⦌ 𝐵 mod 𝑁 ) )
15 13 14 ax-mp ⊢ ⦋ 𝑥 / 𝑘 ⦌ ( 𝐵 mod 𝑁 ) = ( ⦋ 𝑥 / 𝑘 ⦌ 𝐵 mod 𝑁 )
16 simpr ⊢ ( ( 𝑁 ∈ ℕ ∧ ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ ℤ ) → ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ ℤ )
17 simpl ⊢ ( ( 𝑁 ∈ ℕ ∧ ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ ℤ ) → 𝑁 ∈ ℕ )
18 16 17 zmodcld ⊢ ( ( 𝑁 ∈ ℕ ∧ ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ ℤ ) → ( ⦋ 𝑥 / 𝑘 ⦌ 𝐵 mod 𝑁 ) ∈ ℕ0 )
19 18 nn0zd ⊢ ( ( 𝑁 ∈ ℕ ∧ ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ ℤ ) → ( ⦋ 𝑥 / 𝑘 ⦌ 𝐵 mod 𝑁 ) ∈ ℤ )
20 15 19 eqeltrid ⊢ ( ( 𝑁 ∈ ℕ ∧ ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ ℤ ) → ⦋ 𝑥 / 𝑘 ⦌ ( 𝐵 mod 𝑁 ) ∈ ℤ )
21 20 ex ⊢ ( 𝑁 ∈ ℕ → ( ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ ℤ → ⦋ 𝑥 / 𝑘 ⦌ ( 𝐵 mod 𝑁 ) ∈ ℤ ) )
22 21 3ad2ant2 ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) → ( ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ ℤ → ⦋ 𝑥 / 𝑘 ⦌ ( 𝐵 mod 𝑁 ) ∈ ℤ ) )
23 22 adantr ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) ∧ 𝑥 ∈ ( 𝐴 ∪ { 𝑧 } ) ) → ( ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ ℤ → ⦋ 𝑥 / 𝑘 ⦌ ( 𝐵 mod 𝑁 ) ∈ ℤ ) )
24 12 23 mpd ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) ∧ 𝑥 ∈ ( 𝐴 ∪ { 𝑧 } ) ) → ⦋ 𝑥 / 𝑘 ⦌ ( 𝐵 mod 𝑁 ) ∈ ℤ )
25 8 24 fsumzcl ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) → Σ 𝑥 ∈ ( 𝐴 ∪ { 𝑧 } ) ⦋ 𝑥 / 𝑘 ⦌ ( 𝐵 mod 𝑁 ) ∈ ℤ )
26 4 25 eqeltrid ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) → Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) ∈ ℤ )