Theorem esumpad2

Description: Remove zeroes from an extended sum. (Contributed by Thierry Arnoux, 5-Jun-2020)

	Ref	Expression
Hypotheses	esumpad.1	$$⊢\phi \to A\in V$$
	esumpad.2	$$⊢\phi \to B\in W$$
	esumpad.3	$$⊢\left(\phi \wedge k\in A\right)\to C\in \left[0,\mathrm{+\infty }\right]$$
	esumpad.4	$$⊢\left(\phi \wedge k\in B\right)\to C=0$$
Assertion	esumpad2	$$⊢\phi \to \underset{k\in A\setminus B}{{\sum }^{*}}C=\underset{k\in A}{{\sum }^{*}}C$$

Proof

Step	Hyp	Ref	Expression
1		esumpad.1	$$⊢\phi \to A\in V$$
2		esumpad.2	$$⊢\phi \to B\in W$$
3		esumpad.3	$$⊢\left(\phi \wedge k\in A\right)\to C\in \left[0,\mathrm{+\infty }\right]$$
4		esumpad.4	$$⊢\left(\phi \wedge k\in B\right)\to C=0$$
5		nfv	$$⊢Ⅎk\phi$$
6		difssd	$$⊢\phi \to A\setminus B\subseteq A$$
7	5 1 3 6	esummono	$$⊢\phi \to \underset{k\in A\setminus B}{{\sum }^{*}}C\le \underset{k\in A}{{\sum }^{*}}C$$
8		unexg	$$⊢\left(A\in V\wedge B\in W\right)\to A\cup B\in \mathrm{V}$$
9	1 2 8	syl2anc	$$⊢\phi \to A\cup B\in \mathrm{V}$$
10		elun	$$⊢k\in \left(A\cup B\right)\leftrightarrow \left(k\in A\vee k\in B\right)$$
11		0e0iccpnf	$$⊢0\in \left[0,\mathrm{+\infty }\right]$$
12	4 11	eqeltrdi	$$⊢\left(\phi \wedge k\in B\right)\to C\in \left[0,\mathrm{+\infty }\right]$$
13	3 12	jaodan	$$⊢\left(\phi \wedge \left(k\in A\vee k\in B\right)\right)\to C\in \left[0,\mathrm{+\infty }\right]$$
14	10 13	sylan2b	$$⊢\left(\phi \wedge k\in \left(A\cup B\right)\right)\to C\in \left[0,\mathrm{+\infty }\right]$$
15		ssun1	$$⊢A\subseteq A\cup B$$
16	15	a1i	$$⊢\phi \to A\subseteq A\cup B$$
17	5 9 14 16	esummono	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}C\le \underset{k\in A\cup B}{{\sum }^{*}}C$$
18		undif1	$$⊢\left(A\setminus B\right)\cup B=A\cup B$$
19		esumeq1	$$⊢\left(A\setminus B\right)\cup B=A\cup B\to \underset{k\in \left(A\setminus B\right)\cup B}{{\sum }^{*}}C=\underset{k\in A\cup B}{{\sum }^{*}}C$$
20	18 19	ax-mp	$$⊢\underset{k\in \left(A\setminus B\right)\cup B}{{\sum }^{*}}C=\underset{k\in A\cup B}{{\sum }^{*}}C$$
21	1	difexd	$$⊢\phi \to A\setminus B\in \mathrm{V}$$
22	6	sselda	$$⊢\left(\phi \wedge k\in \left(A\setminus B\right)\right)\to k\in A$$
23	22 3	syldan	$$⊢\left(\phi \wedge k\in \left(A\setminus B\right)\right)\to C\in \left[0,\mathrm{+\infty }\right]$$
24	21 2 23 4	esumpad	$$⊢\phi \to \underset{k\in \left(A\setminus B\right)\cup B}{{\sum }^{*}}C=\underset{k\in A\setminus B}{{\sum }^{*}}C$$
25	20 24	eqtr3id	$$⊢\phi \to \underset{k\in A\cup B}{{\sum }^{*}}C=\underset{k\in A\setminus B}{{\sum }^{*}}C$$
26	17 25	breqtrd	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}C\le \underset{k\in A\setminus B}{{\sum }^{*}}C$$
27	7 26	jca	$$⊢\phi \to \left(\underset{k\in A\setminus B}{{\sum }^{*}}C\le \underset{k\in A}{{\sum }^{*}}C\wedge \underset{k\in A}{{\sum }^{*}}C\le \underset{k\in A\setminus B}{{\sum }^{*}}C\right)$$
28		iccssxr	$$⊢\left[0,\mathrm{+\infty }\right]\subseteq {ℝ}^{*}$$
29	23	ralrimiva	$$⊢\phi \to \forall k\in \left(A\setminus B\right)C\in \left[0,\mathrm{+\infty }\right]$$
30		nfcv	$$⊢\underset{\_}{Ⅎ}k\left(A\setminus B\right)$$
31	30	esumcl	$$⊢\left(A\setminus B\in \mathrm{V}\wedge \forall k\in \left(A\setminus B\right)C\in \left[0,\mathrm{+\infty }\right]\right)\to \underset{k\in A\setminus B}{{\sum }^{*}}C\in \left[0,\mathrm{+\infty }\right]$$
32	21 29 31	syl2anc	$$⊢\phi \to \underset{k\in A\setminus B}{{\sum }^{*}}C\in \left[0,\mathrm{+\infty }\right]$$
33	28 32	sselid	$$⊢\phi \to \underset{k\in A\setminus B}{{\sum }^{*}}C\in {ℝ}^{*}$$
34	3	ralrimiva	$$⊢\phi \to \forall k\in AC\in \left[0,\mathrm{+\infty }\right]$$
35		nfcv	$$⊢\underset{\_}{Ⅎ}kA$$
36	35	esumcl	$$⊢\left(A\in V\wedge \forall k\in AC\in \left[0,\mathrm{+\infty }\right]\right)\to \underset{k\in A}{{\sum }^{*}}C\in \left[0,\mathrm{+\infty }\right]$$
37	1 34 36	syl2anc	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}C\in \left[0,\mathrm{+\infty }\right]$$
38	28 37	sselid	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}C\in {ℝ}^{*}$$
39		xrletri3	$$⊢\left(\underset{k\in A\setminus B}{{\sum }^{*}}C\in {ℝ}^{*}\wedge \underset{k\in A}{{\sum }^{*}}C\in {ℝ}^{*}\right)\to \left(\underset{k\in A\setminus B}{{\sum }^{*}}C=\underset{k\in A}{{\sum }^{*}}C\leftrightarrow \left(\underset{k\in A\setminus B}{{\sum }^{*}}C\le \underset{k\in A}{{\sum }^{*}}C\wedge \underset{k\in A}{{\sum }^{*}}C\le \underset{k\in A\setminus B}{{\sum }^{*}}C\right)\right)$$
40	33 38 39	syl2anc	$$⊢\phi \to \left(\underset{k\in A\setminus B}{{\sum }^{*}}C=\underset{k\in A}{{\sum }^{*}}C\leftrightarrow \left(\underset{k\in A\setminus B}{{\sum }^{*}}C\le \underset{k\in A}{{\sum }^{*}}C\wedge \underset{k\in A}{{\sum }^{*}}C\le \underset{k\in A\setminus B}{{\sum }^{*}}C\right)\right)$$
41	27 40	mpbird	$$⊢\phi \to \underset{k\in A\setminus B}{{\sum }^{*}}C=\underset{k\in A}{{\sum }^{*}}C$$