Metamath Proof Explorer

Theorem modfsummod

Description: A finite sum modulo a positive integer equals the finite sum of their summands modulo the positive integer, modulo the positive integer. (Contributed by Alexander van der Vekens, 1-Sep-2018)

Ref Expression
Hypotheses modfsummod.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
modfsummod.1 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
modfsummod.2 ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ )
Assertion modfsummod ( 𝜑 → ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) )

Proof

Step Hyp Ref Expression
1 modfsummod.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2 modfsummod.1 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
3 modfsummod.2 ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ )
4 raleq ⊢ ( 𝑥 = ∅ → ( ∀ 𝑘 ∈ 𝑥 𝐵 ∈ ℤ ↔ ∀ 𝑘 ∈ ∅ 𝐵 ∈ ℤ ) )
5 4 anbi1d ⊢ ( 𝑥 = ∅ → ( ( ∀ 𝑘 ∈ 𝑥 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ↔ ( ∀ 𝑘 ∈ ∅ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ) )
6 sumeq1 ⊢ ( 𝑥 = ∅ → Σ 𝑘 ∈ 𝑥 𝐵 = Σ 𝑘 ∈ ∅ 𝐵 )
7 6 oveq1d ⊢ ( 𝑥 = ∅ → ( Σ 𝑘 ∈ 𝑥 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ ∅ 𝐵 mod 𝑁 ) )
8 sumeq1 ⊢ ( 𝑥 = ∅ → Σ 𝑘 ∈ 𝑥 ( 𝐵 mod 𝑁 ) = Σ 𝑘 ∈ ∅ ( 𝐵 mod 𝑁 ) )
9 8 oveq1d ⊢ ( 𝑥 = ∅ → ( Σ 𝑘 ∈ 𝑥 ( 𝐵 mod 𝑁 ) mod 𝑁 ) = ( Σ 𝑘 ∈ ∅ ( 𝐵 mod 𝑁 ) mod 𝑁 ) )
10 7 9 eqeq12d ⊢ ( 𝑥 = ∅ → ( ( Σ 𝑘 ∈ 𝑥 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝑥 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ↔ ( Σ 𝑘 ∈ ∅ 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ ∅ ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) )
11 5 10 imbi12d ⊢ ( 𝑥 = ∅ → ( ( ( ∀ 𝑘 ∈ 𝑥 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( Σ 𝑘 ∈ 𝑥 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝑥 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) ↔ ( ( ∀ 𝑘 ∈ ∅ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( Σ 𝑘 ∈ ∅ 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ ∅ ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) ) )
12 raleq ⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑘 ∈ 𝑥 𝐵 ∈ ℤ ↔ ∀ 𝑘 ∈ 𝑦 𝐵 ∈ ℤ ) )
13 12 anbi1d ⊢ ( 𝑥 = 𝑦 → ( ( ∀ 𝑘 ∈ 𝑥 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ↔ ( ∀ 𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ) )
14 sumeq1 ⊢ ( 𝑥 = 𝑦 → Σ 𝑘 ∈ 𝑥 𝐵 = Σ 𝑘 ∈ 𝑦 𝐵 )
15 14 oveq1d ⊢ ( 𝑥 = 𝑦 → ( Σ 𝑘 ∈ 𝑥 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝑦 𝐵 mod 𝑁 ) )
16 sumeq1 ⊢ ( 𝑥 = 𝑦 → Σ 𝑘 ∈ 𝑥 ( 𝐵 mod 𝑁 ) = Σ 𝑘 ∈ 𝑦 ( 𝐵 mod 𝑁 ) )
17 16 oveq1d ⊢ ( 𝑥 = 𝑦 → ( Σ 𝑘 ∈ 𝑥 ( 𝐵 mod 𝑁 ) mod 𝑁 ) = ( Σ 𝑘 ∈ 𝑦 ( 𝐵 mod 𝑁 ) mod 𝑁 ) )
18 15 17 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( Σ 𝑘 ∈ 𝑥 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝑥 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ↔ ( Σ 𝑘 ∈ 𝑦 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝑦 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) )
19 13 18 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( ∀ 𝑘 ∈ 𝑥 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( Σ 𝑘 ∈ 𝑥 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝑥 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) ↔ ( ( ∀ 𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( Σ 𝑘 ∈ 𝑦 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝑦 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) ) )
20 raleq ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ∀ 𝑘 ∈ 𝑥 𝐵 ∈ ℤ ↔ ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) )
21 20 anbi1d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( ∀ 𝑘 ∈ 𝑥 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ↔ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ) )
22 sumeq1 ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → Σ 𝑘 ∈ 𝑥 𝐵 = Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 )
23 22 oveq1d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( Σ 𝑘 ∈ 𝑥 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 mod 𝑁 ) )
24 sumeq1 ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → Σ 𝑘 ∈ 𝑥 ( 𝐵 mod 𝑁 ) = Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) )
25 24 oveq1d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( Σ 𝑘 ∈ 𝑥 ( 𝐵 mod 𝑁 ) mod 𝑁 ) = ( Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) mod 𝑁 ) )
26 23 25 eqeq12d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( Σ 𝑘 ∈ 𝑥 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝑥 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ↔ ( Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) )
27 21 26 imbi12d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( ( ∀ 𝑘 ∈ 𝑥 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( Σ 𝑘 ∈ 𝑥 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝑥 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) ↔ ( ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) ) )
28 raleq ⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑘 ∈ 𝑥 𝐵 ∈ ℤ ↔ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) )
29 28 anbi1d ⊢ ( 𝑥 = 𝐴 → ( ( ∀ 𝑘 ∈ 𝑥 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ↔ ( ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ) )
30 sumeq1 ⊢ ( 𝑥 = 𝐴 → Σ 𝑘 ∈ 𝑥 𝐵 = Σ 𝑘 ∈ 𝐴 𝐵 )
31 30 oveq1d ⊢ ( 𝑥 = 𝐴 → ( Σ 𝑘 ∈ 𝑥 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) )
32 sumeq1 ⊢ ( 𝑥 = 𝐴 → Σ 𝑘 ∈ 𝑥 ( 𝐵 mod 𝑁 ) = Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) )
33 32 oveq1d ⊢ ( 𝑥 = 𝐴 → ( Σ 𝑘 ∈ 𝑥 ( 𝐵 mod 𝑁 ) mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) )
34 31 33 eqeq12d ⊢ ( 𝑥 = 𝐴 → ( ( Σ 𝑘 ∈ 𝑥 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝑥 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ↔ ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) )
35 29 34 imbi12d ⊢ ( 𝑥 = 𝐴 → ( ( ( ∀ 𝑘 ∈ 𝑥 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( Σ 𝑘 ∈ 𝑥 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝑥 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) ↔ ( ( ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) ) )
36 sum0 ⊢ Σ 𝑘 ∈ ∅ 𝐵 = 0
37 36 oveq1i ⊢ ( Σ 𝑘 ∈ ∅ 𝐵 mod 𝑁 ) = ( 0 mod 𝑁 )
38 sum0 ⊢ Σ 𝑘 ∈ ∅ ( 𝐵 mod 𝑁 ) = 0
39 38 a1i ⊢ ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ ∅ ( 𝐵 mod 𝑁 ) = 0 )
40 39 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( Σ 𝑘 ∈ ∅ ( 𝐵 mod 𝑁 ) mod 𝑁 ) = ( 0 mod 𝑁 ) )
41 37 40 eqtr4id ⊢ ( 𝑁 ∈ ℕ → ( Σ 𝑘 ∈ ∅ 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ ∅ ( 𝐵 mod 𝑁 ) mod 𝑁 ) )
42 41 adantl ⊢ ( ( ∀ 𝑘 ∈ ∅ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( Σ 𝑘 ∈ ∅ 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ ∅ ( 𝐵 mod 𝑁 ) mod 𝑁 ) )
43 simpll ⊢ ( ( ( 𝑦 ∈ Fin ∧ ( ∀ 𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ) ∧ ∀ 𝑘 ∈ { 𝑧 } 𝐵 ∈ ℤ ) → 𝑦 ∈ Fin )
44 simplrr ⊢ ( ( ( 𝑦 ∈ Fin ∧ ( ∀ 𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ) ∧ ∀ 𝑘 ∈ { 𝑧 } 𝐵 ∈ ℤ ) → 𝑁 ∈ ℕ )
45 ralun ⊢ ( ( ∀ 𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ ∀ 𝑘 ∈ { 𝑧 } 𝐵 ∈ ℤ ) → ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ ℤ )
46 45 ex ⊢ ( ∀ 𝑘 ∈ 𝑦 𝐵 ∈ ℤ → ( ∀ 𝑘 ∈ { 𝑧 } 𝐵 ∈ ℤ → ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) )
47 46 ad2antrl ⊢ ( ( 𝑦 ∈ Fin ∧ ( ∀ 𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ) → ( ∀ 𝑘 ∈ { 𝑧 } 𝐵 ∈ ℤ → ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) )
48 47 imp ⊢ ( ( ( 𝑦 ∈ Fin ∧ ( ∀ 𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ) ∧ ∀ 𝑘 ∈ { 𝑧 } 𝐵 ∈ ℤ ) → ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ ℤ )
49 modfsummods ⊢ ( ( 𝑦 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) → ( ( Σ 𝑘 ∈ 𝑦 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝑦 ( 𝐵 mod 𝑁 ) mod 𝑁 ) → ( Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) )
50 43 44 48 49 syl3anc ⊢ ( ( ( 𝑦 ∈ Fin ∧ ( ∀ 𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ) ∧ ∀ 𝑘 ∈ { 𝑧 } 𝐵 ∈ ℤ ) → ( ( Σ 𝑘 ∈ 𝑦 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝑦 ( 𝐵 mod 𝑁 ) mod 𝑁 ) → ( Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) )
51 50 ex ⊢ ( ( 𝑦 ∈ Fin ∧ ( ∀ 𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ) → ( ∀ 𝑘 ∈ { 𝑧 } 𝐵 ∈ ℤ → ( ( Σ 𝑘 ∈ 𝑦 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝑦 ( 𝐵 mod 𝑁 ) mod 𝑁 ) → ( Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) ) )
52 51 com23 ⊢ ( ( 𝑦 ∈ Fin ∧ ( ∀ 𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ) → ( ( Σ 𝑘 ∈ 𝑦 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝑦 ( 𝐵 mod 𝑁 ) mod 𝑁 ) → ( ∀ 𝑘 ∈ { 𝑧 } 𝐵 ∈ ℤ → ( Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) ) )
53 52 ex ⊢ ( 𝑦 ∈ Fin → ( ( ∀ 𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( Σ 𝑘 ∈ 𝑦 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝑦 ( 𝐵 mod 𝑁 ) mod 𝑁 ) → ( ∀ 𝑘 ∈ { 𝑧 } 𝐵 ∈ ℤ → ( Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) ) ) )
54 53 a2d ⊢ ( 𝑦 ∈ Fin → ( ( ( ∀ 𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( Σ 𝑘 ∈ 𝑦 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝑦 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) → ( ( ∀ 𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ∀ 𝑘 ∈ { 𝑧 } 𝐵 ∈ ℤ → ( Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) ) ) )
55 ralunb ⊢ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ↔ ( ∀ 𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ ∀ 𝑘 ∈ { 𝑧 } 𝐵 ∈ ℤ ) )
56 55 anbi1i ⊢ ( ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ↔ ( ( ∀ 𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ ∀ 𝑘 ∈ { 𝑧 } 𝐵 ∈ ℤ ) ∧ 𝑁 ∈ ℕ ) )
57 56 imbi1i ⊢ ( ( ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) ↔ ( ( ( ∀ 𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ ∀ 𝑘 ∈ { 𝑧 } 𝐵 ∈ ℤ ) ∧ 𝑁 ∈ ℕ ) → ( Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) )
58 an32 ⊢ ( ( ( ∀ 𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ ∀ 𝑘 ∈ { 𝑧 } 𝐵 ∈ ℤ ) ∧ 𝑁 ∈ ℕ ) ↔ ( ( ∀ 𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ∀ 𝑘 ∈ { 𝑧 } 𝐵 ∈ ℤ ) )
59 58 imbi1i ⊢ ( ( ( ( ∀ 𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ ∀ 𝑘 ∈ { 𝑧 } 𝐵 ∈ ℤ ) ∧ 𝑁 ∈ ℕ ) → ( Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) ↔ ( ( ( ∀ 𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ∀ 𝑘 ∈ { 𝑧 } 𝐵 ∈ ℤ ) → ( Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) )
60 impexp ⊢ ( ( ( ( ∀ 𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ∀ 𝑘 ∈ { 𝑧 } 𝐵 ∈ ℤ ) → ( Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) ↔ ( ( ∀ 𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ∀ 𝑘 ∈ { 𝑧 } 𝐵 ∈ ℤ → ( Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) ) )
61 57 59 60 3bitri ⊢ ( ( ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) ↔ ( ( ∀ 𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ∀ 𝑘 ∈ { 𝑧 } 𝐵 ∈ ℤ → ( Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) ) )
62 54 61 imbitrrdi ⊢ ( 𝑦 ∈ Fin → ( ( ( ∀ 𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( Σ 𝑘 ∈ 𝑦 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝑦 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) → ( ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) ) )
63 11 19 27 35 42 62 findcard2 ⊢ ( 𝐴 ∈ Fin → ( ( ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) )
64 2 63 syl ⊢ ( 𝜑 → ( ( ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) ) )
65 3 1 64 mp2and ⊢ ( 𝜑 → ( Σ 𝑘 ∈ 𝐴 𝐵 mod 𝑁 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑁 ) mod 𝑁 ) )