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 
|- ( ph -> A e. Fin )
sumeven.b 
|- ( ( ph /\ k e. A ) -> B e. ZZ )
sumeven.e 
|- ( ( ph /\ k e. A ) -> 2 || B )
Assertion sumeven 
|- ( ph -> 2 || sum_ k e. A B )

Proof

Step Hyp Ref Expression
1 sumeven.a 
 |-  ( ph -> A e. Fin )
2 sumeven.b 
 |-  ( ( ph /\ k e. A ) -> B e. ZZ )
3 sumeven.e 
 |-  ( ( ph /\ k e. A ) -> 2 || B )
4 sumeq1 
 |-  ( x = (/) -> sum_ k e. x B = sum_ k e. (/) B )
5 4 breq2d 
 |-  ( x = (/) -> ( 2 || sum_ k e. x B <-> 2 || sum_ k e. (/) B ) )
6 sumeq1 
 |-  ( x = y -> sum_ k e. x B = sum_ k e. y B )
7 6 breq2d 
 |-  ( x = y -> ( 2 || sum_ k e. x B <-> 2 || sum_ k e. y B ) )
8 sumeq1 
 |-  ( x = ( y u. { z } ) -> sum_ k e. x B = sum_ k e. ( y u. { z } ) B )
9 8 breq2d 
 |-  ( x = ( y u. { z } ) -> ( 2 || sum_ k e. x B <-> 2 || sum_ k e. ( y u. { z } ) B ) )
10 sumeq1 
 |-  ( x = A -> sum_ k e. x B = sum_ k e. A B )
11 10 breq2d 
 |-  ( x = A -> ( 2 || sum_ k e. x B <-> 2 || sum_ k e. A B ) )
12 z0even 
 |-  2 || 0
13 sum0 
 |-  sum_ k e. (/) B = 0
14 12 13 breqtrri 
 |-  2 || sum_ k e. (/) B
15 14 a1i 
 |-  ( ph -> 2 || sum_ k e. (/) B )
16 2z 
 |-  2 e. ZZ
17 16 a1i 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> 2 e. ZZ )
18 ssfi 
 |-  ( ( A e. Fin /\ y C_ A ) -> y e. Fin )
19 18 expcom 
 |-  ( y C_ A -> ( A e. Fin -> y e. Fin ) )
20 19 adantr 
 |-  ( ( y C_ A /\ z e. ( A \ y ) ) -> ( A e. Fin -> y e. Fin ) )
21 1 20 mpan9 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> y e. Fin )
22 simpll 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ k e. y ) -> ph )
23 ssel 
 |-  ( y C_ A -> ( k e. y -> k e. A ) )
24 23 adantr 
 |-  ( ( y C_ A /\ z e. ( A \ y ) ) -> ( k e. y -> k e. A ) )
25 24 adantl 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( k e. y -> k e. A ) )
26 25 imp 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ k e. y ) -> k e. A )
27 22 26 2 syl2anc 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ k e. y ) -> B e. ZZ )
28 21 27 fsumzcl 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> sum_ k e. y B e. ZZ )
29 eldifi 
 |-  ( z e. ( A \ y ) -> z e. A )
30 29 adantl 
 |-  ( ( y C_ A /\ z e. ( A \ y ) ) -> z e. A )
31 30 adantl 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> z e. A )
32 2 adantlr 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ k e. A ) -> B e. ZZ )
33 32 ralrimiva 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> A. k e. A B e. ZZ )
34 rspcsbela 
 |-  ( ( z e. A /\ A. k e. A B e. ZZ ) -> [_ z / k ]_ B e. ZZ )
35 31 33 34 syl2anc 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> [_ z / k ]_ B e. ZZ )
36 17 28 35 3jca 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( 2 e. ZZ /\ sum_ k e. y B e. ZZ /\ [_ z / k ]_ B e. ZZ ) )
37 36 adantr 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ 2 || sum_ k e. y B ) -> ( 2 e. ZZ /\ sum_ k e. y B e. ZZ /\ [_ z / k ]_ B e. ZZ ) )
38 3 ralrimiva 
 |-  ( ph -> A. k e. A 2 || B )
39 nfcv 
 |-  F/_ k 2
40 nfcv 
 |-  F/_ k ||
41 nfcsb1v 
 |-  F/_ k [_ z / k ]_ B
42 39 40 41 nfbr 
 |-  F/ k 2 || [_ z / k ]_ B
43 csbeq1a 
 |-  ( k = z -> B = [_ z / k ]_ B )
44 43 breq2d 
 |-  ( k = z -> ( 2 || B <-> 2 || [_ z / k ]_ B ) )
