Metamath Proof Explorer

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 ⊢ Z = ℤ/Nℤ
rpvmasum.l ⊢ L = ℤRHom ⁡ Z
rpvmasum.a ⊢ φ → N ∈ ℕ
rpvmasum.g ⊢ G = DChr ⁡ N
rpvmasum.d ⊢ D = Base G
rpvmasum.1 ⊢ 1 ˙ = 0 G
dchrisum.b ⊢ φ → X ∈ D
dchrisum.n1 ⊢ φ → X ≠ 1 ˙
dchrisum.2 ⊢ n = x → A = B
dchrisum.3 ⊢ φ → M ∈ ℕ
dchrisum.4 ⊢ φ ∧ n ∈ ℝ + → A ∈ ℝ
dchrisum.5 ⊢ φ ∧ n ∈ ℝ + ∧ x ∈ ℝ + ∧ M ≤ n ∧ n ≤ x → B ≤ A
dchrisum.6 ⊢ φ → n ∈ ℝ + ⟼ A ⇝ℝ 0
dchrisum.7 ⊢ F = n ∈ ℕ ⟼ X ⁡ L ⁡ n ⁢ A
Assertion dchrisum ⊢ φ → ∃ t ∃ c ∈ 0 +∞ seq 1 + F ⇝ t ∧ ∀ x ∈ M +∞ seq 1 + F ⁡ x − t ≤ c ⁢ B

Proof

