dchrisum - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > dchrisum		Structured version Visualization version GIF version

Theorem dchrisum 27474

Description: If 𝑛 ∈ [𝑀, +∞) ↦ 𝐴(𝑛) is a positive decreasing function approaching zero, then the infinite sum Σ𝑛, 𝑋(𝑛)𝐴(𝑛) is convergent, with the partial sum Σ𝑛 ≤ 𝑥, 𝑋(𝑛)𝐴(𝑛) within 𝑂(𝐴(𝑀)) of the limit 𝑇. Lemma 9.4.1 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 2-May-2016.)

**Hypotheses**
Ref	Expression
rpvmasum.z	⊢ 𝑍 = (ℤ/nℤ‘𝑁)
rpvmasum.l	⊢ 𝐿 = (ℤRHom‘𝑍)
rpvmasum.a	⊢ (𝜑 → 𝑁 ∈ ℕ)
rpvmasum.g	⊢ 𝐺 = (DChr‘𝑁)
rpvmasum.d	⊢ 𝐷 = (Base‘𝐺)
rpvmasum.1	⊢ 1 = (0_g‘𝐺)
dchrisum.b	⊢ (𝜑 → 𝑋 ∈ 𝐷)
dchrisum.n1	⊢ (𝜑 → 𝑋 ≠ 1 )
dchrisum.2	⊢ (𝑛 = 𝑥 → 𝐴 = 𝐵)
dchrisum.3	⊢ (𝜑 → 𝑀 ∈ ℕ)
dchrisum.4	⊢ ((𝜑 ∧ 𝑛 ∈ ℝ⁺) → 𝐴 ∈ ℝ)
dchrisum.5	⊢ ((𝜑 ∧ (𝑛 ∈ ℝ⁺ ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴)
dchrisum.6	⊢ (𝜑 → (𝑛 ∈ ℝ⁺ ↦ 𝐴) ⇝_𝑟 0)
dchrisum.7	⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) · 𝐴))

**Assertion**
Ref	Expression
dchrisum	⊢ (𝜑 → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵)))

Distinct variable groups: 𝑥,𝑛,𝑐,𝑡, 1 𝐹,𝑐,𝑛,𝑡,𝑥 𝐴,𝑐,𝑡,𝑥 𝑁,𝑐,𝑛,𝑡,𝑥 𝜑,𝑐,𝑛,𝑡,𝑥 𝐵,𝑐,𝑛 𝑛,𝑍,𝑥 𝐷,𝑐,𝑛,𝑡,𝑥 𝐿,𝑐,𝑛,𝑡,𝑥 𝑀,𝑐,𝑛,𝑥 𝑋,𝑐,𝑛,𝑡,𝑥 Allowed substitution hints: 𝐴(𝑛) 𝐵(𝑥,𝑡) 𝐺(𝑥,𝑡,𝑛,𝑐) 𝑀(𝑡) 𝑍(𝑡,𝑐)

