Theorem esumcvg2

Description: Simpler version of esumcvg . (Contributed by Thierry Arnoux, 5-Sep-2017)

	Ref	Expression
Hypotheses	esumcvg2.j	$$⊢J=\mathrm{TopOpen}\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)$$
	esumcvg2.a	$$⊢\left(\phi \wedge k\in \mathbb{N}\right)\to A\in \left[0,\mathrm{+\infty }\right]$$
	esumcvg2.l	$$⊢k=l\to A=B$$
	esumcvg2.m	$$⊢k=m\to A=C$$
Assertion	esumcvg2	$$⊢\phi \to \left(n\in \mathbb{N}⟼\underset{k=1}{\overset{n}{{\sum }^{*}}}A\right)\underset{t}{⇝}\left(J\right)\underset{k\in \mathbb{N}}{{\sum }^{*}}A$$

Proof

Step	Hyp	Ref	Expression
1		esumcvg2.j	$$⊢J=\mathrm{TopOpen}\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)$$
2		esumcvg2.a	$$⊢\left(\phi \wedge k\in \mathbb{N}\right)\to A\in \left[0,\mathrm{+\infty }\right]$$
3		esumcvg2.l	$$⊢k=l\to A=B$$
4		esumcvg2.m	$$⊢k=m\to A=C$$
5	4	cbvesumv	$$⊢\underset{k=1}{\overset{i}{{\sum }^{*}}}A=\underset{m=1}{\overset{i}{{\sum }^{*}}}C$$
6		oveq2	$$⊢i=n\to \left(1\dots i\right)=\left(1\dots n\right)$$
7		esumeq1	$$⊢\left(1\dots i\right)=\left(1\dots n\right)\to \underset{k=1}{\overset{i}{{\sum }^{*}}}A=\underset{k=1}{\overset{n}{{\sum }^{*}}}A$$
8	6 7	syl	$$⊢i=n\to \underset{k=1}{\overset{i}{{\sum }^{*}}}A=\underset{k=1}{\overset{n}{{\sum }^{*}}}A$$
9	5 8	syl5eqr	$$⊢i=n\to \underset{m=1}{\overset{i}{{\sum }^{*}}}C=\underset{k=1}{\overset{n}{{\sum }^{*}}}A$$
10	9	cbvmptv	$$⊢\left(i\in \mathbb{N}⟼\underset{m=1}{\overset{i}{{\sum }^{*}}}C\right)=\left(n\in \mathbb{N}⟼\underset{k=1}{\overset{n}{{\sum }^{*}}}A\right)$$
11	1 10 2 3	esumcvg	$$⊢\phi \to \left(i\in \mathbb{N}⟼\underset{m=1}{\overset{i}{{\sum }^{*}}}C\right)\underset{t}{⇝}\left(J\right)\underset{k\in \mathbb{N}}{{\sum }^{*}}A$$
12	10 11	eqbrtrrid	$$⊢\phi \to \left(n\in \mathbb{N}⟼\underset{k=1}{\overset{n}{{\sum }^{*}}}A\right)\underset{t}{⇝}\left(J\right)\underset{k\in \mathbb{N}}{{\sum }^{*}}A$$