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 ∩ Fin sum^ ⁡ 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 ∩ Fin sum^ ⁡ 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 ∩ Fin sum^ ⁡ x ∈ A ⟼ B ↾ y ≤ C ↔ ∀ y ∈ 𝒫 A ∩ Fin sum^ ⁡ x ∈ y ⟼ B ≤ C
13 12 a1i ⊢ φ → ∀ y ∈ 𝒫 A ∩ Fin sum^ ⁡ x ∈ A ⟼ B ↾ y ≤ C ↔ ∀ y ∈ 𝒫 A ∩ Fin sum^ ⁡ x ∈ y ⟼ B ≤ C
14 7 13 bitrd ⊢ φ → sum^ ⁡ x ∈ A ⟼ B ≤ C ↔ ∀ y ∈ 𝒫 A ∩ Fin sum^ ⁡ x ∈ y ⟼ B ≤ C