Metamath Proof Explorer

Theorem sumodd

Description: If every term in a sum is odd, then the sum is even iff the number of terms in the sum is even. (Contributed by AV, 14-Aug-2021)

Ref Expression
Hypotheses sumeven.a 
|- ( ph -> A e. Fin )
sumeven.b 
|- ( ( ph /\ k e. A ) -> B e. ZZ )
sumodd.o 
|- ( ( ph /\ k e. A ) -> -. 2 || B )
Assertion sumodd 
|- ( ph -> ( 2 || ( # ` A ) <-> 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 sumodd.o 
 |-  ( ( ph /\ k e. A ) -> -. 2 || B )
4 fveq2 
 |-  ( x = (/) -> ( # ` x ) = ( # ` (/) ) )
5 hash0 
 |-  ( # ` (/) ) = 0
6 4 5 eqtrdi 
 |-  ( x = (/) -> ( # ` x ) = 0 )
7 6 breq2d 
 |-  ( x = (/) -> ( 2 || ( # ` x ) <-> 2 || 0 ) )
8 sumeq1 
 |-  ( x = (/) -> sum_ k e. x B = sum_ k e. (/) B )
9 sum0 
 |-  sum_ k e. (/) B = 0
10 8 9 eqtrdi 
 |-  ( x = (/) -> sum_ k e. x B = 0 )
11 10 breq2d 
 |-  ( x = (/) -> ( 2 || sum_ k e. x B <-> 2 || 0 ) )
12 7 11 bibi12d 
 |-  ( x = (/) -> ( ( 2 || ( # ` x ) <-> 2 || sum_ k e. x B ) <-> ( 2 || 0 <-> 2 || 0 ) ) )
13 fveq2 
 |-  ( x = y -> ( # ` x ) = ( # ` y ) )
14 13 breq2d 
 |-  ( x = y -> ( 2 || ( # ` x ) <-> 2 || ( # ` y ) ) )
15 sumeq1 
 |-  ( x = y -> sum_ k e. x B = sum_ k e. y B )
16 15 breq2d 
 |-  ( x = y -> ( 2 || sum_ k e. x B <-> 2 || sum_ k e. y B ) )
17 14 16 bibi12d 
 |-  ( x = y -> ( ( 2 || ( # ` x ) <-> 2 || sum_ k e. x B ) <-> ( 2 || ( # ` y ) <-> 2 || sum_ k e. y B ) ) )
18 fveq2 
 |-  ( x = ( y u. { z } ) -> ( # ` x ) = ( # ` ( y u. { z } ) ) )
19 18 breq2d 
 |-  ( x = ( y u. { z } ) -> ( 2 || ( # ` x ) <-> 2 || ( # ` ( y u. { z } ) ) ) )
20 sumeq1 
 |-  ( x = ( y u. { z } ) -> sum_ k e. x B = sum_ k e. ( y u. { z } ) B )
21 20 breq2d 
 |-  ( x = ( y u. { z } ) -> ( 2 || sum_ k e. x B <-> 2 || sum_ k e. ( y u. { z } ) B ) )
22 19 21 bibi12d 
 |-  ( x = ( y u. { z } ) -> ( ( 2 || ( # ` x ) <-> 2 || sum_ k e. x B ) <-> ( 2 || ( # ` ( y u. { z } ) ) <-> 2 || sum_ k e. ( y u. { z } ) B ) ) )
23 fveq2 
 |-  ( x = A -> ( # ` x ) = ( # ` A ) )
24 23 breq2d 
 |-  ( x = A -> ( 2 || ( # ` x ) <-> 2 || ( # ` A ) ) )
25 sumeq1 
 |-  ( x = A -> sum_ k e. x B = sum_ k e. A B )
26 25 breq2d 
 |-  ( x = A -> ( 2 || sum_ k e. x B <-> 2 || sum_ k e. A B ) )
27 24 26 bibi12d 
 |-  ( x = A -> ( ( 2 || ( # ` x ) <-> 2 || sum_ k e. x B ) <-> ( 2 || ( # ` A ) <-> 2 || sum_ k e. A B ) ) )
28 biidd 
 |-  ( ph -> ( 2 || 0 <-> 2 || 0 ) )
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 3 ralrimiva 
 |-  ( ph -> A. k e. A -. 2 || B )
37 nfcv 
 |-  F/_ k 2
38 nfcv 
 |-  F/_ k ||
39 nfcsb1v 
 |-  F/_ k [_ z / k ]_ B
40 37 38 39 nfbr 
 |-  F/ k 2 || [_ z / k ]_ B
41 40 nfn 
 |-  F/ k -. 2 || [_ z / k ]_ B
42 csbeq1a 
 |-  ( k = z -> B = [_ z / k ]_ B )
43 42 breq2d 
 |-  ( k = z -> ( 2 || B <-> 2 || [_ z / k ]_ B ) )
44 43 notbid 
 |-  ( k = z -> ( -. 2 || B <-> -. 2 || [_ z / k ]_ B ) )
45 41 44 rspc 
 |-  ( z e. A -> ( A. k e. A -. 2 || B -> -. 2 || [_ z / k ]_ B ) )
46 29 45 syl 
 |-  ( z e. ( A \ y ) -> ( A. k e. A -. 2 || B -> -. 2 || [_ z / k ]_ B ) )
47 36 46 syl5com 
 |-  ( ph -> ( z e. ( A \ y ) -> -. 2 || [_ z / k ]_ B ) )
48 47 a1d 
 |-  ( ph -> ( y C_ A -> ( z e. ( A \ y ) -> -. 2 || [_ z / k ]_ B ) ) )
49 48 imp32 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> -. 2 || [_ z / k ]_ B )
50 35 49 jca 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( [_ z / k ]_ B e. ZZ /\ -. 2 || [_ z / k ]_ B ) )
51 50 adantr 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ 2 || sum_ k e. y B ) -> ( [_ z / k ]_ B e. ZZ /\ -. 2 || [_ z / k ]_ B ) )
52 ssfi 
 |-  ( ( A e. Fin /\ y C_ A ) -> y e. Fin )
53 52 expcom 
 |-  ( y C_ A -> ( A e. Fin -> y e. Fin ) )
54 53 adantr 
 |-  ( ( y C_ A /\ z e. ( A \ y ) ) -> ( A e. Fin -> y e. Fin ) )
55 1 54 syl5com 
 |-  ( ph -> ( ( y C_ A /\ z e. ( A \ y ) ) -> y e. Fin ) )
56 55 imp 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> y e. Fin )
57 simpll 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ k e. y ) -> ph )
58 ssel 
 |-  ( y C_ A -> ( k e. y -> k e. A ) )
59 58 adantr 
 |-  ( ( y C_ A /\ z e. ( A \ y ) ) -> ( k e. y -> k e. A ) )
60 59 adantl 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( k e. y -> k e. A ) )
61 60 imp 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ k e. y ) -> k e. A )
62 57 61 2 syl2anc 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ k e. y ) -> B e. ZZ )
63 56 62 fsumzcl 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> sum_ k e. y B e. ZZ )
64 63 anim1i 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ 2 || sum_ k e. y B ) -> ( sum_ k e. y B e. ZZ /\ 2 || sum_ k e. y B ) )
65 opeo 
 |-  ( ( ( [_ z / k ]_ B e. ZZ /\ -. 2 || [_ z / k ]_ B ) /\ ( sum_ k e. y B e. ZZ /\ 2 || sum_ k e. y B ) ) -> -. 2 || ( [_ z / k ]_ B + sum_ k e. y B ) )
66 51 64 65 syl2anc 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ 2 || sum_ k e. y B ) -> -. 2 || ( [_ z / k ]_ B + sum_ k e. y B ) )
67 63 zcnd 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> sum_ k e. y B e. CC )
68 35 zcnd 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> [_ z / k ]_ B e. CC )
69 addcom 
 |-  ( ( sum_ k e. y B e. CC /\ [_ z / k ]_ B e. CC ) -> ( sum_ k e. y B + [_ z / k ]_ B ) = ( [_ z / k ]_ B + sum_ k e. y B ) )
70 69 breq2d 
 |-  ( ( sum_ k e. y B e. CC /\ [_ z / k ]_ B e. CC ) -> ( 2 || ( sum_ k e. y B + [_ z / k ]_ B ) <-> 2 || ( [_ z / k ]_ B + sum_ k e. y B ) ) )
71 70 notbid 
 |-  ( ( sum_ k e. y B e. CC /\ [_ z / k ]_ B e. CC ) -> ( -. 2 || ( sum_ k e. y B + [_ z / k ]_ B ) <-> -. 2 || ( [_ z / k ]_ B + sum_ k e. y B ) ) )
72 67 68 71 syl2anc 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( -. 2 || ( sum_ k e. y B + [_ z / k ]_ B ) <-> -. 2 || ( [_ z / k ]_ B + sum_ k e. y B ) ) )
73 72 adantr 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ 2 || sum_ k e. y B ) -> ( -. 2 || ( sum_ k e. y B + [_ z / k ]_ B ) <-> -. 2 || ( [_ z / k ]_ B + sum_ k e. y B ) ) )
74 66 73 mpbird 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ 2 || sum_ k e. y B ) -> -. 2 || ( sum_ k e. y B + [_ z / k ]_ B ) )
75 74 ex 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( 2 || sum_ k e. y B -> -. 2 || ( sum_ k e. y B + [_ z / k ]_ B ) ) )
76 63 anim1i 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ -. 2 || sum_ k e. y B ) -> ( sum_ k e. y B e. ZZ /\ -. 2 || sum_ k e. y B ) )
77 50 adantr 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ -. 2 || sum_ k e. y B ) -> ( [_ z / k ]_ B e. ZZ /\ -. 2 || [_ z / k ]_ B ) )
78 opoe 
 |-  ( ( ( sum_ k e. y B e. ZZ /\ -. 2 || sum_ k e. y B ) /\ ( [_ z / k ]_ B e. ZZ /\ -. 2 || [_ z / k ]_ B ) ) -> 2 || ( sum_ k e. y B + [_ z / k ]_ B ) )
79 76 77 78 syl2anc 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ -. 2 || sum_ k e. y B ) -> 2 || ( sum_ k e. y B + [_ z / k ]_ B ) )
80 79 ex 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( -. 2 || sum_ k e. y B -> 2 || ( sum_ k e. y B + [_ z / k ]_ B ) ) )
81 80 con1d 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( -. 2 || ( sum_ k e. y B + [_ z / k ]_ B ) -> 2 || sum_ k e. y B ) )
82 75 81 impbid 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( 2 || sum_ k e. y B <-> -. 2 || ( sum_ k e. y B + [_ z / k ]_ B ) ) )
83 bitr3 
 |-  ( ( 2 || sum_ k e. y B <-> -. 2 || ( sum_ k e. y B + [_ z / k ]_ B ) ) -> ( ( 2 || sum_ k e. y B <-> -. 2 || ( ( # ` y ) + 1 ) ) -> ( -. 2 || ( sum_ k e. y B + [_ z / k ]_ B ) <-> -. 2 || ( ( # ` y ) + 1 ) ) ) )
84 82 83 syl 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( ( 2 || sum_ k e. y B <-> -. 2 || ( ( # ` y ) + 1 ) ) -> ( -. 2 || ( sum_ k e. y B + [_ z / k ]_ B ) <-> -. 2 || ( ( # ` y ) + 1 ) ) ) )
85 bicom 
 |-  ( ( -. 2 || ( ( # ` y ) + 1 ) <-> 2 || sum_ k e. y B ) <-> ( 2 || sum_ k e. y B <-> -. 2 || ( ( # ` y ) + 1 ) ) )
86 bicom 
 |-  ( ( -. 2 || ( ( # ` y ) + 1 ) <-> -. 2 || ( sum_ k e. y B + [_ z / k ]_ B ) ) <-> ( -. 2 || ( sum_ k e. y B + [_ z / k ]_ B ) <-> -. 2 || ( ( # ` y ) + 1 ) ) )
87 84 85 86 3imtr4g 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( ( -. 2 || ( ( # ` y ) + 1 ) <-> 2 || sum_ k e. y B ) -> ( -. 2 || ( ( # ` y ) + 1 ) <-> -. 2 || ( sum_ k e. y B + [_ z / k ]_ B ) ) ) )
88 notnotb 
 |-  ( 2 || ( # ` y ) <-> -. -. 2 || ( # ` y ) )
89 hashcl 
 |-  ( y e. Fin -> ( # ` y ) e. NN0 )
90 56 89 syl 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( # ` y ) e. NN0 )
91 90 nn0zd 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( # ` y ) e. ZZ )
92 oddp1even 
 |-  ( ( # ` y ) e. ZZ -> ( -. 2 || ( # ` y ) <-> 2 || ( ( # ` y ) + 1 ) ) )
93 91 92 syl 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( -. 2 || ( # ` y ) <-> 2 || ( ( # ` y ) + 1 ) ) )
94 93 notbid 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( -. -. 2 || ( # ` y ) <-> -. 2 || ( ( # ` y ) + 1 ) ) )
95 88 94 bitrid 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( 2 || ( # ` y ) <-> -. 2 || ( ( # ` y ) + 1 ) ) )
96 95 bibi1d 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( ( 2 || ( # ` y ) <-> 2 || sum_ k e. y B ) <-> ( -. 2 || ( ( # ` y ) + 1 ) <-> 2 || sum_ k e. y B ) ) )
97 simprr 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> z e. ( A \ y ) )
98 eldifn 
 |-  ( z e. ( A \ y ) -> -. z e. y )
99 98 adantl 
 |-  ( ( y C_ A /\ z e. ( A \ y ) ) -> -. z e. y )
100 99 adantl 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> -. z e. y )
101 56 100 jca 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( y e. Fin /\ -. z e. y ) )
102 hashunsng 
 |-  ( z e. ( A \ y ) -> ( ( y e. Fin /\ -. z e. y ) -> ( # ` ( y u. { z } ) ) = ( ( # ` y ) + 1 ) ) )
103 97 101 102 sylc 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( # ` ( y u. { z } ) ) = ( ( # ` y ) + 1 ) )
104 103 breq2d 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( 2 || ( # ` ( y u. { z } ) ) <-> 2 || ( ( # ` y ) + 1 ) ) )
105 vex 
 |-  z e. _V
106 105 a1i 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> z e. _V )
107 df-nel 
 |-  ( z e/ y <-> -. z e. y )
108 100 107 sylibr 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> z e/ y )
109 simpll 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ k e. ( y u. { z } ) ) -> ph )
110 elun 
 |-  ( k e. ( y u. { z } ) <-> ( k e. y \/ k e. { z } ) )
111 59 com12 
 |-  ( k e. y -> ( ( y C_ A /\ z e. ( A \ y ) ) -> k e. A ) )
112 elsni 
 |-  ( k e. { z } -> k = z )
113 eleq1w 
 |-  ( k = z -> ( k e. A <-> z e. A ) )
114 30 113 imbitrrid 
 |-  ( k = z -> ( ( y C_ A /\ z e. ( A \ y ) ) -> k e. A ) )
115 112 114 syl 
 |-  ( k e. { z } -> ( ( y C_ A /\ z e. ( A \ y ) ) -> k e. A ) )
116 111 115 jaoi 
 |-  ( ( k e. y \/ k e. { z } ) -> ( ( y C_ A /\ z e. ( A \ y ) ) -> k e. A ) )
117 110 116 sylbi 
 |-  ( k e. ( y u. { z } ) -> ( ( y C_ A /\ z e. ( A \ y ) ) -> k e. A ) )
118 117 com12 
 |-  ( ( y C_ A /\ z e. ( A \ y ) ) -> ( k e. ( y u. { z } ) -> k e. A ) )
119 118 adantl 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( k e. ( y u. { z } ) -> k e. A ) )
120 119 imp 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ k e. ( y u. { z } ) ) -> k e. A )
121 109 120 2 syl2anc 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ k e. ( y u. { z } ) ) -> B e. ZZ )
122 121 ralrimiva 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> A. k e. ( y u. { z } ) B e. ZZ )
123 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 ) )
124 56 106 108 122 123 syl121anc 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> sum_ k e. ( y u. { z } ) B = ( sum_ k e. y B + [_ z / k ]_ B ) )
125 124 breq2d 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( 2 || sum_ k e. ( y u. { z } ) B <-> 2 || ( sum_ k e. y B + [_ z / k ]_ B ) ) )
126 104 125 bibi12d 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( ( 2 || ( # ` ( y u. { z } ) ) <-> 2 || sum_ k e. ( y u. { z } ) B ) <-> ( 2 || ( ( # ` y ) + 1 ) <-> 2 || ( sum_ k e. y B + [_ z / k ]_ B ) ) ) )
127 notbi 
 |-  ( ( 2 || ( ( # ` y ) + 1 ) <-> 2 || ( sum_ k e. y B + [_ z / k ]_ B ) ) <-> ( -. 2 || ( ( # ` y ) + 1 ) <-> -. 2 || ( sum_ k e. y B + [_ z / k ]_ B ) ) )
128 126 127 bitrdi 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( ( 2 || ( # ` ( y u. { z } ) ) <-> 2 || sum_ k e. ( y u. { z } ) B ) <-> ( -. 2 || ( ( # ` y ) + 1 ) <-> -. 2 || ( sum_ k e. y B + [_ z / k ]_ B ) ) ) )
129 87 96 128 3imtr4d 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( ( 2 || ( # ` y ) <-> 2 || sum_ k e. y B ) -> ( 2 || ( # ` ( y u. { z } ) ) <-> 2 || sum_ k e. ( y u. { z } ) B ) ) )
130 12 17 22 27 28 129 1 findcard2d 
 |-  ( ph -> ( 2 || ( # ` A ) <-> 2 || sum_ k e. A B ) )