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 ⊢ Ⅎ x φ
sge0gerpmpt.a ⊢ φ → A ∈ V
sge0gerpmpt.b ⊢ φ ∧ x ∈ A → B ∈ 0 +∞
sge0gerpmpt.c ⊢ φ → C ∈ ℝ *
sge0gerpmpt.rp ⊢ φ ∧ y ∈ ℝ + → ∃ z ∈ 𝒫 A ∩ Fin C ≤ sum^ ⁡ x ∈ z ⟼ B + 𝑒 y
Assertion sge0gerpmpt ⊢ φ → C ≤ sum^ ⁡ x ∈ A ⟼ B

Proof

Step Hyp Ref Expression
1 sge0gerpmpt.xph ⊢ Ⅎ x φ
2 sge0gerpmpt.a ⊢ φ → A ∈ V
3 sge0gerpmpt.b ⊢ φ ∧ x ∈ A → B ∈ 0 +∞
4 sge0gerpmpt.c ⊢ φ → C ∈ ℝ *
5 sge0gerpmpt.rp ⊢ φ ∧ y ∈ ℝ + → ∃ z ∈ 𝒫 A ∩ Fin C ≤ sum^ ⁡ x ∈ z ⟼ B + 𝑒 y
6 eqid ⊢ x ∈ A ⟼ B = x ∈ A ⟼ B
7 1 3 6 fmptdf ⊢ φ → x ∈ A ⟼ B : A ⟶ 0 +∞
8 elpwinss ⊢ z ∈ 𝒫 A ∩ Fin → z ⊆ A
9 8 resmptd ⊢ z ∈ 𝒫 A ∩ Fin → x ∈ A ⟼ B ↾ z = x ∈ z ⟼ B
10 9 eqcomd ⊢ z ∈ 𝒫 A ∩ Fin → x ∈ z ⟼ B = x ∈ A ⟼ B ↾ z
11 10 fveq2d ⊢ z ∈ 𝒫 A ∩ Fin → sum^ ⁡ x ∈ z ⟼ B = sum^ ⁡ x ∈ A ⟼ B ↾ z
12 11 oveq1d ⊢ z ∈ 𝒫 A ∩ Fin → sum^ ⁡ x ∈ z ⟼ B + 𝑒 y = sum^ ⁡ x ∈ A ⟼ B ↾ z + 𝑒 y
13 12 breq2d ⊢ z ∈ 𝒫 A ∩ Fin → C ≤ sum^ ⁡ x ∈ z ⟼ B + 𝑒 y ↔ C ≤ sum^ ⁡ x ∈ A ⟼ B ↾ z + 𝑒 y
14 13 biimpd ⊢ z ∈ 𝒫 A ∩ Fin → C ≤ sum^ ⁡ x ∈ z ⟼ B + 𝑒 y → C ≤ sum^ ⁡ x ∈ A ⟼ B ↾ z + 𝑒 y
15 14 adantl ⊢ φ ∧ y ∈ ℝ + ∧ z ∈ 𝒫 A ∩ Fin → C ≤ sum^ ⁡ x ∈ z ⟼ B + 𝑒 y → C ≤ sum^ ⁡ x ∈ A ⟼ B ↾ z + 𝑒 y
16 15 reximdva ⊢ φ ∧ y ∈ ℝ + → ∃ z ∈ 𝒫 A ∩ Fin C ≤ sum^ ⁡ x ∈ z ⟼ B + 𝑒 y → ∃ z ∈ 𝒫 A ∩ Fin C ≤ sum^ ⁡ x ∈ A ⟼ B ↾ z + 𝑒 y
17 5 16 mpd ⊢ φ ∧ y ∈ ℝ + → ∃ z ∈ 𝒫 A ∩ Fin C ≤ sum^ ⁡ x ∈ A ⟼ B ↾ z + 𝑒 y
18 2 7 4 17 sge0gerp ⊢ φ → C ≤ sum^ ⁡ x ∈ A ⟼ B