Theorem dchrisum

Description: If n e. [ M , +oo ) |-> A ( n ) is a positive decreasing function approaching zero, then the infinite sum sum_ n , X ( n ) A ( n ) is convergent, with the partial sum sum_ n <_ x , X ( n ) A ( n ) within O ( A ( M ) ) of the limit T . Lemma 9.4.1 of Shapiro, p. 377. (Contributed by Mario Carneiro, 2-May-2016)

	Ref	Expression
Hypotheses	rpvmasum.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
	rpvmasum.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
	rpvmasum.a	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	rpvmasum.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
	rpvmasum.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
	rpvmasum.1	⊢ 1 = ( 0g ‘ 𝐺 )
	dchrisum.b	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
	dchrisum.n1	⊢ ( 𝜑 → 𝑋 ≠ 1 )
	dchrisum.2	⊢ ( 𝑛 = 𝑥 → 𝐴 = 𝐵 )
	dchrisum.3	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
	dchrisum.4	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℝ+ ) → 𝐴 ∈ ℝ )
	dchrisum.5	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → 𝐵 ≤ 𝐴 )
	dchrisum.6	⊢ ( 𝜑 → ( 𝑛 ∈ ℝ+ ↦ 𝐴 ) ⇝𝑟 0 )
	dchrisum.7	⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · 𝐴 ) )
Assertion	dchrisum	⊢ ( 𝜑 → ∃ 𝑡 ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , 𝐹 ) ⇝ 𝑡 ∧ ∀ 𝑥 ∈ ( 𝑀 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · 𝐵 ) ) )

Proof

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