sge0prle

Description: The sum of a pair of nonnegative extended reals is less than or equal their extended addition. When it is a distinct pair, than equality holds, see sge0pr . (Contributed by Glauco Siliprandi, 17-Aug-2020)

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

Proof

Step	Hyp	Ref	Expression
1		sge0prle.a	$⊢ φ \to A \in V$
2		sge0prle.b	$⊢ φ \to B \in W$
3		sge0prle.d	$⊢ φ \to D \in [0, +∞]$
4		sge0prle.e	$⊢ φ \to E \in [0, +∞]$
5		sge0prle.cd	$⊢ k = A \to C = D$
6		sge0prle.ce	$⊢ k = B \to C = E$
7		preq1	$⊢ A = B \to \{A, B\} = \{B, B\}$
8		dfsn2	$⊢ \{B\} = \{B, B\}$
9	8	eqcomi	$⊢ \{B, B\} = \{B\}$
10	9	a1i	$⊢ A = B \to \{B, B\} = \{B\}$
11	7 10	eqtrd	$⊢ A = B \to \{A, B\} = \{B\}$
12	11	mpteq1d	$⊢ A = B \to (k \in \{A, B\} ⟼ C) = (k \in \{B\} ⟼ C)$
13	12	fveq2d	$⊢ A = B \to sum^((k \in \{A, B\} ⟼ C)) = sum^((k \in \{B\} ⟼ C))$
14	13	adantl	$⊢ (φ \land A = B) \to sum^((k \in \{A, B\} ⟼ C)) = sum^((k \in \{B\} ⟼ C))$
15	2 4 6	sge0snmpt	$⊢ φ \to sum^((k \in \{B\} ⟼ C)) = E$
16	15	adantr	$⊢ (φ \land A = B) \to sum^((k \in \{B\} ⟼ C)) = E$
17	14 16	eqtrd	$⊢ (φ \land A = B) \to sum^((k \in \{A, B\} ⟼ C)) = E$
18		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
19	18 4	sselid	$⊢ φ \to E \in ℝ^{*}$
20	19	xaddid2d	$⊢ φ \to 0 +_{𝑒} E = E$
21	20	eqcomd	$⊢ φ \to E = 0 +_{𝑒} E$
22		0xr	$⊢ 0 \in ℝ^{*}$
23	22	a1i	$⊢ φ \to 0 \in ℝ^{*}$
24	18 3	sselid	$⊢ φ \to D \in ℝ^{*}$
25		pnfxr	$⊢ +∞ \in ℝ^{*}$
26	25	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
27		iccgelb	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{} \land D \in [0, +∞]) \to 0 \leq D$
28	23 26 3 27	syl3anc	$⊢ φ \to 0 \leq D$
29	23 24 19 28	xleadd1d	$⊢ φ \to 0 +_{𝑒} E \leq D +_{𝑒} E$
30	21 29	eqbrtrd	$⊢ φ \to E \leq D +_{𝑒} E$
31	30	adantr	$⊢ (φ \land A = B) \to E \leq D +_{𝑒} E$
32	17 31	eqbrtrd	$⊢ (φ \land A = B) \to sum^((k \in \{A, B\} ⟼ C)) \leq D +_{𝑒} E$
33	1	adantr	$⊢ (φ \land \neg A = B) \to A \in V$
34	2	adantr	$⊢ (φ \land \neg A = B) \to B \in W$
35	3	adantr	$⊢ (φ \land \neg A = B) \to D \in [0, +∞]$
36	4	adantr	$⊢ (φ \land \neg A = B) \to E \in [0, +∞]$
37		neqne	$⊢ \neg A = B \to A \neq B$
38	37	adantl	$⊢ (φ \land \neg A = B) \to A \neq B$
39	33 34 35 36 5 6 38	sge0pr	$⊢ (φ \land \neg A = B) \to sum^((k \in \{A, B\} ⟼ C)) = D +_{𝑒} E$
40	24 19	xaddcld	$⊢ φ \to D +_{𝑒} E \in ℝ^{*}$
41	40	xrleidd	$⊢ φ \to D +_{𝑒} E \leq D +_{𝑒} E$
42	41	adantr	$⊢ (φ \land \neg A = B) \to D +_{𝑒} E \leq D +_{𝑒} E$
43	39 42	eqbrtrd	$⊢ (φ \land \neg A = B) \to sum^((k \in \{A, B\} ⟼ C)) \leq D +_{𝑒} E$
44	32 43	pm2.61dan	$⊢ φ \to sum^((k \in \{A, B\} ⟼ C)) \leq D +_{𝑒} E$

Metamath Proof Explorer

Theorem sge0prle

Proof