Metamath Proof Explorer

Theorem sumeven

Description: If every term in a sum is even, then so is the sum. (Contributed by AV, 14-Aug-2021)

Ref Expression
Hypotheses sumeven.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
sumeven.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℤ )
sumeven.e ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 2 ∥ 𝐵 )
Assertion sumeven ( 𝜑 → 2 ∥ Σ 𝑘 ∈ 𝐴 𝐵 )

Proof

Step Hyp Ref Expression
1 sumeven.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
2 sumeven.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℤ )
3 sumeven.e ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 2 ∥ 𝐵 )
4 sumeq1 ⊢ ( 𝑥 = ∅ → Σ 𝑘 ∈ 𝑥 𝐵 = Σ 𝑘 ∈ ∅ 𝐵 )
5 4 breq2d ⊢ ( 𝑥 = ∅ → ( 2 ∥ Σ 𝑘 ∈ 𝑥 𝐵 ↔ 2 ∥ Σ 𝑘 ∈ ∅ 𝐵 ) )
6 sumeq1 ⊢ ( 𝑥 = 𝑦 → Σ 𝑘 ∈ 𝑥 𝐵 = Σ 𝑘 ∈ 𝑦 𝐵 )
7 6 breq2d ⊢ ( 𝑥 = 𝑦 → ( 2 ∥ Σ 𝑘 ∈ 𝑥 𝐵 ↔ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) )
8 sumeq1 ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → Σ 𝑘 ∈ 𝑥 𝐵 = Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 )
9 8 breq2d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 2 ∥ Σ 𝑘 ∈ 𝑥 𝐵 ↔ 2 ∥ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) )
10 sumeq1 ⊢ ( 𝑥 = 𝐴 → Σ 𝑘 ∈ 𝑥 𝐵 = Σ 𝑘 ∈ 𝐴 𝐵 )
11 10 breq2d ⊢ ( 𝑥 = 𝐴 → ( 2 ∥ Σ 𝑘 ∈ 𝑥 𝐵 ↔ 2 ∥ Σ 𝑘 ∈ 𝐴 𝐵 ) )
12 z0even ⊢ 2 ∥ 0
13 sum0 ⊢ Σ 𝑘 ∈ ∅ 𝐵 = 0
14 12 13 breqtrri ⊢ 2 ∥ Σ 𝑘 ∈ ∅ 𝐵
15 14 a1i ⊢ ( 𝜑 → 2 ∥ Σ 𝑘 ∈ ∅ 𝐵 )
16 2z ⊢ 2 ∈ ℤ
17 16 a1i ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → 2 ∈ ℤ )
18 ssfi ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑦 ⊆ 𝐴 ) → 𝑦 ∈ Fin )
19 18 expcom ⊢ ( 𝑦 ⊆ 𝐴 → ( 𝐴 ∈ Fin → 𝑦 ∈ Fin ) )
20 19 adantr ⊢ ( ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) → ( 𝐴 ∈ Fin → 𝑦 ∈ Fin ) )
21 1 20 mpan9 ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → 𝑦 ∈ Fin )
22 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 𝑘 ∈ 𝑦 ) → 𝜑 )
23 ssel ⊢ ( 𝑦 ⊆ 𝐴 → ( 𝑘 ∈ 𝑦 → 𝑘 ∈ 𝐴 ) )
24 23 adantr ⊢ ( ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) → ( 𝑘 ∈ 𝑦 → 𝑘 ∈ 𝐴 ) )
25 24 adantl ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( 𝑘 ∈ 𝑦 → 𝑘 ∈ 𝐴 ) )
26 25 imp ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 𝑘 ∈ 𝑦 ) → 𝑘 ∈ 𝐴 )
27 22 26 2 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 𝑘 ∈ 𝑦 ) → 𝐵 ∈ ℤ )
28 21 27 fsumzcl ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → Σ 𝑘 ∈ 𝑦 𝐵 ∈ ℤ )
29 eldifi ⊢ ( 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) → 𝑧 ∈ 𝐴 )
30 29 adantl ⊢ ( ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) → 𝑧 ∈ 𝐴 )
31 30 adantl ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → 𝑧 ∈ 𝐴 )
32 2 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℤ )
33 32 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ )
34 rspcsbela ⊢ ( ( 𝑧 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) → ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℤ )
35 31 33 34 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℤ )
36 17 28 35 3jca ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( 2 ∈ ℤ ∧ Σ 𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℤ ) )
37 36 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) → ( 2 ∈ ℤ ∧ Σ 𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℤ ) )
38 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 2 ∥ 𝐵 )
39 nfcv ⊢ Ⅎ 𝑘 2
40 nfcv ⊢ Ⅎ 𝑘 ∥
41 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑧 / 𝑘 ⦌ 𝐵
42 39 40 41 nfbr ⊢ Ⅎ 𝑘 2 ∥ ⦋ 𝑧 / 𝑘 ⦌ 𝐵
43 csbeq1a ⊢ ( 𝑘 = 𝑧 → 𝐵 = ⦋ 𝑧 / 𝑘 ⦌ 𝐵 )
44 43 breq2d ⊢ ( 𝑘 = 𝑧 → ( 2 ∥ 𝐵 ↔ 2 ∥ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
45 42 44 rspc ⊢ ( 𝑧 ∈ 𝐴 → ( ∀ 𝑘 ∈ 𝐴 2 ∥ 𝐵 → 2 ∥ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
46 29 38 45 syl2imc ⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) → 2 ∥ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
47 46 a1d ⊢ ( 𝜑 → ( 𝑦 ⊆ 𝐴 → ( 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) → 2 ∥ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) )
48 47 imp32 ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → 2 ∥ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 )
49 48 anim1ci ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) → ( 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ∧ 2 ∥ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
50 dvds2add ⊢ ( ( 2 ∈ ℤ ∧ Σ 𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℤ ) → ( ( 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ∧ 2 ∥ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) → 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) )
51 37 49 50 sylc ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) → 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
52 vex ⊢ 𝑧 ∈ V
53 52 a1i ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → 𝑧 ∈ V )
54 eldif ⊢ ( 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ↔ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦 ) )
55 df-nel ⊢ ( 𝑧 ∉ 𝑦 ↔ ¬ 𝑧 ∈ 𝑦 )
56 55 biimpri ⊢ ( ¬ 𝑧 ∈ 𝑦 → 𝑧 ∉ 𝑦 )
57 54 56 simplbiim ⊢ ( 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) → 𝑧 ∉ 𝑦 )
58 57 adantl ⊢ ( ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) → 𝑧 ∉ 𝑦 )
59 58 adantl ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → 𝑧 ∉ 𝑦 )
60 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ) → 𝜑 )
61 elun ⊢ ( 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ↔ ( 𝑘 ∈ 𝑦 ∨ 𝑘 ∈ { 𝑧 } ) )
62 24 com12 ⊢ ( 𝑘 ∈ 𝑦 → ( ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) → 𝑘 ∈ 𝐴 ) )
63 elsni ⊢ ( 𝑘 ∈ { 𝑧 } → 𝑘 = 𝑧 )
64 eleq1w ⊢ ( 𝑘 = 𝑧 → ( 𝑘 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) )
65 30 64 imbitrrid ⊢ ( 𝑘 = 𝑧 → ( ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) → 𝑘 ∈ 𝐴 ) )
66 63 65 syl ⊢ ( 𝑘 ∈ { 𝑧 } → ( ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) → 𝑘 ∈ 𝐴 ) )
67 62 66 jaoi ⊢ ( ( 𝑘 ∈ 𝑦 ∨ 𝑘 ∈ { 𝑧 } ) → ( ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) → 𝑘 ∈ 𝐴 ) )
68 67 com12 ⊢ ( ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) → ( ( 𝑘 ∈ 𝑦 ∨ 𝑘 ∈ { 𝑧 } ) → 𝑘 ∈ 𝐴 ) )
69 61 68 biimtrid ⊢ ( ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) → ( 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) → 𝑘 ∈ 𝐴 ) )
70 69 adantl ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) → 𝑘 ∈ 𝐴 ) )
71 70 imp ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ) → 𝑘 ∈ 𝐴 )
72 60 71 2 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ) → 𝐵 ∈ ℤ )
73 72 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ ℤ )
74 fsumsplitsnun ⊢ ( ( 𝑦 ∈ Fin ∧ ( 𝑧 ∈ V ∧ 𝑧 ∉ 𝑦 ) ∧ ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) → Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 = ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
75 21 53 59 73 74 syl121anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 = ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
76 75 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) → Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 = ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
77 51 76 breqtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) → 2 ∥ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 )
78 77 ex ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 → 2 ∥ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) )
79 5 7 9 11 15 78 1 findcard2d ⊢ ( 𝜑 → 2 ∥ Σ 𝑘 ∈ 𝐴 𝐵 )