Metamath Proof Explorer

Theorem esumnul

Description: Extended sum over the empty set. (Contributed by Thierry Arnoux, 19-Feb-2017)

Ref Expression
Assertion esumnul ⊢∑*x∈∅A=0

Proof

Step Hyp Ref Expression
1 nftru ⊢Ⅎx⊤
2 nfcv ⊢Ⅎ_x∅
3 0ex ⊢∅∈V
4 3 a1i ⊢⊤→∅∈V
5 ral0 ⊢∀x∈∅A∈0+∞
6 5 a1i ⊢⊤→∀x∈∅A∈0+∞
7 6 r19.21bi ⊢⊤∧x∈∅→A∈0+∞
8 pw0 ⊢𝒫∅=∅
9 8 ineq1i ⊢𝒫∅∩Fin=∅∩Fin
10 0fin ⊢∅∈Fin
11 snssi ⊢∅∈Fin→∅⊆Fin
12 df-ss ⊢∅⊆Fin↔∅∩Fin=∅
13 11 12 sylib ⊢∅∈Fin→∅∩Fin=∅
14 10 13 ax-mp ⊢∅∩Fin=∅
15 9 14 eqtri ⊢𝒫∅∩Fin=∅
16 15 eleq2i ⊢y∈𝒫∅∩Fin↔y∈∅
17 velsn ⊢y∈∅↔y=∅
18 16 17 sylbb ⊢y∈𝒫∅∩Fin→y=∅
19 18 mpteq1d ⊢y∈𝒫∅∩Fin→x∈y⟼A=x∈∅⟼A
20 mpt0 ⊢x∈∅⟼A=∅
21 19 20 eqtrdi ⊢y∈𝒫∅∩Fin→x∈y⟼A=∅
22 21 oveq2d ⊢y∈𝒫∅∩Fin→∑ℝ𝑠*↾𝑠0+∞x∈yA=∑ℝ𝑠*↾𝑠0+∞∅
23 xrge00 ⊢0=0ℝ𝑠*↾𝑠0+∞
24 23 gsum0 ⊢∑ℝ𝑠*↾𝑠0+∞∅=0
25 22 24 eqtrdi ⊢y∈𝒫∅∩Fin→∑ℝ𝑠*↾𝑠0+∞x∈yA=0
26 25 adantl ⊢⊤∧y∈𝒫∅∩Fin→∑ℝ𝑠*↾𝑠0+∞x∈yA=0
27 1 2 4 7 26 esumval ⊢⊤→∑*x∈∅A=supran⁡y∈𝒫∅∩Fin⟼0ℝ*<
28 27 mptru ⊢∑*x∈∅A=supran⁡y∈𝒫∅∩Fin⟼0ℝ*<
29 fconstmpt ⊢𝒫∅∩Fin×0=y∈𝒫∅∩Fin⟼0
30 29 eqcomi ⊢y∈𝒫∅∩Fin⟼0=𝒫∅∩Fin×0
31 0xr ⊢0∈ℝ*
32 31 rgenw ⊢∀y∈𝒫∅∩Fin0∈ℝ*
33 eqid ⊢y∈𝒫∅∩Fin⟼0=y∈𝒫∅∩Fin⟼0
34 33 fnmpt ⊢∀y∈𝒫∅∩Fin0∈ℝ*→y∈𝒫∅∩Fin⟼0Fn𝒫∅∩Fin
35 32 34 ax-mp ⊢y∈𝒫∅∩Fin⟼0Fn𝒫∅∩Fin
36 3 snnz ⊢∅≠∅
37 15 36 eqnetri ⊢𝒫∅∩Fin≠∅
38 fconst5 ⊢y∈𝒫∅∩Fin⟼0Fn𝒫∅∩Fin∧𝒫∅∩Fin≠∅→y∈𝒫∅∩Fin⟼0=𝒫∅∩Fin×0↔ran⁡y∈𝒫∅∩Fin⟼0=0
39 35 37 38 mp2an ⊢y∈𝒫∅∩Fin⟼0=𝒫∅∩Fin×0↔ran⁡y∈𝒫∅∩Fin⟼0=0
40 30 39 mpbi ⊢ran⁡y∈𝒫∅∩Fin⟼0=0
41 40 supeq1i ⊢supran⁡y∈𝒫∅∩Fin⟼0ℝ*<=sup0ℝ*<
42 xrltso ⊢<Orℝ*
43 supsn ⊢<Orℝ*∧0∈ℝ*→sup0ℝ*<=0
44 42 31 43 mp2an ⊢sup0ℝ*<=0
45 28 41 44 3eqtri ⊢∑*x∈∅A=0