Metamath Proof Explorer

Theorem sge0lefimpt

Description: A sum of nonnegative extended reals is smaller than a given extended real if and only if every finite subsum is smaller than it. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses sge0lefimpt.xph ⊢Ⅎxφ
sge0lefimpt.a ⊢φ→A∈V
sge0lefimpt.b ⊢φ∧x∈A→B∈0+∞
sge0lefimpt.c ⊢φ→C∈ℝ*
Assertion sge0lefimpt ⊢φ→sum^⁡x∈A⟼B≤C↔∀y∈𝒫A∩Finsum^⁡x∈y⟼B≤C

Proof

Step Hyp Ref Expression
1 sge0lefimpt.xph ⊢Ⅎxφ
2 sge0lefimpt.a ⊢φ→A∈V
3 sge0lefimpt.b ⊢φ∧x∈A→B∈0+∞
4 sge0lefimpt.c ⊢φ→C∈ℝ*
5 eqid ⊢x∈A⟼B=x∈A⟼B
6 1 3 5 fmptdf ⊢φ→x∈A⟼B:A⟶0+∞
7 2 6 4 sge0lefi ⊢φ→sum^⁡x∈A⟼B≤C↔∀y∈𝒫A∩Finsum^⁡x∈A⟼B↾y≤C
8 elpwinss ⊢y∈𝒫A∩Fin→y⊆A
9 8 resmptd ⊢y∈𝒫A∩Fin→x∈A⟼B↾y=x∈y⟼B
10 9 fveq2d ⊢y∈𝒫A∩Fin→sum^⁡x∈A⟼B↾y=sum^⁡x∈y⟼B
11 10 breq1d ⊢y∈𝒫A∩Fin→sum^⁡x∈A⟼B↾y≤C↔sum^⁡x∈y⟼B≤C
12 11 ralbiia ⊢∀y∈𝒫A∩Finsum^⁡x∈A⟼B↾y≤C↔∀y∈𝒫A∩Finsum^⁡x∈y⟼B≤C
13 12 a1i ⊢φ→∀y∈𝒫A∩Finsum^⁡x∈A⟼B↾y≤C↔∀y∈𝒫A∩Finsum^⁡x∈y⟼B≤C
14 7 13 bitrd ⊢φ→sum^⁡x∈A⟼B≤C↔∀y∈𝒫A∩Finsum^⁡x∈y⟼B≤C