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 36 45	syl2imc	$$⊢\phi \to \left(z\in \left(A\setminus y\right)\to \neg 2\parallel ⦋z/k⦌B\right)$$
47	46	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)$$
48	47	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$$
49	35 48	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)$$
50	49	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)$$
51		ssfi	$$⊢\left(A\in \mathrm{Fin}\wedge y\subseteq A\right)\to y\in \mathrm{Fin}$$
52	51	expcom	$$⊢y\subseteq A\to \left(A\in \mathrm{Fin}\to y\in \mathrm{Fin}\right)$$
53	52	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)$$
54	1 53	mpan9	$$⊢\left(\phi \wedge \left(y\subseteq A\wedge z\in \left(A\setminus y\right)\right)\right)\to y\in \mathrm{Fin}$$
55		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$$
56		ssel	$$⊢y\subseteq A\to \left(k\in y\to k\in A\right)$$
57	56	adantr	$$⊢\left(y\subseteq A\wedge z\in \left(A\setminus y\right)\right)\to \left(k\in y\to k\in A\right)$$
58	57	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)$$
59	58	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$$
60	55 59 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}$$
61	54 60	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}$$
62	61	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)$$
63		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)$$
64	50 62 63	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)$$
65	61	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 ℂ$$
66	35	zcnd	$$⊢\left(\phi \wedge \left(y\subseteq A\wedge z\in \left(A\setminus y\right)\right)\right)\to ⦋z/k⦌B\in ℂ$$
67		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$$
68	67	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)$$
69	68	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)$$
70	65 66 69	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)$$
71	70	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)$$
72	64 71	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)$$
73	72	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)$$
74	61	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)$$
75	49	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)$$
76		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)$$
77	74 75 76	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)$$
78	77	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)$$
79	78	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)$$
80	73 79	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)$$
81		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)$$
82	80 81	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)$$
83		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)$$
84		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)$$
85	82 83 84	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)$$
86		notnotb	$$⊢2\parallel \left|y\right|\leftrightarrow \neg \neg 2\parallel \left|y\right|$$
87		hashcl	$$⊢y\in \mathrm{Fin}\to \left|y\right|\in {\mathbb{N}}_0$$
88	54 87	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$$
89	88	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}$$
90		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)$$
91	89 90	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)$$
92	91	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)$$
93	86 92	bitrid	$$⊢\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)$$
94	93	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)$$
95		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)$$
96		eldifn	$$⊢z\in \left(A\setminus y\right)\to \neg z\in y$$
97	96	adantl	$$⊢\left(y\subseteq A\wedge z\in \left(A\setminus y\right)\right)\to \neg z\in y$$
98	97	adantl	$$⊢\left(\phi \wedge \left(y\subseteq A\wedge z\in \left(A\setminus y\right)\right)\right)\to \neg z\in y$$
99	54 98	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)$$
100		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)$$
101	95 99 100	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$$
102	101	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)$$
103		vex	$$⊢z\in \mathrm{V}$$
104	103	a1i	$$⊢\left(\phi \wedge \left(y\subseteq A\wedge z\in \left(A\setminus y\right)\right)\right)\to z\in \mathrm{V}$$
105		df-nel	$$⊢z\notin y\leftrightarrow \neg z\in y$$
106	98 105	sylibr	$$⊢\left(\phi \wedge \left(y\subseteq A\wedge z\in \left(A\setminus y\right)\right)\right)\to z\notin y$$
107		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$$
108		elun	$$⊢k\in \left(y\cup \left\{z\right\}\right)\leftrightarrow \left(k\in y\vee k\in \left\{z\right\}\right)$$
109	57	com12	$$⊢k\in y\to \left(\left(y\subseteq A\wedge z\in \left(A\setminus y\right)\right)\to k\in A\right)$$
110		elsni	$$⊢k\in \left\{z\right\}\to k=z$$
111		eleq1w	$$⊢k=z\to \left(k\in A\leftrightarrow z\in A\right)$$
112	30 111	imbitrrid	$$⊢k=z\to \left(\left(y\subseteq A\wedge z\in \left(A\setminus y\right)\right)\to k\in A\right)$$
113	110 112	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)$$
114	109 113	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)$$
115	108 114	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)$$
116	115	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)$$
117	116	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)$$
118	117	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$$
119	107 118 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}$$
120	119	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}$$
121		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$$
122	54 104 106 120 121	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$$
123	122	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)$$
124	102 123	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)$$
125		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)$$
126	124 125	bitrdi	$$⊢\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)$$
127	85 94 126	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)$$
128	12 17 22 27 28 127 1	findcard2d	$$⊢\phi \to \left(2\parallel \left|A\right|\leftrightarrow 2\parallel \sum _{k\in A}B\right)$$