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 27731

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 14041	. . 3 ⊢ (0..^𝑁) ∈ Fin
2		fzofi 14041	. . . . . . 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 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (0..^𝑢)) → 𝑋 ∈ 𝐷)
10		elfzoelz 13717	. . . . . . . 8 ⊢ (𝑚 ∈ (0..^𝑢) → 𝑚 ∈ ℤ)
11	10	adantl 487	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (0..^𝑢)) → 𝑚 ∈ ℤ)
12	4, 5, 6, 7, 9, 11	dchrzrhcl 27484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (0..^𝑢)) → (𝑋‘(𝐿‘𝑚)) ∈ ℂ)
13	3, 12	fsumcl 15822	. . . . 5 ⊢ (𝜑 → Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚)) ∈ ℂ)
14	13	abscld 15529	. . . 4 ⊢ (𝜑 → (abs‘Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚))) ∈ ℝ)
15	14	ralrimivw 3158	. . 3 ⊢ (𝜑 → ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚))) ∈ ℝ)
16		fimaxre3 12188	. . 3 ⊢ (((0..^𝑁) ∈ Fin ∧ ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚))) ∈ ℝ) → ∃𝑟 ∈ ℝ ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚))) ≤ 𝑟)
17	1, 15, 16	sylancr 599	. 2 ⊢ (𝜑 → ∃𝑟 ∈ ℝ ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚))) ≤ 𝑟)
18		rpvmasum.a	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℕ)
19	18	adantr 486	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚))) ≤ 𝑟)) → 𝑁 ∈ ℕ)
20		rpvmasum.1	. . 3 ⊢ 1 = (0_g‘𝐺)
21	8	adantr 486	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚))) ≤ 𝑟)) → 𝑋 ∈ 𝐷)
22		dchrisum.n1	. . . 4 ⊢ (𝜑 → 𝑋 ≠ 1 )
23	22	adantr 486	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚))) ≤ 𝑟)) → 𝑋 ≠ 1 )
24		dchrisum.2	. . 3 ⊢ (𝑛 = 𝑥 → 𝐴 = 𝐵)
25		dchrisum.3	. . . 4 ⊢ (𝜑 → 𝑀 ∈ ℕ)
26	25	adantr 486	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚))) ≤ 𝑟)) → 𝑀 ∈ ℕ)
27		dchrisum.4	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℝ⁺) → 𝐴 ∈ ℝ)
28	27	adantlr 728	. . 3 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚))) ≤ 𝑟)) ∧ 𝑛 ∈ ℝ⁺) → 𝐴 ∈ ℝ)
29		dchrisum.5	. . . 4 ⊢ ((𝜑 ∧ (𝑛 ∈ ℝ⁺ ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴)
30	29	3adant1r 1196	. . 3 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚))) ≤ 𝑟)) ∧ (𝑛 ∈ ℝ⁺ ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴)
31		dchrisum.6	. . . 4 ⊢ (𝜑 → (𝑛 ∈ ℝ⁺ ↦ 𝐴) ⇝_𝑟 0)
32	31	adantr 486	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚))) ≤ 𝑟)) → (𝑛 ∈ ℝ⁺ ↦ 𝐴) ⇝_𝑟 0)
33		dchrisum.7	. . 3 ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) · 𝐴))
34		simprl 783	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚))) ≤ 𝑟)) → 𝑟 ∈ ℝ)
35		simprr 785	. . . 4 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚))) ≤ 𝑟)) → ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚))) ≤ 𝑟)
36		2fveq3 6884	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (𝑋‘(𝐿‘𝑚)) = (𝑋‘(𝐿‘𝑛)))
37	36	cbvsumv 15786	. . . . . . . 8 ⊢ Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚)) = Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑛))
38		oveq2 7422	. . . . . . . . 9 ⊢ (𝑢 = 𝑖 → (0..^𝑢) = (0..^𝑖))
39	38	sumeq1d 15790	. . . . . . . 8 ⊢ (𝑢 = 𝑖 → Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿‘𝑛)))
40	37, 39	eqtrid 2807	. . . . . . 7 ⊢ (𝑢 = 𝑖 → Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚)) = Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿‘𝑛)))
41	40	fveq2d 6883	. . . . . 6 ⊢ (𝑢 = 𝑖 → (abs‘Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚))) = (abs‘Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿‘𝑛))))
42	41	breq1d 5113	. . . . 5 ⊢ (𝑢 = 𝑖 → ((abs‘Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚))) ≤ 𝑟 ↔ (abs‘Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿‘𝑛))) ≤ 𝑟))
43	42	cbvralvw 3240	. . . 4 ⊢ (∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚))) ≤ 𝑟 ↔ ∀𝑖 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿‘𝑛))) ≤ 𝑟)
44	35, 43	sylib 221	. . 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 27730	. 2 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑚 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑚))) ≤ 𝑟)) → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵)))
46	17, 45	rexlimddv 3169	1 ⊢ (𝜑 → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∃wex 1812 ∈ wcel 2145 ≠ wne 2955 ∀wral 3076 ∃wrex 3086 class class class wbr 5103 ↦ cmpt 5186 ‘cfv 6533 (class class class)co 7414 Fincfn 8955 ℝcr 11126 0cc0 11127 1c1 11128 + caddc 11130 · cmul 11132 +∞cpnf 11267 ≤ cle 11271 − cmin 11468 ℕcn 12260 ℤcz 12618 ℝ⁺crp 13045 [,)cico 13403 ..^cfzo 13712 ⌊cfl 13854 seqcseq 14068 abscabs 15324 ⇝ cli 15574 ⇝_𝑟 crli 15575 Σcsu 15776 Basecbs 17304 0_gc0g 17527 ℤRHomczrh 21715 ℤ/nℤczn 21718 DChrcdchr 27471

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5232 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7737 ax-inf2 9623 ax-cnex 11183 ax-resscn 11184 ax-1cn 11185 ax-icn 11186 ax-addcl 11187 ax-addrcl 11188 ax-mulcl 11189 ax-mulrcl 11190 ax-mulcom 11191 ax-addass 11192 ax-mulass 11193 ax-distr 11194 ax-i2m1 11195 ax-1ne0 11196 ax-1rid 11197 ax-rnegex 11198 ax-rrecex 11199 ax-cnre 11200 ax-pre-lttri 11201 ax-pre-lttrn 11202 ax-pre-ltadd 11203 ax-pre-mulgt0 11204 ax-pre-sup 11205 ax-addf 11206 ax-mulf 11207

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-se 5609 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6299 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-isom 6542 df-riota 7371 df-ov 7417 df-oprab 7418 df-mpo 7419 df-of 7679 df-om 7864 df-1st 7987 df-2nd 7988 df-tpos 8225 df-frecs 8281 df-wrecs 8312 df-recs 8361 df-rdg 8400 df-1o 8458 df-oadd 8462 df-er 8699 df-ec 8701 df-qs 8705 df-map 8831 df-pm 8832 df-en 8956 df-dom 8957 df-sdom 8958 df-fin 8959 df-sup 9415 df-inf 9416 df-oi 9485 df-card 9947 df-pnf 11272 df-mnf 11273 df-xr 11274 df-ltxr 11275 df-le 11276 df-sub 11470 df-neg 11471 df-div 11899 df-nn 12261 df-2 12330 df-3 12331 df-4 12332 df-5 12333 df-6 12334 df-7 12335 df-8 12336 df-9 12337 df-n0 12532 df-xnn0 12605 df-z 12619 df-dec 12740 df-uz 12891 df-rp 13046 df-ico 13407 df-fz 13565 df-fzo 13713 df-fl 13856 df-mod 13934 df-seq 14069 df-exp 14129 df-hash 14398 df-cj 15189 df-re 15190 df-im 15191 df-sqrt 15325 df-abs 15326 df-limsup 15561 df-clim 15578 df-rlim 15579 df-sum 15777 df-dvds 16346 df-gcd 16588 df-phi 16860 df-struct 17242 df-sets 17259 df-slot 17277 df-ndx 17289 df-base 17305 df-ress 17326 df-plusg 17358 df-mulr 17359 df-starv 17360 df-sca 17361 df-vsca 17362 df-ip 17363 df-tset 17364 df-ple 17365 df-ds 17367 df-unif 17368 df-0g 17529 df-imas 17597 df-qus 17598 df-mgm 18733 df-sgrp 18824 df-mnd 18840 df-mhm 18894 df-grp 19063 df-minusg 19064 df-sbg 19065 df-mulg 19194 df-subg 19249 df-nsg 19250 df-eqg 19251 df-ghm 19344 df-cmn 19912 df-abl 19913 df-mgp 20277 df-rng 20291 df-ur 20324 df-ring 20377 df-cring 20378 df-oppr 20481 df-dvdsr 20501 df-unit 20502 df-invr 20532 df-rhm 20616 df-subrng 20711 df-subrg 20735 df-lmod 21049 df-lss 21119 df-lsp 21159 df-sra 21360 df-rgmod 21361 df-lidl 21398 df-rsp 21399 df-2idl 21455 df-cnfld 21589 df-zring 21663 df-zrh 21719 df-zn 21722 df-dchr 27472

This theorem is used by: dchrmusumlema 27732 dchrvmasumlema 27739 dchrisum0lema 27753

W3C validator