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 ⊢φ→A∈V
sge0prle.b ⊢φ→B∈W
sge0prle.d ⊢φ→D∈0+∞
sge0prle.e ⊢φ→E∈0+∞
sge0prle.cd ⊢k=A→C=D
sge0prle.ce ⊢k=B→C=E
Assertion sge0prle ⊢φ→sum^⁡k∈AB⟼C≤D+𝑒E

Proof

Step Hyp Ref Expression
1 sge0prle.a ⊢φ→A∈V
2 sge0prle.b ⊢φ→B∈W
3 sge0prle.d ⊢φ→D∈0+∞
4 sge0prle.e ⊢φ→E∈0+∞
5 sge0prle.cd ⊢k=A→C=D
6 sge0prle.ce ⊢k=B→C=E
7 preq1 ⊢A=B→AB=BB
8 dfsn2 ⊢B=BB
9 8 eqcomi ⊢BB=B
10 9 a1i ⊢A=B→BB=B
11 7 10 eqtrd ⊢A=B→AB=B
12 11 mpteq1d ⊢A=B→k∈AB⟼C=k∈B⟼C
13 12 fveq2d ⊢A=B→sum^⁡k∈AB⟼C=sum^⁡k∈B⟼C
14 13 adantl ⊢φ∧A=B→sum^⁡k∈AB⟼C=sum^⁡k∈B⟼C
15 2 4 6 sge0snmpt ⊢φ→sum^⁡k∈B⟼C=E
16 15 adantr ⊢φ∧A=B→sum^⁡k∈B⟼C=E
17 14 16 eqtrd ⊢φ∧A=B→sum^⁡k∈AB⟼C=E
18 iccssxr ⊢0+∞⊆ℝ*
19 18 4 sselid ⊢φ→E∈ℝ*
20 19 xaddlidd ⊢φ→0+𝑒E=E
21 20 eqcomd ⊢φ→E=0+𝑒E
22 0xr ⊢0∈ℝ*
23 22 a1i ⊢φ→0∈ℝ*
24 18 3 sselid ⊢φ→D∈ℝ*
25 pnfxr ⊢+∞∈ℝ*
26 25 a1i ⊢φ→+∞∈ℝ*
27 iccgelb ⊢0∈ℝ*∧+∞∈ℝ*∧D∈0+∞→0≤D
28 23 26 3 27 syl3anc ⊢φ→0≤D
29 23 24 19 28 xleadd1d ⊢φ→0+𝑒E≤D+𝑒E
30 21 29 eqbrtrd ⊢φ→E≤D+𝑒E
31 30 adantr ⊢φ∧A=B→E≤D+𝑒E
32 17 31 eqbrtrd ⊢φ∧A=B→sum^⁡k∈AB⟼C≤D+𝑒E
33 1 adantr ⊢φ∧¬A=B→A∈V
34 2 adantr ⊢φ∧¬A=B→B∈W
35 3 adantr ⊢φ∧¬A=B→D∈0+∞
36 4 adantr ⊢φ∧¬A=B→E∈0+∞
37 neqne ⊢¬A=B→A≠B
38 37 adantl ⊢φ∧¬A=B→A≠B
39 33 34 35 36 5 6 38 sge0pr ⊢φ∧¬A=B→sum^⁡k∈AB⟼C=D+𝑒E
40 24 19 xaddcld ⊢φ→D+𝑒E∈ℝ*
41 40 xrleidd ⊢φ→D+𝑒E≤D+𝑒E
42 41 adantr ⊢φ∧¬A=B→D+𝑒E≤D+𝑒E
43 39 42 eqbrtrd ⊢φ∧¬A=B→sum^⁡k∈AB⟼C≤D+𝑒E
44 32 43 pm2.61dan ⊢φ→sum^⁡k∈AB⟼C≤D+𝑒E