sge0pr

Description: Sum of a pair of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0pr.a	$⊢ φ \to A \in V$
	sge0pr.b	$⊢ φ \to B \in W$
	sge0pr.d	$⊢ φ \to D \in [0, +∞]$
	sge0pr.e	$⊢ φ \to E \in [0, +∞]$
	sge0pr.cd	$⊢ k = A \to C = D$
	sge0pr.ce	$⊢ k = B \to C = E$
	sge0pr.ab	$⊢ φ \to A \neq B$
Assertion	sge0pr	$⊢ φ \to sum^((k \in \{A, B\} ⟼ C)) = D +_{𝑒} E$

Proof

Step	Hyp	Ref	Expression
1		sge0pr.a	$⊢ φ \to A \in V$
2		sge0pr.b	$⊢ φ \to B \in W$
3		sge0pr.d	$⊢ φ \to D \in [0, +∞]$
4		sge0pr.e	$⊢ φ \to E \in [0, +∞]$
5		sge0pr.cd	$⊢ k = A \to C = D$
6		sge0pr.ce	$⊢ k = B \to C = E$
7		sge0pr.ab	$⊢ φ \to A \neq B$
8		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
9	8 4	sselid	$⊢ φ \to E \in ℝ^{*}$
10		mnfxr	$⊢ −∞ \in ℝ^{*}$
11	10	a1i	$⊢ φ \to −∞ \in ℝ^{*}$
12		0xr	$⊢ 0 \in ℝ^{*}$
13	12	a1i	$⊢ φ \to 0 \in ℝ^{*}$
14		mnflt0	$⊢ −∞ < 0$
15	14	a1i	$⊢ φ \to −∞ < 0$
16		pnfxr	$⊢ +∞ \in ℝ^{*}$
17	16	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
18		iccgelb	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{} \land E \in [0, +∞]) \to 0 \leq E$
19	13 17 4 18	syl3anc	$⊢ φ \to 0 \leq E$
20	11 13 9 15 19	xrltletrd	$⊢ φ \to −∞ < E$
21	11 9 20	xrgtned	$⊢ φ \to E \neq −∞$
22		xaddpnf2	$⊢ (E \in ℝ^{*} \land E \neq −∞) \to +∞ +_{𝑒} E = +∞$
23	9 21 22	syl2anc	$⊢ φ \to +∞ +_{𝑒} E = +∞$
24	23	eqcomd	$⊢ φ \to +∞ = +∞ +_{𝑒} E$
25	24	adantr	$⊢ (φ \land D = +∞) \to +∞ = +∞ +_{𝑒} E$
26		prex	$⊢ \{A, B\} \in V$
27	26	a1i	$⊢ (φ \land D = +∞) \to \{A, B\} \in V$
28	5	adantl	$⊢ (φ \land k = A) \to C = D$
29	3	adantr	$⊢ (φ \land k = A) \to D \in [0, +∞]$
30	28 29	eqeltrd	$⊢ (φ \land k = A) \to C \in [0, +∞]$
31	30	adantlr	$⊢ ((φ \land k \in \{A, B\}) \land k = A) \to C \in [0, +∞]$
32		simpll	$⊢ ((φ \land k \in \{A, B\}) \land \neg k = A) \to φ$
33		simpl	$⊢ (k \in \{A, B\} \land \neg k = A) \to k \in \{A, B\}$
34		neqne	$⊢ \neg k = A \to k \neq A$
35	34	adantl	$⊢ (k \in \{A, B\} \land \neg k = A) \to k \neq A$
36		elprn1	$⊢ (k \in \{A, B\} \land k \neq A) \to k = B$
37	33 35 36	syl2anc	$⊢ (k \in \{A, B\} \land \neg k = A) \to k = B$
38	37	adantll	$⊢ ((φ \land k \in \{A, B\}) \land \neg k = A) \to k = B$
39	6	adantl	$⊢ (φ \land k = B) \to C = E$
40	4	adantr	$⊢ (φ \land k = B) \to E \in [0, +∞]$
41	39 40	eqeltrd	$⊢ (φ \land k = B) \to C \in [0, +∞]$
42	32 38 41	syl2anc	$⊢ ((φ \land k \in \{A, B\}) \land \neg k = A) \to C \in [0, +∞]$
43	31 42	pm2.61dan	$⊢ (φ \land k \in \{A, B\}) \to C \in [0, +∞]$
44		eqid	$⊢ (k \in \{A, B\} ⟼ C) = (k \in \{A, B\} ⟼ C)$
45	43 44	fmptd	$⊢ φ \to (k \in \{A, B\} ⟼ C) : \{A, B\} ⟶ [0, +∞]$
46	45	adantr	$⊢ (φ \land D = +∞) \to (k \in \{A, B\} ⟼ C) : \{A, B\} ⟶ [0, +∞]$
47		id	$⊢ D = +∞ \to D = +∞$
48	47	eqcomd	$⊢ D = +∞ \to +∞ = D$
49	48	adantl	$⊢ (φ \land D = +∞) \to +∞ = D$
50		prid1g	$⊢ D \in [0, +∞] \to D \in \{D, E\}$
51	3 50	syl	$⊢ φ \to D \in \{D, E\}$
52	1 2 44 5 6	rnmptpr	$⊢ φ \to ran (k \in \{A, B\} ⟼ C) = \{D, E\}$
53	52	eqcomd	$⊢ φ \to \{D, E\} = ran (k \in \{A, B\} ⟼ C)$
54	51 53	eleqtrd	$⊢ φ \to D \in ran (k \in \{A, B\} ⟼ C)$
55	54	adantr	$⊢ (φ \land D = +∞) \to D \in ran (k \in \{A, B\} ⟼ C)$
56	49 55	eqeltrd	$⊢ (φ \land D = +∞) \to +∞ \in ran (k \in \{A, B\} ⟼ C)$
57	27 46 56	sge0pnfval	$⊢ (φ \land D = +∞) \to sum^((k \in \{A, B\} ⟼ C)) = +∞$
58		oveq1	$⊢ D = +∞ \to D +_{𝑒} E = +∞ +_{𝑒} E$
59	58	adantl	$⊢ (φ \land D = +∞) \to D +_{𝑒} E = +∞ +_{𝑒} E$
60	25 57 59	3eqtr4d	$⊢ (φ \land D = +∞) \to sum^((k \in \{A, B\} ⟼ C)) = D +_{𝑒} E$
61	8 3	sselid	$⊢ φ \to D \in ℝ^{*}$
62		iccgelb	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{} \land D \in [0, +∞]) \to 0 \leq D$
63	13 17 3 62	syl3anc	$⊢ φ \to 0 \leq D$
64	11 13 61 15 63	xrltletrd	$⊢ φ \to −∞ < D$
65	11 61 64	xrgtned	$⊢ φ \to D \neq −∞$
66		xaddpnf1	$⊢ (D \in ℝ^{*} \land D \neq −∞) \to D +_{𝑒} +∞ = +∞$
67	61 65 66	syl2anc	$⊢ φ \to D +_{𝑒} +∞ = +∞$
68	67	eqcomd	$⊢ φ \to +∞ = D +_{𝑒} +∞$
69	68	adantr	$⊢ (φ \land E = +∞) \to +∞ = D +_{𝑒} +∞$
70	26	a1i	$⊢ (φ \land E = +∞) \to \{A, B\} \in V$
71	45	adantr	$⊢ (φ \land E = +∞) \to (k \in \{A, B\} ⟼ C) : \{A, B\} ⟶ [0, +∞]$
72		id	$⊢ E = +∞ \to E = +∞$
73	72	eqcomd	$⊢ E = +∞ \to +∞ = E$
74	73	adantl	$⊢ (φ \land E = +∞) \to +∞ = E$
75		prid2g	$⊢ E \in [0, +∞] \to E \in \{D, E\}$
76	4 75	syl	$⊢ φ \to E \in \{D, E\}$
77	76 53	eleqtrd	$⊢ φ \to E \in ran (k \in \{A, B\} ⟼ C)$
78	77	adantr	$⊢ (φ \land E = +∞) \to E \in ran (k \in \{A, B\} ⟼ C)$
79	74 78	eqeltrd	$⊢ (φ \land E = +∞) \to +∞ \in ran (k \in \{A, B\} ⟼ C)$
80	70 71 79	sge0pnfval	$⊢ (φ \land E = +∞) \to sum^((k \in \{A, B\} ⟼ C)) = +∞$
81		oveq2	$⊢ E = +∞ \to D +_{𝑒} E = D +_{𝑒} +∞$
82	81	adantl	$⊢ (φ \land E = +∞) \to D +_{𝑒} E = D +_{𝑒} +∞$
83	69 80 82	3eqtr4d	$⊢ (φ \land E = +∞) \to sum^((k \in \{A, B\} ⟼ C)) = D +_{𝑒} E$
84	83	adantlr	$⊢ ((φ \land \neg D = +∞) \land E = +∞) \to sum^((k \in \{A, B\} ⟼ C)) = D +_{𝑒} E$
85		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
86		ax-resscn	$⊢ ℝ \subseteq ℂ$
87	85 86	sstri	$⊢ [0, +∞) \subseteq ℂ$
88	12	a1i	$⊢ (φ \land \neg D = +∞) \to 0 \in ℝ^{*}$
89	16	a1i	$⊢ (φ \land \neg D = +∞) \to +∞ \in ℝ^{*}$
90	61	adantr	$⊢ (φ \land \neg D = +∞) \to D \in ℝ^{*}$
91	63	adantr	$⊢ (φ \land \neg D = +∞) \to 0 \leq D$
92		pnfge	$⊢ D \in ℝ^{*} \to D \leq +∞$
93	61 92	syl	$⊢ φ \to D \leq +∞$
94	93	adantr	$⊢ (φ \land \neg D = +∞) \to D \leq +∞$
95	47	necon3bi	$⊢ \neg D = +∞ \to D \neq +∞$
96	95	adantl	$⊢ (φ \land \neg D = +∞) \to D \neq +∞$
97	90 89 94 96	xrleneltd	$⊢ (φ \land \neg D = +∞) \to D < +∞$
98	88 89 90 91 97	elicod	$⊢ (φ \land \neg D = +∞) \to D \in [0, +∞)$
99	98	adantr	$⊢ ((φ \land \neg D = +∞) \land \neg E = +∞) \to D \in [0, +∞)$
100	87 99	sselid	$⊢ ((φ \land \neg D = +∞) \land \neg E = +∞) \to D \in ℂ$
101	12	a1i	$⊢ (φ \land \neg E = +∞) \to 0 \in ℝ^{*}$
102	16	a1i	$⊢ (φ \land \neg E = +∞) \to +∞ \in ℝ^{*}$
103	9	adantr	$⊢ (φ \land \neg E = +∞) \to E \in ℝ^{*}$
104	19	adantr	$⊢ (φ \land \neg E = +∞) \to 0 \leq E$
105		pnfge	$⊢ E \in ℝ^{*} \to E \leq +∞$
106	9 105	syl	$⊢ φ \to E \leq +∞$
107	106	adantr	$⊢ (φ \land \neg E = +∞) \to E \leq +∞$
108	72	necon3bi	$⊢ \neg E = +∞ \to E \neq +∞$
109	108	adantl	$⊢ (φ \land \neg E = +∞) \to E \neq +∞$
110	103 102 107 109	xrleneltd	$⊢ (φ \land \neg E = +∞) \to E < +∞$
111	101 102 103 104 110	elicod	$⊢ (φ \land \neg E = +∞) \to E \in [0, +∞)$
112	87 111	sselid	$⊢ (φ \land \neg E = +∞) \to E \in ℂ$
113	112	adantlr	$⊢ ((φ \land \neg D = +∞) \land \neg E = +∞) \to E \in ℂ$
114	100 113	jca	$⊢ ((φ \land \neg D = +∞) \land \neg E = +∞) \to (D \in ℂ \land E \in ℂ)$
115	1 2	jca	$⊢ φ \to (A \in V \land B \in W)$
116	115	ad2antrr	$⊢ ((φ \land \neg D = +∞) \land \neg E = +∞) \to (A \in V \land B \in W)$
117	7	ad2antrr	$⊢ ((φ \land \neg D = +∞) \land \neg E = +∞) \to A \neq B$
118	5 6 114 116 117	sumpr	$⊢ ((φ \land \neg D = +∞) \land \neg E = +∞) \to \sum_{k \in \{A, B\}} C = D + E$
119		prfi	$⊢ \{A, B\} \in Fin$
120	119	a1i	$⊢ ((φ \land \neg D = +∞) \land \neg E = +∞) \to \{A, B\} \in Fin$
121	5	adantl	$⊢ ((φ \land \neg D = +∞) \land k = A) \to C = D$
122	98	adantr	$⊢ ((φ \land \neg D = +∞) \land k = A) \to D \in [0, +∞)$
123	121 122	eqeltrd	$⊢ ((φ \land \neg D = +∞) \land k = A) \to C \in [0, +∞)$
124	123	ad4ant14	$⊢ ((((φ \land \neg D = +∞) \land \neg E = +∞) \land k \in \{A, B\}) \land k = A) \to C \in [0, +∞)$
125		simp-4l	$⊢ ((((φ \land \neg D = +∞) \land \neg E = +∞) \land k \in \{A, B\}) \land \neg k = A) \to φ$
126		simpllr	$⊢ ((((φ \land \neg D = +∞) \land \neg E = +∞) \land k \in \{A, B\}) \land \neg k = A) \to \neg E = +∞$
127	37	adantll	$⊢ ((((φ \land \neg D = +∞) \land \neg E = +∞) \land k \in \{A, B\}) \land \neg k = A) \to k = B$
128	39	3adant2	$⊢ (φ \land \neg E = +∞ \land k = B) \to C = E$
129	111	3adant3	$⊢ (φ \land \neg E = +∞ \land k = B) \to E \in [0, +∞)$
130	128 129	eqeltrd	$⊢ (φ \land \neg E = +∞ \land k = B) \to C \in [0, +∞)$
131	125 126 127 130	syl3anc	$⊢ ((((φ \land \neg D = +∞) \land \neg E = +∞) \land k \in \{A, B\}) \land \neg k = A) \to C \in [0, +∞)$
132	124 131	pm2.61dan	$⊢ (((φ \land \neg D = +∞) \land \neg E = +∞) \land k \in \{A, B\}) \to C \in [0, +∞)$
133	120 132	sge0fsummpt	$⊢ ((φ \land \neg D = +∞) \land \neg E = +∞) \to sum^((k \in \{A, B\} ⟼ C)) = \sum_{k \in \{A, B\}} C$
134	85 99	sselid	$⊢ ((φ \land \neg D = +∞) \land \neg E = +∞) \to D \in ℝ$
135	85 111	sselid	$⊢ (φ \land \neg E = +∞) \to E \in ℝ$
136	135	adantlr	$⊢ ((φ \land \neg D = +∞) \land \neg E = +∞) \to E \in ℝ$
137		rexadd	$⊢ (D \in ℝ \land E \in ℝ) \to D +_{𝑒} E = D + E$
138	134 136 137	syl2anc	$⊢ ((φ \land \neg D = +∞) \land \neg E = +∞) \to D +_{𝑒} E = D + E$
139	118 133 138	3eqtr4d	$⊢ ((φ \land \neg D = +∞) \land \neg E = +∞) \to sum^((k \in \{A, B\} ⟼ C)) = D +_{𝑒} E$
140	84 139	pm2.61dan	$⊢ (φ \land \neg D = +∞) \to sum^((k \in \{A, B\} ⟼ C)) = D +_{𝑒} E$
141	60 140	pm2.61dan	$⊢ φ \to sum^((k \in \{A, B\} ⟼ C)) = D +_{𝑒} E$

Metamath Proof Explorer

Theorem sge0pr

Proof