Metamath Proof Explorer


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 sseldi ( 𝜑𝐸 ∈ ℝ* )
20 19 xaddid2d ( 𝜑 → ( 0 +𝑒 𝐸 ) = 𝐸 )
21 20 eqcomd ( 𝜑𝐸 = ( 0 +𝑒 𝐸 ) )
22 0xr 0 ∈ ℝ*
23 22 a1i ( 𝜑 → 0 ∈ ℝ* )
24 18 3 sseldi ( 𝜑𝐷 ∈ ℝ* )
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 ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ { 𝐴 , 𝐵 } ↦ 𝐶 ) ) ≤ ( 𝐷 +𝑒 𝐸 ) )