Metamath Proof Explorer

Theorem sge0gerp

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 sge0gerp.x ⊢ φ → X ∈ V
sge0gerp.f ⊢ φ → F : X ⟶ 0 +∞
sge0gerp.a ⊢ φ → A ∈ ℝ *
sge0gerp.z ⊢ φ ∧ x ∈ ℝ + → ∃ z ∈ 𝒫 X ∩ Fin A ≤ sum^ ⁡ F ↾ z + 𝑒 x
Assertion sge0gerp ⊢ φ → A ≤ sum^ ⁡ F

Proof

Step Hyp Ref Expression
1 sge0gerp.x ⊢ φ → X ∈ V
2 sge0gerp.f ⊢ φ → F : X ⟶ 0 +∞
3 sge0gerp.a ⊢ φ → A ∈ ℝ *
4 sge0gerp.z ⊢ φ ∧ x ∈ ℝ + → ∃ z ∈ 𝒫 X ∩ Fin A ≤ sum^ ⁡ F ↾ z + 𝑒 x
5 nfv ⊢ Ⅎ x φ
6 simpr ⊢ φ ∧ z ∈ 𝒫 X ∩ Fin → z ∈ 𝒫 X ∩ Fin
7 2 adantr ⊢ φ ∧ z ∈ 𝒫 X ∩ Fin → F : X ⟶ 0 +∞
8 elinel1 ⊢ z ∈ 𝒫 X ∩ Fin → z ∈ 𝒫 X
9 elpwi ⊢ z ∈ 𝒫 X → z ⊆ X
10 8 9 syl ⊢ z ∈ 𝒫 X ∩ Fin → z ⊆ X
11 10 adantl ⊢ φ ∧ z ∈ 𝒫 X ∩ Fin → z ⊆ X
12 7 11 fssresd ⊢ φ ∧ z ∈ 𝒫 X ∩ Fin → F ↾ z : z ⟶ 0 +∞
13 6 12 sge0xrcl ⊢ φ ∧ z ∈ 𝒫 X ∩ Fin → sum^ ⁡ F ↾ z ∈ ℝ *
14 13 ralrimiva ⊢ φ → ∀ z ∈ 𝒫 X ∩ Fin sum^ ⁡ F ↾ z ∈ ℝ *
15 eqid ⊢ z ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ z = z ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ z
16 15 rnmptss ⊢ ∀ z ∈ 𝒫 X ∩ Fin sum^ ⁡ F ↾ z ∈ ℝ * → ran ⁡ z ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ z ⊆ ℝ *
17 14 16 syl ⊢ φ → ran ⁡ z ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ z ⊆ ℝ *
18 nfv ⊢ Ⅎ z φ ∧ x ∈ ℝ +
19 nfmpt1 ⊢ Ⅎ _ z z ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ z
20 19 nfrn ⊢ Ⅎ _ z ran ⁡ z ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ z
21 nfv ⊢ Ⅎ z A ≤ y + 𝑒 x
22 20 21 nfrex ⊢ Ⅎ z ∃ y ∈ ran ⁡ z ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ z A ≤ y + 𝑒 x
23 id ⊢ z ∈ 𝒫 X ∩ Fin → z ∈ 𝒫 X ∩ Fin
24 fvexd ⊢ z ∈ 𝒫 X ∩ Fin → sum^ ⁡ F ↾ z ∈ V
25 15 elrnmpt1 ⊢ z ∈ 𝒫 X ∩ Fin ∧ sum^ ⁡ F ↾ z ∈ V → sum^ ⁡ F ↾ z ∈ ran ⁡ z ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ z
26 23 24 25 syl2anc ⊢ z ∈ 𝒫 X ∩ Fin → sum^ ⁡ F ↾ z ∈ ran ⁡ z ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ z
27 26 3ad2ant2 ⊢ φ ∧ x ∈ ℝ + ∧ z ∈ 𝒫 X ∩ Fin ∧ A ≤ sum^ ⁡ F ↾ z + 𝑒 x → sum^ ⁡ F ↾ z ∈ ran ⁡ z ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ z
28 simp3 ⊢ φ ∧ x ∈ ℝ + ∧ z ∈ 𝒫 X ∩ Fin ∧ A ≤ sum^ ⁡ F ↾ z + 𝑒 x → A ≤ sum^ ⁡ F ↾ z + 𝑒 x
29 nfv ⊢ Ⅎ y A ≤ sum^ ⁡ F ↾ z + 𝑒 x
30 oveq1 ⊢ y = sum^ ⁡ F ↾ z → y + 𝑒 x = sum^ ⁡ F ↾ z + 𝑒 x
31 30 breq2d ⊢ y = sum^ ⁡ F ↾ z → A ≤ y + 𝑒 x ↔ A ≤ sum^ ⁡ F ↾ z + 𝑒 x
32 29 31 rspce ⊢ sum^ ⁡ F ↾ z ∈ ran ⁡ z ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ z ∧ A ≤ sum^ ⁡ F ↾ z + 𝑒 x → ∃ y ∈ ran ⁡ z ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ z A ≤ y + 𝑒 x
33 27 28 32 syl2anc ⊢ φ ∧ x ∈ ℝ + ∧ z ∈ 𝒫 X ∩ Fin ∧ A ≤ sum^ ⁡ F ↾ z + 𝑒 x → ∃ y ∈ ran ⁡ z ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ z A ≤ y + 𝑒 x
34 33 3exp ⊢ φ ∧ x ∈ ℝ + → z ∈ 𝒫 X ∩ Fin → A ≤ sum^ ⁡ F ↾ z + 𝑒 x → ∃ y ∈ ran ⁡ z ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ z A ≤ y + 𝑒 x
35 18 22 34 rexlimd ⊢ φ ∧ x ∈ ℝ + → ∃ z ∈ 𝒫 X ∩ Fin A ≤ sum^ ⁡ F ↾ z + 𝑒 x → ∃ y ∈ ran ⁡ z ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ z A ≤ y + 𝑒 x
36 4 35 mpd ⊢ φ ∧ x ∈ ℝ + → ∃ y ∈ ran ⁡ z ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ z A ≤ y + 𝑒 x
37 5 17 3 36 supxrge ⊢ φ → A ≤ sup ran ⁡ z ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ z ℝ * <
38 1 2 sge0sup ⊢ φ → sum^ ⁡ F = sup ran ⁡ z ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ z ℝ * <
39 38 eqcomd ⊢ φ → sup ran ⁡ z ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ z ℝ * < = sum^ ⁡ F
40 37 39 breqtrd ⊢ φ → A ≤ sum^ ⁡ F