# Metamath Proof Explorer

## Theorem esumpcvgval

Description: The value of the extended sum when the corresponding series sum is convergent. (Contributed by Thierry Arnoux, 31-Jul-2017)

Ref Expression
Hypotheses esumpcvgval.1 ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {A}\in \left[0,\mathrm{+\infty }\right)$
esumpcvgval.2 ${⊢}{k}={l}\to {A}={B}$
esumpcvgval.3 ${⊢}{\phi }\to \left({n}\in ℕ⟼\sum _{{k}=1}^{{n}}{A}\right)\in \mathrm{dom}⇝$
Assertion esumpcvgval ${⊢}{\phi }\to \underset{{k}\in ℕ}{{\sum }^{*}}{A}=\sum _{{k}\in ℕ}{A}$

### Proof

Step Hyp Ref Expression
1 esumpcvgval.1 ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {A}\in \left[0,\mathrm{+\infty }\right)$
2 esumpcvgval.2 ${⊢}{k}={l}\to {A}={B}$
3 esumpcvgval.3 ${⊢}{\phi }\to \left({n}\in ℕ⟼\sum _{{k}=1}^{{n}}{A}\right)\in \mathrm{dom}⇝$
4 xrltso ${⊢}<\mathrm{Or}{ℝ}^{*}$
5 4 a1i ${⊢}{\phi }\to <\mathrm{Or}{ℝ}^{*}$
6 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
7 1zzd ${⊢}{\phi }\to 1\in ℤ$
8 eqcom ${⊢}{k}={l}↔{l}={k}$
9 eqcom ${⊢}{A}={B}↔{B}={A}$
10 2 8 9 3imtr3i ${⊢}{l}={k}\to {B}={A}$
11 10 cbvmptv ${⊢}\left({l}\in ℕ⟼{B}\right)=\left({k}\in ℕ⟼{A}\right)$
12 1 11 fmptd ${⊢}{\phi }\to \left({l}\in ℕ⟼{B}\right):ℕ⟶\left[0,\mathrm{+\infty }\right)$
13 12 ffvelrnda ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left({l}\in ℕ⟼{B}\right)\left({x}\right)\in \left[0,\mathrm{+\infty }\right)$
14 elrege0 ${⊢}\left({l}\in ℕ⟼{B}\right)\left({x}\right)\in \left[0,\mathrm{+\infty }\right)↔\left(\left({l}\in ℕ⟼{B}\right)\left({x}\right)\in ℝ\wedge 0\le \left({l}\in ℕ⟼{B}\right)\left({x}\right)\right)$
15 14 simplbi ${⊢}\left({l}\in ℕ⟼{B}\right)\left({x}\right)\in \left[0,\mathrm{+\infty }\right)\to \left({l}\in ℕ⟼{B}\right)\left({x}\right)\in ℝ$
16 13 15 syl ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left({l}\in ℕ⟼{B}\right)\left({x}\right)\in ℝ$
17 6 7 16 serfre ${⊢}{\phi }\to seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right):ℕ⟶ℝ$
18 12 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({l}\in ℕ⟼{B}\right):ℕ⟶\left[0,\mathrm{+\infty }\right)$
19 simpr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {n}\in ℕ$
20 19 peano2nnd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {n}+1\in ℕ$
21 18 20 ffvelrnd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({l}\in ℕ⟼{B}\right)\left({n}+1\right)\in \left[0,\mathrm{+\infty }\right)$
22 elrege0 ${⊢}\left({l}\in ℕ⟼{B}\right)\left({n}+1\right)\in \left[0,\mathrm{+\infty }\right)↔\left(\left({l}\in ℕ⟼{B}\right)\left({n}+1\right)\in ℝ\wedge 0\le \left({l}\in ℕ⟼{B}\right)\left({n}+1\right)\right)$
23 22 simprbi ${⊢}\left({l}\in ℕ⟼{B}\right)\left({n}+1\right)\in \left[0,\mathrm{+\infty }\right)\to 0\le \left({l}\in ℕ⟼{B}\right)\left({n}+1\right)$
24 21 23 syl ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to 0\le \left({l}\in ℕ⟼{B}\right)\left({n}+1\right)$
25 17 ffvelrnda ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)\in ℝ$
26 22 simplbi ${⊢}\left({l}\in ℕ⟼{B}\right)\left({n}+1\right)\in \left[0,\mathrm{+\infty }\right)\to \left({l}\in ℕ⟼{B}\right)\left({n}+1\right)\in ℝ$
27 21 26 syl ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({l}\in ℕ⟼{B}\right)\left({n}+1\right)\in ℝ$
28 25 27 addge01d ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left(0\le \left({l}\in ℕ⟼{B}\right)\left({n}+1\right)↔seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)\le seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)+\left({l}\in ℕ⟼{B}\right)\left({n}+1\right)\right)$
29 24 28 mpbid ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)\le seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)+\left({l}\in ℕ⟼{B}\right)\left({n}+1\right)$
30 19 6 eleqtrdi ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {n}\in {ℤ}_{\ge 1}$
31 seqp1 ${⊢}{n}\in {ℤ}_{\ge 1}\to seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}+1\right)=seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)+\left({l}\in ℕ⟼{B}\right)\left({n}+1\right)$
32 30 31 syl ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}+1\right)=seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)+\left({l}\in ℕ⟼{B}\right)\left({n}+1\right)$
33 29 32 breqtrrd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)\le seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}+1\right)$
34 simpr ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {k}\in ℕ$
35 11 fvmpt2 ${⊢}\left({k}\in ℕ\wedge {A}\in \left[0,\mathrm{+\infty }\right)\right)\to \left({l}\in ℕ⟼{B}\right)\left({k}\right)={A}$
36 34 1 35 syl2anc ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to \left({l}\in ℕ⟼{B}\right)\left({k}\right)={A}$
37 rge0ssre ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq ℝ$
38 37 1 sseldi ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {A}\in ℝ$
39 17 feqmptd ${⊢}{\phi }\to seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)=\left({n}\in ℕ⟼seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)\right)$
40 simpll ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {k}\in \left(1\dots {n}\right)\right)\to {\phi }$
41 elfznn ${⊢}{k}\in \left(1\dots {n}\right)\to {k}\in ℕ$
42 41 adantl ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {k}\in \left(1\dots {n}\right)\right)\to {k}\in ℕ$
43 40 42 36 syl2anc ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {k}\in \left(1\dots {n}\right)\right)\to \left({l}\in ℕ⟼{B}\right)\left({k}\right)={A}$
44 38 recnd ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {A}\in ℂ$
45 40 42 44 syl2anc ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {k}\in \left(1\dots {n}\right)\right)\to {A}\in ℂ$
46 43 30 45 fsumser ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \sum _{{k}=1}^{{n}}{A}=seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)$
47 46 eqcomd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)=\sum _{{k}=1}^{{n}}{A}$
48 47 mpteq2dva ${⊢}{\phi }\to \left({n}\in ℕ⟼seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)\right)=\left({n}\in ℕ⟼\sum _{{k}=1}^{{n}}{A}\right)$
49 39 48 eqtr2d ${⊢}{\phi }\to \left({n}\in ℕ⟼\sum _{{k}=1}^{{n}}{A}\right)=seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)$
50 49 3 eqeltrrd ${⊢}{\phi }\to seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\in \mathrm{dom}⇝$
51 6 7 36 38 50 isumrecl ${⊢}{\phi }\to \sum _{{k}\in ℕ}{A}\in ℝ$
52 1zzd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to 1\in ℤ$
53 fzfid ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left(1\dots {n}\right)\in \mathrm{Fin}$
54 fzssuz ${⊢}\left(1\dots {n}\right)\subseteq {ℤ}_{\ge 1}$
55 54 6 sseqtrri ${⊢}\left(1\dots {n}\right)\subseteq ℕ$
56 55 a1i ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left(1\dots {n}\right)\subseteq ℕ$
57 36 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {k}\in ℕ\right)\to \left({l}\in ℕ⟼{B}\right)\left({k}\right)={A}$
58 38 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {k}\in ℕ\right)\to {A}\in ℝ$
59 1 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {k}\in ℕ\right)\to {A}\in \left[0,\mathrm{+\infty }\right)$
60 elrege0 ${⊢}{A}\in \left[0,\mathrm{+\infty }\right)↔\left({A}\in ℝ\wedge 0\le {A}\right)$
61 60 simprbi ${⊢}{A}\in \left[0,\mathrm{+\infty }\right)\to 0\le {A}$
62 59 61 syl ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {k}\in ℕ\right)\to 0\le {A}$
63 50 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\in \mathrm{dom}⇝$
64 6 52 53 56 57 58 62 63 isumless ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \sum _{{k}=1}^{{n}}{A}\le \sum _{{k}\in ℕ}{A}$
65 46 64 eqbrtrrd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)\le \sum _{{k}\in ℕ}{A}$
66 65 ralrimiva ${⊢}{\phi }\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)\le \sum _{{k}\in ℕ}{A}$
67 brralrspcev ${⊢}\left(\sum _{{k}\in ℕ}{A}\in ℝ\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)\le \sum _{{k}\in ℕ}{A}\right)\to \exists {s}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)\le {s}$
68 51 66 67 syl2anc ${⊢}{\phi }\to \exists {s}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)\le {s}$
69 6 7 17 33 68 climsup ${⊢}{\phi }\to seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)⇝sup\left(\mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right),ℝ,<\right)$
70 6 7 69 25 climrecl ${⊢}{\phi }\to sup\left(\mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right),ℝ,<\right)\in ℝ$
71 70 rexrd ${⊢}{\phi }\to sup\left(\mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right),ℝ,<\right)\in {ℝ}^{*}$
72 eqid ${⊢}\left({b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {b}}{A}\right)=\left({b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {b}}{A}\right)$
73 sumex ${⊢}\sum _{{k}\in {b}}{A}\in \mathrm{V}$
74 72 73 elrnmpti ${⊢}{x}\in \mathrm{ran}\left({b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {b}}{A}\right)↔\exists {b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{x}=\sum _{{k}\in {b}}{A}$
75 ssnnssfz ${⊢}{b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)\to \exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}{b}\subseteq \left(1\dots {m}\right)$
76 fzfid ${⊢}\left({\phi }\wedge {b}\subseteq \left(1\dots {m}\right)\right)\to \left(1\dots {m}\right)\in \mathrm{Fin}$
77 elfznn ${⊢}{k}\in \left(1\dots {m}\right)\to {k}\in ℕ$
78 77 1 sylan2 ${⊢}\left({\phi }\wedge {k}\in \left(1\dots {m}\right)\right)\to {A}\in \left[0,\mathrm{+\infty }\right)$
79 60 simplbi ${⊢}{A}\in \left[0,\mathrm{+\infty }\right)\to {A}\in ℝ$
80 78 79 syl ${⊢}\left({\phi }\wedge {k}\in \left(1\dots {m}\right)\right)\to {A}\in ℝ$
81 80 adantlr ${⊢}\left(\left({\phi }\wedge {b}\subseteq \left(1\dots {m}\right)\right)\wedge {k}\in \left(1\dots {m}\right)\right)\to {A}\in ℝ$
82 78 61 syl ${⊢}\left({\phi }\wedge {k}\in \left(1\dots {m}\right)\right)\to 0\le {A}$
83 82 adantlr ${⊢}\left(\left({\phi }\wedge {b}\subseteq \left(1\dots {m}\right)\right)\wedge {k}\in \left(1\dots {m}\right)\right)\to 0\le {A}$
84 simpr ${⊢}\left({\phi }\wedge {b}\subseteq \left(1\dots {m}\right)\right)\to {b}\subseteq \left(1\dots {m}\right)$
85 76 81 83 84 fsumless ${⊢}\left({\phi }\wedge {b}\subseteq \left(1\dots {m}\right)\right)\to \sum _{{k}\in {b}}{A}\le \sum _{{k}=1}^{{m}}{A}$
86 85 ex ${⊢}{\phi }\to \left({b}\subseteq \left(1\dots {m}\right)\to \sum _{{k}\in {b}}{A}\le \sum _{{k}=1}^{{m}}{A}\right)$
87 86 reximdv ${⊢}{\phi }\to \left(\exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}{b}\subseteq \left(1\dots {m}\right)\to \exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}\sum _{{k}\in {b}}{A}\le \sum _{{k}=1}^{{m}}{A}\right)$
88 87 imp ${⊢}\left({\phi }\wedge \exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}{b}\subseteq \left(1\dots {m}\right)\right)\to \exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}\sum _{{k}\in {b}}{A}\le \sum _{{k}=1}^{{m}}{A}$
89 75 88 sylan2 ${⊢}\left({\phi }\wedge {b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)\right)\to \exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}\sum _{{k}\in {b}}{A}\le \sum _{{k}=1}^{{m}}{A}$
90 breq1 ${⊢}{x}=\sum _{{k}\in {b}}{A}\to \left({x}\le \sum _{{k}=1}^{{m}}{A}↔\sum _{{k}\in {b}}{A}\le \sum _{{k}=1}^{{m}}{A}\right)$
91 90 rexbidv ${⊢}{x}=\sum _{{k}\in {b}}{A}\to \left(\exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}{x}\le \sum _{{k}=1}^{{m}}{A}↔\exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}\sum _{{k}\in {b}}{A}\le \sum _{{k}=1}^{{m}}{A}\right)$
92 89 91 syl5ibrcom ${⊢}\left({\phi }\wedge {b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)\right)\to \left({x}=\sum _{{k}\in {b}}{A}\to \exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}{x}\le \sum _{{k}=1}^{{m}}{A}\right)$
93 92 rexlimdva ${⊢}{\phi }\to \left(\exists {b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{x}=\sum _{{k}\in {b}}{A}\to \exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}{x}\le \sum _{{k}=1}^{{m}}{A}\right)$
94 93 imp ${⊢}\left({\phi }\wedge \exists {b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{x}=\sum _{{k}\in {b}}{A}\right)\to \exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}{x}\le \sum _{{k}=1}^{{m}}{A}$
95 74 94 sylan2b ${⊢}\left({\phi }\wedge {x}\in \mathrm{ran}\left({b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {b}}{A}\right)\right)\to \exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}{x}\le \sum _{{k}=1}^{{m}}{A}$
96 simpr ${⊢}\left(\left({\phi }\wedge {b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)\right)\wedge {x}=\sum _{{k}\in {b}}{A}\right)\to {x}=\sum _{{k}\in {b}}{A}$
97 inss2 ${⊢}𝒫ℕ\cap \mathrm{Fin}\subseteq \mathrm{Fin}$
98 simpr ${⊢}\left({\phi }\wedge {b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)\right)\to {b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)$
99 97 98 sseldi ${⊢}\left({\phi }\wedge {b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)\right)\to {b}\in \mathrm{Fin}$
100 simpll ${⊢}\left(\left({\phi }\wedge {b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)\right)\wedge {k}\in {b}\right)\to {\phi }$
101 inss1 ${⊢}𝒫ℕ\cap \mathrm{Fin}\subseteq 𝒫ℕ$
102 simplr ${⊢}\left(\left({\phi }\wedge {b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)\right)\wedge {k}\in {b}\right)\to {b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)$
103 101 102 sseldi ${⊢}\left(\left({\phi }\wedge {b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)\right)\wedge {k}\in {b}\right)\to {b}\in 𝒫ℕ$
104 103 elpwid ${⊢}\left(\left({\phi }\wedge {b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)\right)\wedge {k}\in {b}\right)\to {b}\subseteq ℕ$
105 simpr ${⊢}\left(\left({\phi }\wedge {b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)\right)\wedge {k}\in {b}\right)\to {k}\in {b}$
106 104 105 sseldd ${⊢}\left(\left({\phi }\wedge {b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)\right)\wedge {k}\in {b}\right)\to {k}\in ℕ$
107 100 106 1 syl2anc ${⊢}\left(\left({\phi }\wedge {b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)\right)\wedge {k}\in {b}\right)\to {A}\in \left[0,\mathrm{+\infty }\right)$
108 107 79 syl ${⊢}\left(\left({\phi }\wedge {b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)\right)\wedge {k}\in {b}\right)\to {A}\in ℝ$
109 99 108 fsumrecl ${⊢}\left({\phi }\wedge {b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)\right)\to \sum _{{k}\in {b}}{A}\in ℝ$
110 109 adantr ${⊢}\left(\left({\phi }\wedge {b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)\right)\wedge {x}=\sum _{{k}\in {b}}{A}\right)\to \sum _{{k}\in {b}}{A}\in ℝ$
111 96 110 eqeltrd ${⊢}\left(\left({\phi }\wedge {b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)\right)\wedge {x}=\sum _{{k}\in {b}}{A}\right)\to {x}\in ℝ$
112 111 r19.29an ${⊢}\left({\phi }\wedge \exists {b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{x}=\sum _{{k}\in {b}}{A}\right)\to {x}\in ℝ$
113 74 112 sylan2b ${⊢}\left({\phi }\wedge {x}\in \mathrm{ran}\left({b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {b}}{A}\right)\right)\to {x}\in ℝ$
114 113 adantr ${⊢}\left(\left({\phi }\wedge {x}\in \mathrm{ran}\left({b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {b}}{A}\right)\right)\wedge \left({m}\in ℕ\wedge {x}\le \sum _{{k}=1}^{{m}}{A}\right)\right)\to {x}\in ℝ$
115 fzfid ${⊢}{\phi }\to \left(1\dots {m}\right)\in \mathrm{Fin}$
116 115 80 fsumrecl ${⊢}{\phi }\to \sum _{{k}=1}^{{m}}{A}\in ℝ$
117 116 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in \mathrm{ran}\left({b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {b}}{A}\right)\right)\wedge \left({m}\in ℕ\wedge {x}\le \sum _{{k}=1}^{{m}}{A}\right)\right)\to \sum _{{k}=1}^{{m}}{A}\in ℝ$
118 70 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in \mathrm{ran}\left({b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {b}}{A}\right)\right)\wedge \left({m}\in ℕ\wedge {x}\le \sum _{{k}=1}^{{m}}{A}\right)\right)\to sup\left(\mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right),ℝ,<\right)\in ℝ$
119 simprr ${⊢}\left(\left({\phi }\wedge {x}\in \mathrm{ran}\left({b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {b}}{A}\right)\right)\wedge \left({m}\in ℕ\wedge {x}\le \sum _{{k}=1}^{{m}}{A}\right)\right)\to {x}\le \sum _{{k}=1}^{{m}}{A}$
120 17 frnd ${⊢}{\phi }\to \mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\subseteq ℝ$
121 120 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in \mathrm{ran}\left({b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {b}}{A}\right)\right)\wedge \left({m}\in ℕ\wedge {x}\le \sum _{{k}=1}^{{m}}{A}\right)\right)\to \mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\subseteq ℝ$
122 1nn ${⊢}1\in ℕ$
123 122 ne0ii ${⊢}ℕ\ne \varnothing$
124 dm0rn0 ${⊢}\mathrm{dom}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)=\varnothing ↔\mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)=\varnothing$
125 17 fdmd ${⊢}{\phi }\to \mathrm{dom}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)=ℕ$
126 125 eqeq1d ${⊢}{\phi }\to \left(\mathrm{dom}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)=\varnothing ↔ℕ=\varnothing \right)$
127 124 126 syl5bbr ${⊢}{\phi }\to \left(\mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)=\varnothing ↔ℕ=\varnothing \right)$
128 127 necon3bid ${⊢}{\phi }\to \left(\mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\ne \varnothing ↔ℕ\ne \varnothing \right)$
129 123 128 mpbiri ${⊢}{\phi }\to \mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\ne \varnothing$
130 129 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in \mathrm{ran}\left({b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {b}}{A}\right)\right)\wedge \left({m}\in ℕ\wedge {x}\le \sum _{{k}=1}^{{m}}{A}\right)\right)\to \mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\ne \varnothing$
131 1z ${⊢}1\in ℤ$
132 seqfn ${⊢}1\in ℤ\to seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)Fn{ℤ}_{\ge 1}$
133 131 132 ax-mp ${⊢}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)Fn{ℤ}_{\ge 1}$
134 6 fneq2i ${⊢}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)Fnℕ↔seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)Fn{ℤ}_{\ge 1}$
135 133 134 mpbir ${⊢}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)Fnℕ$
136 dffn5 ${⊢}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)Fnℕ↔seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)=\left({n}\in ℕ⟼seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)\right)$
137 135 136 mpbi ${⊢}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)=\left({n}\in ℕ⟼seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)\right)$
138 fvex ${⊢}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)\in \mathrm{V}$
139 137 138 elrnmpti ${⊢}{z}\in \mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)↔\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{z}=seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)$
140 r19.29 ${⊢}\left(\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)\le {s}\wedge \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{z}=seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)\right)\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)\le {s}\wedge {z}=seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)\right)$
141 breq1 ${⊢}{z}=seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)\to \left({z}\le {s}↔seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)\le {s}\right)$
142 141 biimparc ${⊢}\left(seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)\le {s}\wedge {z}=seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)\right)\to {z}\le {s}$
143 142 rexlimivw ${⊢}\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)\le {s}\wedge {z}=seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)\right)\to {z}\le {s}$
144 140 143 syl ${⊢}\left(\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)\le {s}\wedge \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{z}=seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)\right)\to {z}\le {s}$
145 139 144 sylan2b ${⊢}\left(\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)\le {s}\wedge {z}\in \mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\right)\to {z}\le {s}$
146 145 ralrimiva ${⊢}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)\le {s}\to \forall {z}\in \mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\phantom{\rule{.4em}{0ex}}{z}\le {s}$
147 146 reximi ${⊢}\exists {s}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)\le {s}\to \exists {s}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\phantom{\rule{.4em}{0ex}}{z}\le {s}$
148 68 147 syl ${⊢}{\phi }\to \exists {s}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\phantom{\rule{.4em}{0ex}}{z}\le {s}$
149 148 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in \mathrm{ran}\left({b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {b}}{A}\right)\right)\wedge \left({m}\in ℕ\wedge {x}\le \sum _{{k}=1}^{{m}}{A}\right)\right)\to \exists {s}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\phantom{\rule{.4em}{0ex}}{z}\le {s}$
150 simpr ${⊢}\left({\phi }\wedge {m}\in ℕ\right)\to {m}\in ℕ$
151 simpll ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge {k}\in \left(1\dots {m}\right)\right)\to {\phi }$
152 77 adantl ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge {k}\in \left(1\dots {m}\right)\right)\to {k}\in ℕ$
153 151 152 36 syl2anc ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge {k}\in \left(1\dots {m}\right)\right)\to \left({l}\in ℕ⟼{B}\right)\left({k}\right)={A}$
154 150 6 eleqtrdi ${⊢}\left({\phi }\wedge {m}\in ℕ\right)\to {m}\in {ℤ}_{\ge 1}$
155 151 152 1 syl2anc ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge {k}\in \left(1\dots {m}\right)\right)\to {A}\in \left[0,\mathrm{+\infty }\right)$
156 155 79 syl ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge {k}\in \left(1\dots {m}\right)\right)\to {A}\in ℝ$
157 156 recnd ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge {k}\in \left(1\dots {m}\right)\right)\to {A}\in ℂ$
158 153 154 157 fsumser ${⊢}\left({\phi }\wedge {m}\in ℕ\right)\to \sum _{{k}=1}^{{m}}{A}=seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({m}\right)$
159 fveq2 ${⊢}{n}={m}\to seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)=seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({m}\right)$
160 159 rspceeqv ${⊢}\left({m}\in ℕ\wedge \sum _{{k}=1}^{{m}}{A}=seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({m}\right)\right)\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\sum _{{k}=1}^{{m}}{A}=seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)$
161 150 158 160 syl2anc ${⊢}\left({\phi }\wedge {m}\in ℕ\right)\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\sum _{{k}=1}^{{m}}{A}=seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)$
162 137 138 elrnmpti ${⊢}\sum _{{k}=1}^{{m}}{A}\in \mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)↔\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\sum _{{k}=1}^{{m}}{A}=seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)$
163 161 162 sylibr ${⊢}\left({\phi }\wedge {m}\in ℕ\right)\to \sum _{{k}=1}^{{m}}{A}\in \mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)$
164 163 ad2ant2r ${⊢}\left(\left({\phi }\wedge {x}\in \mathrm{ran}\left({b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {b}}{A}\right)\right)\wedge \left({m}\in ℕ\wedge {x}\le \sum _{{k}=1}^{{m}}{A}\right)\right)\to \sum _{{k}=1}^{{m}}{A}\in \mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)$
165 suprub ${⊢}\left(\left(\mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\subseteq ℝ\wedge \mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\ne \varnothing \wedge \exists {s}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\phantom{\rule{.4em}{0ex}}{z}\le {s}\right)\wedge \sum _{{k}=1}^{{m}}{A}\in \mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\right)\to \sum _{{k}=1}^{{m}}{A}\le sup\left(\mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right),ℝ,<\right)$
166 121 130 149 164 165 syl31anc ${⊢}\left(\left({\phi }\wedge {x}\in \mathrm{ran}\left({b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {b}}{A}\right)\right)\wedge \left({m}\in ℕ\wedge {x}\le \sum _{{k}=1}^{{m}}{A}\right)\right)\to \sum _{{k}=1}^{{m}}{A}\le sup\left(\mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right),ℝ,<\right)$
167 114 117 118 119 166 letrd ${⊢}\left(\left({\phi }\wedge {x}\in \mathrm{ran}\left({b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {b}}{A}\right)\right)\wedge \left({m}\in ℕ\wedge {x}\le \sum _{{k}=1}^{{m}}{A}\right)\right)\to {x}\le sup\left(\mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right),ℝ,<\right)$
168 95 167 rexlimddv ${⊢}\left({\phi }\wedge {x}\in \mathrm{ran}\left({b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {b}}{A}\right)\right)\to {x}\le sup\left(\mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right),ℝ,<\right)$
169 70 adantr ${⊢}\left({\phi }\wedge {x}\in \mathrm{ran}\left({b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {b}}{A}\right)\right)\to sup\left(\mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right),ℝ,<\right)\in ℝ$
170 113 169 lenltd ${⊢}\left({\phi }\wedge {x}\in \mathrm{ran}\left({b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {b}}{A}\right)\right)\to \left({x}\le sup\left(\mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right),ℝ,<\right)↔¬sup\left(\mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right),ℝ,<\right)<{x}\right)$
171 168 170 mpbid ${⊢}\left({\phi }\wedge {x}\in \mathrm{ran}\left({b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {b}}{A}\right)\right)\to ¬sup\left(\mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right),ℝ,<\right)<{x}$
172 simpr1r ${⊢}\left({\phi }\wedge \left(\left({x}\in {ℝ}^{*}\wedge {x}
173 172 3anassrs ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {x}
174 71 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {x}
175 pnfnlt ${⊢}sup\left(\mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right),ℝ,<\right)\in {ℝ}^{*}\to ¬\mathrm{+\infty }
176 174 175 syl ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {x}
177 breq1 ${⊢}{x}=\mathrm{+\infty }\to \left({x}
178 177 notbid ${⊢}{x}=\mathrm{+\infty }\to \left(¬{x}
179 178 adantl ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {x}
180 176 179 mpbird ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {x}
181 173 180 pm2.21dd ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {x}
182 simplll ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {x}
183 simpr1l ${⊢}\left({\phi }\wedge \left(\left({x}\in {ℝ}^{*}\wedge {x}
184 183 3anassrs ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {x}
185 simplr ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {x}
186 simpr ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {x}
187 0xr ${⊢}0\in {ℝ}^{*}$
188 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
189 elico1 ${⊢}\left(0\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)\to \left({x}\in \left[0,\mathrm{+\infty }\right)↔\left({x}\in {ℝ}^{*}\wedge 0\le {x}\wedge {x}<\mathrm{+\infty }\right)\right)$
190 187 188 189 mp2an ${⊢}{x}\in \left[0,\mathrm{+\infty }\right)↔\left({x}\in {ℝ}^{*}\wedge 0\le {x}\wedge {x}<\mathrm{+\infty }\right)$
191 184 185 186 190 syl3anbrc ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {x}
192 simpr1r ${⊢}\left({\phi }\wedge \left(\left({x}\in {ℝ}^{*}\wedge {x}
193 192 3anassrs ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {x}
194 120 adantr ${⊢}\left({\phi }\wedge \left({x}\in \left[0,\mathrm{+\infty }\right)\wedge {x}
195 129 adantr ${⊢}\left({\phi }\wedge \left({x}\in \left[0,\mathrm{+\infty }\right)\wedge {x}
196 148 adantr ${⊢}\left({\phi }\wedge \left({x}\in \left[0,\mathrm{+\infty }\right)\wedge {x}
197 194 195 196 3jca ${⊢}\left({\phi }\wedge \left({x}\in \left[0,\mathrm{+\infty }\right)\wedge {x}
198 simprl ${⊢}\left({\phi }\wedge \left({x}\in \left[0,\mathrm{+\infty }\right)\wedge {x}
199 37 198 sseldi ${⊢}\left({\phi }\wedge \left({x}\in \left[0,\mathrm{+\infty }\right)\wedge {x}
200 simprr ${⊢}\left({\phi }\wedge \left({x}\in \left[0,\mathrm{+\infty }\right)\wedge {x}
201 suprlub ${⊢}\left(\left(\mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\subseteq ℝ\wedge \mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\ne \varnothing \wedge \exists {s}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\phantom{\rule{.4em}{0ex}}{z}\le {s}\right)\wedge {x}\in ℝ\right)\to \left({x}
202 201 biimpa ${⊢}\left(\left(\left(\mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\subseteq ℝ\wedge \mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\ne \varnothing \wedge \exists {s}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\phantom{\rule{.4em}{0ex}}{z}\le {s}\right)\wedge {x}\in ℝ\right)\wedge {x}
203 197 199 200 202 syl21anc ${⊢}\left({\phi }\wedge \left({x}\in \left[0,\mathrm{+\infty }\right)\wedge {x}
204 41 ssriv ${⊢}\left(1\dots {n}\right)\subseteq ℕ$
205 ovex ${⊢}\left(1\dots {n}\right)\in \mathrm{V}$
206 205 elpw ${⊢}\left(1\dots {n}\right)\in 𝒫ℕ↔\left(1\dots {n}\right)\subseteq ℕ$
207 204 206 mpbir ${⊢}\left(1\dots {n}\right)\in 𝒫ℕ$
208 fzfi ${⊢}\left(1\dots {n}\right)\in \mathrm{Fin}$
209 elin ${⊢}\left(1\dots {n}\right)\in \left(𝒫ℕ\cap \mathrm{Fin}\right)↔\left(\left(1\dots {n}\right)\in 𝒫ℕ\wedge \left(1\dots {n}\right)\in \mathrm{Fin}\right)$
210 207 208 209 mpbir2an ${⊢}\left(1\dots {n}\right)\in \left(𝒫ℕ\cap \mathrm{Fin}\right)$
211 210 a1i ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {y}=seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)\right)\to \left(1\dots {n}\right)\in \left(𝒫ℕ\cap \mathrm{Fin}\right)$
212 simpr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {y}=seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)\right)\to {y}=seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)$
213 46 adantr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {y}=seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)\right)\to \sum _{{k}=1}^{{n}}{A}=seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)$
214 212 213 eqtr4d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {y}=seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)\right)\to {y}=\sum _{{k}=1}^{{n}}{A}$
215 sumeq1 ${⊢}{b}=\left(1\dots {n}\right)\to \sum _{{k}\in {b}}{A}=\sum _{{k}=1}^{{n}}{A}$
216 215 rspceeqv ${⊢}\left(\left(1\dots {n}\right)\in \left(𝒫ℕ\cap \mathrm{Fin}\right)\wedge {y}=\sum _{{k}=1}^{{n}}{A}\right)\to \exists {b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{y}=\sum _{{k}\in {b}}{A}$
217 211 214 216 syl2anc ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {y}=seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)\right)\to \exists {b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{y}=\sum _{{k}\in {b}}{A}$
218 217 ex ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({y}=seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)\to \exists {b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{y}=\sum _{{k}\in {b}}{A}\right)$
219 218 rexlimdva ${⊢}{\phi }\to \left(\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{y}=seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)\to \exists {b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{y}=\sum _{{k}\in {b}}{A}\right)$
220 137 138 elrnmpti ${⊢}{y}\in \mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)↔\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{y}=seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\left({n}\right)$
221 72 73 elrnmpti ${⊢}{y}\in \mathrm{ran}\left({b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {b}}{A}\right)↔\exists {b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{y}=\sum _{{k}\in {b}}{A}$
222 219 220 221 3imtr4g ${⊢}{\phi }\to \left({y}\in \mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\to {y}\in \mathrm{ran}\left({b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {b}}{A}\right)\right)$
223 222 ssrdv ${⊢}{\phi }\to \mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\subseteq \mathrm{ran}\left({b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {b}}{A}\right)$
224 ssrexv ${⊢}\mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\subseteq \mathrm{ran}\left({b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {b}}{A}\right)\to \left(\exists {y}\in \mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\phantom{\rule{.4em}{0ex}}{x}<{y}\to \exists {y}\in \mathrm{ran}\left({b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {b}}{A}\right)\phantom{\rule{.4em}{0ex}}{x}<{y}\right)$
225 223 224 syl ${⊢}{\phi }\to \left(\exists {y}\in \mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\phantom{\rule{.4em}{0ex}}{x}<{y}\to \exists {y}\in \mathrm{ran}\left({b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {b}}{A}\right)\phantom{\rule{.4em}{0ex}}{x}<{y}\right)$
226 225 imp ${⊢}\left({\phi }\wedge \exists {y}\in \mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right)\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\to \exists {y}\in \mathrm{ran}\left({b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {b}}{A}\right)\phantom{\rule{.4em}{0ex}}{x}<{y}$
227 203 226 syldan ${⊢}\left({\phi }\wedge \left({x}\in \left[0,\mathrm{+\infty }\right)\wedge {x}
228 182 191 193 227 syl12anc ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {x}
229 simplrl ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {x}
230 xrlelttric ${⊢}\left(\mathrm{+\infty }\in {ℝ}^{*}\wedge {x}\in {ℝ}^{*}\right)\to \left(\mathrm{+\infty }\le {x}\vee {x}<\mathrm{+\infty }\right)$
231 188 230 mpan ${⊢}{x}\in {ℝ}^{*}\to \left(\mathrm{+\infty }\le {x}\vee {x}<\mathrm{+\infty }\right)$
232 xgepnf ${⊢}{x}\in {ℝ}^{*}\to \left(\mathrm{+\infty }\le {x}↔{x}=\mathrm{+\infty }\right)$
233 232 orbi1d ${⊢}{x}\in {ℝ}^{*}\to \left(\left(\mathrm{+\infty }\le {x}\vee {x}<\mathrm{+\infty }\right)↔\left({x}=\mathrm{+\infty }\vee {x}<\mathrm{+\infty }\right)\right)$
234 231 233 mpbid ${⊢}{x}\in {ℝ}^{*}\to \left({x}=\mathrm{+\infty }\vee {x}<\mathrm{+\infty }\right)$
235 229 234 syl ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {x}
236 181 228 235 mpjaodan ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {x}
237 0elpw ${⊢}\varnothing \in 𝒫ℕ$
238 0fin ${⊢}\varnothing \in \mathrm{Fin}$
239 elin ${⊢}\varnothing \in \left(𝒫ℕ\cap \mathrm{Fin}\right)↔\left(\varnothing \in 𝒫ℕ\wedge \varnothing \in \mathrm{Fin}\right)$
240 237 238 239 mpbir2an ${⊢}\varnothing \in \left(𝒫ℕ\cap \mathrm{Fin}\right)$
241 sum0 ${⊢}\sum _{{k}\in \varnothing }{A}=0$
242 241 eqcomi ${⊢}0=\sum _{{k}\in \varnothing }{A}$
243 sumeq1 ${⊢}{b}=\varnothing \to \sum _{{k}\in {b}}{A}=\sum _{{k}\in \varnothing }{A}$
244 243 rspceeqv ${⊢}\left(\varnothing \in \left(𝒫ℕ\cap \mathrm{Fin}\right)\wedge 0=\sum _{{k}\in \varnothing }{A}\right)\to \exists {b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}0=\sum _{{k}\in {b}}{A}$
245 240 242 244 mp2an ${⊢}\exists {b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}0=\sum _{{k}\in {b}}{A}$
246 72 73 elrnmpti ${⊢}0\in \mathrm{ran}\left({b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {b}}{A}\right)↔\exists {b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}0=\sum _{{k}\in {b}}{A}$
247 245 246 mpbir ${⊢}0\in \mathrm{ran}\left({b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {b}}{A}\right)$
248 breq2 ${⊢}{y}=0\to \left({x}<{y}↔{x}<0\right)$
249 248 rspcev ${⊢}\left(0\in \mathrm{ran}\left({b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {b}}{A}\right)\wedge {x}<0\right)\to \exists {y}\in \mathrm{ran}\left({b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {b}}{A}\right)\phantom{\rule{.4em}{0ex}}{x}<{y}$
250 247 249 mpan ${⊢}{x}<0\to \exists {y}\in \mathrm{ran}\left({b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {b}}{A}\right)\phantom{\rule{.4em}{0ex}}{x}<{y}$
251 250 adantl ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {x}
252 xrlelttric ${⊢}\left(0\in {ℝ}^{*}\wedge {x}\in {ℝ}^{*}\right)\to \left(0\le {x}\vee {x}<0\right)$
253 187 252 mpan ${⊢}{x}\in {ℝ}^{*}\to \left(0\le {x}\vee {x}<0\right)$
254 253 ad2antrl ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {x}
255 236 251 254 mpjaodan ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {x}
256 5 71 171 255 eqsupd ${⊢}{\phi }\to sup\left(\mathrm{ran}\left({b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {b}}{A}\right),{ℝ}^{*},<\right)=sup\left(\mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right),ℝ,<\right)$
257 nfv ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
258 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}ℕ$
259 nnex ${⊢}ℕ\in \mathrm{V}$
260 259 a1i ${⊢}{\phi }\to ℕ\in \mathrm{V}$
261 icossicc ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq \left[0,\mathrm{+\infty }\right]$
262 261 1 sseldi ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {A}\in \left[0,\mathrm{+\infty }\right]$
263 elex ${⊢}{b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)\to {b}\in \mathrm{V}$
264 263 adantl ${⊢}\left({\phi }\wedge {b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)\right)\to {b}\in \mathrm{V}$
265 107 fmpttd ${⊢}\left({\phi }\wedge {b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)\right)\to \left({k}\in {b}⟼{A}\right):{b}⟶\left[0,\mathrm{+\infty }\right)$
266 esumpfinvallem ${⊢}\left({b}\in \mathrm{V}\wedge \left({k}\in {b}⟼{A}\right):{b}⟶\left[0,\mathrm{+\infty }\right)\right)\to \underset{{k}\in {b}}{{\sum }_{{ℂ}_{\mathrm{fld}}}}{A}=\underset{{k}\in {b}}{{\sum }_{{ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]}}{A}$
267 264 265 266 syl2anc ${⊢}\left({\phi }\wedge {b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)\right)\to \underset{{k}\in {b}}{{\sum }_{{ℂ}_{\mathrm{fld}}}}{A}=\underset{{k}\in {b}}{{\sum }_{{ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]}}{A}$
268 108 recnd ${⊢}\left(\left({\phi }\wedge {b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)\right)\wedge {k}\in {b}\right)\to {A}\in ℂ$
269 99 268 gsumfsum ${⊢}\left({\phi }\wedge {b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)\right)\to \underset{{k}\in {b}}{{\sum }_{{ℂ}_{\mathrm{fld}}}}{A}=\sum _{{k}\in {b}}{A}$
270 267 269 eqtr3d ${⊢}\left({\phi }\wedge {b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)\right)\to \underset{{k}\in {b}}{{\sum }_{{ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]}}{A}=\sum _{{k}\in {b}}{A}$
271 257 258 260 262 270 esumval ${⊢}{\phi }\to \underset{{k}\in ℕ}{{\sum }^{*}}{A}=sup\left(\mathrm{ran}\left({b}\in \left(𝒫ℕ\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {b}}{A}\right),{ℝ}^{*},<\right)$
272 6 7 36 44 69 isumclim ${⊢}{\phi }\to \sum _{{k}\in ℕ}{A}=sup\left(\mathrm{ran}seq1\left(+,\left({l}\in ℕ⟼{B}\right)\right),ℝ,<\right)$
273 256 271 272 3eqtr4d ${⊢}{\phi }\to \underset{{k}\in ℕ}{{\sum }^{*}}{A}=\sum _{{k}\in ℕ}{A}$