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 45 syl ⊢ ( 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) → ( ∀ 𝑘 ∈ 𝐴 ¬ 2 ∥ 𝐵 → ¬ 2 ∥ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
47 36 46 syl5com ⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) → ¬ 2 ∥ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
48 47 a1d ⊢ ( 𝜑 → ( 𝑦 ⊆ 𝐴 → ( 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) → ¬ 2 ∥ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) )
49 48 imp32 ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ¬ 2 ∥ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 )
50 35 49 jca ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℤ ∧ ¬ 2 ∥ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
51 50 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) → ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℤ ∧ ¬ 2 ∥ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
52 ssfi ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑦 ⊆ 𝐴 ) → 𝑦 ∈ Fin )
53 52 expcom ⊢ ( 𝑦 ⊆ 𝐴 → ( 𝐴 ∈ Fin → 𝑦 ∈ Fin ) )
54 53 adantr ⊢ ( ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) → ( 𝐴 ∈ Fin → 𝑦 ∈ Fin ) )
55 1 54 syl5com ⊢ ( 𝜑 → ( ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) → 𝑦 ∈ Fin ) )
56 55 imp ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → 𝑦 ∈ Fin )
57 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 𝑘 ∈ 𝑦 ) → 𝜑 )
58 ssel ⊢ ( 𝑦 ⊆ 𝐴 → ( 𝑘 ∈ 𝑦 → 𝑘 ∈ 𝐴 ) )
59 58 adantr ⊢ ( ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) → ( 𝑘 ∈ 𝑦 → 𝑘 ∈ 𝐴 ) )
60 59 adantl ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( 𝑘 ∈ 𝑦 → 𝑘 ∈ 𝐴 ) )
61 60 imp ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 𝑘 ∈ 𝑦 ) → 𝑘 ∈ 𝐴 )
62 57 61 2 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 𝑘 ∈ 𝑦 ) → 𝐵 ∈ ℤ )
63 56 62 fsumzcl ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → Σ 𝑘 ∈ 𝑦 𝐵 ∈ ℤ )
64 63 anim1i ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) → ( Σ 𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) )
65 opeo ⊢ ( ( ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℤ ∧ ¬ 2 ∥ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ∧ ( Σ 𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) ) → ¬ 2 ∥ ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 + Σ 𝑘 ∈ 𝑦 𝐵 ) )
66 51 64 65 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) → ¬ 2 ∥ ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 + Σ 𝑘 ∈ 𝑦 𝐵 ) )
67 63 zcnd ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → Σ 𝑘 ∈ 𝑦 𝐵 ∈ ℂ )
68 35 zcnd ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℂ )
69 addcom ⊢ ( ( Σ 𝑘 ∈ 𝑦 𝐵 ∈ ℂ ∧ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℂ ) → ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) = ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 + Σ 𝑘 ∈ 𝑦 𝐵 ) )
70 69 breq2d ⊢ ( ( Σ 𝑘 ∈ 𝑦 𝐵 ∈ ℂ ∧ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℂ ) → ( 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ↔ 2 ∥ ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 + Σ 𝑘 ∈ 𝑦 𝐵 ) ) )
71 70 notbid ⊢ ( ( Σ 𝑘 ∈ 𝑦 𝐵 ∈ ℂ ∧ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℂ ) → ( ¬ 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ↔ ¬ 2 ∥ ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 + Σ 𝑘 ∈ 𝑦 𝐵 ) ) )
72 67 68 71 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( ¬ 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ↔ ¬ 2 ∥ ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 + Σ 𝑘 ∈ 𝑦 𝐵 ) ) )
73 72 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) → ( ¬ 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ↔ ¬ 2 ∥ ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 + Σ 𝑘 ∈ 𝑦 𝐵 ) ) )
74 66 73 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) → ¬ 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
75 74 ex ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 → ¬ 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) )
76 63 anim1i ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ ¬ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) → ( Σ 𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ ¬ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) )
77 50 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ ¬ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) → ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℤ ∧ ¬ 2 ∥ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
78 opoe ⊢ ( ( ( Σ 𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ ¬ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) ∧ ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℤ ∧ ¬ 2 ∥ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) → 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
79 76 77 78 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ ¬ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) → 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
80 79 ex ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( ¬ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 → 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) )
81 80 con1d ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( ¬ 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) → 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) )
82 75 81 impbid ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ↔ ¬ 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) )
83 bitr3 ⊢ ( ( 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ↔ ¬ 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) → ( ( 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ↔ ¬ 2 ∥ ( ( ♯ ‘ 𝑦 ) + 1 ) ) → ( ¬ 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ↔ ¬ 2 ∥ ( ( ♯ ‘ 𝑦 ) + 1 ) ) ) )
84 82 83 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( ( 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ↔ ¬ 2 ∥ ( ( ♯ ‘ 𝑦 ) + 1 ) ) → ( ¬ 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ↔ ¬ 2 ∥ ( ( ♯ ‘ 𝑦 ) + 1 ) ) ) )
85 bicom ⊢ ( ( ¬ 2 ∥ ( ( ♯ ‘ 𝑦 ) + 1 ) ↔ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) ↔ ( 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ↔ ¬ 2 ∥ ( ( ♯ ‘ 𝑦 ) + 1 ) ) )
86 bicom ⊢ ( ( ¬ 2 ∥ ( ( ♯ ‘ 𝑦 ) + 1 ) ↔ ¬ 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) ↔ ( ¬ 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ↔ ¬ 2 ∥ ( ( ♯ ‘ 𝑦 ) + 1 ) ) )
87 84 85 86 3imtr4g ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( ( ¬ 2 ∥ ( ( ♯ ‘ 𝑦 ) + 1 ) ↔ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) → ( ¬ 2 ∥ ( ( ♯ ‘ 𝑦 ) + 1 ) ↔ ¬ 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) ) )
88 notnotb ⊢ ( 2 ∥ ( ♯ ‘ 𝑦 ) ↔ ¬ ¬ 2 ∥ ( ♯ ‘ 𝑦 ) )
89 hashcl ⊢ ( 𝑦 ∈ Fin → ( ♯ ‘ 𝑦 ) ∈ ℕ0 )
90 56 89 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( ♯ ‘ 𝑦 ) ∈ ℕ0 )
91 90 nn0zd ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( ♯ ‘ 𝑦 ) ∈ ℤ )
92 oddp1even ⊢ ( ( ♯ ‘ 𝑦 ) ∈ ℤ → ( ¬ 2 ∥ ( ♯ ‘ 𝑦 ) ↔ 2 ∥ ( ( ♯ ‘ 𝑦 ) + 1 ) ) )
93 91 92 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( ¬ 2 ∥ ( ♯ ‘ 𝑦 ) ↔ 2 ∥ ( ( ♯ ‘ 𝑦 ) + 1 ) ) )
94 93 notbid ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( ¬ ¬ 2 ∥ ( ♯ ‘ 𝑦 ) ↔ ¬ 2 ∥ ( ( ♯ ‘ 𝑦 ) + 1 ) ) )
95 88 94 bitrid ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( 2 ∥ ( ♯ ‘ 𝑦 ) ↔ ¬ 2 ∥ ( ( ♯ ‘ 𝑦 ) + 1 ) ) )
96 95 bibi1d ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( ( 2 ∥ ( ♯ ‘ 𝑦 ) ↔ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) ↔ ( ¬ 2 ∥ ( ( ♯ ‘ 𝑦 ) + 1 ) ↔ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) ) )
97 simprr ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) )
98 eldifn ⊢ ( 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) → ¬ 𝑧 ∈ 𝑦 )
99 98 adantl ⊢ ( ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) → ¬ 𝑧 ∈ 𝑦 )
100 99 adantl ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ¬ 𝑧 ∈ 𝑦 )
101 56 100 jca ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) )
102 hashunsng ⊢ ( 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) → ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( ♯ ‘ 𝑦 ) + 1 ) ) )
103 97 101 102 sylc ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( ♯ ‘ 𝑦 ) + 1 ) )
104 103 breq2d ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( 2 ∥ ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ↔ 2 ∥ ( ( ♯ ‘ 𝑦 ) + 1 ) ) )
105 vex ⊢ 𝑧 ∈ V
106 105 a1i ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → 𝑧 ∈ V )
107 df-nel ⊢ ( 𝑧 ∉ 𝑦 ↔ ¬ 𝑧 ∈ 𝑦 )
108 100 107 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → 𝑧 ∉ 𝑦 )
109 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ) → 𝜑 )
110 elun ⊢ ( 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ↔ ( 𝑘 ∈ 𝑦 ∨ 𝑘 ∈ { 𝑧 } ) )
111 59 com12 ⊢ ( 𝑘 ∈ 𝑦 → ( ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) → 𝑘 ∈ 𝐴 ) )
112 elsni ⊢ ( 𝑘 ∈ { 𝑧 } → 𝑘 = 𝑧 )
113 eleq1w ⊢ ( 𝑘 = 𝑧 → ( 𝑘 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) )
114 30 113 imbitrrid ⊢ ( 𝑘 = 𝑧 → ( ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) → 𝑘 ∈ 𝐴 ) )
115 112 114 syl ⊢ ( 𝑘 ∈ { 𝑧 } → ( ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) → 𝑘 ∈ 𝐴 ) )
116 111 115 jaoi ⊢ ( ( 𝑘 ∈ 𝑦 ∨ 𝑘 ∈ { 𝑧 } ) → ( ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) → 𝑘 ∈ 𝐴 ) )
117 110 116 sylbi ⊢ ( 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) → 𝑘 ∈ 𝐴 ) )
118 117 com12 ⊢ ( ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) → ( 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) → 𝑘 ∈ 𝐴 ) )
119 118 adantl ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) → 𝑘 ∈ 𝐴 ) )
120 119 imp ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ) → 𝑘 ∈ 𝐴 )
121 109 120 2 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ) → 𝐵 ∈ ℤ )
122 121 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ ℤ )
123 fsumsplitsnun ⊢ ( ( 𝑦 ∈ Fin ∧ ( 𝑧 ∈ V ∧ 𝑧 ∉ 𝑦 ) ∧ ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) → Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 = ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
124 56 106 108 122 123 syl121anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 = ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
125 124 breq2d ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( 2 ∥ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ↔ 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) )
126 104 125 bibi12d ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( ( 2 ∥ ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ↔ 2 ∥ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ↔ ( 2 ∥ ( ( ♯ ‘ 𝑦 ) + 1 ) ↔ 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) ) )
127 notbi ⊢ ( ( 2 ∥ ( ( ♯ ‘ 𝑦 ) + 1 ) ↔ 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) ↔ ( ¬ 2 ∥ ( ( ♯ ‘ 𝑦 ) + 1 ) ↔ ¬ 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) )
128 126 127 bitrdi ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( ( 2 ∥ ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ↔ 2 ∥ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ↔ ( ¬ 2 ∥ ( ( ♯ ‘ 𝑦 ) + 1 ) ↔ ¬ 2 ∥ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) ) )
129 87 96 128 3imtr4d ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( ( 2 ∥ ( ♯ ‘ 𝑦 ) ↔ 2 ∥ Σ 𝑘 ∈ 𝑦 𝐵 ) → ( 2 ∥ ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ↔ 2 ∥ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ) )
130 12 17 22 27 28 129 1 findcard2d ⊢ ( 𝜑 → ( 2 ∥ ( ♯ ‘ 𝐴 ) ↔ 2 ∥ Σ 𝑘 ∈ 𝐴 𝐵 ) )