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 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
sumeven.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℤ )
sumodd.o ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ¬ 2 ∥ 𝐵 )
Assertion sumodd ( 𝜑 → ( 2 ∥ ( ♯ ‘ 𝐴 ) ↔ 2 ∥ Σ 𝑘 ∈ 𝐴 𝐵 ) )

Proof

Step Hyp Ref Expression
1 sumeven.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
2 sumeven.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℤ )
3 sumodd.o ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ¬ 2 ∥ 𝐵 )
4 fveq2 ⊢ ( 𝑥 = ∅ → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ ∅ ) )
5 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
6 4 5 eqtrdi ⊢ ( 𝑥 = ∅ → ( ♯ ‘ 𝑥 ) = 0 )
7 6 breq2d ⊢ ( 𝑥 = ∅ → ( 2 ∥ ( ♯ ‘ 𝑥 ) ↔ 2 ∥ 0 ) )
8 sumeq1 ⊢ ( 𝑥 = ∅ → Σ 𝑘 ∈ 𝑥 𝐵 = Σ 𝑘 ∈ ∅ 𝐵 )
9 sum0 ⊢ Σ 𝑘 ∈ ∅ 𝐵 = 0
10 8 9 eqtrdi ⊢ ( 𝑥 = ∅ → Σ 𝑘 ∈ 𝑥 𝐵 = 0 )
11 10 breq2d ⊢ ( 𝑥 = ∅ → ( 2 ∥ Σ 𝑘 ∈ 𝑥 𝐵 ↔ 2 ∥ 0 ) )
12 7 11 bibi12d ⊢ ( 𝑥 = ∅ → ( ( 2 ∥ ( ♯ ‘ 𝑥 ) ↔ 2 ∥ Σ 𝑘 ∈ 𝑥 𝐵 ) ↔ ( 2 ∥ 0 ↔ 2 ∥ 0 ) ) )
13 fveq2 ⊢ ( 𝑥 = 𝑦 → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) )
14 13 breq2d ⊢ ( 𝑥 = 𝑦 → ( 2 ∥ ( ♯ ‘ 𝑥 ) ↔ 2 ∥ ( ♯ ‘ 𝑦 ) ) )
15 sumeq1 ⊢ ( 𝑥 = 𝑦 → Σ 𝑘 ∈ 𝑥 𝐵 = Σ 𝑘 ∈ 𝑦 𝐵 )
16 15 breq2d ⊢ ( 𝑥 = 𝑦 → ( 2 ∥ Σ 𝑘 ∈ 𝑥 𝐵 ↔ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) )
17 14 16 bibi12d ⊢ ( 𝑥 = 𝑦 → ( ( 2 ∥ ( ♯ ‘ 𝑥 ) ↔ 2 ∥ Σ 𝑘 ∈ 𝑥 𝐵 ) ↔ ( 2 ∥ ( ♯ ‘ 𝑦 ) ↔ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) ) )
18 fveq2 ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) )
19 18 breq2d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 2 ∥ ( ♯ ‘ 𝑥 ) ↔ 2 ∥ ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) )
20 sumeq1 ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → Σ 𝑘 ∈ 𝑥 𝐵 = Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 )
21 20 breq2d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 2 ∥ Σ 𝑘 ∈ 𝑥 𝐵 ↔ 2 ∥ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) )
22 19 21 bibi12d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( 2 ∥ ( ♯ ‘ 𝑥 ) ↔ 2 ∥ Σ 𝑘 ∈ 𝑥 𝐵 ) ↔ ( 2 ∥ ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ↔ 2 ∥ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) )
23 fveq2 ⊢ ( 𝑥 = 𝐴 → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) )
24 23 breq2d ⊢ ( 𝑥 = 𝐴 → ( 2 ∥ ( ♯ ‘ 𝑥 ) ↔ 2 ∥ ( ♯ ‘ 𝐴 ) ) )
25 sumeq1 ⊢ ( 𝑥 = 𝐴 → Σ 𝑘 ∈ 𝑥 𝐵 = Σ 𝑘 ∈ 𝐴 𝐵 )
26 25 breq2d ⊢ ( 𝑥 = 𝐴 → ( 2 ∥ Σ 𝑘 ∈ 𝑥 𝐵 ↔ 2 ∥ Σ 𝑘 ∈ 𝐴 𝐵 ) )
27 24 26 bibi12d ⊢ ( 𝑥 = 𝐴 → ( ( 2 ∥ ( ♯ ‘ 𝑥 ) ↔ 2 ∥ Σ 𝑘 ∈ 𝑥 𝐵 ) ↔ ( 2 ∥ ( ♯ ‘ 𝐴 ) ↔ 2 ∥ Σ 𝑘 ∈ 𝐴 𝐵 ) ) )
28 biidd ⊢ ( 𝜑 → ( 2 ∥ 0 ↔ 2 ∥ 0 ) )
29 eldifi ⊢ ( 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) → 𝑧 ∈ 𝐴 )
30 29 adantl ⊢ ( ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) → 𝑧 ∈ 𝐴 )
31 30 adantl ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → 𝑧 ∈ 𝐴 )
32 2 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℤ )
33 32 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ )
34 rspcsbela ⊢ ( ( 𝑧 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) → ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℤ )
35 31 33 34 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℤ )
36 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 ¬ 2 ∥ 𝐵 )
37 nfcv ⊢ Ⅎ 𝑘 2
38 nfcv ⊢ Ⅎ 𝑘 ∥
39 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑧 / 𝑘 ⦌ 𝐵
40 37 38 39 nfbr ⊢ Ⅎ 𝑘 2 ∥ ⦋ 𝑧 / 𝑘 ⦌ 𝐵
41 40 nfn ⊢ Ⅎ 𝑘 ¬ 2 ∥ ⦋ 𝑧 / 𝑘 ⦌ 𝐵
42 csbeq1a ⊢ ( 𝑘 = 𝑧 → 𝐵 = ⦋ 𝑧 / 𝑘 ⦌ 𝐵 )
43 42 breq2d ⊢ ( 𝑘 = 𝑧 → ( 2 ∥ 𝐵 ↔ 2 ∥ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
44 43 notbid ⊢ ( 𝑘 = 𝑧 → ( ¬ 2 ∥ 𝐵 ↔ ¬ 2 ∥ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
45 41 44 rspc ⊢ ( 𝑧 ∈ 𝐴 → ( ∀ 𝑘 ∈ 𝐴 ¬ 2 ∥ 𝐵 → ¬ 2 ∥ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
46 29 36 45 syl2imc ⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) → ¬ 2 ∥ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
47 46 a1d ⊢ ( 𝜑 → ( 𝑦 ⊆ 𝐴 → ( 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) → ¬ 2 ∥ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) )
48 47 imp32 ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ¬ 2 ∥ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 )
49 35 48 jca ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℤ ∧ ¬ 2 ∥ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
50 49 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) → ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℤ ∧ ¬ 2 ∥ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
51 ssfi ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑦 ⊆ 𝐴 ) → 𝑦 ∈ Fin )
52 51 expcom ⊢ ( 𝑦 ⊆ 𝐴 → ( 𝐴 ∈ Fin → 𝑦 ∈ Fin ) )
53 52 adantr ⊢ ( ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) → ( 𝐴 ∈ Fin → 𝑦 ∈ Fin ) )
54 1 53 mpan9 ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → 𝑦 ∈ Fin )
55 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 𝑘 ∈ 𝑦 ) → 𝜑 )
56 ssel ⊢ ( 𝑦 ⊆ 𝐴 → ( 𝑘 ∈ 𝑦 → 𝑘 ∈ 𝐴 ) )
57 56 adantr ⊢ ( ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) → ( 𝑘 ∈ 𝑦 → 𝑘 ∈ 𝐴 ) )
58 57 adantl ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( 𝑘 ∈ 𝑦 → 𝑘 ∈ 𝐴 ) )
59 58 imp ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 𝑘 ∈ 𝑦 ) → 𝑘 ∈ 𝐴 )
60 55 59 2 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 𝑘 ∈ 𝑦 ) → 𝐵 ∈ ℤ )
61 54 60 fsumzcl ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → Σ 𝑘 ∈ 𝑦 𝐵 ∈ ℤ )
62 61 anim1i ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) → ( Σ 𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) )
63 opeo ⊢ ( ( ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℤ ∧ ¬ 2 ∥ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ∧ ( Σ 𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) ) → ¬ 2 ∥ ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 + Σ 𝑘 ∈ 𝑦 𝐵 ) )
64 50 62 63 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) → ¬ 2 ∥ ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 + Σ 𝑘 ∈ 𝑦 𝐵 ) )
65 61 zcnd ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → Σ 𝑘 ∈ 𝑦 𝐵 ∈ ℂ )
66 35 zcnd ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℂ )
67 addcom ⊢ ( ( Σ 𝑘 ∈ 𝑦 𝐵 ∈ ℂ ∧ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℂ ) → ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) = ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 + Σ 𝑘 ∈ 𝑦 𝐵 ) )
68 67 breq2d ⊢ ( ( Σ 𝑘 ∈ 𝑦 𝐵 ∈ ℂ ∧ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℂ ) → ( 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ↔ 2 ∥ ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 + Σ 𝑘 ∈ 𝑦 𝐵 ) ) )
69 68 notbid ⊢ ( ( Σ 𝑘 ∈ 𝑦 𝐵 ∈ ℂ ∧ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℂ ) → ( ¬ 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ↔ ¬ 2 ∥ ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 + Σ 𝑘 ∈ 𝑦 𝐵 ) ) )
70 65 66 69 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( ¬ 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ↔ ¬ 2 ∥ ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 + Σ 𝑘 ∈ 𝑦 𝐵 ) ) )
71 70 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) → ( ¬ 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ↔ ¬ 2 ∥ ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 + Σ 𝑘 ∈ 𝑦 𝐵 ) ) )
72 64 71 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) → ¬ 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
73 72 ex ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 → ¬ 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) )
74 61 anim1i ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ ¬ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) → ( Σ 𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ ¬ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) )
75 49 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ ¬ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) → ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℤ ∧ ¬ 2 ∥ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
76 opoe ⊢ ( ( ( Σ 𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ ¬ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) ∧ ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℤ ∧ ¬ 2 ∥ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) → 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
77 74 75 76 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ ¬ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) → 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
78 77 ex ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( ¬ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 → 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) )
79 78 con1d ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( ¬ 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) → 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) )
80 73 79 impbid ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ↔ ¬ 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) )
81 bitr3 ⊢ ( ( 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ↔ ¬ 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) → ( ( 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ↔ ¬ 2 ∥ ( ( ♯ ‘ 𝑦 ) + 1 ) ) → ( ¬ 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ↔ ¬ 2 ∥ ( ( ♯ ‘ 𝑦 ) + 1 ) ) ) )
82 80 81 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( ( 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ↔ ¬ 2 ∥ ( ( ♯ ‘ 𝑦 ) + 1 ) ) → ( ¬ 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ↔ ¬ 2 ∥ ( ( ♯ ‘ 𝑦 ) + 1 ) ) ) )
83 bicom ⊢ ( ( ¬ 2 ∥ ( ( ♯ ‘ 𝑦 ) + 1 ) ↔ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) ↔ ( 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ↔ ¬ 2 ∥ ( ( ♯ ‘ 𝑦 ) + 1 ) ) )
84 bicom ⊢ ( ( ¬ 2 ∥ ( ( ♯ ‘ 𝑦 ) + 1 ) ↔ ¬ 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) ↔ ( ¬ 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ↔ ¬ 2 ∥ ( ( ♯ ‘ 𝑦 ) + 1 ) ) )
85 82 83 84 3imtr4g ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( ( ¬ 2 ∥ ( ( ♯ ‘ 𝑦 ) + 1 ) ↔ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) → ( ¬ 2 ∥ ( ( ♯ ‘ 𝑦 ) + 1 ) ↔ ¬ 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) ) )
86 notnotb ⊢ ( 2 ∥ ( ♯ ‘ 𝑦 ) ↔ ¬ ¬ 2 ∥ ( ♯ ‘ 𝑦 ) )
87 hashcl ⊢ ( 𝑦 ∈ Fin → ( ♯ ‘ 𝑦 ) ∈ ℕ0 )
88 54 87 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( ♯ ‘ 𝑦 ) ∈ ℕ0 )
89 88 nn0zd ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( ♯ ‘ 𝑦 ) ∈ ℤ )
90 oddp1even ⊢ ( ( ♯ ‘ 𝑦 ) ∈ ℤ → ( ¬ 2 ∥ ( ♯ ‘ 𝑦 ) ↔ 2 ∥ ( ( ♯ ‘ 𝑦 ) + 1 ) ) )
91 89 90 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( ¬ 2 ∥ ( ♯ ‘ 𝑦 ) ↔ 2 ∥ ( ( ♯ ‘ 𝑦 ) + 1 ) ) )
92 91 notbid ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( ¬ ¬ 2 ∥ ( ♯ ‘ 𝑦 ) ↔ ¬ 2 ∥ ( ( ♯ ‘ 𝑦 ) + 1 ) ) )
93 86 92 bitrid ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( 2 ∥ ( ♯ ‘ 𝑦 ) ↔ ¬ 2 ∥ ( ( ♯ ‘ 𝑦 ) + 1 ) ) )
94 93 bibi1d ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( ( 2 ∥ ( ♯ ‘ 𝑦 ) ↔ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) ↔ ( ¬ 2 ∥ ( ( ♯ ‘ 𝑦 ) + 1 ) ↔ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) ) )
95 simprr ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) )
96 eldifn ⊢ ( 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) → ¬ 𝑧 ∈ 𝑦 )
97 96 adantl ⊢ ( ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) → ¬ 𝑧 ∈ 𝑦 )
98 97 adantl ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ¬ 𝑧 ∈ 𝑦 )
99 54 98 jca ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) )
100 hashunsng ⊢ ( 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) → ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( ♯ ‘ 𝑦 ) + 1 ) ) )
101 95 99 100 sylc ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( ♯ ‘ 𝑦 ) + 1 ) )
102 101 breq2d ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( 2 ∥ ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ↔ 2 ∥ ( ( ♯ ‘ 𝑦 ) + 1 ) ) )
103 vex ⊢ 𝑧 ∈ V
104 103 a1i ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → 𝑧 ∈ V )
105 df-nel ⊢ ( 𝑧 ∉ 𝑦 ↔ ¬ 𝑧 ∈ 𝑦 )
106 98 105 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → 𝑧 ∉ 𝑦 )
107 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ) → 𝜑 )
108 elun ⊢ ( 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ↔ ( 𝑘 ∈ 𝑦 ∨ 𝑘 ∈ { 𝑧 } ) )
109 57 com12 ⊢ ( 𝑘 ∈ 𝑦 → ( ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) → 𝑘 ∈ 𝐴 ) )
110 elsni ⊢ ( 𝑘 ∈ { 𝑧 } → 𝑘 = 𝑧 )
111 eleq1w ⊢ ( 𝑘 = 𝑧 → ( 𝑘 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) )
112 30 111 imbitrrid ⊢ ( 𝑘 = 𝑧 → ( ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) → 𝑘 ∈ 𝐴 ) )
113 110 112 syl ⊢ ( 𝑘 ∈ { 𝑧 } → ( ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) → 𝑘 ∈ 𝐴 ) )
114 109 113 jaoi ⊢ ( ( 𝑘 ∈ 𝑦 ∨ 𝑘 ∈ { 𝑧 } ) → ( ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) → 𝑘 ∈ 𝐴 ) )
115 108 114 sylbi ⊢ ( 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) → 𝑘 ∈ 𝐴 ) )
116 115 com12 ⊢ ( ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) → ( 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) → 𝑘 ∈ 𝐴 ) )
117 116 adantl ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) → 𝑘 ∈ 𝐴 ) )
118 117 imp ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ) → 𝑘 ∈ 𝐴 )
119 107 118 2 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ) → 𝐵 ∈ ℤ )
120 119 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ ℤ )
121 fsumsplitsnun ⊢ ( ( 𝑦 ∈ Fin ∧ ( 𝑧 ∈ V ∧ 𝑧 ∉ 𝑦 ) ∧ ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) → Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 = ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
122 54 104 106 120 121 syl121anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 = ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
123 122 breq2d ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( 2 ∥ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ↔ 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) )
124 102 123 bibi12d ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( ( 2 ∥ ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ↔ 2 ∥ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ↔ ( 2 ∥ ( ( ♯ ‘ 𝑦 ) + 1 ) ↔ 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) ) )
125 notbi ⊢ ( ( 2 ∥ ( ( ♯ ‘ 𝑦 ) + 1 ) ↔ 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) ↔ ( ¬ 2 ∥ ( ( ♯ ‘ 𝑦 ) + 1 ) ↔ ¬ 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) )
126 124 125 bitrdi ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( ( 2 ∥ ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ↔ 2 ∥ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ↔ ( ¬ 2 ∥ ( ( ♯ ‘ 𝑦 ) + 1 ) ↔ ¬ 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) ) )
127 85 94 126 3imtr4d ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( ( 2 ∥ ( ♯ ‘ 𝑦 ) ↔ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) → ( 2 ∥ ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ↔ 2 ∥ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) )
128 12 17 22 27 28 127 1 findcard2d ⊢ ( 𝜑 → ( 2 ∥ ( ♯ ‘ 𝐴 ) ↔ 2 ∥ Σ 𝑘 ∈ 𝐴 𝐵 ) )