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∈AB

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∈xB=∑k∈∅B
9 sum0 ⊢∑k∈∅B=0
10 8 9 eqtrdi ⊢x=∅→∑k∈xB=0
11 10 breq2d ⊢x=∅→2∥∑k∈xB↔2∥0
12 7 11 bibi12d ⊢x=∅→2∥x↔2∥∑k∈xB↔2∥0↔2∥0
13 fveq2 ⊢x=y→x=y
14 13 breq2d ⊢x=y→2∥x↔2∥y
15 sumeq1 ⊢x=y→∑k∈xB=∑k∈yB
16 15 breq2d ⊢x=y→2∥∑k∈xB↔2∥∑k∈yB
17 14 16 bibi12d ⊢x=y→2∥x↔2∥∑k∈xB↔2∥y↔2∥∑k∈yB
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∈xB=∑k∈y∪zB
21 20 breq2d ⊢x=y∪z→2∥∑k∈xB↔2∥∑k∈y∪zB
22 19 21 bibi12d ⊢x=y∪z→2∥x↔2∥∑k∈xB↔2∥y∪z↔2∥∑k∈y∪zB
23 fveq2 ⊢x=A→x=A
24 23 breq2d ⊢x=A→2∥x↔2∥A
25 sumeq1 ⊢x=A→∑k∈xB=∑k∈AB
26 25 breq2d ⊢x=A→2∥∑k∈xB↔2∥∑k∈AB
27 24 26 bibi12d ⊢x=A→2∥x↔2∥∑k∈xB↔2∥A↔2∥∑k∈AB
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∈AB∈ℤ
34 rspcsbela ⊢z∈A∧∀k∈AB∈ℤ→⦋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 ⊢Ⅎ_k2
38 nfcv ⊢Ⅎ_k∥
39 nfcsb1v ⊢Ⅎ_k⦋z/k⦌B
40 37 38 39 nfbr ⊢Ⅎk2∥⦋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∈yB→⦋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∈yB∈ℤ
64 63 anim1i ⊢φ∧y⊆A∧z∈A∖y∧2∥∑k∈yB→∑k∈yB∈ℤ∧2∥∑k∈yB
65 opeo ⊢⦋z/k⦌B∈ℤ∧¬2∥⦋z/k⦌B∧∑k∈yB∈ℤ∧2∥∑k∈yB→¬2∥⦋z/k⦌B+∑k∈yB
66 51 64 65 syl2anc ⊢φ∧y⊆A∧z∈A∖y∧2∥∑k∈yB→¬2∥⦋z/k⦌B+∑k∈yB
67 63 zcnd ⊢φ∧y⊆A∧z∈A∖y→∑k∈yB∈ℂ
68 35 zcnd ⊢φ∧y⊆A∧z∈A∖y→⦋z/k⦌B∈ℂ
69 addcom ⊢∑k∈yB∈ℂ∧⦋z/k⦌B∈ℂ→∑k∈yB+⦋z/k⦌B=⦋z/k⦌B+∑k∈yB
70 69 breq2d ⊢∑k∈yB∈ℂ∧⦋z/k⦌B∈ℂ→2∥∑k∈yB+⦋z/k⦌B↔2∥⦋z/k⦌B+∑k∈yB
71 70 notbid ⊢∑k∈yB∈ℂ∧⦋z/k⦌B∈ℂ→¬2∥∑k∈yB+⦋z/k⦌B↔¬2∥⦋z/k⦌B+∑k∈yB
72 67 68 71 syl2anc ⊢φ∧y⊆A∧z∈A∖y→¬2∥∑k∈yB+⦋z/k⦌B↔¬2∥⦋z/k⦌B+∑k∈yB
73 72 adantr ⊢φ∧y⊆A∧z∈A∖y∧2∥∑k∈yB→¬2∥∑k∈yB+⦋z/k⦌B↔¬2∥⦋z/k⦌B+∑k∈yB
74 66 73 mpbird ⊢φ∧y⊆A∧z∈A∖y∧2∥∑k∈yB→¬2∥∑k∈yB+⦋z/k⦌B
75 74 ex ⊢φ∧y⊆A∧z∈A∖y→2∥∑k∈yB→¬2∥∑k∈yB+⦋z/k⦌B
76 63 anim1i ⊢φ∧y⊆A∧z∈A∖y∧¬2∥∑k∈yB→∑k∈yB∈ℤ∧¬2∥∑k∈yB
77 50 adantr ⊢φ∧y⊆A∧z∈A∖y∧¬2∥∑k∈yB→⦋z/k⦌B∈ℤ∧¬2∥⦋z/k⦌B
78 opoe ⊢∑k∈yB∈ℤ∧¬2∥∑k∈yB∧⦋z/k⦌B∈ℤ∧¬2∥⦋z/k⦌B→2∥∑k∈yB+⦋z/k⦌B
79 76 77 78 syl2anc ⊢φ∧y⊆A∧z∈A∖y∧¬2∥∑k∈yB→2∥∑k∈yB+⦋z/k⦌B
80 79 ex ⊢φ∧y⊆A∧z∈A∖y→¬2∥∑k∈yB→2∥∑k∈yB+⦋z/k⦌B
81 80 con1d ⊢φ∧y⊆A∧z∈A∖y→¬2∥∑k∈yB+⦋z/k⦌B→2∥∑k∈yB
82 75 81 impbid ⊢φ∧y⊆A∧z∈A∖y→2∥∑k∈yB↔¬2∥∑k∈yB+⦋z/k⦌B
83 bitr3 ⊢2∥∑k∈yB↔¬2∥∑k∈yB+⦋z/k⦌B→2∥∑k∈yB↔¬2∥y+1→¬2∥∑k∈yB+⦋z/k⦌B↔¬2∥y+1
84 82 83 syl ⊢φ∧y⊆A∧z∈A∖y→2∥∑k∈yB↔¬2∥y+1→¬2∥∑k∈yB+⦋z/k⦌B↔¬2∥y+1
85 bicom ⊢¬2∥y+1↔2∥∑k∈yB↔2∥∑k∈yB↔¬2∥y+1
86 bicom ⊢¬2∥y+1↔¬2∥∑k∈yB+⦋z/k⦌B↔¬2∥∑k∈yB+⦋z/k⦌B↔¬2∥y+1
87 84 85 86 3imtr4g ⊢φ∧y⊆A∧z∈A∖y→¬2∥y+1↔2∥∑k∈yB→¬2∥y+1↔¬2∥∑k∈yB+⦋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 bitrid ⊢φ∧y⊆A∧z∈A∖y→2∥y↔¬2∥y+1
96 95 bibi1d ⊢φ∧y⊆A∧z∈A∖y→2∥y↔2∥∑k∈yB↔¬2∥y+1↔2∥∑k∈yB
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 imbitrrid ⊢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∪zB∈ℤ
123 fsumsplitsnun ⊢y∈Fin∧z∈V∧z∉y∧∀k∈y∪zB∈ℤ→∑k∈y∪zB=∑k∈yB+⦋z/k⦌B
124 56 106 108 122 123 syl121anc ⊢φ∧y⊆A∧z∈A∖y→∑k∈y∪zB=∑k∈yB+⦋z/k⦌B
125 124 breq2d ⊢φ∧y⊆A∧z∈A∖y→2∥∑k∈y∪zB↔2∥∑k∈yB+⦋z/k⦌B
126 104 125 bibi12d ⊢φ∧y⊆A∧z∈A∖y→2∥y∪z↔2∥∑k∈y∪zB↔2∥y+1↔2∥∑k∈yB+⦋z/k⦌B
127 notbi ⊢2∥y+1↔2∥∑k∈yB+⦋z/k⦌B↔¬2∥y+1↔¬2∥∑k∈yB+⦋z/k⦌B
128 126 127 bitrdi ⊢φ∧y⊆A∧z∈A∖y→2∥y∪z↔2∥∑k∈y∪zB↔¬2∥y+1↔¬2∥∑k∈yB+⦋z/k⦌B
129 87 96 128 3imtr4d ⊢φ∧y⊆A∧z∈A∖y→2∥y↔2∥∑k∈yB→2∥y∪z↔2∥∑k∈y∪zB
130 12 17 22 27 28 129 1 findcard2d ⊢φ→2∥A↔2∥∑k∈AB