Proof of Theorem dchrisum Dummy variables 𝑚 𝑢 𝑖 𝑟 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fzofi 13909	. . 3 ⊢ (0..^𝑁) ∈ Fin
2		fzofi 13909	. . . . . . 7 ⊢ (0..^𝑢) ∈ Fin
3	2	a1i 11	. . . . . 6 ⊢ (𝜑 → (0..^𝑢) ∈ Fin)
4		rpvmasum.g	. . . . . . 7 ⊢ 𝐺 = (DChr‘𝑁)
5		rpvmasum.z	. . . . . . 7 ⊢ 𝑍 = (ℤ/nℤ‘𝑁)
6		rpvmasum.d	. . . . . . 7 ⊢ 𝐷 = (Base‘𝐺)
7		rpvmasum.l	. . . . . . 7 ⊢ 𝐿 = (ℤRHom‘𝑍)
8		dchrisum.b	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ 𝐷)
9	8	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (0..^𝑢)) → 𝑋 ∈ 𝐷)
10		elfzoelz 13587	. . . . . . . 8 ⊢ (𝑚 ∈ (0..^𝑢) → 𝑚 ∈ ℤ)
11	10	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (0..^𝑢)) → 𝑚 ∈ ℤ)
12	4, 5, 6, 7, 9, 11	dchrzrhcl 27227	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (0..^𝑢)) → (𝑋‘(𝐿‘𝑚)) ∈ ℂ)
13	3, 12	fsumcl 15668	. . . . 5 ⊢ (𝜑 → Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚)) ∈ ℂ)
14	13	abscld 15374	. . . 4 ⊢ (𝜑 → (abs‘Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚))) ∈ ℝ)
15	14	ralrimivw 3134	. . 3 ⊢ (𝜑 → ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚))) ∈ ℝ)
16		fimaxre3 12100	. . 3 ⊢ (((0..^𝑁) ∈ Fin ∧ ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚))) ∈ ℝ) → ∃𝑟 ∈ ℝ ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚))) ≤ 𝑟)
17	1, 15, 16	sylancr 588	. 2 ⊢ (𝜑 → ∃𝑟 ∈ ℝ ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚))) ≤ 𝑟)
18		rpvmasum.a	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℕ)
19	18	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚))) ≤ 𝑟)) → 𝑁 ∈ ℕ)
20		rpvmasum.1	. . 3 ⊢ 1 = (0_g‘𝐺)
21	8	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚))) ≤ 𝑟)) → 𝑋 ∈ 𝐷)
22		dchrisum.n1	. . . 4 ⊢ (𝜑 → 𝑋 ≠ 1 )
23	22	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚))) ≤ 𝑟)) → 𝑋 ≠ 1 )
24		dchrisum.2	. . 3 ⊢ (𝑛 = 𝑥 → 𝐴 = 𝐵)
25		dchrisum.3	. . . 4 ⊢ (𝜑 → 𝑀 ∈ ℕ)
26	25	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚))) ≤ 𝑟)) → 𝑀 ∈ ℕ)
27		dchrisum.4	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℝ⁺) → 𝐴 ∈ ℝ)
28	27	adantlr 716	. . 3 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚))) ≤ 𝑟)) ∧ 𝑛 ∈ ℝ⁺) → 𝐴 ∈ ℝ)
29		dchrisum.5	. . . 4 ⊢ ((𝜑 ∧ (𝑛 ∈ ℝ⁺ ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴)
30	29	3adant1r 1179	. . 3 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚))) ≤ 𝑟)) ∧ (𝑛 ∈ ℝ⁺ ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴)
31		dchrisum.6	. . . 4 ⊢ (𝜑 → (𝑛 ∈ ℝ⁺ ↦ 𝐴) ⇝_𝑟 0)
32	31	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚))) ≤ 𝑟)) → (𝑛 ∈ ℝ⁺ ↦ 𝐴) ⇝_𝑟 0)
33		dchrisum.7	. . 3 ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) · 𝐴))
34		simprl 771	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚))) ≤ 𝑟)) → 𝑟 ∈ ℝ)
35		simprr 773	. . . 4 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚))) ≤ 𝑟)) → ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚))) ≤ 𝑟)
36		2fveq3 6847	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (𝑋‘(𝐿‘𝑚)) = (𝑋‘(𝐿‘𝑛)))
37	36	cbvsumv 15631	. . . . . . . 8 ⊢ Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚)) = Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑛))
38		oveq2 7376	. . . . . . . . 9 ⊢ (𝑢 = 𝑖 → (0..^𝑢) = (0..^𝑖))
39	38	sumeq1d 15635	. . . . . . . 8 ⊢ (𝑢 = 𝑖 → Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿‘𝑛)))
40	37, 39	eqtrid 2784	. . . . . . 7 ⊢ (𝑢 = 𝑖 → Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚)) = Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿‘𝑛)))
41	40	fveq2d 6846	. . . . . 6 ⊢ (𝑢 = 𝑖 → (abs‘Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚))) = (abs‘Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿‘𝑛))))
42	41	breq1d 5110	. . . . 5 ⊢ (𝑢 = 𝑖 → ((abs‘Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚))) ≤ 𝑟 ↔ (abs‘Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿‘𝑛))) ≤ 𝑟))
43	42	cbvralvw 3216	. . . 4 ⊢ (∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚))) ≤ 𝑟 ↔ ∀𝑖 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿‘𝑛))) ≤ 𝑟)
44	35, 43	sylib 218	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚))) ≤ 𝑟)) → ∀𝑖 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿‘𝑛))) ≤ 𝑟)
45	5, 7, 19, 4, 6, 20, 21, 23, 24, 26, 28, 30, 32, 33, 34, 44	dchrisumlem3 27473	. 2 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚))) ≤ 𝑟)) → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵)))
46	17, 45	rexlimddv 3145	1 ⊢ (𝜑 → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∃wex 1781 ∈ wcel 2114 ≠ wne 2933 ∀wral 3052 ∃wrex 3062 class class class wbr 5100 ↦ cmpt 5181 ‘cfv 6500 (class class class)co 7368 Fincfn 8895 ℝcr 11037 0cc0 11038 1c1 11039 + caddc 11041 · cmul 11043 +∞cpnf 11175 ≤ cle 11179 − cmin 11376 ℕcn 12157 ℤcz 12500 ℝ⁺crp 12917 [,)cico 13275 ..^cfzo 13582 ⌊cfl 13722 seqcseq 13936 abscabs 15169 ⇝ cli 15419 ⇝_𝑟 crli 15420 Σcsu 15621 Basecbs 17148 0_gc0g 17371 ℤRHomczrh 21469 ℤ/nℤczn 21472 DChrcdchr 27214

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5226 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690 ax-inf2 9562 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115 ax-pre-sup 11116 ax-addf 11117 ax-mulf 11118

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-tp 4587 df-op 4589 df-uni 4866 df-int 4905 df-iun 4950 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5527 df-eprel 5532 df-po 5540 df-so 5541 df-fr 5585 df-se 5586 df-we 5587 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-pred 6267 df-ord 6328 df-on 6329 df-lim 6330 df-suc 6331 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-isom 6509 df-riota 7325 df-ov 7371 df-oprab 7372 df-mpo 7373 df-of 7632 df-om 7819 df-1st 7943 df-2nd 7944 df-tpos 8178 df-frecs 8233 df-wrecs 8264 df-recs 8313 df-rdg 8351 df-1o 8407 df-oadd 8411 df-er 8645 df-ec 8647 df-qs 8651 df-map 8777 df-pm 8778 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-sup 9357 df-inf 9358 df-oi 9427 df-card 9863 df-pnf 11180 df-mnf 11181 df-xr 11182 df-ltxr 11183 df-le 11184 df-sub 11378 df-neg 11379 df-div 11807 df-nn 12158 df-2 12220 df-3 12221 df-4 12222 df-5 12223 df-6 12224 df-7 12225 df-8 12226 df-9 12227 df-n0 12414 df-xnn0 12487 df-z 12501 df-dec 12620 df-uz 12764 df-rp 12918 df-ico 13279 df-fz 13436 df-fzo 13583 df-fl 13724 df-mod 13802 df-seq 13937 df-exp 13997 df-hash 14266 df-cj 15034 df-re 15035 df-im 15036 df-sqrt 15170 df-abs 15171 df-limsup 15406 df-clim 15423 df-rlim 15424 df-sum 15622 df-dvds 16192 df-gcd 16434 df-phi 16705 df-struct 17086 df-sets 17103 df-slot 17121 df-ndx 17133 df-base 17149 df-ress 17170 df-plusg 17202 df-mulr 17203 df-starv 17204 df-sca 17205 df-vsca 17206 df-ip 17207 df-tset 17208 df-ple 17209 df-ds 17211 df-unif 17212 df-0g 17373 df-imas 17441 df-qus 17442 df-mgm 18577 df-sgrp 18656 df-mnd 18672 df-mhm 18720 df-grp 18881 df-minusg 18882 df-sbg 18883 df-mulg 19013 df-subg 19068 df-nsg 19069 df-eqg 19070 df-ghm 19157 df-cmn 19726 df-abl 19727 df-mgp 20091 df-rng 20103 df-ur 20132 df-ring 20185 df-cring 20186 df-oppr 20288 df-dvdsr 20308 df-unit 20309 df-invr 20339 df-rhm 20423 df-subrng 20494 df-subrg 20518 df-lmod 20828 df-lss 20898 df-lsp 20938 df-sra 21140 df-rgmod 21141 df-lidl 21178 df-rsp 21179 df-2idl 21220 df-cnfld 21325 df-zring 21417 df-zrh 21473 df-zn 21476 df-dchr 27215

This theorem is referenced by: dchrmusumlema 27475 dchrvmasumlema 27482 dchrisum0lema 27496

W3C validator