Metamath Proof Explorer

Theorem isumless

Description: A finite sum of nonnegative numbers is less than or equal to its limit. (Contributed by Mario Carneiro, 24-Apr-2014)

Ref Expression
Hypotheses isumless.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
isumless.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
isumless.3 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
isumless.4 ⊢ ( 𝜑 → 𝐴 ⊆ 𝑍 )
isumless.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐵 )
isumless.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
isumless.7 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 0 ≤ 𝐵 )
isumless.8 ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
Assertion isumless ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 ≤ Σ 𝑘 ∈ 𝑍 𝐵 )

Proof

Step Hyp Ref Expression
1 isumless.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 isumless.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 isumless.3 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
4 isumless.4 ⊢ ( 𝜑 → 𝐴 ⊆ 𝑍 )
5 isumless.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐵 )
6 isumless.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
7 isumless.7 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 0 ≤ 𝐵 )
8 isumless.8 ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
9 4 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑘 ∈ 𝑍 )
10 6 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℂ )
11 9 10 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
12 11 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℂ )
13 1 eqimssi ⊢ 𝑍 ⊆ ( ℤ≥ ‘ 𝑀 )
14 13 orci ⊢ ( 𝑍 ⊆ ( ℤ≥ ‘ 𝑀 ) ∨ 𝑍 ∈ Fin )
15 14 a1i ⊢ ( 𝜑 → ( 𝑍 ⊆ ( ℤ≥ ‘ 𝑀 ) ∨ 𝑍 ∈ Fin ) )
16 sumss2 ⊢ ( ( ( 𝐴 ⊆ 𝑍 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℂ ) ∧ ( 𝑍 ⊆ ( ℤ≥ ‘ 𝑀 ) ∨ 𝑍 ∈ Fin ) ) → Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑘 ∈ 𝑍 if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) )
17 4 12 15 16 syl21anc ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑘 ∈ 𝑍 if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) )
18 eleq1w ⊢ ( 𝑗 = 𝑘 → ( 𝑗 ∈ 𝐴 ↔ 𝑘 ∈ 𝐴 ) )
19 fveq2 ⊢ ( 𝑗 = 𝑘 → ( 𝐹 ‘ 𝑗 ) = ( 𝐹 ‘ 𝑘 ) )
20 18 19 ifbieq1d ⊢ ( 𝑗 = 𝑘 → if ( 𝑗 ∈ 𝐴 , ( 𝐹 ‘ 𝑗 ) , 0 ) = if ( 𝑘 ∈ 𝐴 , ( 𝐹 ‘ 𝑘 ) , 0 ) )
21 eqid ⊢ ( 𝑗 ∈ 𝑍 ↦ if ( 𝑗 ∈ 𝐴 , ( 𝐹 ‘ 𝑗 ) , 0 ) ) = ( 𝑗 ∈ 𝑍 ↦ if ( 𝑗 ∈ 𝐴 , ( 𝐹 ‘ 𝑗 ) , 0 ) )
22 fvex ⊢ ( 𝐹 ‘ 𝑘 ) ∈ V
23 c0ex ⊢ 0 ∈ V
24 22 23 ifex ⊢ if ( 𝑘 ∈ 𝐴 , ( 𝐹 ‘ 𝑘 ) , 0 ) ∈ V
25 20 21 24 fvmpt ⊢ ( 𝑘 ∈ 𝑍 → ( ( 𝑗 ∈ 𝑍 ↦ if ( 𝑗 ∈ 𝐴 , ( 𝐹 ‘ 𝑗 ) , 0 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐴 , ( 𝐹 ‘ 𝑘 ) , 0 ) )
26 25 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑗 ∈ 𝑍 ↦ if ( 𝑗 ∈ 𝐴 , ( 𝐹 ‘ 𝑗 ) , 0 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐴 , ( 𝐹 ‘ 𝑘 ) , 0 ) )
27 5 ifeq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → if ( 𝑘 ∈ 𝐴 , ( 𝐹 ‘ 𝑘 ) , 0 ) = if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) )
28 26 27 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑗 ∈ 𝑍 ↦ if ( 𝑗 ∈ 𝐴 , ( 𝐹 ‘ 𝑗 ) , 0 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) )
29 0re ⊢ 0 ∈ ℝ
30 ifcl ⊢ ( ( 𝐵 ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ∈ ℝ )
31 6 29 30 sylancl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ∈ ℝ )
32 leid ⊢ ( 𝐵 ∈ ℝ → 𝐵 ≤ 𝐵 )
33 breq1 ⊢ ( 𝐵 = if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) → ( 𝐵 ≤ 𝐵 ↔ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ≤ 𝐵 ) )
34 breq1 ⊢ ( 0 = if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) → ( 0 ≤ 𝐵 ↔ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ≤ 𝐵 ) )
35 33 34 ifboth ⊢ ( ( 𝐵 ≤ 𝐵 ∧ 0 ≤ 𝐵 ) → if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ≤ 𝐵 )
36 32 35 sylan ⊢ ( ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) → if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ≤ 𝐵 )
37 6 7 36 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ≤ 𝐵 )
38 1 2 3 4 28 11 fsumcvg3 ⊢ ( 𝜑 → seq 𝑀 ( + , ( 𝑗 ∈ 𝑍 ↦ if ( 𝑗 ∈ 𝐴 , ( 𝐹 ‘ 𝑗 ) , 0 ) ) ) ∈ dom ⇝ )
39 1 2 28 31 5 6 37 38 8 isumle ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑍 if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ≤ Σ 𝑘 ∈ 𝑍 𝐵 )
40 17 39 eqbrtrd ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 ≤ Σ 𝑘 ∈ 𝑍 𝐵 )