esumcvgsum - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > esumcvgsum		Structured version Visualization version GIF version

Theorem esumcvgsum 29931

Description: The value of the extended sum when the corresponding sum is convergent. (Contributed by Thierry Arnoux, 29-Oct-2019.)

**Hypotheses**
Ref	Expression
esumcvgsum.1	⊢ (𝑘 = 𝑖 → 𝐴 = 𝐵)
esumcvgsum.2	⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,)+∞))
esumcvgsum.3	⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = 𝐴)
esumcvgsum.4	⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝐿)
esumcvgsum.5	⊢ (𝜑 → 𝐿 ∈ ℝ)

**Assertion**
Ref	Expression
esumcvgsum	⊢ (𝜑 → Σ^*𝑘 ∈ ℕ𝐴 = Σ𝑘 ∈ ℕ 𝐴)

Distinct variable groups: 𝑖,𝑘 𝐴,𝑖 𝐵,𝑘 𝑘,𝐹 𝜑,𝑘 Allowed substitution hints: 𝜑(𝑖) 𝐴(𝑘) 𝐵(𝑖) 𝐹(𝑖) 𝐿(𝑖,𝑘)

Proof of Theorem esumcvgsum Dummy variable 𝑗 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		esumcvgsum.2	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,)+∞))
2		esumcvgsum.1	. 2 ⊢ (𝑘 = 𝑖 → 𝐴 = 𝐵)
3		simpll 789	. . . . . 6 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑗)) → 𝜑)
4		elfznn 12312	. . . . . . 7 ⊢ (𝑘 ∈ (1...𝑗) → 𝑘 ∈ ℕ)
5	4	adantl 482	. . . . . 6 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑗)) → 𝑘 ∈ ℕ)
6		esumcvgsum.3	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = 𝐴)
7	3, 5, 6	syl2anc 692	. . . . 5 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑗)) → (𝐹‘𝑘) = 𝐴)
8		nnuz 11667	. . . . . . . 8 ⊢ ℕ = (ℤ_≥‘1)
9	8	eleq2i 2690	. . . . . . 7 ⊢ (𝑗 ∈ ℕ ↔ 𝑗 ∈ (ℤ_≥‘1))
10	9	biimpi 206	. . . . . 6 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ (ℤ_≥‘1))
11	10	adantl 482	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ (ℤ_≥‘1))
12		mnfxr 10040	. . . . . . . . 9 ⊢ -∞ ∈ ℝ^*
13		pnfxr 10036	. . . . . . . . 9 ⊢ +∞ ∈ ℝ^*
14		0re 9984	. . . . . . . . . 10 ⊢ 0 ∈ ℝ
15		mnflt 11901	. . . . . . . . . 10 ⊢ (0 ∈ ℝ → -∞ < 0)
16	14, 15	ax-mp 5	. . . . . . . . 9 ⊢ -∞ < 0
17		pnfge 11908	. . . . . . . . . 10 ⊢ (+∞ ∈ ℝ^* → +∞ ≤ +∞)
18	13, 17	ax-mp 5	. . . . . . . . 9 ⊢ +∞ ≤ +∞
19		icossioo 12206	. . . . . . . . 9 ⊢ (((-∞ ∈ ℝ^* ∧ +∞ ∈ ℝ^*) ∧ (-∞ < 0 ∧ +∞ ≤ +∞)) → (0[,)+∞) ⊆ (-∞(,)+∞))
20	12, 13, 16, 18, 19	mp4an 708	. . . . . . . 8 ⊢ (0[,)+∞) ⊆ (-∞(,)+∞)
21		ioomax 12190	. . . . . . . 8 ⊢ (-∞(,)+∞) = ℝ
22	20, 21	sseqtri 3616	. . . . . . 7 ⊢ (0[,)+∞) ⊆ ℝ
23	3, 5, 1	syl2anc 692	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑗)) → 𝐴 ∈ (0[,)+∞))
24	22, 23	sseldi 3581	. . . . . 6 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑗)) → 𝐴 ∈ ℝ)
25	24	recnd 10012	. . . . 5 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑗)) → 𝐴 ∈ ℂ)
26	7, 11, 25	fsumser 14394	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → Σ𝑘 ∈ (1...𝑗)𝐴 = (seq1( + , 𝐹)‘𝑗))
27	26	mpteq2dva 4704	. . 3 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ Σ𝑘 ∈ (1...𝑗)𝐴) = (𝑗 ∈ ℕ ↦ (seq1( + , 𝐹)‘𝑗)))
28		1z 11351	. . . . . . 7 ⊢ 1 ∈ ℤ
29		seqfn 12753	. . . . . . 7 ⊢ (1 ∈ ℤ → seq1( + , 𝐹) Fn (ℤ_≥‘1))
30	28, 29	ax-mp 5	. . . . . 6 ⊢ seq1( + , 𝐹) Fn (ℤ_≥‘1)
31		fneq2 5938	. . . . . . 7 ⊢ (ℕ = (ℤ_≥‘1) → (seq1( + , 𝐹) Fn ℕ ↔ seq1( + , 𝐹) Fn (ℤ_≥‘1)))
32	8, 31	ax-mp 5	. . . . . 6 ⊢ (seq1( + , 𝐹) Fn ℕ ↔ seq1( + , 𝐹) Fn (ℤ_≥‘1))
33	30, 32	mpbir 221	. . . . 5 ⊢ seq1( + , 𝐹) Fn ℕ
34		dffn5 6198	. . . . 5 ⊢ (seq1( + , 𝐹) Fn ℕ ↔ seq1( + , 𝐹) = (𝑗 ∈ ℕ ↦ (seq1( + , 𝐹)‘𝑗)))
35	33, 34	mpbi 220	. . . 4 ⊢ seq1( + , 𝐹) = (𝑗 ∈ ℕ ↦ (seq1( + , 𝐹)‘𝑗))
36		seqex 12743	. . . . . 6 ⊢ seq1( + , 𝐹) ∈ V
37	36	a1i 11	. . . . 5 ⊢ (𝜑 → seq1( + , 𝐹) ∈ V)
38		esumcvgsum.5	. . . . 5 ⊢ (𝜑 → 𝐿 ∈ ℝ)
39		esumcvgsum.4	. . . . 5 ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝐿)
40		breldmg 5290	. . . . 5 ⊢ ((seq1( + , 𝐹) ∈ V ∧ 𝐿 ∈ ℝ ∧ seq1( + , 𝐹) ⇝ 𝐿) → seq1( + , 𝐹) ∈ dom ⇝ )
41	37, 38, 39, 40	syl3anc 1323	. . . 4 ⊢ (𝜑 → seq1( + , 𝐹) ∈ dom ⇝ )
42	35, 41	syl5eqelr 2703	. . 3 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (seq1( + , 𝐹)‘𝑗)) ∈ dom ⇝ )
43	27, 42	eqeltrd 2698	. 2 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ Σ𝑘 ∈ (1...𝑗)𝐴) ∈ dom ⇝ )
44	1, 2, 43	esumpcvgval 29921	1 ⊢ (𝜑 → Σ^*𝑘 ∈ ℕ𝐴 = Σ𝑘 ∈ ℕ 𝐴)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 384 = wceq 1480 ∈ wcel 1987 Vcvv 3186 ⊆ wss 3555 class class class wbr 4613 ↦ cmpt 4673 dom cdm 5074 Fn wfn 5842 ‘cfv 5847 (class class class)co 6604 ℝcr 9879 0cc0 9880 1c1 9881 + caddc 9883 +∞cpnf 10015 -∞cmnf 10016 ℝ^*cxr 10017 < clt 10018 ≤ cle 10019 ℕcn 10964 ℤcz 11321 ℤ_≥cuz 11631 (,)cioo 12117 [,)cico 12119 ...cfz 12268 seqcseq 12741 ⇝ cli 14149 Σcsu 14350 Σ^*cesum 29870

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1719 ax-4 1734 ax-5 1836 ax-6 1885 ax-7 1932 ax-8 1989 ax-9 1996 ax-10 2016 ax-11 2031 ax-12 2044 ax-13 2245 ax-ext 2601 ax-rep 4731 ax-sep 4741 ax-nul 4749 ax-pow 4803 ax-pr 4867 ax-un 6902 ax-inf2 8482 ax-cnex 9936 ax-resscn 9937 ax-1cn 9938 ax-icn 9939 ax-addcl 9940 ax-addrcl 9941 ax-mulcl 9942 ax-mulrcl 9943 ax-mulcom 9944 ax-addass 9945 ax-mulass 9946 ax-distr 9947 ax-i2m1 9948 ax-1ne0 9949 ax-1rid 9950 ax-rnegex 9951 ax-rrecex 9952 ax-cnre 9953 ax-pre-lttri 9954 ax-pre-lttrn 9955 ax-pre-ltadd 9956 ax-pre-mulgt0 9957 ax-pre-sup 9958 ax-addf 9959 ax-mulf 9960

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1037 df-3an 1038 df-tru 1483 df-fal 1486 df-ex 1702 df-nf 1707 df-sb 1878 df-eu 2473 df-mo 2474 df-clab 2608 df-cleq 2614 df-clel 2617 df-nfc 2750 df-ne 2791 df-nel 2894 df-ral 2912 df-rex 2913 df-reu 2914 df-rmo 2915 df-rab 2916 df-v 3188 df-sbc 3418 df-csb 3515 df-dif 3558 df-un 3560 df-in 3562 df-ss 3569 df-pss 3571 df-nul 3892 df-if 4059 df-pw 4132 df-sn 4149 df-pr 4151 df-tp 4153 df-op 4155 df-uni 4403 df-int 4441 df-iun 4487 df-iin 4488 df-br 4614 df-opab 4674 df-mpt 4675 df-tr 4713 df-eprel 4985 df-id 4989 df-po 4995 df-so 4996 df-fr 5033 df-se 5034 df-we 5035 df-xp 5080 df-rel 5081 df-cnv 5082 df-co 5083 df-dm 5084 df-rn 5085 df-res 5086 df-ima 5087 df-pred 5639 df-ord 5685 df-on 5686 df-lim 5687 df-suc 5688 df-iota 5810 df-fun 5849 df-fn 5850 df-f 5851 df-f1 5852 df-fo 5853 df-f1o 5854 df-fv 5855 df-isom 5856 df-riota 6565 df-ov 6607 df-oprab 6608 df-mpt2 6609 df-of 6850 df-om 7013 df-1st 7113 df-2nd 7114 df-supp 7241 df-wrecs 7352 df-recs 7413 df-rdg 7451 df-1o 7505 df-oadd 7509 df-er 7687 df-map 7804 df-pm 7805 df-en 7900 df-dom 7901 df-sdom 7902 df-fin 7903 df-fsupp 8220 df-fi 8261 df-sup 8292 df-inf 8293 df-oi 8359 df-card 8709 df-pnf 10020 df-mnf 10021 df-xr 10022 df-ltxr 10023 df-le 10024 df-sub 10212 df-neg 10213 df-div 10629 df-nn 10965 df-2 11023 df-3 11024 df-4 11025 df-5 11026 df-6 11027 df-7 11028 df-8 11029 df-9 11030 df-n0 11237 df-z 11322 df-dec 11438 df-uz 11632 df-q 11733 df-rp 11777 df-xadd 11891 df-ioo 12121 df-ioc 12122 df-ico 12123 df-icc 12124 df-fz 12269 df-fzo 12407 df-fl 12533 df-seq 12742 df-exp 12801 df-hash 13058 df-cj 13773 df-re 13774 df-im 13775 df-sqrt 13909 df-abs 13910 df-clim 14153 df-rlim 14154 df-sum 14351 df-struct 15783 df-ndx 15784 df-slot 15785 df-base 15786 df-sets 15787 df-ress 15788 df-plusg 15875 df-mulr 15876 df-starv 15877 df-tset 15881 df-ple 15882 df-ds 15885 df-unif 15886 df-rest 16004 df-topn 16005 df-0g 16023 df-gsum 16024 df-topgen 16025 df-ordt 16082 df-xrs 16083 df-mre 16167 df-mrc 16168 df-acs 16170 df-ps 17121 df-tsr 17122 df-mgm 17163 df-sgrp 17205 df-mnd 17216 df-submnd 17257 df-grp 17346 df-minusg 17347 df-cntz 17671 df-cmn 18116 df-abl 18117 df-mgp 18411 df-ur 18423 df-ring 18470 df-cring 18471 df-fbas 19662 df-fg 19663 df-cnfld 19666 df-top 20621 df-bases 20622 df-topon 20623 df-topsp 20624 df-ntr 20734 df-nei 20812 df-cn 20941 df-haus 21029 df-fil 21560 df-fm 21652 df-flim 21653 df-flf 21654 df-tsms 21840 df-esum 29871

This theorem is referenced by: omssubadd 30143

W3C validator