Metamath Proof Explorer

Theorem esumlef

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 esumaddf.0 ⊢ Ⅎ 𝑘 𝜑
esumaddf.a ⊢ Ⅎ 𝑘 𝐴
esumaddf.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
esumaddf.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
esumaddf.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
esumlef.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ≤ 𝐶 )
Assertion esumlef ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 ≤ Σ* 𝑘 ∈ 𝐴 𝐶 )

Proof

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