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 φ A Fin
sumeven.b φ k A B
sumodd.o φ k A ¬ 2 B
Assertion sumodd φ 2 A 2 k A B

Proof

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