Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sge0cl Structured version   Visualization version   GIF version

Theorem sge0cl 44612
Description: The arbitrary sum of nonnegative extended reals is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypotheses
Ref Expression
sge0cl.x (𝜑𝑋𝑉)
sge0cl.f (𝜑𝐹:𝑋⟶(0[,]+∞))
Assertion
Ref Expression
sge0cl (𝜑 → (Σ^𝐹) ∈ (0[,]+∞))

Proof of Theorem sge0cl
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 6842 . . . . 5 (𝐹 = ∅ → (Σ^𝐹) = (Σ^‘∅))
2 sge00 44607 . . . . . 6 ^‘∅) = 0
32a1i 11 . . . . 5 (𝐹 = ∅ → (Σ^‘∅) = 0)
41, 3eqtrd 2776 . . . 4 (𝐹 = ∅ → (Σ^𝐹) = 0)
5 0e0iccpnf 13376 . . . . 5 0 ∈ (0[,]+∞)
65a1i 11 . . . 4 (𝐹 = ∅ → 0 ∈ (0[,]+∞))
74, 6eqeltrd 2838 . . 3 (𝐹 = ∅ → (Σ^𝐹) ∈ (0[,]+∞))
87adantl 482 . 2 ((𝜑𝐹 = ∅) → (Σ^𝐹) ∈ (0[,]+∞))
9 sge0cl.x . . . . . . 7 (𝜑𝑋𝑉)
109adantr 481 . . . . . 6 ((𝜑 ∧ +∞ ∈ ran 𝐹) → 𝑋𝑉)
11 sge0cl.f . . . . . . 7 (𝜑𝐹:𝑋⟶(0[,]+∞))
1211adantr 481 . . . . . 6 ((𝜑 ∧ +∞ ∈ ran 𝐹) → 𝐹:𝑋⟶(0[,]+∞))
13 simpr 485 . . . . . 6 ((𝜑 ∧ +∞ ∈ ran 𝐹) → +∞ ∈ ran 𝐹)
1410, 12, 13sge0pnfval 44604 . . . . 5 ((𝜑 ∧ +∞ ∈ ran 𝐹) → (Σ^𝐹) = +∞)
15 pnfel0pnf 43756 . . . . . 6 +∞ ∈ (0[,]+∞)
1615a1i 11 . . . . 5 ((𝜑 ∧ +∞ ∈ ran 𝐹) → +∞ ∈ (0[,]+∞))
1714, 16eqeltrd 2838 . . . 4 ((𝜑 ∧ +∞ ∈ ran 𝐹) → (Σ^𝐹) ∈ (0[,]+∞))
1817adantlr 713 . . 3 (((𝜑 ∧ ¬ 𝐹 = ∅) ∧ +∞ ∈ ran 𝐹) → (Σ^𝐹) ∈ (0[,]+∞))
19 simpll 765 . . . 4 (((𝜑 ∧ ¬ 𝐹 = ∅) ∧ ¬ +∞ ∈ ran 𝐹) → 𝜑)
20 neqne 2951 . . . . 5 𝐹 = ∅ → 𝐹 ≠ ∅)
2120ad2antlr 725 . . . 4 (((𝜑 ∧ ¬ 𝐹 = ∅) ∧ ¬ +∞ ∈ ran 𝐹) → 𝐹 ≠ ∅)
22 simpr 485 . . . 4 (((𝜑 ∧ ¬ 𝐹 = ∅) ∧ ¬ +∞ ∈ ran 𝐹) → ¬ +∞ ∈ ran 𝐹)
23 0xr 11202 . . . . . 6 0 ∈ ℝ*
2423a1i 11 . . . . 5 (((𝜑𝐹 ≠ ∅) ∧ ¬ +∞ ∈ ran 𝐹) → 0 ∈ ℝ*)
25 pnfxr 11209 . . . . . 6 +∞ ∈ ℝ*
2625a1i 11 . . . . 5 (((𝜑𝐹 ≠ ∅) ∧ ¬ +∞ ∈ ran 𝐹) → +∞ ∈ ℝ*)
279adantr 481 . . . . . . . 8 ((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) → 𝑋𝑉)
2811adantr 481 . . . . . . . . 9 ((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) → 𝐹:𝑋⟶(0[,]+∞))
29 simpr 485 . . . . . . . . 9 ((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) → ¬ +∞ ∈ ran 𝐹)
3028, 29fge0iccico 44601 . . . . . . . 8 ((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) → 𝐹:𝑋⟶(0[,)+∞))
3127, 30sge0reval 44603 . . . . . . 7 ((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) → (Σ^𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)), ℝ*, < ))
32 elinel2 4156 . . . . . . . . . . . . 13 (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → 𝑥 ∈ Fin)
3332adantl 482 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑥 ∈ Fin)
3411ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦𝑥) → 𝐹:𝑋⟶(0[,]+∞))
35 elinel1 4155 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → 𝑥 ∈ 𝒫 𝑋)
36 elpwi 4567 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ 𝒫 𝑋𝑥𝑋)
3735, 36syl 17 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → 𝑥𝑋)
3837adantl 482 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑥𝑋)
3938adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦𝑥) → 𝑥𝑋)
40 simpr 485 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦𝑥) → 𝑦𝑥)
4139, 40sseldd 3945 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦𝑥) → 𝑦𝑋)
4234, 41ffvelcdmd 7036 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦𝑥) → (𝐹𝑦) ∈ (0[,]+∞))
4342adantllr 717 . . . . . . . . . . . . 13 ((((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦𝑥) → (𝐹𝑦) ∈ (0[,]+∞))
44 nne 2947 . . . . . . . . . . . . . . . . . 18 (¬ (𝐹𝑦) ≠ +∞ ↔ (𝐹𝑦) = +∞)
4544biimpi 215 . . . . . . . . . . . . . . . . 17 (¬ (𝐹𝑦) ≠ +∞ → (𝐹𝑦) = +∞)
4645eqcomd 2742 . . . . . . . . . . . . . . . 16 (¬ (𝐹𝑦) ≠ +∞ → +∞ = (𝐹𝑦))
4746adantl 482 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦𝑥) ∧ ¬ (𝐹𝑦) ≠ +∞) → +∞ = (𝐹𝑦))
4811ffund 6672 . . . . . . . . . . . . . . . . . 18 (𝜑 → Fun 𝐹)
49483ad2ant1 1133 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑦𝑥) → Fun 𝐹)
50413impa 1110 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑦𝑥) → 𝑦𝑋)
5111fdmd 6679 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → dom 𝐹 = 𝑋)
5251eqcomd 2742 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑋 = dom 𝐹)
53523ad2ant1 1133 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑦𝑥) → 𝑋 = dom 𝐹)
5450, 53eleqtrd 2840 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑦𝑥) → 𝑦 ∈ dom 𝐹)
55 fvelrn 7027 . . . . . . . . . . . . . . . . 17 ((Fun 𝐹𝑦 ∈ dom 𝐹) → (𝐹𝑦) ∈ ran 𝐹)
5649, 54, 55syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑦𝑥) → (𝐹𝑦) ∈ ran 𝐹)
5756ad5ant134 1367 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦𝑥) ∧ ¬ (𝐹𝑦) ≠ +∞) → (𝐹𝑦) ∈ ran 𝐹)
5847, 57eqeltrd 2838 . . . . . . . . . . . . . 14 (((((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦𝑥) ∧ ¬ (𝐹𝑦) ≠ +∞) → +∞ ∈ ran 𝐹)
5929ad3antrrr 728 . . . . . . . . . . . . . 14 (((((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦𝑥) ∧ ¬ (𝐹𝑦) ≠ +∞) → ¬ +∞ ∈ ran 𝐹)
6058, 59condan 816 . . . . . . . . . . . . 13 ((((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦𝑥) → (𝐹𝑦) ≠ +∞)
61 ge0xrre 43759 . . . . . . . . . . . . 13 (((𝐹𝑦) ∈ (0[,]+∞) ∧ (𝐹𝑦) ≠ +∞) → (𝐹𝑦) ∈ ℝ)
6243, 60, 61syl2anc 584 . . . . . . . . . . . 12 ((((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦𝑥) → (𝐹𝑦) ∈ ℝ)
6333, 62fsumrecl 15619 . . . . . . . . . . 11 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → Σ𝑦𝑥 (𝐹𝑦) ∈ ℝ)
6463ralrimiva 3143 . . . . . . . . . 10 ((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) → ∀𝑥 ∈ (𝒫 𝑋 ∩ Fin)Σ𝑦𝑥 (𝐹𝑦) ∈ ℝ)
65 eqid 2736 . . . . . . . . . . 11 (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) = (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))
6665rnmptss 7070 . . . . . . . . . 10 (∀𝑥 ∈ (𝒫 𝑋 ∩ Fin)Σ𝑦𝑥 (𝐹𝑦) ∈ ℝ → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) ⊆ ℝ)
6764, 66syl 17 . . . . . . . . 9 ((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) ⊆ ℝ)
68 ressxr 11199 . . . . . . . . . 10 ℝ ⊆ ℝ*
6968a1i 11 . . . . . . . . 9 ((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) → ℝ ⊆ ℝ*)
7067, 69sstrd 3954 . . . . . . . 8 ((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) ⊆ ℝ*)
71 supxrcl 13234 . . . . . . . 8 (ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) ⊆ ℝ* → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)), ℝ*, < ) ∈ ℝ*)
7270, 71syl 17 . . . . . . 7 ((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)), ℝ*, < ) ∈ ℝ*)
7331, 72eqeltrd 2838 . . . . . 6 ((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) → (Σ^𝐹) ∈ ℝ*)
7473adantlr 713 . . . . 5 (((𝜑𝐹 ≠ ∅) ∧ ¬ +∞ ∈ ran 𝐹) → (Σ^𝐹) ∈ ℝ*)
7552adantr 481 . . . . . . . . 9 ((𝜑𝐹 ≠ ∅) → 𝑋 = dom 𝐹)
76 neneq 2949 . . . . . . . . . . . 12 (𝐹 ≠ ∅ → ¬ 𝐹 = ∅)
7776adantl 482 . . . . . . . . . . 11 ((𝜑𝐹 ≠ ∅) → ¬ 𝐹 = ∅)
78 frel 6673 . . . . . . . . . . . . . 14 (𝐹:𝑋⟶(0[,]+∞) → Rel 𝐹)
7911, 78syl 17 . . . . . . . . . . . . 13 (𝜑 → Rel 𝐹)
8079adantr 481 . . . . . . . . . . . 12 ((𝜑𝐹 ≠ ∅) → Rel 𝐹)
81 reldm0 5883 . . . . . . . . . . . 12 (Rel 𝐹 → (𝐹 = ∅ ↔ dom 𝐹 = ∅))
8280, 81syl 17 . . . . . . . . . . 11 ((𝜑𝐹 ≠ ∅) → (𝐹 = ∅ ↔ dom 𝐹 = ∅))
8377, 82mtbid 323 . . . . . . . . . 10 ((𝜑𝐹 ≠ ∅) → ¬ dom 𝐹 = ∅)
8483neqned 2950 . . . . . . . . 9 ((𝜑𝐹 ≠ ∅) → dom 𝐹 ≠ ∅)
8575, 84eqnetrd 3011 . . . . . . . 8 ((𝜑𝐹 ≠ ∅) → 𝑋 ≠ ∅)
86 n0 4306 . . . . . . . 8 (𝑋 ≠ ∅ ↔ ∃𝑧 𝑧𝑋)
8785, 86sylib 217 . . . . . . 7 ((𝜑𝐹 ≠ ∅) → ∃𝑧 𝑧𝑋)
8887adantr 481 . . . . . 6 (((𝜑𝐹 ≠ ∅) ∧ ¬ +∞ ∈ ran 𝐹) → ∃𝑧 𝑧𝑋)
8923a1i 11 . . . . . . . . . 10 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑧𝑋) → 0 ∈ ℝ*)
9011ffvelcdmda 7035 . . . . . . . . . . . . 13 ((𝜑𝑧𝑋) → (𝐹𝑧) ∈ (0[,]+∞))
9190adantlr 713 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑧𝑋) → (𝐹𝑧) ∈ (0[,]+∞))
92 nne 2947 . . . . . . . . . . . . . . . . 17 (¬ (𝐹𝑧) ≠ +∞ ↔ (𝐹𝑧) = +∞)
9392biimpi 215 . . . . . . . . . . . . . . . 16 (¬ (𝐹𝑧) ≠ +∞ → (𝐹𝑧) = +∞)
9493eqcomd 2742 . . . . . . . . . . . . . . 15 (¬ (𝐹𝑧) ≠ +∞ → +∞ = (𝐹𝑧))
9594adantl 482 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑧𝑋) ∧ ¬ (𝐹𝑧) ≠ +∞) → +∞ = (𝐹𝑧))
9611adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝑋) → 𝐹:𝑋⟶(0[,]+∞))
9796ffund 6672 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝑋) → Fun 𝐹)
98 simpr 485 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝑋) → 𝑧𝑋)
9952adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝑋) → 𝑋 = dom 𝐹)
10098, 99eleqtrd 2840 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝑋) → 𝑧 ∈ dom 𝐹)
101 fvelrn 7027 . . . . . . . . . . . . . . . . 17 ((Fun 𝐹𝑧 ∈ dom 𝐹) → (𝐹𝑧) ∈ ran 𝐹)
10297, 100, 101syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝜑𝑧𝑋) → (𝐹𝑧) ∈ ran 𝐹)
103102adantlr 713 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑧𝑋) → (𝐹𝑧) ∈ ran 𝐹)
104103adantr 481 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑧𝑋) ∧ ¬ (𝐹𝑧) ≠ +∞) → (𝐹𝑧) ∈ ran 𝐹)
10595, 104eqeltrd 2838 . . . . . . . . . . . . 13 ((((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑧𝑋) ∧ ¬ (𝐹𝑧) ≠ +∞) → +∞ ∈ ran 𝐹)
10629ad2antrr 724 . . . . . . . . . . . . 13 ((((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑧𝑋) ∧ ¬ (𝐹𝑧) ≠ +∞) → ¬ +∞ ∈ ran 𝐹)
107105, 106condan 816 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑧𝑋) → (𝐹𝑧) ≠ +∞)
108 ge0xrre 43759 . . . . . . . . . . . 12 (((𝐹𝑧) ∈ (0[,]+∞) ∧ (𝐹𝑧) ≠ +∞) → (𝐹𝑧) ∈ ℝ)
10991, 107, 108syl2anc 584 . . . . . . . . . . 11 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑧𝑋) → (𝐹𝑧) ∈ ℝ)
110109rexrd 11205 . . . . . . . . . 10 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑧𝑋) → (𝐹𝑧) ∈ ℝ*)
11173adantr 481 . . . . . . . . . 10 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑧𝑋) → (Σ^𝐹) ∈ ℝ*)
11223a1i 11 . . . . . . . . . . . 12 ((𝜑𝑧𝑋) → 0 ∈ ℝ*)
11325a1i 11 . . . . . . . . . . . 12 ((𝜑𝑧𝑋) → +∞ ∈ ℝ*)
114 iccgelb 13320 . . . . . . . . . . . 12 ((0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ (𝐹𝑧) ∈ (0[,]+∞)) → 0 ≤ (𝐹𝑧))
115112, 113, 90, 114syl3anc 1371 . . . . . . . . . . 11 ((𝜑𝑧𝑋) → 0 ≤ (𝐹𝑧))
116115adantlr 713 . . . . . . . . . 10 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑧𝑋) → 0 ≤ (𝐹𝑧))
11770adantr 481 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑧𝑋) → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) ⊆ ℝ*)
118 snelpwi 5400 . . . . . . . . . . . . . . . 16 (𝑧𝑋 → {𝑧} ∈ 𝒫 𝑋)
119 snfi 8988 . . . . . . . . . . . . . . . . 17 {𝑧} ∈ Fin
120119a1i 11 . . . . . . . . . . . . . . . 16 (𝑧𝑋 → {𝑧} ∈ Fin)
121118, 120elind 4154 . . . . . . . . . . . . . . 15 (𝑧𝑋 → {𝑧} ∈ (𝒫 𝑋 ∩ Fin))
122121adantl 482 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑧𝑋) → {𝑧} ∈ (𝒫 𝑋 ∩ Fin))
123 simpr 485 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑧𝑋) → 𝑧𝑋)
124109recnd 11183 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑧𝑋) → (𝐹𝑧) ∈ ℂ)
125 fveq2 6842 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑧 → (𝐹𝑦) = (𝐹𝑧))
126125sumsn 15631 . . . . . . . . . . . . . . . 16 ((𝑧𝑋 ∧ (𝐹𝑧) ∈ ℂ) → Σ𝑦 ∈ {𝑧} (𝐹𝑦) = (𝐹𝑧))
127123, 124, 126syl2anc 584 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑧𝑋) → Σ𝑦 ∈ {𝑧} (𝐹𝑦) = (𝐹𝑧))
128127eqcomd 2742 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑧𝑋) → (𝐹𝑧) = Σ𝑦 ∈ {𝑧} (𝐹𝑦))
129 sumeq1 15573 . . . . . . . . . . . . . . 15 (𝑥 = {𝑧} → Σ𝑦𝑥 (𝐹𝑦) = Σ𝑦 ∈ {𝑧} (𝐹𝑦))
130129rspceeqv 3595 . . . . . . . . . . . . . 14 (({𝑧} ∈ (𝒫 𝑋 ∩ Fin) ∧ (𝐹𝑧) = Σ𝑦 ∈ {𝑧} (𝐹𝑦)) → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)(𝐹𝑧) = Σ𝑦𝑥 (𝐹𝑦))
131122, 128, 130syl2anc 584 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑧𝑋) → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)(𝐹𝑧) = Σ𝑦𝑥 (𝐹𝑦))
13265elrnmpt 5911 . . . . . . . . . . . . . 14 ((𝐹𝑧) ∈ (0[,]+∞) → ((𝐹𝑧) ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) ↔ ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)(𝐹𝑧) = Σ𝑦𝑥 (𝐹𝑦)))
13391, 132syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑧𝑋) → ((𝐹𝑧) ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) ↔ ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)(𝐹𝑧) = Σ𝑦𝑥 (𝐹𝑦)))
134131, 133mpbird 256 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑧𝑋) → (𝐹𝑧) ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)))
135 supxrub 13243 . . . . . . . . . . . 12 ((ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) ⊆ ℝ* ∧ (𝐹𝑧) ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))) → (𝐹𝑧) ≤ sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)), ℝ*, < ))
136117, 134, 135syl2anc 584 . . . . . . . . . . 11 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑧𝑋) → (𝐹𝑧) ≤ sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)), ℝ*, < ))
13731eqcomd 2742 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)), ℝ*, < ) = (Σ^𝐹))
138137adantr 481 . . . . . . . . . . 11 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑧𝑋) → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)), ℝ*, < ) = (Σ^𝐹))
139136, 138breqtrd 5131 . . . . . . . . . 10 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑧𝑋) → (𝐹𝑧) ≤ (Σ^𝐹))
14089, 110, 111, 116, 139xrletrd 13081 . . . . . . . . 9 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑧𝑋) → 0 ≤ (Σ^𝐹))
141140ex 413 . . . . . . . 8 ((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) → (𝑧𝑋 → 0 ≤ (Σ^𝐹)))
142141adantlr 713 . . . . . . 7 (((𝜑𝐹 ≠ ∅) ∧ ¬ +∞ ∈ ran 𝐹) → (𝑧𝑋 → 0 ≤ (Σ^𝐹)))
143142exlimdv 1936 . . . . . 6 (((𝜑𝐹 ≠ ∅) ∧ ¬ +∞ ∈ ran 𝐹) → (∃𝑧 𝑧𝑋 → 0 ≤ (Σ^𝐹)))
14488, 143mpd 15 . . . . 5 (((𝜑𝐹 ≠ ∅) ∧ ¬ +∞ ∈ ran 𝐹) → 0 ≤ (Σ^𝐹))
145 pnfge 13051 . . . . . . 7 ((Σ^𝐹) ∈ ℝ* → (Σ^𝐹) ≤ +∞)
14673, 145syl 17 . . . . . 6 ((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) → (Σ^𝐹) ≤ +∞)
147146adantlr 713 . . . . 5 (((𝜑𝐹 ≠ ∅) ∧ ¬ +∞ ∈ ran 𝐹) → (Σ^𝐹) ≤ +∞)
14824, 26, 74, 144, 147eliccxrd 43755 . . . 4 (((𝜑𝐹 ≠ ∅) ∧ ¬ +∞ ∈ ran 𝐹) → (Σ^𝐹) ∈ (0[,]+∞))
14919, 21, 22, 148syl21anc 836 . . 3 (((𝜑 ∧ ¬ 𝐹 = ∅) ∧ ¬ +∞ ∈ ran 𝐹) → (Σ^𝐹) ∈ (0[,]+∞))
15018, 149pm2.61dan 811 . 2 ((𝜑 ∧ ¬ 𝐹 = ∅) → (Σ^𝐹) ∈ (0[,]+∞))
1518, 150pm2.61dan 811 1 (𝜑 → (Σ^𝐹) ∈ (0[,]+∞))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wex 1781  wcel 2106  wne 2943  wral 3064  wrex 3073  cin 3909  wss 3910  c0 4282  𝒫 cpw 4560  {csn 4586   class class class wbr 5105  cmpt 5188  dom cdm 5633  ran crn 5634  Rel wrel 5638  Fun wfun 6490  wf 6492  cfv 6496  (class class class)co 7357  Fincfn 8883  supcsup 9376  cc 11049  cr 11050  0cc0 11051  +∞cpnf 11186  *cxr 11188   < clt 11189  cle 11190  [,]cicc 13267  Σcsu 15570  Σ^csumge0 44593
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-inf2 9577  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-sup 9378  df-oi 9446  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-n0 12414  df-z 12500  df-uz 12764  df-rp 12916  df-ico 13270  df-icc 13271  df-fz 13425  df-fzo 13568  df-seq 13907  df-exp 13968  df-hash 14231  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-clim 15370  df-sum 15571  df-sumge0 44594
This theorem is referenced by:  sge0ge0  44615  sge0xrcl  44616  sge0split  44640  sge0iunmptlemre  44646  sge0iunmpt  44649  sge0nemnf  44651  sge0clmpt  44656  sge0isum  44658  psmeasure  44702  ovnsupge0  44788  ovnsubaddlem1  44801  sge0hsphoire  44820  hoidmvlelem1  44826  hspmbllem2  44858
  Copyright terms: Public domain W3C validator