Theorem 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	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	sge0prle.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	sge0prle.d	⊢ ( 𝜑 → 𝐷 ∈ ( 0 [,] +∞ ) )
	sge0prle.e	⊢ ( 𝜑 → 𝐸 ∈ ( 0 [,] +∞ ) )
	sge0prle.cd	⊢ ( 𝑘 = 𝐴 → 𝐶 = 𝐷 )
	sge0prle.ce	⊢ ( 𝑘 = 𝐵 → 𝐶 = 𝐸 )
Assertion	sge0prle	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ { 𝐴 , 𝐵 } ↦ 𝐶 ) ) ≤ ( 𝐷 +𝑒 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		sge0prle.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		sge0prle.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3		sge0prle.d	⊢ ( 𝜑 → 𝐷 ∈ ( 0 [,] +∞ ) )
4		sge0prle.e	⊢ ( 𝜑 → 𝐸 ∈ ( 0 [,] +∞ ) )
5		sge0prle.cd	⊢ ( 𝑘 = 𝐴 → 𝐶 = 𝐷 )
6		sge0prle.ce	⊢ ( 𝑘 = 𝐵 → 𝐶 = 𝐸 )
7		preq1	⊢ ( 𝐴 = 𝐵 → { 𝐴 , 𝐵 } = { 𝐵 , 𝐵 } )
8		dfsn2	⊢ { 𝐵 } = { 𝐵 , 𝐵 }
9	8	eqcomi	⊢ { 𝐵 , 𝐵 } = { 𝐵 }
10	9	a1i	⊢ ( 𝐴 = 𝐵 → { 𝐵 , 𝐵 } = { 𝐵 } )
11	7 10	eqtrd	⊢ ( 𝐴 = 𝐵 → { 𝐴 , 𝐵 } = { 𝐵 } )
12	11	mpteq1d	⊢ ( 𝐴 = 𝐵 → ( 𝑘 ∈ { 𝐴 , 𝐵 } ↦ 𝐶 ) = ( 𝑘 ∈ { 𝐵 } ↦ 𝐶 ) )
13	12	fveq2d	⊢ ( 𝐴 = 𝐵 → ( Σ^ ‘ ( 𝑘 ∈ { 𝐴 , 𝐵 } ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑘 ∈ { 𝐵 } ↦ 𝐶 ) ) )
14	13	adantl	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( Σ^ ‘ ( 𝑘 ∈ { 𝐴 , 𝐵 } ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑘 ∈ { 𝐵 } ↦ 𝐶 ) ) )
15	2 4 6	sge0snmpt	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ { 𝐵 } ↦ 𝐶 ) ) = 𝐸 )
16	15	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( Σ^ ‘ ( 𝑘 ∈ { 𝐵 } ↦ 𝐶 ) ) = 𝐸 )
17	14 16	eqtrd	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( Σ^ ‘ ( 𝑘 ∈ { 𝐴 , 𝐵 } ↦ 𝐶 ) ) = 𝐸 )
18		iccssxr	⊢ ( 0 [,] +∞ ) ⊆ ℝ*
19	18 4	sselid	⊢ ( 𝜑 → 𝐸 ∈ ℝ* )
20	19	xaddid2d	⊢ ( 𝜑 → ( 0 +𝑒 𝐸 ) = 𝐸 )
21	20	eqcomd	⊢ ( 𝜑 → 𝐸 = ( 0 +𝑒 𝐸 ) )
22		0xr	⊢ 0 ∈ ℝ*
23	22	a1i	⊢ ( 𝜑 → 0 ∈ ℝ* )
24	18 3	sselid	⊢ ( 𝜑 → 𝐷 ∈ ℝ* )
25		pnfxr	⊢ +∞ ∈ ℝ*
26	25	a1i	⊢ ( 𝜑 → +∞ ∈ ℝ* )
27		iccgelb	⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐷 ∈ ( 0 [,] +∞ ) ) → 0 ≤ 𝐷 )
28	23 26 3 27	syl3anc	⊢ ( 𝜑 → 0 ≤ 𝐷 )
29	23 24 19 28	xleadd1d	⊢ ( 𝜑 → ( 0 +𝑒 𝐸 ) ≤ ( 𝐷 +𝑒 𝐸 ) )
30	21 29	eqbrtrd	⊢ ( 𝜑 → 𝐸 ≤ ( 𝐷 +𝑒 𝐸 ) )
31	30	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐸 ≤ ( 𝐷 +𝑒 𝐸 ) )
32	17 31	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( Σ^ ‘ ( 𝑘 ∈ { 𝐴 , 𝐵 } ↦ 𝐶 ) ) ≤ ( 𝐷 +𝑒 𝐸 ) )
33	1	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = 𝐵 ) → 𝐴 ∈ 𝑉 )
34	2	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = 𝐵 ) → 𝐵 ∈ 𝑊 )
35	3	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = 𝐵 ) → 𝐷 ∈ ( 0 [,] +∞ ) )
36	4	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = 𝐵 ) → 𝐸 ∈ ( 0 [,] +∞ ) )
37		neqne	⊢ ( ¬ 𝐴 = 𝐵 → 𝐴 ≠ 𝐵 )
38	37	adantl	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = 𝐵 ) → 𝐴 ≠ 𝐵 )
39	33 34 35 36 5 6 38	sge0pr	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = 𝐵 ) → ( Σ^ ‘ ( 𝑘 ∈ { 𝐴 , 𝐵 } ↦ 𝐶 ) ) = ( 𝐷 +𝑒 𝐸 ) )
40	24 19	xaddcld	⊢ ( 𝜑 → ( 𝐷 +𝑒 𝐸 ) ∈ ℝ* )
41	40	xrleidd	⊢ ( 𝜑 → ( 𝐷 +𝑒 𝐸 ) ≤ ( 𝐷 +𝑒 𝐸 ) )
42	41	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = 𝐵 ) → ( 𝐷 +𝑒 𝐸 ) ≤ ( 𝐷 +𝑒 𝐸 ) )
43	39 42	eqbrtrd	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = 𝐵 ) → ( Σ^ ‘ ( 𝑘 ∈ { 𝐴 , 𝐵 } ↦ 𝐶 ) ) ≤ ( 𝐷 +𝑒 𝐸 ) )
44	32 43	pm2.61dan	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ { 𝐴 , 𝐵 } ↦ 𝐶 ) ) ≤ ( 𝐷 +𝑒 𝐸 ) )