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 ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
sumeven.b ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℤ$
sumodd.o ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to ¬2\parallel {B}$
Assertion sumodd ${⊢}{\phi }\to \left(2\parallel \left|{A}\right|↔2\parallel \sum _{{k}\in {A}}{B}\right)$

Proof

Step Hyp Ref Expression
1 sumeven.a ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
2 sumeven.b ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℤ$
3 sumodd.o ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to ¬2\parallel {B}$
4 fveq2 ${⊢}{x}=\varnothing \to \left|{x}\right|=\left|\varnothing \right|$
5 hash0 ${⊢}\left|\varnothing \right|=0$
6 4 5 syl6eq ${⊢}{x}=\varnothing \to \left|{x}\right|=0$
7 6 breq2d ${⊢}{x}=\varnothing \to \left(2\parallel \left|{x}\right|↔2\parallel 0\right)$
8 sumeq1 ${⊢}{x}=\varnothing \to \sum _{{k}\in {x}}{B}=\sum _{{k}\in \varnothing }{B}$
9 sum0 ${⊢}\sum _{{k}\in \varnothing }{B}=0$
10 8 9 syl6eq ${⊢}{x}=\varnothing \to \sum _{{k}\in {x}}{B}=0$
11 10 breq2d ${⊢}{x}=\varnothing \to \left(2\parallel \sum _{{k}\in {x}}{B}↔2\parallel 0\right)$
12 7 11 bibi12d ${⊢}{x}=\varnothing \to \left(\left(2\parallel \left|{x}\right|↔2\parallel \sum _{{k}\in {x}}{B}\right)↔\left(2\parallel 0↔2\parallel 0\right)\right)$
13 fveq2 ${⊢}{x}={y}\to \left|{x}\right|=\left|{y}\right|$
14 13 breq2d ${⊢}{x}={y}\to \left(2\parallel \left|{x}\right|↔2\parallel \left|{y}\right|\right)$
15 sumeq1 ${⊢}{x}={y}\to \sum _{{k}\in {x}}{B}=\sum _{{k}\in {y}}{B}$
16 15 breq2d ${⊢}{x}={y}\to \left(2\parallel \sum _{{k}\in {x}}{B}↔2\parallel \sum _{{k}\in {y}}{B}\right)$
17 14 16 bibi12d ${⊢}{x}={y}\to \left(\left(2\parallel \left|{x}\right|↔2\parallel \sum _{{k}\in {x}}{B}\right)↔\left(2\parallel \left|{y}\right|↔2\parallel \sum _{{k}\in {y}}{B}\right)\right)$
18 fveq2 ${⊢}{x}={y}\cup \left\{{z}\right\}\to \left|{x}\right|=\left|{y}\cup \left\{{z}\right\}\right|$
19 18 breq2d ${⊢}{x}={y}\cup \left\{{z}\right\}\to \left(2\parallel \left|{x}\right|↔2\parallel \left|{y}\cup \left\{{z}\right\}\right|\right)$
20 sumeq1 ${⊢}{x}={y}\cup \left\{{z}\right\}\to \sum _{{k}\in {x}}{B}=\sum _{{k}\in {y}\cup \left\{{z}\right\}}{B}$
21 20 breq2d ${⊢}{x}={y}\cup \left\{{z}\right\}\to \left(2\parallel \sum _{{k}\in {x}}{B}↔2\parallel \sum _{{k}\in {y}\cup \left\{{z}\right\}}{B}\right)$
22 19 21 bibi12d ${⊢}{x}={y}\cup \left\{{z}\right\}\to \left(\left(2\parallel \left|{x}\right|↔2\parallel \sum _{{k}\in {x}}{B}\right)↔\left(2\parallel \left|{y}\cup \left\{{z}\right\}\right|↔2\parallel \sum _{{k}\in {y}\cup \left\{{z}\right\}}{B}\right)\right)$
23 fveq2 ${⊢}{x}={A}\to \left|{x}\right|=\left|{A}\right|$
24 23 breq2d ${⊢}{x}={A}\to \left(2\parallel \left|{x}\right|↔2\parallel \left|{A}\right|\right)$
25 sumeq1 ${⊢}{x}={A}\to \sum _{{k}\in {x}}{B}=\sum _{{k}\in {A}}{B}$
26 25 breq2d ${⊢}{x}={A}\to \left(2\parallel \sum _{{k}\in {x}}{B}↔2\parallel \sum _{{k}\in {A}}{B}\right)$
27 24 26 bibi12d ${⊢}{x}={A}\to \left(\left(2\parallel \left|{x}\right|↔2\parallel \sum _{{k}\in {x}}{B}\right)↔\left(2\parallel \left|{A}\right|↔2\parallel \sum _{{k}\in {A}}{B}\right)\right)$
28 biidd ${⊢}{\phi }\to \left(2\parallel 0↔2\parallel 0\right)$
29 eldifi ${⊢}{z}\in \left({A}\setminus {y}\right)\to {z}\in {A}$
30 29 adantl ${⊢}\left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\to {z}\in {A}$
31 30 adantl ${⊢}\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\to {z}\in {A}$
32 2 adantlr ${⊢}\left(\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\wedge {k}\in {A}\right)\to {B}\in ℤ$
33 32 ralrimiva ${⊢}\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\to \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in ℤ$
34 rspcsbela
35 31 33 34 syl2anc
36 3 ralrimiva ${⊢}{\phi }\to \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}¬2\parallel {B}$
37 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}2$
38 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\parallel$
39 nfcsb1v
40 37 38 39 nfbr
41 40 nfn
42 csbeq1a
43 42 breq2d
44 43 notbid
45 41 44 rspc
46 29 45 syl
47 36 46 syl5com
48 47 a1d
49 48 imp32
50 35 49 jca
52 ssfi ${⊢}\left({A}\in \mathrm{Fin}\wedge {y}\subseteq {A}\right)\to {y}\in \mathrm{Fin}$
53 52 expcom ${⊢}{y}\subseteq {A}\to \left({A}\in \mathrm{Fin}\to {y}\in \mathrm{Fin}\right)$
54 53 adantr ${⊢}\left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\to \left({A}\in \mathrm{Fin}\to {y}\in \mathrm{Fin}\right)$
55 1 54 syl5com ${⊢}{\phi }\to \left(\left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\to {y}\in \mathrm{Fin}\right)$
56 55 imp ${⊢}\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\to {y}\in \mathrm{Fin}$
57 simpll ${⊢}\left(\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\wedge {k}\in {y}\right)\to {\phi }$
58 ssel ${⊢}{y}\subseteq {A}\to \left({k}\in {y}\to {k}\in {A}\right)$
59 58 adantr ${⊢}\left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\to \left({k}\in {y}\to {k}\in {A}\right)$
60 59 adantl ${⊢}\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\to \left({k}\in {y}\to {k}\in {A}\right)$
61 60 imp ${⊢}\left(\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\wedge {k}\in {y}\right)\to {k}\in {A}$
62 57 61 2 syl2anc ${⊢}\left(\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\wedge {k}\in {y}\right)\to {B}\in ℤ$
63 56 62 fsumzcl ${⊢}\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\to \sum _{{k}\in {y}}{B}\in ℤ$
64 63 anim1i ${⊢}\left(\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\wedge 2\parallel \sum _{{k}\in {y}}{B}\right)\to \left(\sum _{{k}\in {y}}{B}\in ℤ\wedge 2\parallel \sum _{{k}\in {y}}{B}\right)$
65 opeo
66 51 64 65 syl2anc
67 63 zcnd ${⊢}\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\to \sum _{{k}\in {y}}{B}\in ℂ$
68 35 zcnd
70 69 breq2d
71 70 notbid
72 67 68 71 syl2anc
74 66 73 mpbird
75 74 ex
76 63 anim1i ${⊢}\left(\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\wedge ¬2\parallel \sum _{{k}\in {y}}{B}\right)\to \left(\sum _{{k}\in {y}}{B}\in ℤ\wedge ¬2\parallel \sum _{{k}\in {y}}{B}\right)$
78 opoe
79 76 77 78 syl2anc
80 79 ex
81 80 con1d
82 75 81 impbid
83 bitr3
84 82 83 syl
85 bicom ${⊢}\left(¬2\parallel \left(\left|{y}\right|+1\right)↔2\parallel \sum _{{k}\in {y}}{B}\right)↔\left(2\parallel \sum _{{k}\in {y}}{B}↔¬2\parallel \left(\left|{y}\right|+1\right)\right)$
86 bicom
87 84 85 86 3imtr4g
88 notnotb ${⊢}2\parallel \left|{y}\right|↔¬¬2\parallel \left|{y}\right|$
89 hashcl ${⊢}{y}\in \mathrm{Fin}\to \left|{y}\right|\in {ℕ}_{0}$
90 56 89 syl ${⊢}\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\to \left|{y}\right|\in {ℕ}_{0}$
91 90 nn0zd ${⊢}\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\to \left|{y}\right|\in ℤ$
92 oddp1even ${⊢}\left|{y}\right|\in ℤ\to \left(¬2\parallel \left|{y}\right|↔2\parallel \left(\left|{y}\right|+1\right)\right)$
93 91 92 syl ${⊢}\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\to \left(¬2\parallel \left|{y}\right|↔2\parallel \left(\left|{y}\right|+1\right)\right)$
94 93 notbid ${⊢}\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\to \left(¬¬2\parallel \left|{y}\right|↔¬2\parallel \left(\left|{y}\right|+1\right)\right)$
95 88 94 syl5bb ${⊢}\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\to \left(2\parallel \left|{y}\right|↔¬2\parallel \left(\left|{y}\right|+1\right)\right)$
96 95 bibi1d ${⊢}\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\to \left(\left(2\parallel \left|{y}\right|↔2\parallel \sum _{{k}\in {y}}{B}\right)↔\left(¬2\parallel \left(\left|{y}\right|+1\right)↔2\parallel \sum _{{k}\in {y}}{B}\right)\right)$
97 simprr ${⊢}\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\to {z}\in \left({A}\setminus {y}\right)$
98 eldifn ${⊢}{z}\in \left({A}\setminus {y}\right)\to ¬{z}\in {y}$
99 98 adantl ${⊢}\left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\to ¬{z}\in {y}$
100 99 adantl ${⊢}\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\to ¬{z}\in {y}$
101 56 100 jca ${⊢}\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\to \left({y}\in \mathrm{Fin}\wedge ¬{z}\in {y}\right)$
102 hashunsng ${⊢}{z}\in \left({A}\setminus {y}\right)\to \left(\left({y}\in \mathrm{Fin}\wedge ¬{z}\in {y}\right)\to \left|{y}\cup \left\{{z}\right\}\right|=\left|{y}\right|+1\right)$
103 97 101 102 sylc ${⊢}\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\to \left|{y}\cup \left\{{z}\right\}\right|=\left|{y}\right|+1$
104 103 breq2d ${⊢}\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\to \left(2\parallel \left|{y}\cup \left\{{z}\right\}\right|↔2\parallel \left(\left|{y}\right|+1\right)\right)$
105 vex ${⊢}{z}\in \mathrm{V}$
106 105 a1i ${⊢}\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\to {z}\in \mathrm{V}$
107 df-nel ${⊢}{z}\notin {y}↔¬{z}\in {y}$
108 100 107 sylibr ${⊢}\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\to {z}\notin {y}$
109 simpll ${⊢}\left(\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\wedge {k}\in \left({y}\cup \left\{{z}\right\}\right)\right)\to {\phi }$
110 elun ${⊢}{k}\in \left({y}\cup \left\{{z}\right\}\right)↔\left({k}\in {y}\vee {k}\in \left\{{z}\right\}\right)$
111 59 com12 ${⊢}{k}\in {y}\to \left(\left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\to {k}\in {A}\right)$
112 elsni ${⊢}{k}\in \left\{{z}\right\}\to {k}={z}$
113 eleq1w ${⊢}{k}={z}\to \left({k}\in {A}↔{z}\in {A}\right)$
114 30 113 syl5ibr ${⊢}{k}={z}\to \left(\left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\to {k}\in {A}\right)$
115 112 114 syl ${⊢}{k}\in \left\{{z}\right\}\to \left(\left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\to {k}\in {A}\right)$
116 111 115 jaoi ${⊢}\left({k}\in {y}\vee {k}\in \left\{{z}\right\}\right)\to \left(\left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\to {k}\in {A}\right)$
117 110 116 sylbi ${⊢}{k}\in \left({y}\cup \left\{{z}\right\}\right)\to \left(\left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\to {k}\in {A}\right)$
118 117 com12 ${⊢}\left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\to \left({k}\in \left({y}\cup \left\{{z}\right\}\right)\to {k}\in {A}\right)$
119 118 adantl ${⊢}\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\to \left({k}\in \left({y}\cup \left\{{z}\right\}\right)\to {k}\in {A}\right)$
120 119 imp ${⊢}\left(\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\wedge {k}\in \left({y}\cup \left\{{z}\right\}\right)\right)\to {k}\in {A}$
121 109 120 2 syl2anc ${⊢}\left(\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\wedge {k}\in \left({y}\cup \left\{{z}\right\}\right)\right)\to {B}\in ℤ$
122 121 ralrimiva ${⊢}\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\to \forall {k}\in \left({y}\cup \left\{{z}\right\}\right)\phantom{\rule{.4em}{0ex}}{B}\in ℤ$
123 fsumsplitsnun
124 56 106 108 122 123 syl121anc
125 124 breq2d
126 104 125 bibi12d
127 notbi
128 126 127 syl6bb
129 87 96 128 3imtr4d ${⊢}\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\to \left(\left(2\parallel \left|{y}\right|↔2\parallel \sum _{{k}\in {y}}{B}\right)\to \left(2\parallel \left|{y}\cup \left\{{z}\right\}\right|↔2\parallel \sum _{{k}\in {y}\cup \left\{{z}\right\}}{B}\right)\right)$
130 12 17 22 27 28 129 1 findcard2d ${⊢}{\phi }\to \left(2\parallel \left|{A}\right|↔2\parallel \sum _{{k}\in {A}}{B}\right)$