Metamath Proof Explorer

Theorem sge0rnbnd

Description: The range used in the definition of sum^ is bounded, when the whole sum is a real number. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0rnbnd.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
sge0rnbnd.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
sge0rnbnd.re ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) ∈ ℝ )
Assertion sge0rnbnd ( 𝜑 → ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) 𝑤 ≤ 𝑧 )

Proof

Step Hyp Ref Expression
1 sge0rnbnd.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
2 sge0rnbnd.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
3 sge0rnbnd.re ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) ∈ ℝ )
4 simpl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) → 𝜑 )
5 vex ⊢ 𝑤 ∈ V
6 eqid ⊢ ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) = ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
7 6 elrnmpt ⊢ ( 𝑤 ∈ V → ( 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑤 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) )
8 5 7 ax-mp ⊢ ( 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑤 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
9 8 bilani ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) → ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑤 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
10 simp3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑤 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → 𝑤 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
11 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝑋 ∈ 𝑉 )
12 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
13 1 2 3 sge0rern ⊢ ( 𝜑 → ¬ +∞ ∈ ran 𝐹 )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ¬ +∞ ∈ ran 𝐹 )
15 12 14 fge0iccico ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝐹 : 𝑋 ⟶ ( 0 [,) +∞ ) )
16 elpwinss ⊢ ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) → 𝑥 ⊆ 𝑋 )
17 16 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝑥 ⊆ 𝑋 )
18 elinel2 ⊢ ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) → 𝑥 ∈ Fin )
19 18 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝑥 ∈ Fin )
20 11 15 17 19 fsumlesge0 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ≤ ( Σ^ ‘ 𝐹 ) )
21 20 3adant3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑤 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ≤ ( Σ^ ‘ 𝐹 ) )
22 10 21 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑤 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → 𝑤 ≤ ( Σ^ ‘ 𝐹 ) )
23 22 3exp ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) → ( 𝑤 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) → 𝑤 ≤ ( Σ^ ‘ 𝐹 ) ) ) )
24 23 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑤 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) → 𝑤 ≤ ( Σ^ ‘ 𝐹 ) ) )
25 4 9 24 sylc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) → 𝑤 ≤ ( Σ^ ‘ 𝐹 ) )
26 25 ralrimiva ⊢ ( 𝜑 → ∀ 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) 𝑤 ≤ ( Σ^ ‘ 𝐹 ) )
27 brralrspcev ⊢ ( ( ( Σ^ ‘ 𝐹 ) ∈ ℝ ∧ ∀ 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) 𝑤 ≤ ( Σ^ ‘ 𝐹 ) ) → ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) 𝑤 ≤ 𝑧 )
28 3 26 27 syl2anc ⊢ ( 𝜑 → ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) 𝑤 ≤ 𝑧 )