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 ( 𝜑 → Σ* 𝑘𝐴 𝐵 ≤ Σ* 𝑘𝐴 𝐶 )