Metamath Proof Explorer

Theorem esum0

Description: Extended sum of zero. (Contributed by Thierry Arnoux, 3-Mar-2017)

Ref Expression
Hypothesis esum0.k ⊢ Ⅎ _ k A
Assertion esum0 ⊢ A ∈ V → ∑ * k ∈ A 0 = 0

Proof

Step Hyp Ref Expression
1 esum0.k ⊢ Ⅎ _ k A
2 1 nfel1 ⊢ Ⅎ k A ∈ V
3 id ⊢ A ∈ V → A ∈ V
4 0e0iccpnf ⊢ 0 ∈ 0 +∞
5 4 a1i ⊢ A ∈ V ∧ k ∈ A → 0 ∈ 0 +∞
6 xrge0cmn ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ CMnd
7 cmnmnd ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ CMnd → ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ Mnd
8 6 7 ax-mp ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ Mnd
9 vex ⊢ x ∈ V
10 xrge00 ⊢ 0 = 0 ℝ 𝑠 * ↾ 𝑠 0 +∞
11 10 gsumz ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ Mnd ∧ x ∈ V → ∑ ℝ 𝑠 * ↾ 𝑠 0 +∞ k ∈ x 0 = 0
12 8 9 11 mp2an ⊢ ∑ ℝ 𝑠 * ↾ 𝑠 0 +∞ k ∈ x 0 = 0
13 12 a1i ⊢ A ∈ V ∧ x ∈ 𝒫 A ∩ Fin → ∑ ℝ 𝑠 * ↾ 𝑠 0 +∞ k ∈ x 0 = 0
14 2 1 3 5 13 esumval ⊢ A ∈ V → ∑ * k ∈ A 0 = sup ran ⁡ x ∈ 𝒫 A ∩ Fin ⟼ 0 ℝ * <
15 fconstmpt ⊢ 𝒫 A ∩ Fin × 0 = x ∈ 𝒫 A ∩ Fin ⟼ 0
16 15 eqcomi ⊢ x ∈ 𝒫 A ∩ Fin ⟼ 0 = 𝒫 A ∩ Fin × 0
17 0xr ⊢ 0 ∈ ℝ *
18 17 rgenw ⊢ ∀ x ∈ 𝒫 A ∩ Fin 0 ∈ ℝ *
19 eqid ⊢ x ∈ 𝒫 A ∩ Fin ⟼ 0 = x ∈ 𝒫 A ∩ Fin ⟼ 0
20 19 fnmpt ⊢ ∀ x ∈ 𝒫 A ∩ Fin 0 ∈ ℝ * → x ∈ 𝒫 A ∩ Fin ⟼ 0 Fn 𝒫 A ∩ Fin
21 18 20 ax-mp ⊢ x ∈ 𝒫 A ∩ Fin ⟼ 0 Fn 𝒫 A ∩ Fin
22 0elpw ⊢ ∅ ∈ 𝒫 A
23 0fin ⊢ ∅ ∈ Fin
24 elin ⊢ ∅ ∈ 𝒫 A ∩ Fin ↔ ∅ ∈ 𝒫 A ∧ ∅ ∈ Fin
25 22 23 24 mpbir2an ⊢ ∅ ∈ 𝒫 A ∩ Fin
26 25 ne0ii ⊢ 𝒫 A ∩ Fin ≠ ∅
27 fconst5 ⊢ x ∈ 𝒫 A ∩ Fin ⟼ 0 Fn 𝒫 A ∩ Fin ∧ 𝒫 A ∩ Fin ≠ ∅ → x ∈ 𝒫 A ∩ Fin ⟼ 0 = 𝒫 A ∩ Fin × 0 ↔ ran ⁡ x ∈ 𝒫 A ∩ Fin ⟼ 0 = 0
28 21 26 27 mp2an ⊢ x ∈ 𝒫 A ∩ Fin ⟼ 0 = 𝒫 A ∩ Fin × 0 ↔ ran ⁡ x ∈ 𝒫 A ∩ Fin ⟼ 0 = 0
29 16 28 mpbi ⊢ ran ⁡ x ∈ 𝒫 A ∩ Fin ⟼ 0 = 0
30 29 a1i ⊢ A ∈ V → ran ⁡ x ∈ 𝒫 A ∩ Fin ⟼ 0 = 0
31 30 supeq1d ⊢ A ∈ V → sup ran ⁡ x ∈ 𝒫 A ∩ Fin ⟼ 0 ℝ * < = sup 0 ℝ * <
32 xrltso ⊢ < Or ℝ *
33 supsn ⊢ < Or ℝ * ∧ 0 ∈ ℝ * → sup 0 ℝ * < = 0
34 32 17 33 mp2an ⊢ sup 0 ℝ * < = 0
35 31 34 eqtrdi ⊢ A ∈ V → sup ran ⁡ x ∈ 𝒫 A ∩ Fin ⟼ 0 ℝ * < = 0
36 14 35 eqtrd ⊢ A ∈ V → ∑ * k ∈ A 0 = 0