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

Theorem sge0sn 40914
 Description: A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypotheses
Ref Expression
sge0sn.1 (𝜑𝐴𝑉)
sge0sn.2 (𝜑𝐹:{𝐴}⟶(0[,]+∞))
Assertion
Ref Expression
sge0sn (𝜑 → (Σ^𝐹) = (𝐹𝐴))

Proof of Theorem sge0sn
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 snex 4938 . . . . 5 {𝐴} ∈ V
21a1i 11 . . . 4 ((𝜑 ∧ (𝐹𝐴) = +∞) → {𝐴} ∈ V)
3 sge0sn.2 . . . . 5 (𝜑𝐹:{𝐴}⟶(0[,]+∞))
43adantr 480 . . . 4 ((𝜑 ∧ (𝐹𝐴) = +∞) → 𝐹:{𝐴}⟶(0[,]+∞))
5 id 22 . . . . . . 7 ((𝐹𝐴) = +∞ → (𝐹𝐴) = +∞)
65eqcomd 2657 . . . . . 6 ((𝐹𝐴) = +∞ → +∞ = (𝐹𝐴))
76adantl 481 . . . . 5 ((𝜑 ∧ (𝐹𝐴) = +∞) → +∞ = (𝐹𝐴))
8 ffun 6086 . . . . . . . 8 (𝐹:{𝐴}⟶(0[,]+∞) → Fun 𝐹)
93, 8syl 17 . . . . . . 7 (𝜑 → Fun 𝐹)
109adantr 480 . . . . . 6 ((𝜑 ∧ (𝐹𝐴) = +∞) → Fun 𝐹)
11 sge0sn.1 . . . . . . . . 9 (𝜑𝐴𝑉)
12 snidg 4239 . . . . . . . . 9 (𝐴𝑉𝐴 ∈ {𝐴})
1311, 12syl 17 . . . . . . . 8 (𝜑𝐴 ∈ {𝐴})
14 fdm 6089 . . . . . . . . . 10 (𝐹:{𝐴}⟶(0[,]+∞) → dom 𝐹 = {𝐴})
153, 14syl 17 . . . . . . . . 9 (𝜑 → dom 𝐹 = {𝐴})
1615eqcomd 2657 . . . . . . . 8 (𝜑 → {𝐴} = dom 𝐹)
1713, 16eleqtrd 2732 . . . . . . 7 (𝜑𝐴 ∈ dom 𝐹)
1817adantr 480 . . . . . 6 ((𝜑 ∧ (𝐹𝐴) = +∞) → 𝐴 ∈ dom 𝐹)
19 fvelrn 6392 . . . . . 6 ((Fun 𝐹𝐴 ∈ dom 𝐹) → (𝐹𝐴) ∈ ran 𝐹)
2010, 18, 19syl2anc 694 . . . . 5 ((𝜑 ∧ (𝐹𝐴) = +∞) → (𝐹𝐴) ∈ ran 𝐹)
217, 20eqeltrd 2730 . . . 4 ((𝜑 ∧ (𝐹𝐴) = +∞) → +∞ ∈ ran 𝐹)
222, 4, 21sge0pnfval 40908 . . 3 ((𝜑 ∧ (𝐹𝐴) = +∞) → (Σ^𝐹) = +∞)
23 simpr 476 . . 3 ((𝜑 ∧ (𝐹𝐴) = +∞) → (𝐹𝐴) = +∞)
2422, 23eqtr4d 2688 . 2 ((𝜑 ∧ (𝐹𝐴) = +∞) → (Σ^𝐹) = (𝐹𝐴))
251a1i 11 . . . 4 ((𝜑 ∧ ¬ (𝐹𝐴) = +∞) → {𝐴} ∈ V)
263adantr 480 . . . . 5 ((𝜑 ∧ ¬ (𝐹𝐴) = +∞) → 𝐹:{𝐴}⟶(0[,]+∞))
27 elsni 4227 . . . . . . . . 9 (+∞ ∈ {(𝐹𝐴)} → +∞ = (𝐹𝐴))
2827eqcomd 2657 . . . . . . . 8 (+∞ ∈ {(𝐹𝐴)} → (𝐹𝐴) = +∞)
2928con3i 150 . . . . . . 7 (¬ (𝐹𝐴) = +∞ → ¬ +∞ ∈ {(𝐹𝐴)})
3029adantl 481 . . . . . 6 ((𝜑 ∧ ¬ (𝐹𝐴) = +∞) → ¬ +∞ ∈ {(𝐹𝐴)})
3111, 3rnsnf 39684 . . . . . . . 8 (𝜑 → ran 𝐹 = {(𝐹𝐴)})
3231eqcomd 2657 . . . . . . 7 (𝜑 → {(𝐹𝐴)} = ran 𝐹)
3332adantr 480 . . . . . 6 ((𝜑 ∧ ¬ (𝐹𝐴) = +∞) → {(𝐹𝐴)} = ran 𝐹)
3430, 33neleqtrd 2751 . . . . 5 ((𝜑 ∧ ¬ (𝐹𝐴) = +∞) → ¬ +∞ ∈ ran 𝐹)
3526, 34fge0iccico 40905 . . . 4 ((𝜑 ∧ ¬ (𝐹𝐴) = +∞) → 𝐹:{𝐴}⟶(0[,)+∞))
3625, 35sge0reval 40907 . . 3 ((𝜑 ∧ ¬ (𝐹𝐴) = +∞) → (Σ^𝐹) = sup(ran (𝑥 ∈ (𝒫 {𝐴} ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)), ℝ*, < ))
37 sum0 14496 . . . . . . . 8 Σ𝑦 ∈ ∅ (𝐹𝑦) = 0
3837eqcomi 2660 . . . . . . 7 0 = Σ𝑦 ∈ ∅ (𝐹𝑦)
3938a1i 11 . . . . . 6 ((𝜑 ∧ ¬ (𝐹𝐴) = +∞) → 0 = Σ𝑦 ∈ ∅ (𝐹𝑦))
40 nfcvd 2794 . . . . . . . 8 ((𝜑 ∧ ¬ (𝐹𝐴) = +∞) → 𝑦(𝐹𝐴))
41 nfv 1883 . . . . . . . 8 𝑦(𝜑 ∧ ¬ (𝐹𝐴) = +∞)
42 fveq2 6229 . . . . . . . . 9 (𝑦 = 𝐴 → (𝐹𝑦) = (𝐹𝐴))
4342adantl 481 . . . . . . . 8 (((𝜑 ∧ ¬ (𝐹𝐴) = +∞) ∧ 𝑦 = 𝐴) → (𝐹𝑦) = (𝐹𝐴))
4411adantr 480 . . . . . . . 8 ((𝜑 ∧ ¬ (𝐹𝐴) = +∞) → 𝐴𝑉)
45 rge0ssre 12318 . . . . . . . . . 10 (0[,)+∞) ⊆ ℝ
46 ax-resscn 10031 . . . . . . . . . 10 ℝ ⊆ ℂ
4745, 46sstri 3645 . . . . . . . . 9 (0[,)+∞) ⊆ ℂ
4844, 12syl 17 . . . . . . . . . 10 ((𝜑 ∧ ¬ (𝐹𝐴) = +∞) → 𝐴 ∈ {𝐴})
4935, 48ffvelrnd 6400 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝐹𝐴) = +∞) → (𝐹𝐴) ∈ (0[,)+∞))
5047, 49sseldi 3634 . . . . . . . 8 ((𝜑 ∧ ¬ (𝐹𝐴) = +∞) → (𝐹𝐴) ∈ ℂ)
5140, 41, 43, 44, 50sumsnd 39499 . . . . . . 7 ((𝜑 ∧ ¬ (𝐹𝐴) = +∞) → Σ𝑦 ∈ {𝐴} (𝐹𝑦) = (𝐹𝐴))
5251eqcomd 2657 . . . . . 6 ((𝜑 ∧ ¬ (𝐹𝐴) = +∞) → (𝐹𝐴) = Σ𝑦 ∈ {𝐴} (𝐹𝑦))
5339, 52preq12d 4308 . . . . 5 ((𝜑 ∧ ¬ (𝐹𝐴) = +∞) → {0, (𝐹𝐴)} = {Σ𝑦 ∈ ∅ (𝐹𝑦), Σ𝑦 ∈ {𝐴} (𝐹𝑦)})
5453supeq1d 8393 . . . 4 ((𝜑 ∧ ¬ (𝐹𝐴) = +∞) → sup({0, (𝐹𝐴)}, ℝ*, < ) = sup({Σ𝑦 ∈ ∅ (𝐹𝑦), Σ𝑦 ∈ {𝐴} (𝐹𝑦)}, ℝ*, < ))
55 xrltso 12012 . . . . . . . 8 < Or ℝ*
5655a1i 11 . . . . . . 7 (𝜑 → < Or ℝ*)
57 0xr 10124 . . . . . . . 8 0 ∈ ℝ*
5857a1i 11 . . . . . . 7 (𝜑 → 0 ∈ ℝ*)
59 iccssxr 12294 . . . . . . . 8 (0[,]+∞) ⊆ ℝ*
603, 13ffvelrnd 6400 . . . . . . . 8 (𝜑 → (𝐹𝐴) ∈ (0[,]+∞))
6159, 60sseldi 3634 . . . . . . 7 (𝜑 → (𝐹𝐴) ∈ ℝ*)
62 suppr 8418 . . . . . . 7 (( < Or ℝ* ∧ 0 ∈ ℝ* ∧ (𝐹𝐴) ∈ ℝ*) → sup({0, (𝐹𝐴)}, ℝ*, < ) = if((𝐹𝐴) < 0, 0, (𝐹𝐴)))
6356, 58, 61, 62syl3anc 1366 . . . . . 6 (𝜑 → sup({0, (𝐹𝐴)}, ℝ*, < ) = if((𝐹𝐴) < 0, 0, (𝐹𝐴)))
64 pnfxr 10130 . . . . . . . . . . 11 +∞ ∈ ℝ*
6564a1i 11 . . . . . . . . . 10 (𝜑 → +∞ ∈ ℝ*)
6658, 65, 603jca 1261 . . . . . . . . 9 (𝜑 → (0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ (𝐹𝐴) ∈ (0[,]+∞)))
67 iccgelb 12268 . . . . . . . . 9 ((0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ (𝐹𝐴) ∈ (0[,]+∞)) → 0 ≤ (𝐹𝐴))
6866, 67syl 17 . . . . . . . 8 (𝜑 → 0 ≤ (𝐹𝐴))
6958, 61xrlenltd 10142 . . . . . . . 8 (𝜑 → (0 ≤ (𝐹𝐴) ↔ ¬ (𝐹𝐴) < 0))
7068, 69mpbid 222 . . . . . . 7 (𝜑 → ¬ (𝐹𝐴) < 0)
7170iffalsed 4130 . . . . . 6 (𝜑 → if((𝐹𝐴) < 0, 0, (𝐹𝐴)) = (𝐹𝐴))
7263, 71eqtr2d 2686 . . . . 5 (𝜑 → (𝐹𝐴) = sup({0, (𝐹𝐴)}, ℝ*, < ))
7372adantr 480 . . . 4 ((𝜑 ∧ ¬ (𝐹𝐴) = +∞) → (𝐹𝐴) = sup({0, (𝐹𝐴)}, ℝ*, < ))
74 pwsn 4460 . . . . . . . . . . . 12 𝒫 {𝐴} = {∅, {𝐴}}
7574ineq1i 3843 . . . . . . . . . . 11 (𝒫 {𝐴} ∩ Fin) = ({∅, {𝐴}} ∩ Fin)
76 0fin 8229 . . . . . . . . . . . . 13 ∅ ∈ Fin
77 snfi 8079 . . . . . . . . . . . . 13 {𝐴} ∈ Fin
78 prssi 4385 . . . . . . . . . . . . 13 ((∅ ∈ Fin ∧ {𝐴} ∈ Fin) → {∅, {𝐴}} ⊆ Fin)
7976, 77, 78mp2an 708 . . . . . . . . . . . 12 {∅, {𝐴}} ⊆ Fin
80 df-ss 3621 . . . . . . . . . . . . 13 ({∅, {𝐴}} ⊆ Fin ↔ ({∅, {𝐴}} ∩ Fin) = {∅, {𝐴}})
8180biimpi 206 . . . . . . . . . . . 12 ({∅, {𝐴}} ⊆ Fin → ({∅, {𝐴}} ∩ Fin) = {∅, {𝐴}})
8279, 81ax-mp 5 . . . . . . . . . . 11 ({∅, {𝐴}} ∩ Fin) = {∅, {𝐴}}
8375, 82eqtri 2673 . . . . . . . . . 10 (𝒫 {𝐴} ∩ Fin) = {∅, {𝐴}}
84 mpteq1 4770 . . . . . . . . . 10 ((𝒫 {𝐴} ∩ Fin) = {∅, {𝐴}} → (𝑥 ∈ (𝒫 {𝐴} ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) = (𝑥 ∈ {∅, {𝐴}} ↦ Σ𝑦𝑥 (𝐹𝑦)))
8583, 84ax-mp 5 . . . . . . . . 9 (𝑥 ∈ (𝒫 {𝐴} ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) = (𝑥 ∈ {∅, {𝐴}} ↦ Σ𝑦𝑥 (𝐹𝑦))
86 0ex 4823 . . . . . . . . . . . . 13 ∅ ∈ V
8786a1i 11 . . . . . . . . . . . 12 (⊤ → ∅ ∈ V)
881a1i 11 . . . . . . . . . . . 12 (⊤ → {𝐴} ∈ V)
89 sumex 14462 . . . . . . . . . . . . 13 Σ𝑦 ∈ ∅ (𝐹𝑦) ∈ V
9089a1i 11 . . . . . . . . . . . 12 (⊤ → Σ𝑦 ∈ ∅ (𝐹𝑦) ∈ V)
91 sumex 14462 . . . . . . . . . . . . 13 Σ𝑦 ∈ {𝐴} (𝐹𝑦) ∈ V
9291a1i 11 . . . . . . . . . . . 12 (⊤ → Σ𝑦 ∈ {𝐴} (𝐹𝑦) ∈ V)
93 sumeq1 14463 . . . . . . . . . . . . 13 (𝑥 = ∅ → Σ𝑦𝑥 (𝐹𝑦) = Σ𝑦 ∈ ∅ (𝐹𝑦))
9493adantl 481 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 = ∅) → Σ𝑦𝑥 (𝐹𝑦) = Σ𝑦 ∈ ∅ (𝐹𝑦))
95 sumeq1 14463 . . . . . . . . . . . . 13 (𝑥 = {𝐴} → Σ𝑦𝑥 (𝐹𝑦) = Σ𝑦 ∈ {𝐴} (𝐹𝑦))
9695adantl 481 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 = {𝐴}) → Σ𝑦𝑥 (𝐹𝑦) = Σ𝑦 ∈ {𝐴} (𝐹𝑦))
9787, 88, 90, 92, 94, 96fmptpr 6479 . . . . . . . . . . 11 (⊤ → {⟨∅, Σ𝑦 ∈ ∅ (𝐹𝑦)⟩, ⟨{𝐴}, Σ𝑦 ∈ {𝐴} (𝐹𝑦)⟩} = (𝑥 ∈ {∅, {𝐴}} ↦ Σ𝑦𝑥 (𝐹𝑦)))
9897trud 1533 . . . . . . . . . 10 {⟨∅, Σ𝑦 ∈ ∅ (𝐹𝑦)⟩, ⟨{𝐴}, Σ𝑦 ∈ {𝐴} (𝐹𝑦)⟩} = (𝑥 ∈ {∅, {𝐴}} ↦ Σ𝑦𝑥 (𝐹𝑦))
9998eqcomi 2660 . . . . . . . . 9 (𝑥 ∈ {∅, {𝐴}} ↦ Σ𝑦𝑥 (𝐹𝑦)) = {⟨∅, Σ𝑦 ∈ ∅ (𝐹𝑦)⟩, ⟨{𝐴}, Σ𝑦 ∈ {𝐴} (𝐹𝑦)⟩}
10085, 99eqtri 2673 . . . . . . . 8 (𝑥 ∈ (𝒫 {𝐴} ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) = {⟨∅, Σ𝑦 ∈ ∅ (𝐹𝑦)⟩, ⟨{𝐴}, Σ𝑦 ∈ {𝐴} (𝐹𝑦)⟩}
101100rneqi 5384 . . . . . . 7 ran (𝑥 ∈ (𝒫 {𝐴} ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) = ran {⟨∅, Σ𝑦 ∈ ∅ (𝐹𝑦)⟩, ⟨{𝐴}, Σ𝑦 ∈ {𝐴} (𝐹𝑦)⟩}
102 rnpropg 5651 . . . . . . . 8 ((∅ ∈ V ∧ {𝐴} ∈ V) → ran {⟨∅, Σ𝑦 ∈ ∅ (𝐹𝑦)⟩, ⟨{𝐴}, Σ𝑦 ∈ {𝐴} (𝐹𝑦)⟩} = {Σ𝑦 ∈ ∅ (𝐹𝑦), Σ𝑦 ∈ {𝐴} (𝐹𝑦)})
10386, 1, 102mp2an 708 . . . . . . 7 ran {⟨∅, Σ𝑦 ∈ ∅ (𝐹𝑦)⟩, ⟨{𝐴}, Σ𝑦 ∈ {𝐴} (𝐹𝑦)⟩} = {Σ𝑦 ∈ ∅ (𝐹𝑦), Σ𝑦 ∈ {𝐴} (𝐹𝑦)}
104101, 103eqtri 2673 . . . . . 6 ran (𝑥 ∈ (𝒫 {𝐴} ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) = {Σ𝑦 ∈ ∅ (𝐹𝑦), Σ𝑦 ∈ {𝐴} (𝐹𝑦)}
105104supeq1i 8394 . . . . 5 sup(ran (𝑥 ∈ (𝒫 {𝐴} ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)), ℝ*, < ) = sup({Σ𝑦 ∈ ∅ (𝐹𝑦), Σ𝑦 ∈ {𝐴} (𝐹𝑦)}, ℝ*, < )
106105a1i 11 . . . 4 ((𝜑 ∧ ¬ (𝐹𝐴) = +∞) → sup(ran (𝑥 ∈ (𝒫 {𝐴} ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)), ℝ*, < ) = sup({Σ𝑦 ∈ ∅ (𝐹𝑦), Σ𝑦 ∈ {𝐴} (𝐹𝑦)}, ℝ*, < ))
10754, 73, 1063eqtr4d 2695 . . 3 ((𝜑 ∧ ¬ (𝐹𝐴) = +∞) → (𝐹𝐴) = sup(ran (𝑥 ∈ (𝒫 {𝐴} ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)), ℝ*, < ))
10836, 107eqtr4d 2688 . 2 ((𝜑 ∧ ¬ (𝐹𝐴) = +∞) → (Σ^𝐹) = (𝐹𝐴))
10924, 108pm2.61dan 849 1 (𝜑 → (Σ^𝐹) = (𝐹𝐴))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   ∧ w3a 1054   = wceq 1523  ⊤wtru 1524   ∈ wcel 2030  Vcvv 3231   ∩ cin 3606   ⊆ wss 3607  ∅c0 3948  ifcif 4119  𝒫 cpw 4191  {csn 4210  {cpr 4212  ⟨cop 4216   class class class wbr 4685   ↦ cmpt 4762   Or wor 5063  dom cdm 5143  ran crn 5144  Fun wfun 5920  ⟶wf 5922  ‘cfv 5926  (class class class)co 6690  Fincfn 7997  supcsup 8387  ℂcc 9972  ℝcr 9973  0cc0 9974  +∞cpnf 10109  ℝ*cxr 10111   < clt 10112   ≤ cle 10113  [,)cico 12215  [,]cicc 12216  Σcsu 14460  Σ^csumge0 40897 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-oi 8456  df-card 8803  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-z 11416  df-uz 11726  df-rp 11871  df-ico 12219  df-icc 12220  df-fz 12365  df-fzo 12505  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-clim 14263  df-sum 14461  df-sumge0 40898 This theorem is referenced by:  sge0snmpt  40918  sge0sup  40926  sge0snmptf  40972  caratheodorylem1  41061
 Copyright terms: Public domain W3C validator