45 42 44 rspc 
 |-  ( z e. A -> ( A. k e. A 2 || B -> 2 || [_ z / k ]_ B ) )
46 29 38 45 syl2imc 
 |-  ( ph -> ( z e. ( A \ y ) -> 2 || [_ z / k ]_ B ) )
47 46 a1d 
 |-  ( ph -> ( y C_ A -> ( z e. ( A \ y ) -> 2 || [_ z / k ]_ B ) ) )
48 47 imp32 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> 2 || [_ z / k ]_ B )
49 48 anim1ci 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ 2 || sum_ k e. y B ) -> ( 2 || sum_ k e. y B /\ 2 || [_ z / k ]_ B ) )
50 dvds2add 
 |-  ( ( 2 e. ZZ /\ sum_ k e. y B e. ZZ /\ [_ z / k ]_ B e. ZZ ) -> ( ( 2 || sum_ k e. y B /\ 2 || [_ z / k ]_ B ) -> 2 || ( sum_ k e. y B + [_ z / k ]_ B ) ) )
51 37 49 50 sylc 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ 2 || sum_ k e. y B ) -> 2 || ( sum_ k e. y B + [_ z / k ]_ B ) )
52 vex 
 |-  z e. _V
53 52 a1i 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> z e. _V )
54 eldif 
 |-  ( z e. ( A \ y ) <-> ( z e. A /\ -. z e. y ) )
55 df-nel 
 |-  ( z e/ y <-> -. z e. y )
56 55 biimpri 
 |-  ( -. z e. y -> z e/ y )
57 54 56 simplbiim 
 |-  ( z e. ( A \ y ) -> z e/ y )
58 57 adantl 
 |-  ( ( y C_ A /\ z e. ( A \ y ) ) -> z e/ y )
59 58 adantl 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> z e/ y )
60 simpll 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ k e. ( y u. { z } ) ) -> ph )
61 elun 
 |-  ( k e. ( y u. { z } ) <-> ( k e. y \/ k e. { z } ) )
62 24 com12 
 |-  ( k e. y -> ( ( y C_ A /\ z e. ( A \ y ) ) -> k e. A ) )
63 elsni 
 |-  ( k e. { z } -> k = z )
64 eleq1w 
 |-  ( k = z -> ( k e. A <-> z e. A ) )
65 30 64 imbitrrid 
 |-  ( k = z -> ( ( y C_ A /\ z e. ( A \ y ) ) -> k e. A ) )
66 63 65 syl 
 |-  ( k e. { z } -> ( ( y C_ A /\ z e. ( A \ y ) ) -> k e. A ) )
67 62 66 jaoi 
 |-  ( ( k e. y \/ k e. { z } ) -> ( ( y C_ A /\ z e. ( A \ y ) ) -> k e. A ) )
68 67 com12 
 |-  ( ( y C_ A /\ z e. ( A \ y ) ) -> ( ( k e. y \/ k e. { z } ) -> k e. A ) )
69 61 68 biimtrid 
 |-  ( ( y C_ A /\ z e. ( A \ y ) ) -> ( k e. ( y u. { z } ) -> k e. A ) )
70 69 adantl 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( k e. ( y u. { z } ) -> k e. A ) )
71 70 imp 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ k e. ( y u. { z } ) ) -> k e. A )
72 60 71 2 syl2anc 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ k e. ( y u. { z } ) ) -> B e. ZZ )
73 72 ralrimiva 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> A. k e. ( y u. { z } ) B e. ZZ )
74 fsumsplitsnun 
 |-  ( ( y e. Fin /\ ( z e. _V /\ z e/ y ) /\ A. k e. ( y u. { z } ) B e. ZZ ) -> sum_ k e. ( y u. { z } ) B = ( sum_ k e. y B + [_ z / k ]_ B ) )
75 21 53 59 73 74 syl121anc 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> sum_ k e. ( y u. { z } ) B = ( sum_ k e. y B + [_ z / k ]_ B ) )
76 75 adantr 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ 2 || sum_ k e. y B ) -> sum_ k e. ( y u. { z } ) B = ( sum_ k e. y B + [_ z / k ]_ B ) )
77 51 76 breqtrrd 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ 2 || sum_ k e. y B ) -> 2 || sum_ k e. ( y u. { z } ) B )
78 77 ex 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( 2 || sum_ k e. y B -> 2 || sum_ k e. ( y u. { z } ) B ) )
79 5 7 9 11 15 78 1 findcard2d 
 |-  ( ph -> 2 || sum_ k e. A B )