Metamath Proof Explorer

Theorem esumle

Description: If all of the terms of an extended sums compare, so do the sums. (Contributed by Thierry Arnoux, 8-Jun-2017)

Ref Expression
Hypotheses esumadd.0 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
esumadd.1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
esumadd.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
esumle.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ≤ 𝐶 )
Assertion esumle ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 ≤ Σ* 𝑘 ∈ 𝐴 𝐶 )

Proof

Step Hyp Ref Expression
1 esumadd.0 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 esumadd.1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
3 esumadd.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
4 esumle.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ≤ 𝐶 )
5 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
6 2 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) )
7 nfcv ⊢ Ⅎ 𝑘 𝐴
8 7 esumcl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) )
9 1 6 8 syl2anc ⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) )
10 5 9 sselid ⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 ∈ ℝ* )
11 5 3 sselid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℝ* )
12 5 2 sselid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
13 12 xnegcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → -𝑒 𝐵 ∈ ℝ* )
14 11 13 xaddcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐶 +𝑒 -𝑒 𝐵 ) ∈ ℝ* )
15 xsubge0 ⊢ ( ( 𝐶 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 0 ≤ ( 𝐶 +𝑒 -𝑒 𝐵 ) ↔ 𝐵 ≤ 𝐶 ) )
16 11 12 15 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 0 ≤ ( 𝐶 +𝑒 -𝑒 𝐵 ) ↔ 𝐵 ≤ 𝐶 ) )
17 4 16 mpbird ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 0 ≤ ( 𝐶 +𝑒 -𝑒 𝐵 ) )
18 pnfge ⊢ ( ( 𝐶 +𝑒 -𝑒 𝐵 ) ∈ ℝ* → ( 𝐶 +𝑒 -𝑒 𝐵 ) ≤ +∞ )
19 14 18 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐶 +𝑒 -𝑒 𝐵 ) ≤ +∞ )
20 0xr ⊢ 0 ∈ ℝ*
21 pnfxr ⊢ +∞ ∈ ℝ*
22 elicc1 ⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( ( 𝐶 +𝑒 -𝑒 𝐵 ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝐶 +𝑒 -𝑒 𝐵 ) ∈ ℝ* ∧ 0 ≤ ( 𝐶 +𝑒 -𝑒 𝐵 ) ∧ ( 𝐶 +𝑒 -𝑒 𝐵 ) ≤ +∞ ) ) )
23 20 21 22 mp2an ⊢ ( ( 𝐶 +𝑒 -𝑒 𝐵 ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝐶 +𝑒 -𝑒 𝐵 ) ∈ ℝ* ∧ 0 ≤ ( 𝐶 +𝑒 -𝑒 𝐵 ) ∧ ( 𝐶 +𝑒 -𝑒 𝐵 ) ≤ +∞ ) )
24 14 17 19 23 syl3anbrc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐶 +𝑒 -𝑒 𝐵 ) ∈ ( 0 [,] +∞ ) )
25 24 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 ( 𝐶 +𝑒 -𝑒 𝐵 ) ∈ ( 0 [,] +∞ ) )
26 7 esumcl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝐶 +𝑒 -𝑒 𝐵 ) ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘 ∈ 𝐴 ( 𝐶 +𝑒 -𝑒 𝐵 ) ∈ ( 0 [,] +∞ ) )
27 1 25 26 syl2anc ⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 ( 𝐶 +𝑒 -𝑒 𝐵 ) ∈ ( 0 [,] +∞ ) )
28 5 27 sselid ⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 ( 𝐶 +𝑒 -𝑒 𝐵 ) ∈ ℝ* )
29 20 a1i ⊢ ( 𝜑 → 0 ∈ ℝ* )
30 21 a1i ⊢ ( 𝜑 → +∞ ∈ ℝ* )
31 elicc4 ⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ Σ* 𝑘 ∈ 𝐴 ( 𝐶 +𝑒 -𝑒 𝐵 ) ∈ ℝ* ) → ( Σ* 𝑘 ∈ 𝐴 ( 𝐶 +𝑒 -𝑒 𝐵 ) ∈ ( 0 [,] +∞ ) ↔ ( 0 ≤ Σ* 𝑘 ∈ 𝐴 ( 𝐶 +𝑒 -𝑒 𝐵 ) ∧ Σ* 𝑘 ∈ 𝐴 ( 𝐶 +𝑒 -𝑒 𝐵 ) ≤ +∞ ) ) )
32 29 30 28 31 syl3anc ⊢ ( 𝜑 → ( Σ* 𝑘 ∈ 𝐴 ( 𝐶 +𝑒 -𝑒 𝐵 ) ∈ ( 0 [,] +∞ ) ↔ ( 0 ≤ Σ* 𝑘 ∈ 𝐴 ( 𝐶 +𝑒 -𝑒 𝐵 ) ∧ Σ* 𝑘 ∈ 𝐴 ( 𝐶 +𝑒 -𝑒 𝐵 ) ≤ +∞ ) ) )
33 27 32 mpbid ⊢ ( 𝜑 → ( 0 ≤ Σ* 𝑘 ∈ 𝐴 ( 𝐶 +𝑒 -𝑒 𝐵 ) ∧ Σ* 𝑘 ∈ 𝐴 ( 𝐶 +𝑒 -𝑒 𝐵 ) ≤ +∞ ) )
34 33 simpld ⊢ ( 𝜑 → 0 ≤ Σ* 𝑘 ∈ 𝐴 ( 𝐶 +𝑒 -𝑒 𝐵 ) )
35 xraddge02 ⊢ ( ( Σ* 𝑘 ∈ 𝐴 𝐵 ∈ ℝ* ∧ Σ* 𝑘 ∈ 𝐴 ( 𝐶 +𝑒 -𝑒 𝐵 ) ∈ ℝ* ) → ( 0 ≤ Σ* 𝑘 ∈ 𝐴 ( 𝐶 +𝑒 -𝑒 𝐵 ) → Σ* 𝑘 ∈ 𝐴 𝐵 ≤ ( Σ* 𝑘 ∈ 𝐴 𝐵 +𝑒 Σ* 𝑘 ∈ 𝐴 ( 𝐶 +𝑒 -𝑒 𝐵 ) ) ) )
36 35 imp ⊢ ( ( ( Σ* 𝑘 ∈ 𝐴 𝐵 ∈ ℝ* ∧ Σ* 𝑘 ∈ 𝐴 ( 𝐶 +𝑒 -𝑒 𝐵 ) ∈ ℝ* ) ∧ 0 ≤ Σ* 𝑘 ∈ 𝐴 ( 𝐶 +𝑒 -𝑒 𝐵 ) ) → Σ* 𝑘 ∈ 𝐴 𝐵 ≤ ( Σ* 𝑘 ∈ 𝐴 𝐵 +𝑒 Σ* 𝑘 ∈ 𝐴 ( 𝐶 +𝑒 -𝑒 𝐵 ) ) )
37 10 28 34 36 syl21anc ⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 ≤ ( Σ* 𝑘 ∈ 𝐴 𝐵 +𝑒 Σ* 𝑘 ∈ 𝐴 ( 𝐶 +𝑒 -𝑒 𝐵 ) ) )
38 xaddcom ⊢ ( ( Σ* 𝑘 ∈ 𝐴 𝐵 ∈ ℝ* ∧ Σ* 𝑘 ∈ 𝐴 ( 𝐶 +𝑒 -𝑒 𝐵 ) ∈ ℝ* ) → ( Σ* 𝑘 ∈ 𝐴 𝐵 +𝑒 Σ* 𝑘 ∈ 𝐴 ( 𝐶 +𝑒 -𝑒 𝐵 ) ) = ( Σ* 𝑘 ∈ 𝐴 ( 𝐶 +𝑒 -𝑒 𝐵 ) +𝑒 Σ* 𝑘 ∈ 𝐴 𝐵 ) )
39 10 28 38 syl2anc ⊢ ( 𝜑 → ( Σ* 𝑘 ∈ 𝐴 𝐵 +𝑒 Σ* 𝑘 ∈ 𝐴 ( 𝐶 +𝑒 -𝑒 𝐵 ) ) = ( Σ* 𝑘 ∈ 𝐴 ( 𝐶 +𝑒 -𝑒 𝐵 ) +𝑒 Σ* 𝑘 ∈ 𝐴 𝐵 ) )
40 37 39 breqtrd ⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 ≤ ( Σ* 𝑘 ∈ 𝐴 ( 𝐶 +𝑒 -𝑒 𝐵 ) +𝑒 Σ* 𝑘 ∈ 𝐴 𝐵 ) )
41 1 24 2 esumadd ⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 ( ( 𝐶 +𝑒 -𝑒 𝐵 ) +𝑒 𝐵 ) = ( Σ* 𝑘 ∈ 𝐴 ( 𝐶 +𝑒 -𝑒 𝐵 ) +𝑒 Σ* 𝑘 ∈ 𝐴 𝐵 ) )
42 xrge0npcan ⊢ ( ( 𝐶 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ≤ 𝐶 ) → ( ( 𝐶 +𝑒 -𝑒 𝐵 ) +𝑒 𝐵 ) = 𝐶 )
43 3 2 4 42 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝐶 +𝑒 -𝑒 𝐵 ) +𝑒 𝐵 ) = 𝐶 )
44 43 esumeq2dv ⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 ( ( 𝐶 +𝑒 -𝑒 𝐵 ) +𝑒 𝐵 ) = Σ* 𝑘 ∈ 𝐴 𝐶 )
45 41 44 eqtr3d ⊢ ( 𝜑 → ( Σ* 𝑘 ∈ 𝐴 ( 𝐶 +𝑒 -𝑒 𝐵 ) +𝑒 Σ* 𝑘 ∈ 𝐴 𝐵 ) = Σ* 𝑘 ∈ 𝐴 𝐶 )
46 40 45 breqtrd ⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 ≤ Σ* 𝑘 ∈ 𝐴 𝐶 )