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 \mathbb{Z}$$
	sumodd.o	$$⊢\left(\phi \wedge k\in A\right)\to \neg 2\parallel B$$
Assertion	sumodd	$$⊢\phi \to \left(2\parallel \left|A\right|\leftrightarrow 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 \mathbb{Z}$$
3		sumodd.o	$$⊢\left(\phi \wedge k\in A\right)\to \neg 2\parallel B$$
4		fveq2	$$⊢x=\varnothing \to \left|x\right|=\left|\varnothing \right|$$
5		hash0	$$⊢\left|\varnothing \right|=0$$
6	4 5	eqtrdi	$$⊢x=\varnothing \to \left|x\right|=0$$
7	6	breq2d	$$⊢x=\varnothing \to \left(2\parallel \left|x\right|\leftrightarrow 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	eqtrdi	$$⊢x=\varnothing \to \sum _{k\in x}B=0$$
11	10	breq2d	$$⊢x=\varnothing \to \left(2\parallel \sum _{k\in x}B\leftrightarrow 2\parallel 0\right)$$
12	7 11	bibi12d	$$⊢x=\varnothing \to \left(\left(2\parallel \left|x\right|\leftrightarrow 2\parallel \sum _{k\in x}B\right)\leftrightarrow \left(2\parallel 0\leftrightarrow 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|\leftrightarrow 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\leftrightarrow 2\parallel \sum _{k\in y}B\right)$$
17	14 16	bibi12d	$$⊢x=y\to \left(\left(2\parallel \left|x\right|\leftrightarrow 2\parallel \sum _{k\in x}B\right)\leftrightarrow \left(2\parallel \left|y\right|\leftrightarrow 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|\leftrightarrow 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\leftrightarrow 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|\leftrightarrow 2\parallel \sum _{k\in x}B\right)\leftrightarrow \left(2\parallel \left|y\cup \left\{z\right\}\right|\leftrightarrow 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|\leftrightarrow 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\leftrightarrow 2\parallel \sum _{k\in A}B\right)$$
27	24 26	bibi12d	$$⊢x=A\to \left(\left(2\parallel \left|x\right|\leftrightarrow 2\parallel \sum _{k\in x}B\right)\leftrightarrow \left(2\parallel \left|A\right|\leftrightarrow 2\parallel \sum _{k\in A}B\right)\right)$$
28		biidd	$$⊢\phi \to \left(2\parallel 0\leftrightarrow 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 \mathbb{Z}$$
33	32	ralrimiva	$$⊢\left(\phi \wedge \left(y\subseteq A\wedge z\in \left(A\setminus y\right)\right)\right)\to \forall k\in AB\in \mathbb{Z}$$
34		rspcsbela	$$⊢\left(z\in A\wedge \forall k\in AB\in \mathbb{Z}\right)\to ⦋z/k⦌B\in \mathbb{Z}$$
35	31 33 34	syl2anc	$$⊢\left(\phi \wedge \left(y\subseteq A\wedge z\in \left(A\setminus y\right)\right)\right)\to ⦋z/k⦌B\in \mathbb{Z}$$
36	3	ralrimiva	$$⊢\phi \to \forall k\in A\neg 2\parallel B$$
37		nfcv	$$⊢\underset{\_}{Ⅎ}k2$$
38		nfcv	$$⊢\underset{\_}{Ⅎ}k\parallel$$
39		nfcsb1v	$$⊢\underset{\_}{Ⅎ}k⦋z/k⦌B$$
40	37 38 39	nfbr	$$⊢Ⅎk2\parallel ⦋z/k⦌B$$
41	40	nfn	$$⊢Ⅎk\neg 2\parallel ⦋z/k⦌B$$
42		csbeq1a	$$⊢k=z\to B=⦋z/k⦌B$$
43	42	breq2d	$$⊢k=z\to \left(2\parallel B\leftrightarrow 2\parallel ⦋z/k⦌B\right)$$
44	43	notbid	$$⊢k=z\to \left(\neg 2\parallel B\leftrightarrow \neg 2\parallel ⦋z/k⦌B\right)$$
45	41 44	rspc	$$⊢z\in A\to \left(\forall k\in A\neg 2\parallel B\to \neg 2\parallel ⦋z/k⦌B\right)$$
46	29 45	syl	$$⊢z\in \left(A\setminus y\right)\to \left(\forall k\in A\neg 2\parallel B\to \neg 2\parallel ⦋z/k⦌B\right)$$
47	36 46	syl5com	$$⊢\phi \to \left(z\in \left(A\setminus y\right)\to \neg 2\parallel ⦋z/k⦌B\right)$$
48	47	a1d	$$⊢\phi \to \left(y\subseteq A\to \left(z\in \left(A\setminus y\right)\to \neg 2\parallel ⦋z/k⦌B\right)\right)$$
49	48	imp32	$$⊢\left(\phi \wedge \left(y\subseteq A\wedge z\in \left(A\setminus y\right)\right)\right)\to \neg 2\parallel ⦋z/k⦌B$$
50	35 49	jca	$$⊢\left(\phi \wedge \left(y\subseteq A\wedge z\in \left(A\setminus y\right)\right)\right)\to \left(⦋z/k⦌B\in \mathbb{Z}\wedge \neg 2\parallel ⦋z/k⦌B\right)$$
51	50	adantr	$$⊢\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(⦋z/k⦌B\in \mathbb{Z}\wedge \neg 2\parallel ⦋z/k⦌B\right)$$
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 \mathbb{Z}$$
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 \mathbb{Z}$$
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 \mathbb{Z}\wedge 2\parallel \sum _{k\in y}B\right)$$
65		opeo	$$⊢\left(\left(⦋z/k⦌B\in \mathbb{Z}\wedge \neg 2\parallel ⦋z/k⦌B\right)\wedge \left(\sum _{k\in y}B\in \mathbb{Z}\wedge 2\parallel \sum _{k\in y}B\right)\right)\to \neg 2\parallel \left(⦋z/k⦌B+\sum _{k\in y}B\right)$$
66	51 64 65	syl2anc	$$⊢\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 \neg 2\parallel \left(⦋z/k⦌B+\sum _{k\in y}B\right)$$
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	$$⊢\left(\phi \wedge \left(y\subseteq A\wedge z\in \left(A\setminus y\right)\right)\right)\to ⦋z/k⦌B\in ℂ$$
69		addcom	$$⊢\left(\sum _{k\in y}B\in ℂ\wedge ⦋z/k⦌B\in ℂ\right)\to \sum _{k\in y}B+⦋z/k⦌B=⦋z/k⦌B+\sum _{k\in y}B$$
70	69	breq2d	$$⊢\left(\sum _{k\in y}B\in ℂ\wedge ⦋z/k⦌B\in ℂ\right)\to \left(2\parallel \left(\sum _{k\in y}B+⦋z/k⦌B\right)\leftrightarrow 2\parallel \left(⦋z/k⦌B+\sum _{k\in y}B\right)\right)$$
71	70	notbid	$$⊢\left(\sum _{k\in y}B\in ℂ\wedge ⦋z/k⦌B\in ℂ\right)\to \left(\neg 2\parallel \left(\sum _{k\in y}B+⦋z/k⦌B\right)\leftrightarrow \neg 2\parallel \left(⦋z/k⦌B+\sum _{k\in y}B\right)\right)$$
72	67 68 71	syl2anc	$$⊢\left(\phi \wedge \left(y\subseteq A\wedge z\in \left(A\setminus y\right)\right)\right)\to \left(\neg 2\parallel \left(\sum _{k\in y}B+⦋z/k⦌B\right)\leftrightarrow \neg 2\parallel \left(⦋z/k⦌B+\sum _{k\in y}B\right)\right)$$
73	72	adantr	$$⊢\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(\neg 2\parallel \left(\sum _{k\in y}B+⦋z/k⦌B\right)\leftrightarrow \neg 2\parallel \left(⦋z/k⦌B+\sum _{k\in y}B\right)\right)$$
74	66 73	mpbird	$$⊢\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 \neg 2\parallel \left(\sum _{k\in y}B+⦋z/k⦌B\right)$$
75	74	ex	$$⊢\left(\phi \wedge \left(y\subseteq A\wedge z\in \left(A\setminus y\right)\right)\right)\to \left(2\parallel \sum _{k\in y}B\to \neg 2\parallel \left(\sum _{k\in y}B+⦋z/k⦌B\right)\right)$$
76	63	anim1i	$$⊢\left(\left(\phi \wedge \left(y\subseteq A\wedge z\in \left(A\setminus y\right)\right)\right)\wedge \neg 2\parallel \sum _{k\in y}B\right)\to \left(\sum _{k\in y}B\in \mathbb{Z}\wedge \neg 2\parallel \sum _{k\in y}B\right)$$
77	50	adantr	$$⊢\left(\left(\phi \wedge \left(y\subseteq A\wedge z\in \left(A\setminus y\right)\right)\right)\wedge \neg 2\parallel \sum _{k\in y}B\right)\to \left(⦋z/k⦌B\in \mathbb{Z}\wedge \neg 2\parallel ⦋z/k⦌B\right)$$
78		opoe	$$⊢\left(\left(\sum _{k\in y}B\in \mathbb{Z}\wedge \neg 2\parallel \sum _{k\in y}B\right)\wedge \left(⦋z/k⦌B\in \mathbb{Z}\wedge \neg 2\parallel ⦋z/k⦌B\right)\right)\to 2\parallel \left(\sum _{k\in y}B+⦋z/k⦌B\right)$$
79	76 77 78	syl2anc	$$⊢\left(\left(\phi \wedge \left(y\subseteq A\wedge z\in \left(A\setminus y\right)\right)\right)\wedge \neg 2\parallel \sum _{k\in y}B\right)\to 2\parallel \left(\sum _{k\in y}B+⦋z/k⦌B\right)$$
80	79	ex	$$⊢\left(\phi \wedge \left(y\subseteq A\wedge z\in \left(A\setminus y\right)\right)\right)\to \left(\neg 2\parallel \sum _{k\in y}B\to 2\parallel \left(\sum _{k\in y}B+⦋z/k⦌B\right)\right)$$
81	80	con1d	$$⊢\left(\phi \wedge \left(y\subseteq A\wedge z\in \left(A\setminus y\right)\right)\right)\to \left(\neg 2\parallel \left(\sum _{k\in y}B+⦋z/k⦌B\right)\to 2\parallel \sum _{k\in y}B\right)$$
82	75 81	impbid	$$⊢\left(\phi \wedge \left(y\subseteq A\wedge z\in \left(A\setminus y\right)\right)\right)\to \left(2\parallel \sum _{k\in y}B\leftrightarrow \neg 2\parallel \left(\sum _{k\in y}B+⦋z/k⦌B\right)\right)$$
83		bitr3	$$⊢\left(2\parallel \sum _{k\in y}B\leftrightarrow \neg 2\parallel \left(\sum _{k\in y}B+⦋z/k⦌B\right)\right)\to \left(\left(2\parallel \sum _{k\in y}B\leftrightarrow \neg 2\parallel \left(\left|y\right|+1\right)\right)\to \left(\neg 2\parallel \left(\sum _{k\in y}B+⦋z/k⦌B\right)\leftrightarrow \neg 2\parallel \left(\left|y\right|+1\right)\right)\right)$$
84	82 83	syl	$$⊢\left(\phi \wedge \left(y\subseteq A\wedge z\in \left(A\setminus y\right)\right)\right)\to \left(\left(2\parallel \sum _{k\in y}B\leftrightarrow \neg 2\parallel \left(\left|y\right|+1\right)\right)\to \left(\neg 2\parallel \left(\sum _{k\in y}B+⦋z/k⦌B\right)\leftrightarrow \neg 2\parallel \left(\left|y\right|+1\right)\right)\right)$$
85		bicom	$$⊢\left(\neg 2\parallel \left(\left|y\right|+1\right)\leftrightarrow 2\parallel \sum _{k\in y}B\right)\leftrightarrow \left(2\parallel \sum _{k\in y}B\leftrightarrow \neg 2\parallel \left(\left|y\right|+1\right)\right)$$
86		bicom	$$⊢\left(\neg 2\parallel \left(\left|y\right|+1\right)\leftrightarrow \neg 2\parallel \left(\sum _{k\in y}B+⦋z/k⦌B\right)\right)\leftrightarrow \left(\neg 2\parallel \left(\sum _{k\in y}B+⦋z/k⦌B\right)\leftrightarrow \neg 2\parallel \left(\left|y\right|+1\right)\right)$$
87	84 85 86	3imtr4g	$$⊢\left(\phi \wedge \left(y\subseteq A\wedge z\in \left(A\setminus y\right)\right)\right)\to \left(\left(\neg 2\parallel \left(\left|y\right|+1\right)\leftrightarrow 2\parallel \sum _{k\in y}B\right)\to \left(\neg 2\parallel \left(\left|y\right|+1\right)\leftrightarrow \neg 2\parallel \left(\sum _{k\in y}B+⦋z/k⦌B\right)\right)\right)$$
88		notnotb	$$⊢2\parallel \left|y\right|\leftrightarrow \neg \neg 2\parallel \left|y\right|$$
89		hashcl	$$⊢y\in \mathrm{Fin}\to \left|y\right|\in {\mathbb{N}}_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 {\mathbb{N}}_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 \mathbb{Z}$$
92		oddp1even	$$⊢\left|y\right|\in \mathbb{Z}\to \left(\neg 2\parallel \left|y\right|\leftrightarrow 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(\neg 2\parallel \left|y\right|\leftrightarrow 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(\neg \neg 2\parallel \left|y\right|\leftrightarrow \neg 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|\leftrightarrow \neg 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|\leftrightarrow 2\parallel \sum _{k\in y}B\right)\leftrightarrow \left(\neg 2\parallel \left(\left|y\right|+1\right)\leftrightarrow 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 \neg z\in y$$
99	98	adantl	$$⊢\left(y\subseteq A\wedge z\in \left(A\setminus y\right)\right)\to \neg z\in y$$
100	99	adantl	$$⊢\left(\phi \wedge \left(y\subseteq A\wedge z\in \left(A\setminus y\right)\right)\right)\to \neg 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 \neg z\in y\right)$$
102		hashunsng	$$⊢z\in \left(A\setminus y\right)\to \left(\left(y\in \mathrm{Fin}\wedge \neg 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|\leftrightarrow 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\leftrightarrow \neg 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)\leftrightarrow \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\leftrightarrow 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 \mathbb{Z}$$
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)B\in \mathbb{Z}$$
123		fsumsplitsnun	$$⊢\left(y\in \mathrm{Fin}\wedge \left(z\in \mathrm{V}\wedge z\notin y\right)\wedge \forall k\in \left(y\cup \left\{z\right\}\right)B\in \mathbb{Z}\right)\to \sum _{k\in y\cup \left\{z\right\}}B=\sum _{k\in y}B+⦋z/k⦌B$$
124	56 106 108 122 123	syl121anc	$$⊢\left(\phi \wedge \left(y\subseteq A\wedge z\in \left(A\setminus y\right)\right)\right)\to \sum _{k\in y\cup \left\{z\right\}}B=\sum _{k\in y}B+⦋z/k⦌B$$
125	124	breq2d	$$⊢\left(\phi \wedge \left(y\subseteq A\wedge z\in \left(A\setminus y\right)\right)\right)\to \left(2\parallel \sum _{k\in y\cup \left\{z\right\}}B\leftrightarrow 2\parallel \left(\sum _{k\in y}B+⦋z/k⦌B\right)\right)$$
126	104 125	bibi12d	$$⊢\left(\phi \wedge \left(y\subseteq A\wedge z\in \left(A\setminus y\right)\right)\right)\to \left(\left(2\parallel \left|y\cup \left\{z\right\}\right|\leftrightarrow 2\parallel \sum _{k\in y\cup \left\{z\right\}}B\right)\leftrightarrow \left(2\parallel \left(\left|y\right|+1\right)\leftrightarrow 2\parallel \left(\sum _{k\in y}B+⦋z/k⦌B\right)\right)\right)$$
127		notbi	$$⊢\left(2\parallel \left(\left|y\right|+1\right)\leftrightarrow 2\parallel \left(\sum _{k\in y}B+⦋z/k⦌B\right)\right)\leftrightarrow \left(\neg 2\parallel \left(\left|y\right|+1\right)\leftrightarrow \neg 2\parallel \left(\sum _{k\in y}B+⦋z/k⦌B\right)\right)$$
128	126 127	syl6bb	$$⊢\left(\phi \wedge \left(y\subseteq A\wedge z\in \left(A\setminus y\right)\right)\right)\to \left(\left(2\parallel \left|y\cup \left\{z\right\}\right|\leftrightarrow 2\parallel \sum _{k\in y\cup \left\{z\right\}}B\right)\leftrightarrow \left(\neg 2\parallel \left(\left|y\right|+1\right)\leftrightarrow \neg 2\parallel \left(\sum _{k\in y}B+⦋z/k⦌B\right)\right)\right)$$
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|\leftrightarrow 2\parallel \sum _{k\in y}B\right)\to \left(2\parallel \left|y\cup \left\{z\right\}\right|\leftrightarrow 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|\leftrightarrow 2\parallel \sum _{k\in A}B\right)$$