Step Hyp Ref Expression
1 rpvmasum.z ⊢ Z = ℤ/Nℤ
2 rpvmasum.l ⊢ L = ℤRHom ⁡ Z
3 rpvmasum.a ⊢ φ → N ∈ ℕ
4 rpvmasum.g ⊢ G = DChr ⁡ N
5 rpvmasum.d ⊢ D = Base G
6 rpvmasum.1 ⊢ 1 ˙ = 0 G
7 dchrisum.b ⊢ φ → X ∈ D
8 dchrisum.n1 ⊢ φ → X ≠ 1 ˙
9 dchrisum.2 ⊢ n = x → A = B
10 dchrisum.3 ⊢ φ → M ∈ ℕ
11 dchrisum.4 ⊢ φ ∧ n ∈ ℝ + → A ∈ ℝ
12 dchrisum.5 ⊢ φ ∧ n ∈ ℝ + ∧ x ∈ ℝ + ∧ M ≤ n ∧ n ≤ x → B ≤ A
13 dchrisum.6 ⊢ φ → n ∈ ℝ + ⟼ A ⇝ℝ 0
14 dchrisum.7 ⊢ F = n ∈ ℕ ⟼ X ⁡ L ⁡ n ⁢ A
15 fzofi ⊢ 0 ..^ N ∈ Fin
16 fzofi ⊢ 0 ..^ u ∈ Fin
17 16 a1i ⊢ φ → 0 ..^ u ∈ Fin
18 7 adantr ⊢ φ ∧ m ∈ 0 ..^ u → X ∈ D
19 elfzoelz ⊢ m ∈ 0 ..^ u → m ∈ ℤ
20 19 adantl ⊢ φ ∧ m ∈ 0 ..^ u → m ∈ ℤ
21 4 1 5 2 18 20 dchrzrhcl ⊢ φ ∧ m ∈ 0 ..^ u → X ⁡ L ⁡ m ∈ ℂ
22 17 21 fsumcl ⊢ φ → ∑ m ∈ 0 ..^ u X ⁡ L ⁡ m ∈ ℂ
23 22 abscld ⊢ φ → ∑ m ∈ 0 ..^ u X ⁡ L ⁡ m ∈ ℝ
24 23 ralrimivw ⊢ φ → ∀ u ∈ 0 ..^ N ∑ m ∈ 0 ..^ u X ⁡ L ⁡ m ∈ ℝ
25 fimaxre3 ⊢ 0 ..^ N ∈ Fin ∧ ∀ u ∈ 0 ..^ N ∑ m ∈ 0 ..^ u X ⁡ L ⁡ m ∈ ℝ → ∃ r ∈ ℝ ∀ u ∈ 0 ..^ N ∑ m ∈ 0 ..^ u X ⁡ L ⁡ m ≤ r
26 15 24 25 sylancr ⊢ φ → ∃ r ∈ ℝ ∀ u ∈ 0 ..^ N ∑ m ∈ 0 ..^ u X ⁡ L ⁡ m ≤ r
27 3 adantr ⊢ φ ∧ r ∈ ℝ ∧ ∀ u ∈ 0 ..^ N ∑ m ∈ 0 ..^ u X ⁡ L ⁡ m ≤ r → N ∈ ℕ
28 7 adantr ⊢ φ ∧ r ∈ ℝ ∧ ∀ u ∈ 0 ..^ N ∑ m ∈ 0 ..^ u X ⁡ L ⁡ m ≤ r → X ∈ D
29 8 adantr ⊢ φ ∧ r ∈ ℝ ∧ ∀ u ∈ 0 ..^ N ∑ m ∈ 0 ..^ u X ⁡ L ⁡ m ≤ r → X ≠ 1 ˙
30 10 adantr ⊢ φ ∧ r ∈ ℝ ∧ ∀ u ∈ 0 ..^ N ∑ m ∈ 0 ..^ u X ⁡ L ⁡ m ≤ r → M ∈ ℕ
31 11 adantlr ⊢ φ ∧ r ∈ ℝ ∧ ∀ u ∈ 0 ..^ N ∑ m ∈ 0 ..^ u X ⁡ L ⁡ m ≤ r ∧ n ∈ ℝ + → A ∈ ℝ
32 12 3adant1r ⊢ φ ∧ r ∈ ℝ ∧ ∀ u ∈ 0 ..^ N ∑ m ∈ 0 ..^ u X ⁡ L ⁡ m ≤ r ∧ n ∈ ℝ + ∧ x ∈ ℝ + ∧ M ≤ n ∧ n ≤ x → B ≤ A
33 13 adantr ⊢ φ ∧ r ∈ ℝ ∧ ∀ u ∈ 0 ..^ N ∑ m ∈ 0 ..^ u X ⁡ L ⁡ m ≤ r → n ∈ ℝ + ⟼ A ⇝ℝ 0
34 simprl ⊢ φ ∧ r ∈ ℝ ∧ ∀ u ∈ 0 ..^ N ∑ m ∈ 0 ..^ u X ⁡ L ⁡ m ≤ r → r ∈ ℝ
35 simprr ⊢ φ ∧ r ∈ ℝ ∧ ∀ u ∈ 0 ..^ N ∑ m ∈ 0 ..^ u X ⁡ L ⁡ m ≤ r → ∀ u ∈ 0 ..^ N ∑ m ∈ 0 ..^ u X ⁡ L ⁡ m ≤ r
36 2fveq3 ⊢ m = n → X ⁡ L ⁡ m = X ⁡ L ⁡ n
37 36 cbvsumv ⊢ ∑ m ∈ 0 ..^ u X ⁡ L ⁡ m = ∑ n ∈ 0 ..^ u X ⁡ L ⁡ n
38 oveq2 ⊢ u = i → 0 ..^ u = 0 ..^ i
39 38 sumeq1d ⊢ u = i → ∑ n ∈ 0 ..^ u X ⁡ L ⁡ n = ∑ n ∈ 0 ..^ i X ⁡ L ⁡ n
40 37 39 syl5eq ⊢ u = i → ∑ m ∈ 0 ..^ u X ⁡ L ⁡ m = ∑ n ∈ 0 ..^ i X ⁡ L ⁡ n
41 40 fveq2d ⊢ u = i → ∑ m ∈ 0 ..^ u X ⁡ L ⁡ m = ∑ n ∈ 0 ..^ i X ⁡ L ⁡ n
42 41 breq1d ⊢ u = i → ∑ m ∈ 0 ..^ u X ⁡ L ⁡ m ≤ r ↔ ∑ n ∈ 0 ..^ i X ⁡ L ⁡ n ≤ r
43 42 cbvralvw ⊢ ∀ u ∈ 0 ..^ N ∑ m ∈ 0 ..^ u X ⁡ L ⁡ m ≤ r ↔ ∀ i ∈ 0 ..^ N ∑ n ∈ 0 ..^ i X ⁡ L ⁡ n ≤ r
44 35 43 sylib ⊢ φ ∧ r ∈ ℝ ∧ ∀ u ∈ 0 ..^ N ∑ m ∈ 0 ..^ u X ⁡ L ⁡ m ≤ r → ∀ i ∈ 0 ..^ N ∑ n ∈ 0 ..^ i X ⁡ L ⁡ n ≤ r
45 1 2 27 4 5 6 28 29 9 30 31 32 33 14 34 44 dchrisumlem3 ⊢ φ ∧ r ∈ ℝ ∧ ∀ u ∈ 0 ..^ N ∑ m ∈ 0 ..^ u X ⁡ L ⁡ m ≤ r → ∃ t ∃ c ∈ 0 +∞ seq 1 + F ⇝ t ∧ ∀ x ∈ M +∞ seq 1 + F ⁡ x − t ≤ c ⁢ B
46 26 45 rexlimddv ⊢ φ → ∃ t ∃ c ∈ 0 +∞ seq 1 + F ⇝ t ∧ ∀ x ∈ M +∞ seq 1 + F ⁡ x − t ≤ c ⁢ B