Metamath Proof Explorer


Theorem esumval

Description: Develop the value of the extended sum. (Contributed by Thierry Arnoux, 4-Jan-2017)

Ref Expression
Hypotheses esumval.p k φ
esumval.0 _ k A
esumval.1 φ A V
esumval.2 φ k A B 0 +∞
esumval.3 φ x 𝒫 A Fin 𝑠 * 𝑠 0 +∞ k x B = C
Assertion esumval φ * k A B = sup ran x 𝒫 A Fin C * <

Proof

Step Hyp Ref Expression
1 esumval.p k φ
2 esumval.0 _ k A
3 esumval.1 φ A V
4 esumval.2 φ k A B 0 +∞
5 esumval.3 φ x 𝒫 A Fin 𝑠 * 𝑠 0 +∞ k x B = C
6 df-esum * k A B = 𝑠 * 𝑠 0 +∞ tsums k A B
7 eqid 𝑠 * 𝑠 0 +∞ = 𝑠 * 𝑠 0 +∞
8 nfcv _ k 0 +∞
9 eqid k A B = k A B
10 1 2 8 4 9 fmptdF φ k A B : A 0 +∞
11 inss1 𝒫 A Fin 𝒫 A
12 11 sseli x 𝒫 A Fin x 𝒫 A
13 12 elpwid x 𝒫 A Fin x A
14 13 adantl φ x 𝒫 A Fin x A
15 nfcv _ k x
16 2 15 resmptf x A k A B x = k x B
17 14 16 syl φ x 𝒫 A Fin k A B x = k x B
18 17 oveq2d φ x 𝒫 A Fin 𝑠 * 𝑠 0 +∞ k A B x = 𝑠 * 𝑠 0 +∞ k x B
19 18 5 eqtr2d φ x 𝒫 A Fin C = 𝑠 * 𝑠 0 +∞ k A B x
20 19 mpteq2dva φ x 𝒫 A Fin C = x 𝒫 A Fin 𝑠 * 𝑠 0 +∞ k A B x
21 20 rneqd φ ran x 𝒫 A Fin C = ran x 𝒫 A Fin 𝑠 * 𝑠 0 +∞ k A B x
22 21 supeq1d φ sup ran x 𝒫 A Fin C * < = sup ran x 𝒫 A Fin 𝑠 * 𝑠 0 +∞ k A B x * <
23 7 3 10 22 xrge0tsmsd φ 𝑠 * 𝑠 0 +∞ tsums k A B = sup ran x 𝒫 A Fin C * <
24 23 unieqd φ 𝑠 * 𝑠 0 +∞ tsums k A B = sup ran x 𝒫 A Fin C * <
25 6 24 syl5eq φ * k A B = sup ran x 𝒫 A Fin C * <
26 xrltso < Or *
27 26 supex sup ran x 𝒫 A Fin C * < V
28 27 unisn sup ran x 𝒫 A Fin C * < = sup ran x 𝒫 A Fin C * <
29 25 28 eqtrdi φ * k A B = sup ran x 𝒫 A Fin C * <