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 36 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 35 48 jca 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( [_ z / k ]_ B e. ZZ /\ -. 2 || [_ z / k ]_ B ) )
50 49 adantr 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ 2 || sum_ k e. y B ) -> ( [_ z / k ]_ B e. ZZ /\ -. 2 || [_ z / k ]_ B ) )
51 ssfi 
 |-  ( ( A e. Fin /\ y C_ A ) -> y e. Fin )
52 51 expcom 
 |-  ( y C_ A -> ( A e. Fin -> y e. Fin ) )
53 52 adantr 
 |-  ( ( y C_ A /\ z e. ( A \ y ) ) -> ( A e. Fin -> y e. Fin ) )
54 1 53 mpan9 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> y e. Fin )
55 simpll 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ k e. y ) -> ph )
56 ssel 
 |-  ( y C_ A -> ( k e. y -> k e. A ) )
57 56 adantr 
 |-  ( ( y C_ A /\ z e. ( A \ y ) ) -> ( k e. y -> k e. A ) )
58 57 adantl 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( k e. y -> k e. A ) )
59 58 imp 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ k e. y ) -> k e. A )
60 55 59 2 syl2anc 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ k e. y ) -> B e. ZZ )
61 54 60 fsumzcl 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> sum_ k e. y B e. ZZ )
62 61 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 ) )
63 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 ) )
64 50 62 63 syl2anc 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ 2 || sum_ k e. y B ) -> -. 2 || ( [_ z / k ]_ B + sum_ k e. y B ) )
65 61 zcnd 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> sum_ k e. y B e. CC )
66 35 zcnd 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> [_ z / k ]_ B e. CC )
67 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 ) )
68 67 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 ) ) )
69 68 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 ) ) )
70 65 66 69 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 ) ) )
71 70 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 ) ) )
72 64 71 mpbird 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ 2 || sum_ k e. y B ) -> -. 2 || ( sum_ k e. y B + [_ z / k ]_ B ) )
73 72 ex 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( 2 || sum_ k e. y B -> -. 2 || ( sum_ k e. y B + [_ z / k ]_ B ) ) )
74 61 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 ) )
75 49 adantr 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ -. 2 || sum_ k e. y B ) -> ( [_ z / k ]_ B e. ZZ /\ -. 2 || [_ z / k ]_ B ) )
76 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 ) )
77 74 75 76 syl2anc 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ -. 2 || sum_ k e. y B ) -> 2 || ( sum_ k e. y B + [_ z / k ]_ B ) )
78 77 ex 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( -. 2 || sum_ k e. y B -> 2 || ( sum_ k e. y B + [_ z / k ]_ B ) ) )
79 78 con1d 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( -. 2 || ( sum_ k e. y B + [_ z / k ]_ B ) -> 2 || sum_ k e. y B ) )
80 73 79 impbid 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( 2 || sum_ k e. y B <-> -. 2 || ( sum_ k e. y B + [_ z / k ]_ B ) ) )
81 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 ) ) ) )
82 80 81 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 ) ) ) )
83 bicom 
 |-  ( ( -. 2 || ( ( # ` y ) + 1 ) <-> 2 || sum_ k e. y B ) <-> ( 2 || sum_ k e. y B <-> -. 2 || ( ( # ` y ) + 1 ) ) )
84 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 ) ) )
85 82 83 84 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 ) ) ) )
86 notnotb 
 |-  ( 2 || ( # ` y ) <-> -. -. 2 || ( # ` y ) )
87 hashcl 
 |-  ( y e. Fin -> ( # ` y ) e. NN0 )
88 54 87 syl 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( # ` y ) e. NN0 )
89 88 nn0zd 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( # ` y ) e. ZZ )
90 oddp1even 
 |-  ( ( # ` y ) e. ZZ -> ( -. 2 || ( # ` y ) <-> 2 || ( ( # ` y ) + 1 ) ) )
91 89 90 syl 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( -. 2 || ( # ` y ) <-> 2 || ( ( # ` y ) + 1 ) ) )
92 91 notbid 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( -. -. 2 || ( # ` y ) <-> -. 2 || ( ( # ` y ) + 1 ) ) )
93 86 92 bitrid 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( 2 || ( # ` y ) <-> -. 2 || ( ( # ` y ) + 1 ) ) )
94 93 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 ) ) )
95 simprr 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> z e. ( A \ y ) )
96 eldifn 
 |-  ( z e. ( A \ y ) -> -. z e. y )
97 96 adantl 
 |-  ( ( y C_ A /\ z e. ( A \ y ) ) -> -. z e. y )
98 97 adantl 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> -. z e. y )
99 54 98 jca 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( y e. Fin /\ -. z e. y ) )
100 hashunsng 
 |-  ( z e. ( A \ y ) -> ( ( y e. Fin /\ -. z e. y ) -> ( # ` ( y u. { z } ) ) = ( ( # ` y ) + 1 ) ) )
101 95 99 100 sylc 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( # ` ( y u. { z } ) ) = ( ( # ` y ) + 1 ) )
102 101 breq2d 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( 2 || ( # ` ( y u. { z } ) ) <-> 2 || ( ( # ` y ) + 1 ) ) )
103 vex 
 |-  z e. _V
104 103 a1i 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> z e. _V )
105 df-nel 
 |-  ( z e/ y <-> -. z e. y )
106 98 105 sylibr 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> z e/ y )
107 simpll 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ k e. ( y u. { z } ) ) -> ph )
108 elun 
 |-  ( k e. ( y u. { z } ) <-> ( k e. y \/ k e. { z } ) )
109 57 com12 
 |-  ( k e. y -> ( ( y C_ A /\ z e. ( A \ y ) ) -> k e. A ) )
110 elsni 
 |-  ( k e. { z } -> k = z )
111 eleq1w 
 |-  ( k = z -> ( k e. A <-> z e. A ) )
112 30 111 imbitrrid 
 |-  ( k = z -> ( ( y C_ A /\ z e. ( A \ y ) ) -> k e. A ) )
113 110 112 syl 
 |-  ( k e. { z } -> ( ( y C_ A /\ z e. ( A \ y ) ) -> k e. A ) )
114 109 113 jaoi 
 |-  ( ( k e. y \/ k e. { z } ) -> ( ( y C_ A /\ z e. ( A \ y ) ) -> k e. A ) )
115 108 114 sylbi 
 |-  ( k e. ( y u. { z } ) -> ( ( y C_ A /\ z e. ( A \ y ) ) -> k e. A ) )
116 115 com12 
 |-  ( ( y C_ A /\ z e. ( A \ y ) ) -> ( k e. ( y u. { z } ) -> k e. A ) )
117 116 adantl 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( k e. ( y u. { z } ) -> k e. A ) )
118 117 imp 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ k e. ( y u. { z } ) ) -> k e. A )
119 107 118 2 syl2anc 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ k e. ( y u. { z } ) ) -> B e. ZZ )
120 119 ralrimiva 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> A. k e. ( y u. { z } ) B e. ZZ )
121 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 ) )
122 54 104 106 120 121 syl121anc 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> sum_ k e. ( y u. { z } ) B = ( sum_ k e. y B + [_ z / k ]_ B ) )
123 122 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 ) ) )
124 102 123 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 ) ) ) )
125 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 ) ) )
126 124 125 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 ) ) ) )
127 85 94 126 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 ) ) )
128 12 17 22 27 28 127 1 findcard2d 
 |-  ( ph -> ( 2 || ( # ` A ) <-> 2 || sum_ k e. A B ) )