Metamath Proof Explorer

Theorem sge0supre

Description: If the arbitrary sum of nonnegative extended reals is real, then it is the supremum (in the real numbers) of finite subsums. Similar to sge0sup , but here we can use sup with respect to RR instead of RR* . (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0supre.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
sge0supre.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
sge0supre.re ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) ∈ ℝ )
Assertion sge0supre ( 𝜑 → ( Σ^ ‘ 𝐹 ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) )

Proof

Step Hyp Ref Expression
1 sge0supre.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
2 sge0supre.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
3 sge0supre.re ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) ∈ ℝ )
4 1 adantr ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → 𝑋 ∈ 𝑉 )
5 2 adantr ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
6 simpr ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → +∞ ∈ ran 𝐹 )
7 4 5 6 sge0pnfval ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → ( Σ^ ‘ 𝐹 ) = +∞ )
8 1 2 sge0repnf ⊢ ( 𝜑 → ( ( Σ^ ‘ 𝐹 ) ∈ ℝ ↔ ¬ ( Σ^ ‘ 𝐹 ) = +∞ ) )
9 3 8 mpbid ⊢ ( 𝜑 → ¬ ( Σ^ ‘ 𝐹 ) = +∞ )
10 9 adantr ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → ¬ ( Σ^ ‘ 𝐹 ) = +∞ )
11 7 10 pm2.65da ⊢ ( 𝜑 → ¬ +∞ ∈ ran 𝐹 )
12 2 11 fge0iccico ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,) +∞ ) )
13 1 12 sge0reval ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) )
14 12 sge0rnre ⊢ ( 𝜑 → ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ⊆ ℝ )
15 sge0rnn0 ⊢ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ≠ ∅
16 15 a1i ⊢ ( 𝜑 → ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ≠ ∅ )
17 simpr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) → 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) )
18 eqid ⊢ ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) = ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
19 18 elrnmpt ⊢ ( 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑤 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) )
20 19 adantl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑤 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) )
21 17 20 mpbid ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) → ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑤 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
22 simp3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑤 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → 𝑤 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
23 ressxr ⊢ ℝ ⊆ ℝ*
24 23 a1i ⊢ ( 𝜑 → ℝ ⊆ ℝ* )
25 14 24 sstrd ⊢ ( 𝜑 → ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ⊆ ℝ* )
26 25 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ⊆ ℝ* )
27 id ⊢ ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) → 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) )
28 sumex ⊢ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ V
29 28 a1i ⊢ ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) → Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ V )
30 18 elrnmpt1 ⊢ ( ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ V ) → Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) )
31 27 29 30 syl2anc ⊢ ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) → Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) )
32 31 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) )
33 supxrub ⊢ ( ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ⊆ ℝ* ∧ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) → Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ≤ sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) )
34 26 32 33 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ≤ sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) )
35 13 eqcomd ⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) = ( Σ^ ‘ 𝐹 ) )
36 35 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) = ( Σ^ ‘ 𝐹 ) )
37 34 36 breqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ≤ ( Σ^ ‘ 𝐹 ) )
38 37 3adant3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑤 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ≤ ( Σ^ ‘ 𝐹 ) )
39 22 38 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑤 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → 𝑤 ≤ ( Σ^ ‘ 𝐹 ) )
40 39 3exp ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) → ( 𝑤 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) → 𝑤 ≤ ( Σ^ ‘ 𝐹 ) ) ) )
41 40 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑤 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) → 𝑤 ≤ ( Σ^ ‘ 𝐹 ) ) )
42 41 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) → ( ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑤 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) → 𝑤 ≤ ( Σ^ ‘ 𝐹 ) ) )
43 21 42 mpd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) → 𝑤 ≤ ( Σ^ ‘ 𝐹 ) )
44 43 ralrimiva ⊢ ( 𝜑 → ∀ 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) 𝑤 ≤ ( Σ^ ‘ 𝐹 ) )
45 brralrspcev ⊢ ( ( ( Σ^ ‘ 𝐹 ) ∈ ℝ ∧ ∀ 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) 𝑤 ≤ ( Σ^ ‘ 𝐹 ) ) → ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) 𝑤 ≤ 𝑧 )
46 3 44 45 syl2anc ⊢ ( 𝜑 → ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) 𝑤 ≤ 𝑧 )
47 supxrre ⊢ ( ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ⊆ ℝ ∧ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ≠ ∅ ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) 𝑤 ≤ 𝑧 ) → sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) )
48 14 16 46 47 syl3anc ⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) )
49 13 48 eqtrd ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) )