sge0xadd

Description: The extended addition of two generalized sums of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypotheses	sge0xadd.kph	$⊢ Ⅎ k φ$
	sge0xadd.a	$⊢ φ \to A \in V$
	sge0xadd.b	$⊢ (φ \land k \in A) \to B \in [0, +∞]$
	sge0xadd.c	$⊢ (φ \land k \in A) \to C \in [0, +∞]$
Assertion	sge0xadd	$⊢ φ \to sum^((k \in A ⟼ B +_{𝑒} C)) = sum^((k \in A ⟼ B)) +_{𝑒} sum^((k \in A ⟼ C))$

Proof

Step	Hyp	Ref	Expression
1		sge0xadd.kph	$⊢ Ⅎ k φ$
2		sge0xadd.a	$⊢ φ \to A \in V$
3		sge0xadd.b	$⊢ (φ \land k \in A) \to B \in [0, +∞]$
4		sge0xadd.c	$⊢ (φ \land k \in A) \to C \in [0, +∞]$
5		simpr	$⊢ (φ \land sum^((k \in A ⟼ B)) = +∞) \to sum^((k \in A ⟼ B)) = +∞$
6	5	oveq1d	$⊢ (φ \land sum^((k \in A ⟼ B)) = +∞) \to sum^((k \in A ⟼ B)) +_{𝑒} sum^((k \in A ⟼ C)) = +∞ +_{𝑒} sum^((k \in A ⟼ C))$
7	1 2 4	sge0xrclmpt	$⊢ φ \to sum^((k \in A ⟼ C)) \in ℝ^{*}$
8		eqid	$⊢ (k \in A ⟼ C) = (k \in A ⟼ C)$
9	1 4 8	fmptdf	$⊢ φ \to (k \in A ⟼ C) : A ⟶ [0, +∞]$
10	2 9	sge0nemnf	$⊢ φ \to sum^((k \in A ⟼ C)) \neq −∞$
11		xaddpnf2	$⊢ (sum^((k \in A ⟼ C)) \in ℝ^{*} \land sum^((k \in A ⟼ C)) \neq −∞) \to +∞ +_{𝑒} sum^((k \in A ⟼ C)) = +∞$
12	7 10 11	syl2anc	$⊢ φ \to +∞ +_{𝑒} sum^((k \in A ⟼ C)) = +∞$
13	12	adantr	$⊢ (φ \land sum^((k \in A ⟼ B)) = +∞) \to +∞ +_{𝑒} sum^((k \in A ⟼ C)) = +∞$
14		ge0xaddcl	$⊢ (B \in [0, +∞] \land C \in [0, +∞]) \to B +_{𝑒} C \in [0, +∞]$
15	3 4 14	syl2anc	$⊢ (φ \land k \in A) \to B +_{𝑒} C \in [0, +∞]$
16	1 2 15	sge0xrclmpt	$⊢ φ \to sum^((k \in A ⟼ B +_{𝑒} C)) \in ℝ^{*}$
17	16	adantr	$⊢ (φ \land sum^((k \in A ⟼ B)) = +∞) \to sum^((k \in A ⟼ B +_{𝑒} C)) \in ℝ^{*}$
18		id	$⊢ sum^((k \in A ⟼ B)) = +∞ \to sum^((k \in A ⟼ B)) = +∞$
19	18	eqcomd	$⊢ sum^((k \in A ⟼ B)) = +∞ \to +∞ = sum^((k \in A ⟼ B))$
20	19	adantl	$⊢ (φ \land sum^((k \in A ⟼ B)) = +∞) \to +∞ = sum^((k \in A ⟼ B))$
21	2	elexd	$⊢ φ \to A \in V$
22		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
23	22 3	sselid	$⊢ (φ \land k \in A) \to B \in ℝ^{*}$
24	23 4	xadd0ge	$⊢ (φ \land k \in A) \to B \leq B +_{𝑒} C$
25	1 21 3 15 24	sge0lempt	$⊢ φ \to sum^((k \in A ⟼ B)) \leq sum^((k \in A ⟼ B +_{𝑒} C))$
26	25	adantr	$⊢ (φ \land sum^((k \in A ⟼ B)) = +∞) \to sum^((k \in A ⟼ B)) \leq sum^((k \in A ⟼ B +_{𝑒} C))$
27	20 26	eqbrtrd	$⊢ (φ \land sum^((k \in A ⟼ B)) = +∞) \to +∞ \leq sum^((k \in A ⟼ B +_{𝑒} C))$
28	17 27	xrgepnfd	$⊢ (φ \land sum^((k \in A ⟼ B)) = +∞) \to sum^((k \in A ⟼ B +_{𝑒} C)) = +∞$
29	28	eqcomd	$⊢ (φ \land sum^((k \in A ⟼ B)) = +∞) \to +∞ = sum^((k \in A ⟼ B +_{𝑒} C))$
30	6 13 29	3eqtrrd	$⊢ (φ \land sum^((k \in A ⟼ B)) = +∞) \to sum^((k \in A ⟼ B +_{𝑒} C)) = sum^((k \in A ⟼ B)) +_{𝑒} sum^((k \in A ⟼ C))$
31		simpl	$⊢ (φ \land \neg sum^((k \in A ⟼ B)) = +∞) \to φ$
32		simpr	$⊢ (φ \land \neg sum^((k \in A ⟼ B)) = +∞) \to \neg sum^((k \in A ⟼ B)) = +∞$
33		eqid	$⊢ (k \in A ⟼ B) = (k \in A ⟼ B)$
34	1 3 33	fmptdf	$⊢ φ \to (k \in A ⟼ B) : A ⟶ [0, +∞]$
35	2 34	sge0repnf	$⊢ φ \to (sum^((k \in A ⟼ B)) \in ℝ \leftrightarrow \neg sum^((k \in A ⟼ B)) = +∞)$
36	35	adantr	$⊢ (φ \land \neg sum^((k \in A ⟼ B)) = +∞) \to (sum^((k \in A ⟼ B)) \in ℝ \leftrightarrow \neg sum^((k \in A ⟼ B)) = +∞)$
37	32 36	mpbird	$⊢ (φ \land \neg sum^((k \in A ⟼ B)) = +∞) \to sum^((k \in A ⟼ B)) \in ℝ$
38		simpr	$⊢ (φ \land sum^((k \in A ⟼ C)) = +∞) \to sum^((k \in A ⟼ C)) = +∞$
39	38	oveq2d	$⊢ (φ \land sum^((k \in A ⟼ C)) = +∞) \to sum^((k \in A ⟼ B)) +_{𝑒} sum^((k \in A ⟼ C)) = sum^((k \in A ⟼ B)) +_{𝑒} +∞$
40	2 34	sge0xrcl	$⊢ φ \to sum^((k \in A ⟼ B)) \in ℝ^{*}$
41	2 34	sge0nemnf	$⊢ φ \to sum^((k \in A ⟼ B)) \neq −∞$
42		xaddpnf1	$⊢ (sum^((k \in A ⟼ B)) \in ℝ^{*} \land sum^((k \in A ⟼ B)) \neq −∞) \to sum^((k \in A ⟼ B)) +_{𝑒} +∞ = +∞$
43	40 41 42	syl2anc	$⊢ φ \to sum^((k \in A ⟼ B)) +_{𝑒} +∞ = +∞$
44	43	adantr	$⊢ (φ \land sum^((k \in A ⟼ C)) = +∞) \to sum^((k \in A ⟼ B)) +_{𝑒} +∞ = +∞$
45	16	adantr	$⊢ (φ \land sum^((k \in A ⟼ C)) = +∞) \to sum^((k \in A ⟼ B +_{𝑒} C)) \in ℝ^{*}$
46		id	$⊢ sum^((k \in A ⟼ C)) = +∞ \to sum^((k \in A ⟼ C)) = +∞$
47	46	eqcomd	$⊢ sum^((k \in A ⟼ C)) = +∞ \to +∞ = sum^((k \in A ⟼ C))$
48	47	adantl	$⊢ (φ \land sum^((k \in A ⟼ C)) = +∞) \to +∞ = sum^((k \in A ⟼ C))$
49	22 4	sselid	$⊢ (φ \land k \in A) \to C \in ℝ^{*}$
50	49 3	xadd0ge2	$⊢ (φ \land k \in A) \to C \leq B +_{𝑒} C$
51	1 2 4 15 50	sge0lempt	$⊢ φ \to sum^((k \in A ⟼ C)) \leq sum^((k \in A ⟼ B +_{𝑒} C))$
52	51	adantr	$⊢ (φ \land sum^((k \in A ⟼ C)) = +∞) \to sum^((k \in A ⟼ C)) \leq sum^((k \in A ⟼ B +_{𝑒} C))$
53	48 52	eqbrtrd	$⊢ (φ \land sum^((k \in A ⟼ C)) = +∞) \to +∞ \leq sum^((k \in A ⟼ B +_{𝑒} C))$
54	45 53	xrgepnfd	$⊢ (φ \land sum^((k \in A ⟼ C)) = +∞) \to sum^((k \in A ⟼ B +_{𝑒} C)) = +∞$
55	54	eqcomd	$⊢ (φ \land sum^((k \in A ⟼ C)) = +∞) \to +∞ = sum^((k \in A ⟼ B +_{𝑒} C))$
56	39 44 55	3eqtrrd	$⊢ (φ \land sum^((k \in A ⟼ C)) = +∞) \to sum^((k \in A ⟼ B +_{𝑒} C)) = sum^((k \in A ⟼ B)) +_{𝑒} sum^((k \in A ⟼ C))$
57	56	adantlr	$⊢ ((φ \land sum^((k \in A ⟼ B)) \in ℝ) \land sum^((k \in A ⟼ C)) = +∞) \to sum^((k \in A ⟼ B +_{𝑒} C)) = sum^((k \in A ⟼ B)) +_{𝑒} sum^((k \in A ⟼ C))$
58		simpl	$⊢ ((φ \land sum^((k \in A ⟼ B)) \in ℝ) \land \neg sum^((k \in A ⟼ C)) = +∞) \to (φ \land sum^((k \in A ⟼ B)) \in ℝ)$
59		simpr	$⊢ (φ \land \neg sum^((k \in A ⟼ C)) = +∞) \to \neg sum^((k \in A ⟼ C)) = +∞$
60	2 9	sge0repnf	$⊢ φ \to (sum^((k \in A ⟼ C)) \in ℝ \leftrightarrow \neg sum^((k \in A ⟼ C)) = +∞)$
61	60	adantr	$⊢ (φ \land \neg sum^((k \in A ⟼ C)) = +∞) \to (sum^((k \in A ⟼ C)) \in ℝ \leftrightarrow \neg sum^((k \in A ⟼ C)) = +∞)$
62	59 61	mpbird	$⊢ (φ \land \neg sum^((k \in A ⟼ C)) = +∞) \to sum^((k \in A ⟼ C)) \in ℝ$
63	62	adantlr	$⊢ ((φ \land sum^((k \in A ⟼ B)) \in ℝ) \land \neg sum^((k \in A ⟼ C)) = +∞) \to sum^((k \in A ⟼ C)) \in ℝ$
64	2	ad2antrr	$⊢ ((φ \land sum^((k \in A ⟼ B)) \in ℝ) \land sum^((k \in A ⟼ C)) \in ℝ) \to A \in V$
65		nfcv	$⊢ \underline{Ⅎ} k sum^$
66		nfmpt1	$⊢ \underline{Ⅎ} k (k \in A ⟼ B)$
67	65 66	nffv	$⊢ \underline{Ⅎ} k sum^((k \in A ⟼ B))$
68		nfcv	$⊢ \underline{Ⅎ} k ℝ$
69	67 68	nfel	$⊢ Ⅎ k sum^((k \in A ⟼ B)) \in ℝ$
70	1 69	nfan	$⊢ Ⅎ k (φ \land sum^((k \in A ⟼ B)) \in ℝ)$
71		nfv	$⊢ Ⅎ k j \in A$
72	70 71	nfan	$⊢ Ⅎ k ((φ \land sum^((k \in A ⟼ B)) \in ℝ) \land j \in A)$
73		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ j / k ⦌ B$
74	73	nfel1	$⊢ Ⅎ k ⦋ j / k ⦌ B \in [0, +∞)$
75	72 74	nfim	$⊢ Ⅎ k (((φ \land sum^((k \in A ⟼ B)) \in ℝ) \land j \in A) \to ⦋ j / k ⦌ B \in [0, +∞))$
76		eleq1w	$⊢ k = j \to (k \in A \leftrightarrow j \in A)$
77	76	anbi2d	$⊢ k = j \to (((φ \land sum^((k \in A ⟼ B)) \in ℝ) \land k \in A) \leftrightarrow ((φ \land sum^((k \in A ⟼ B)) \in ℝ) \land j \in A))$
78		csbeq1a	$⊢ k = j \to B = ⦋ j / k ⦌ B$
79	78	eleq1d	$⊢ k = j \to (B \in [0, +∞) \leftrightarrow ⦋ j / k ⦌ B \in [0, +∞))$
80	77 79	imbi12d	$⊢ k = j \to ((((φ \land sum^((k \in A ⟼ B)) \in ℝ) \land k \in A) \to B \in [0, +∞)) \leftrightarrow (((φ \land sum^((k \in A ⟼ B)) \in ℝ) \land j \in A) \to ⦋ j / k ⦌ B \in [0, +∞)))$
81	2	adantr	$⊢ (φ \land sum^((k \in A ⟼ B)) \in ℝ) \to A \in V$
82	3	adantlr	$⊢ ((φ \land sum^((k \in A ⟼ B)) \in ℝ) \land k \in A) \to B \in [0, +∞]$
83		simpr	$⊢ (φ \land sum^((k \in A ⟼ B)) \in ℝ) \to sum^((k \in A ⟼ B)) \in ℝ$
84	70 81 82 83	sge0rernmpt	$⊢ ((φ \land sum^((k \in A ⟼ B)) \in ℝ) \land k \in A) \to B \in [0, +∞)$
85	75 80 84	chvarfv	$⊢ ((φ \land sum^((k \in A ⟼ B)) \in ℝ) \land j \in A) \to ⦋ j / k ⦌ B \in [0, +∞)$
86	85	adantlr	$⊢ (((φ \land sum^((k \in A ⟼ B)) \in ℝ) \land sum^((k \in A ⟼ C)) \in ℝ) \land j \in A) \to ⦋ j / k ⦌ B \in [0, +∞)$
87		nfmpt1	$⊢ \underline{Ⅎ} k (k \in A ⟼ C)$
88	65 87	nffv	$⊢ \underline{Ⅎ} k sum^((k \in A ⟼ C))$
89	88 68	nfel	$⊢ Ⅎ k sum^((k \in A ⟼ C)) \in ℝ$
90	1 89	nfan	$⊢ Ⅎ k (φ \land sum^((k \in A ⟼ C)) \in ℝ)$
91	90 71	nfan	$⊢ Ⅎ k ((φ \land sum^((k \in A ⟼ C)) \in ℝ) \land j \in A)$
92		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ j / k ⦌ C$
93	92	nfel1	$⊢ Ⅎ k ⦋ j / k ⦌ C \in [0, +∞)$
94	91 93	nfim	$⊢ Ⅎ k (((φ \land sum^((k \in A ⟼ C)) \in ℝ) \land j \in A) \to ⦋ j / k ⦌ C \in [0, +∞))$
95	76	anbi2d	$⊢ k = j \to (((φ \land sum^((k \in A ⟼ C)) \in ℝ) \land k \in A) \leftrightarrow ((φ \land sum^((k \in A ⟼ C)) \in ℝ) \land j \in A))$
96		csbeq1a	$⊢ k = j \to C = ⦋ j / k ⦌ C$
97	96	eleq1d	$⊢ k = j \to (C \in [0, +∞) \leftrightarrow ⦋ j / k ⦌ C \in [0, +∞))$
98	95 97	imbi12d	$⊢ k = j \to ((((φ \land sum^((k \in A ⟼ C)) \in ℝ) \land k \in A) \to C \in [0, +∞)) \leftrightarrow (((φ \land sum^((k \in A ⟼ C)) \in ℝ) \land j \in A) \to ⦋ j / k ⦌ C \in [0, +∞)))$
99	2	adantr	$⊢ (φ \land sum^((k \in A ⟼ C)) \in ℝ) \to A \in V$
100	4	adantlr	$⊢ ((φ \land sum^((k \in A ⟼ C)) \in ℝ) \land k \in A) \to C \in [0, +∞]$
101		simpr	$⊢ (φ \land sum^((k \in A ⟼ C)) \in ℝ) \to sum^((k \in A ⟼ C)) \in ℝ$
102	90 99 100 101	sge0rernmpt	$⊢ ((φ \land sum^((k \in A ⟼ C)) \in ℝ) \land k \in A) \to C \in [0, +∞)$
103	94 98 102	chvarfv	$⊢ ((φ \land sum^((k \in A ⟼ C)) \in ℝ) \land j \in A) \to ⦋ j / k ⦌ C \in [0, +∞)$
104	103	adantllr	$⊢ (((φ \land sum^((k \in A ⟼ B)) \in ℝ) \land sum^((k \in A ⟼ C)) \in ℝ) \land j \in A) \to ⦋ j / k ⦌ C \in [0, +∞)$
105		nfcv	$⊢ \underline{Ⅎ} j B$
106	105 73 78	cbvmpt	$⊢ (k \in A ⟼ B) = (j \in A ⟼ ⦋ j / k ⦌ B)$
107	106	fveq2i	$⊢ sum^((k \in A ⟼ B)) = sum^((j \in A ⟼ ⦋ j / k ⦌ B))$
108		simplr	$⊢ ((φ \land sum^((k \in A ⟼ B)) \in ℝ) \land sum^((k \in A ⟼ C)) \in ℝ) \to sum^((k \in A ⟼ B)) \in ℝ$
109	107 108	eqeltrrid	$⊢ ((φ \land sum^((k \in A ⟼ B)) \in ℝ) \land sum^((k \in A ⟼ C)) \in ℝ) \to sum^((j \in A ⟼ ⦋ j / k ⦌ B)) \in ℝ$
110		nfcv	$⊢ \underline{Ⅎ} j C$
111	110 92 96	cbvmpt	$⊢ (k \in A ⟼ C) = (j \in A ⟼ ⦋ j / k ⦌ C)$
112	111	fveq2i	$⊢ sum^((k \in A ⟼ C)) = sum^((j \in A ⟼ ⦋ j / k ⦌ C))$
113		simpr	$⊢ ((φ \land sum^((k \in A ⟼ B)) \in ℝ) \land sum^((k \in A ⟼ C)) \in ℝ) \to sum^((k \in A ⟼ C)) \in ℝ$
114	112 113	eqeltrrid	$⊢ ((φ \land sum^((k \in A ⟼ B)) \in ℝ) \land sum^((k \in A ⟼ C)) \in ℝ) \to sum^((j \in A ⟼ ⦋ j / k ⦌ C)) \in ℝ$
115	64 86 104 109 114	sge0xaddlem2	$⊢ ((φ \land sum^((k \in A ⟼ B)) \in ℝ) \land sum^((k \in A ⟼ C)) \in ℝ) \to sum^((j \in A ⟼ ⦋ j / k ⦌ B +_{𝑒} ⦋ j / k ⦌ C)) = sum^((j \in A ⟼ ⦋ j / k ⦌ B)) +_{𝑒} sum^((j \in A ⟼ ⦋ j / k ⦌ C))$
116		nfcv	$⊢ \underline{Ⅎ} j (B +_{𝑒} C)$
117		nfcv	$⊢ \underline{Ⅎ} k +_{𝑒}$
118	73 117 92	nfov	$⊢ \underline{Ⅎ} k (⦋ j / k ⦌ B +_{𝑒} ⦋ j / k ⦌ C)$
119	78 96	oveq12d	$⊢ k = j \to B +_{𝑒} C = ⦋ j / k ⦌ B +_{𝑒} ⦋ j / k ⦌ C$
120	116 118 119	cbvmpt	$⊢ (k \in A ⟼ B +_{𝑒} C) = (j \in A ⟼ ⦋ j / k ⦌ B +_{𝑒} ⦋ j / k ⦌ C)$
121	120	fveq2i	$⊢ sum^((k \in A ⟼ B +_{𝑒} C)) = sum^((j \in A ⟼ ⦋ j / k ⦌ B +_{𝑒} ⦋ j / k ⦌ C))$
122	107 112	oveq12i	$⊢ sum^((k \in A ⟼ B)) +_{𝑒} sum^((k \in A ⟼ C)) = sum^((j \in A ⟼ ⦋ j / k ⦌ B)) +_{𝑒} sum^((j \in A ⟼ ⦋ j / k ⦌ C))$
123	121 122	eqeq12i	$⊢ sum^((k \in A ⟼ B +_{𝑒} C)) = sum^((k \in A ⟼ B)) +_{𝑒} sum^((k \in A ⟼ C)) \leftrightarrow sum^((j \in A ⟼ ⦋ j / k ⦌ B +_{𝑒} ⦋ j / k ⦌ C)) = sum^((j \in A ⟼ ⦋ j / k ⦌ B)) +_{𝑒} sum^((j \in A ⟼ ⦋ j / k ⦌ C))$
124	115 123	sylibr	$⊢ ((φ \land sum^((k \in A ⟼ B)) \in ℝ) \land sum^((k \in A ⟼ C)) \in ℝ) \to sum^((k \in A ⟼ B +_{𝑒} C)) = sum^((k \in A ⟼ B)) +_{𝑒} sum^((k \in A ⟼ C))$
125	58 63 124	syl2anc	$⊢ ((φ \land sum^((k \in A ⟼ B)) \in ℝ) \land \neg sum^((k \in A ⟼ C)) = +∞) \to sum^((k \in A ⟼ B +_{𝑒} C)) = sum^((k \in A ⟼ B)) +_{𝑒} sum^((k \in A ⟼ C))$
126	57 125	pm2.61dan	$⊢ (φ \land sum^((k \in A ⟼ B)) \in ℝ) \to sum^((k \in A ⟼ B +_{𝑒} C)) = sum^((k \in A ⟼ B)) +_{𝑒} sum^((k \in A ⟼ C))$
127	31 37 126	syl2anc	$⊢ (φ \land \neg sum^((k \in A ⟼ B)) = +∞) \to sum^((k \in A ⟼ B +_{𝑒} C)) = sum^((k \in A ⟼ B)) +_{𝑒} sum^((k \in A ⟼ C))$
128	30 127	pm2.61dan	$⊢ φ \to sum^((k \in A ⟼ B +_{𝑒} C)) = sum^((k \in A ⟼ B)) +_{𝑒} sum^((k \in A ⟼ C))$

Metamath Proof Explorer

Theorem sge0xadd

Proof