Metamath Proof Explorer


Theorem sge0gerpmpt

Description: The arbitrary sum of nonnegative extended reals is greater than or equal to a given extended real number if this number can be approximated from below by finite subsums. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0gerpmpt.xph 𝑥 𝜑
sge0gerpmpt.a ( 𝜑𝐴𝑉 )
sge0gerpmpt.b ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
sge0gerpmpt.c ( 𝜑𝐶 ∈ ℝ* )
sge0gerpmpt.rp ( ( 𝜑𝑦 ∈ ℝ+ ) → ∃ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝐶 ≤ ( ( Σ^ ‘ ( 𝑥𝑧𝐵 ) ) +𝑒 𝑦 ) )
Assertion sge0gerpmpt ( 𝜑𝐶 ≤ ( Σ^ ‘ ( 𝑥𝐴𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 sge0gerpmpt.xph 𝑥 𝜑
2 sge0gerpmpt.a ( 𝜑𝐴𝑉 )
3 sge0gerpmpt.b ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
4 sge0gerpmpt.c ( 𝜑𝐶 ∈ ℝ* )
5 sge0gerpmpt.rp ( ( 𝜑𝑦 ∈ ℝ+ ) → ∃ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝐶 ≤ ( ( Σ^ ‘ ( 𝑥𝑧𝐵 ) ) +𝑒 𝑦 ) )
6 eqid ( 𝑥𝐴𝐵 ) = ( 𝑥𝐴𝐵 )
7 1 3 6 fmptdf ( 𝜑 → ( 𝑥𝐴𝐵 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
8 elpwinss ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑧𝐴 )
9 8 resmptd ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) → ( ( 𝑥𝐴𝐵 ) ↾ 𝑧 ) = ( 𝑥𝑧𝐵 ) )
10 9 eqcomd ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) → ( 𝑥𝑧𝐵 ) = ( ( 𝑥𝐴𝐵 ) ↾ 𝑧 ) )
11 10 fveq2d ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) → ( Σ^ ‘ ( 𝑥𝑧𝐵 ) ) = ( Σ^ ‘ ( ( 𝑥𝐴𝐵 ) ↾ 𝑧 ) ) )
12 11 oveq1d ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) → ( ( Σ^ ‘ ( 𝑥𝑧𝐵 ) ) +𝑒 𝑦 ) = ( ( Σ^ ‘ ( ( 𝑥𝐴𝐵 ) ↾ 𝑧 ) ) +𝑒 𝑦 ) )
13 12 breq2d ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) → ( 𝐶 ≤ ( ( Σ^ ‘ ( 𝑥𝑧𝐵 ) ) +𝑒 𝑦 ) ↔ 𝐶 ≤ ( ( Σ^ ‘ ( ( 𝑥𝐴𝐵 ) ↾ 𝑧 ) ) +𝑒 𝑦 ) ) )
14 13 biimpd ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) → ( 𝐶 ≤ ( ( Σ^ ‘ ( 𝑥𝑧𝐵 ) ) +𝑒 𝑦 ) → 𝐶 ≤ ( ( Σ^ ‘ ( ( 𝑥𝐴𝐵 ) ↾ 𝑧 ) ) +𝑒 𝑦 ) ) )
15 14 adantl ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐶 ≤ ( ( Σ^ ‘ ( 𝑥𝑧𝐵 ) ) +𝑒 𝑦 ) → 𝐶 ≤ ( ( Σ^ ‘ ( ( 𝑥𝐴𝐵 ) ↾ 𝑧 ) ) +𝑒 𝑦 ) ) )
16 15 reximdva ( ( 𝜑𝑦 ∈ ℝ+ ) → ( ∃ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝐶 ≤ ( ( Σ^ ‘ ( 𝑥𝑧𝐵 ) ) +𝑒 𝑦 ) → ∃ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝐶 ≤ ( ( Σ^ ‘ ( ( 𝑥𝐴𝐵 ) ↾ 𝑧 ) ) +𝑒 𝑦 ) ) )
17 5 16 mpd ( ( 𝜑𝑦 ∈ ℝ+ ) → ∃ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝐶 ≤ ( ( Σ^ ‘ ( ( 𝑥𝐴𝐵 ) ↾ 𝑧 ) ) +𝑒 𝑦 ) )
18 2 7 4 17 sge0gerp ( 𝜑𝐶 ≤ ( Σ^ ‘ ( 𝑥𝐴𝐵 ) ) )