Metamath Proof Explorer

Theorem modfsummods

Description: Induction step for modfsummod . (Contributed by Alexander van der Vekens, 1-Sep-2018)

Ref Expression
Assertion modfsummods ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) → ( ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) → ( Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 snssi ⊢ ( 𝑧 ∈ 𝐴 → { 𝑧 } ⊆ 𝐴 )
2 ssequn1 ⊢ ( { 𝑧 } ⊆ 𝐴 ↔ ( { 𝑧 } ∪ 𝐴 ) = 𝐴 )
3 uncom ⊢ ( { 𝑧 } ∪ 𝐴 ) = ( 𝐴 ∪ { 𝑧 } )
4 3 eqeq1i ⊢ ( ( { 𝑧 } ∪ 𝐴 ) = 𝐴 ↔ ( 𝐴 ∪ { 𝑧 } ) = 𝐴 )
5 sumeq1 ⊢ ( 𝐴 = ( 𝐴 ∪ { 𝑧 } ) → Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 )
6 5 oveq1d ⊢ ( 𝐴 = ( 𝐴 ∪ { 𝑧 } ) → ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 mod 𝑁 ) )
7 sumeq1 ⊢ ( 𝐴 = ( 𝐴 ∪ { 𝑧 } ) → Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) = Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) )
8 7 oveq1d ⊢ ( 𝐴 = ( 𝐴 ∪ { 𝑧 } ) → ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) = ( Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) mod 𝑁 ) )
9 6 8 eqeq12d ⊢ ( 𝐴 = ( 𝐴 ∪ { 𝑧 } ) → ( ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ↔ ( Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) )
10 9 eqcoms ⊢ ( ( 𝐴 ∪ { 𝑧 } ) = 𝐴 → ( ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ↔ ( Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) )
11 4 10 sylbi ⊢ ( ( { 𝑧 } ∪ 𝐴 ) = 𝐴 → ( ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ↔ ( Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) )
12 11 biimpd ⊢ ( ( { 𝑧 } ∪ 𝐴 ) = 𝐴 → ( ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) → ( Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) )
13 12 a1d ⊢ ( ( { 𝑧 } ∪ 𝐴 ) = 𝐴 → ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) → ( ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) → ( Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) ) )
14 2 13 sylbi ⊢ ( { 𝑧 } ⊆ 𝐴 → ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) → ( ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) → ( Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) ) )
15 1 14 syl ⊢ ( 𝑧 ∈ 𝐴 → ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) → ( ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) → ( Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) ) )
16 df-nel ⊢ ( 𝑧 ∉ 𝐴 ↔ ¬ 𝑧 ∈ 𝐴 )
17 simp1 ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) → 𝐴 ∈ Fin )
18 17 ad2antlr ⊢ ( ( ( 𝑧 ∉ 𝐴 ∧ ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) ) ∧ ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) → 𝐴 ∈ Fin )
19 simpl ⊢ ( ( 𝑧 ∉ 𝐴 ∧ ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) ) → 𝑧 ∉ 𝐴 )
20 19 adantr ⊢ ( ( ( 𝑧 ∉ 𝐴 ∧ ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) ) ∧ ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) → 𝑧 ∉ 𝐴 )
21 vex ⊢ 𝑧 ∈ V
22 20 21 jctil ⊢ ( ( ( 𝑧 ∉ 𝐴 ∧ ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) ) ∧ ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) → ( 𝑧 ∈ V ∧ 𝑧 ∉ 𝐴 ) )
23 simplr3 ⊢ ( ( ( 𝑧 ∉ 𝐴 ∧ ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) ) ∧ ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) → ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ )
24 fsumsplitsnun ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑧 ∈ V ∧ 𝑧 ∉ 𝐴 ) ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) → Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 = ( Σ 𝑘 ∈ 𝐴 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
25 18 22 23 24 syl3anc ⊢ ( ( ( 𝑧 ∉ 𝐴 ∧ ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) ) ∧ ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) → Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 = ( Σ 𝑘 ∈ 𝐴 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
26 25 oveq1d ⊢ ( ( ( 𝑧 ∉ 𝐴 ∧ ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) ) ∧ ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) → ( Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 mod 𝑁 ) = ( ( Σ 𝑘 ∈ 𝐴 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) mod 𝑁 ) )
27 ralunb ⊢ ( ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ↔ ( ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ∧ ∀ 𝑘 ∈ { 𝑧 } 𝐵 ∈ ℤ ) )
28 simpl ⊢ ( ( ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ∧ ∀ 𝑘 ∈ { 𝑧 } 𝐵 ∈ ℤ ) → ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ )
29 27 28 sylbi ⊢ ( ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ → ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ )
30 fsumzcl2 ⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) → Σ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ )
31 29 30 sylan2 ⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) → Σ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ )
32 31 3adant2 ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) → Σ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ )
33 32 adantl ⊢ ( ( 𝑧 ∉ 𝐴 ∧ ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) ) → Σ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ )
34 33 zred ⊢ ( ( 𝑧 ∉ 𝐴 ∧ ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) ) → Σ 𝑘 ∈ 𝐴 𝐵 ∈ ℝ )
35 modfsummodslem1 ⊢ ( ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ → ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℤ )
36 35 3ad2ant3 ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) → ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℤ )
37 36 adantl ⊢ ( ( 𝑧 ∉ 𝐴 ∧ ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) ) → ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℤ )
38 37 zred ⊢ ( ( 𝑧 ∉ 𝐴 ∧ ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) ) → ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℝ )
39 nnrp ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ )
40 39 3ad2ant2 ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) → 𝑁 ∈ ℝ+ )
41 40 adantl ⊢ ( ( 𝑧 ∉ 𝐴 ∧ ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) ) → 𝑁 ∈ ℝ+ )
42 modaddabs ⊢ ( ( Σ 𝑘 ∈ 𝐴 𝐵 ∈ ℝ ∧ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → ( ( ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) + ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 mod 𝑁 ) ) mod 𝑁 ) = ( ( Σ 𝑘 ∈ 𝐴 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) mod 𝑁 ) )
43 34 38 41 42 syl3anc ⊢ ( ( 𝑧 ∉ 𝐴 ∧ ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) ) → ( ( ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) + ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 mod 𝑁 ) ) mod 𝑁 ) = ( ( Σ 𝑘 ∈ 𝐴 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) mod 𝑁 ) )
44 43 eqcomd ⊢ ( ( 𝑧 ∉ 𝐴 ∧ ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) ) → ( ( Σ 𝑘 ∈ 𝐴 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) mod 𝑁 ) = ( ( ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) + ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 mod 𝑁 ) ) mod 𝑁 ) )
45 44 adantr ⊢ ( ( ( 𝑧 ∉ 𝐴 ∧ ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) ) ∧ ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) → ( ( Σ 𝑘 ∈ 𝐴 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) mod 𝑁 ) = ( ( ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) + ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 mod 𝑁 ) ) mod 𝑁 ) )
46 simpr ⊢ ( ( ( 𝑧 ∉ 𝐴 ∧ ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) ) ∧ ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) → ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) )
47 35 zred ⊢ ( ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ → ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℝ )
48 47 3ad2ant3 ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) → ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℝ )
49 48 adantl ⊢ ( ( 𝑧 ∉ 𝐴 ∧ ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) ) → ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℝ )
50 49 41 jca ⊢ ( ( 𝑧 ∉ 𝐴 ∧ ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) ) → ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) )
51 50 adantr ⊢ ( ( ( 𝑧 ∉ 𝐴 ∧ ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) ) ∧ ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) → ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) )
52 modabs2 ⊢ ( ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → ( ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 mod 𝑁 ) mod 𝑁 ) = ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 mod 𝑁 ) )
53 52 eqcomd ⊢ ( ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 mod 𝑁 ) = ( ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 mod 𝑁 ) mod 𝑁 ) )
54 51 53 syl ⊢ ( ( ( 𝑧 ∉ 𝐴 ∧ ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) ) ∧ ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) → ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 mod 𝑁 ) = ( ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 mod 𝑁 ) mod 𝑁 ) )
55 46 54 oveq12d ⊢ ( ( ( 𝑧 ∉ 𝐴 ∧ ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) ) ∧ ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) → ( ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) + ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 mod 𝑁 ) ) = ( ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) + ( ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 mod 𝑁 ) mod 𝑁 ) ) )
56 55 oveq1d ⊢ ( ( ( 𝑧 ∉ 𝐴 ∧ ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) ) ∧ ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) → ( ( ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) + ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 mod 𝑁 ) ) mod 𝑁 ) = ( ( ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) + ( ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 mod 𝑁 ) mod 𝑁 ) ) mod 𝑁 ) )
57 45 56 eqtrd ⊢ ( ( ( 𝑧 ∉ 𝐴 ∧ ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) ) ∧ ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) → ( ( Σ 𝑘 ∈ 𝐴 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) mod 𝑁 ) = ( ( ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) + ( ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 mod 𝑁 ) mod 𝑁 ) ) mod 𝑁 ) )
58 zmodcl ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝐵 mod 𝑁 ) ∈ ℕ0 )
59 58 nn0zd ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝐵 mod 𝑁 ) ∈ ℤ )
60 59 expcom ⊢ ( 𝑁 ∈ ℕ → ( 𝐵 ∈ ℤ → ( 𝐵 mod 𝑁 ) ∈ ℤ ) )
61 60 ralimdv ⊢ ( 𝑁 ∈ ℕ → ( ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ → ∀ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) ∈ ℤ ) )
62 61 com12 ⊢ ( ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ → ( 𝑁 ∈ ℕ → ∀ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) ∈ ℤ ) )
63 62 adantr ⊢ ( ( ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ∧ ∀ 𝑘 ∈ { 𝑧 } 𝐵 ∈ ℤ ) → ( 𝑁 ∈ ℕ → ∀ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) ∈ ℤ ) )
64 27 63 sylbi ⊢ ( ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ → ( 𝑁 ∈ ℕ → ∀ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) ∈ ℤ ) )
65 64 impcom ⊢ ( ( 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) → ∀ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) ∈ ℤ )
66 65 3adant1 ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) → ∀ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) ∈ ℤ )
67 17 66 jca ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) → ( 𝐴 ∈ Fin ∧ ∀ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) ∈ ℤ ) )
68 fsumzcl2 ⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) ∈ ℤ ) → Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) ∈ ℤ )
69 68 zred ⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) ∈ ℤ ) → Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) ∈ ℝ )
70 67 69 syl ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) → Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) ∈ ℝ )
71 70 ad2antlr ⊢ ( ( ( 𝑧 ∉ 𝐴 ∧ ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) ) ∧ ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) → Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) ∈ ℝ )
72 35 anim1i ⊢ ( ( ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) )
73 72 ancoms ⊢ ( ( 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) → ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) )
74 zmodcl ⊢ ( ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 mod 𝑁 ) ∈ ℕ0 )
75 73 74 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) → ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 mod 𝑁 ) ∈ ℕ0 )
76 75 nn0red ⊢ ( ( 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) → ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 mod 𝑁 ) ∈ ℝ )
77 76 3adant1 ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) → ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 mod 𝑁 ) ∈ ℝ )
78 77 ad2antlr ⊢ ( ( ( 𝑧 ∉ 𝐴 ∧ ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) ) ∧ ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) → ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 mod 𝑁 ) ∈ ℝ )
79 40 ad2antlr ⊢ ( ( ( 𝑧 ∉ 𝐴 ∧ ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) ) ∧ ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) → 𝑁 ∈ ℝ+ )
80 modaddabs ⊢ ( ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) ∈ ℝ ∧ ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 mod 𝑁 ) ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → ( ( ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) + ( ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 mod 𝑁 ) mod 𝑁 ) ) mod 𝑁 ) = ( ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) + ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 mod 𝑁 ) ) mod 𝑁 ) )
81 71 78 79 80 syl3anc ⊢ ( ( ( 𝑧 ∉ 𝐴 ∧ ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) ) ∧ ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) → ( ( ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) + ( ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 mod 𝑁 ) mod 𝑁 ) ) mod 𝑁 ) = ( ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) + ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 mod 𝑁 ) ) mod 𝑁 ) )
82 60 ralimdv ⊢ ( 𝑁 ∈ ℕ → ( ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ → ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) ∈ ℤ ) )
83 82 imp ⊢ ( ( 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) → ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) ∈ ℤ )
84 83 3adant1 ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) → ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) ∈ ℤ )
85 84 ad2antlr ⊢ ( ( ( 𝑧 ∉ 𝐴 ∧ ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) ) ∧ ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) → ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) ∈ ℤ )
86 fsumsplitsnun ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑧 ∈ V ∧ 𝑧 ∉ 𝐴 ) ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) ∈ ℤ ) → Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) + ⦋ 𝑧 / 𝑘 ⦌ ( 𝐵 mod 𝑁 ) ) )
87 18 22 85 86 syl3anc ⊢ ( ( ( 𝑧 ∉ 𝐴 ∧ ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) ) ∧ ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) → Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) + ⦋ 𝑧 / 𝑘 ⦌ ( 𝐵 mod 𝑁 ) ) )
88 csbov1g ⊢ ( 𝑧 ∈ V → ⦋ 𝑧 / 𝑘 ⦌ ( 𝐵 mod 𝑁 ) = ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 mod 𝑁 ) )
89 21 88 mp1i ⊢ ( ( ( 𝑧 ∉ 𝐴 ∧ ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) ) ∧ ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) → ⦋ 𝑧 / 𝑘 ⦌ ( 𝐵 mod 𝑁 ) = ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 mod 𝑁 ) )
90 89 oveq2d ⊢ ( ( ( 𝑧 ∉ 𝐴 ∧ ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) ) ∧ ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) → ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) + ⦋ 𝑧 / 𝑘 ⦌ ( 𝐵 mod 𝑁 ) ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) + ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 mod 𝑁 ) ) )
91 87 90 eqtrd ⊢ ( ( ( 𝑧 ∉ 𝐴 ∧ ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) ) ∧ ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) → Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) + ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 mod 𝑁 ) ) )
92 91 eqcomd ⊢ ( ( ( 𝑧 ∉ 𝐴 ∧ ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) ) ∧ ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) → ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) + ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 mod 𝑁 ) ) = Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) )
93 92 oveq1d ⊢ ( ( ( 𝑧 ∉ 𝐴 ∧ ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) ) ∧ ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) → ( ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) + ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 mod 𝑁 ) ) mod 𝑁 ) = ( Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) mod 𝑁 ) )
94 81 93 eqtrd ⊢ ( ( ( 𝑧 ∉ 𝐴 ∧ ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) ) ∧ ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) → ( ( ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) + ( ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 mod 𝑁 ) mod 𝑁 ) ) mod 𝑁 ) = ( Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) mod 𝑁 ) )
95 26 57 94 3eqtrd ⊢ ( ( ( 𝑧 ∉ 𝐴 ∧ ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) ) ∧ ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) → ( Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) mod 𝑁 ) )
96 95 exp31 ⊢ ( 𝑧 ∉ 𝐴 → ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) → ( ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) → ( Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) ) )
97 16 96 sylbir ⊢ ( ¬ 𝑧 ∈ 𝐴 → ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) → ( ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) → ( Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) ) )
98 15 97 pm2.61i ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) → ( ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) → ( Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) )