Metamath Proof Explorer

Theorem dchrisum0flb

Description: The divisor sum of a real Dirichlet character, is lower bounded by zero everywhere and one at the squares. Equation 9.4.29 of Shapiro, p. 382. (Contributed by Mario Carneiro, 5-May-2016)

Ref Expression
Hypotheses rpvmasum.z ⊢ Z = ℤ/Nℤ
rpvmasum.l ⊢ L = ℤRHom ⁡ Z
rpvmasum.a ⊢ φ → N ∈ ℕ
rpvmasum2.g ⊢ G = DChr ⁡ N
rpvmasum2.d ⊢ D = Base G
rpvmasum2.1 ⊢ 1 ˙ = 0 G
dchrisum0f.f ⊢ F = b ∈ ℕ ⟼ ∑ v ∈ q ∈ ℕ | q ∥ b X ⁡ L ⁡ v
dchrisum0f.x ⊢ φ → X ∈ D
dchrisum0flb.r ⊢ φ → X : Base Z ⟶ ℝ
dchrisum0flb.a ⊢ φ → A ∈ ℕ
Assertion dchrisum0flb ⊢ φ → if A ∈ ℕ 1 0 ≤ F ⁡ A

Proof

Step Hyp Ref Expression
1 rpvmasum.z ⊢ Z = ℤ/Nℤ
2 rpvmasum.l ⊢ L = ℤRHom ⁡ Z
3 rpvmasum.a ⊢ φ → N ∈ ℕ
4 rpvmasum2.g ⊢ G = DChr ⁡ N
5 rpvmasum2.d ⊢ D = Base G
6 rpvmasum2.1 ⊢ 1 ˙ = 0 G
7 dchrisum0f.f ⊢ F = b ∈ ℕ ⟼ ∑ v ∈ q ∈ ℕ | q ∥ b X ⁡ L ⁡ v
8 dchrisum0f.x ⊢ φ → X ∈ D
9 dchrisum0flb.r ⊢ φ → X : Base Z ⟶ ℝ
10 dchrisum0flb.a ⊢ φ → A ∈ ℕ
11 fveq2 ⊢ y = A → y = A
12 11 eleq1d ⊢ y = A → y ∈ ℕ ↔ A ∈ ℕ
13 12 ifbid ⊢ y = A → if y ∈ ℕ 1 0 = if A ∈ ℕ 1 0
14 fveq2 ⊢ y = A → F ⁡ y = F ⁡ A
15 13 14 breq12d ⊢ y = A → if y ∈ ℕ 1 0 ≤ F ⁡ y ↔ if A ∈ ℕ 1 0 ≤ F ⁡ A
16 oveq2 ⊢ k = 1 → 1 … k = 1 … 1
17 16 raleqdv ⊢ k = 1 → ∀ y ∈ 1 … k if y ∈ ℕ 1 0 ≤ F ⁡ y ↔ ∀ y ∈ 1 … 1 if y ∈ ℕ 1 0 ≤ F ⁡ y
18 17 imbi2d ⊢ k = 1 → φ → ∀ y ∈ 1 … k if y ∈ ℕ 1 0 ≤ F ⁡ y ↔ φ → ∀ y ∈ 1 … 1 if y ∈ ℕ 1 0 ≤ F ⁡ y
19 oveq2 ⊢ k = i → 1 … k = 1 … i
20 19 raleqdv ⊢ k = i → ∀ y ∈ 1 … k if y ∈ ℕ 1 0 ≤ F ⁡ y ↔ ∀ y ∈ 1 … i if y ∈ ℕ 1 0 ≤ F ⁡ y
21 20 imbi2d ⊢ k = i → φ → ∀ y ∈ 1 … k if y ∈ ℕ 1 0 ≤ F ⁡ y ↔ φ → ∀ y ∈ 1 … i if y ∈ ℕ 1 0 ≤ F ⁡ y
22 oveq2 ⊢ k = i + 1 → 1 … k = 1 … i + 1
23 22 raleqdv ⊢ k = i + 1 → ∀ y ∈ 1 … k if y ∈ ℕ 1 0 ≤ F ⁡ y ↔ ∀ y ∈ 1 … i + 1 if y ∈ ℕ 1 0 ≤ F ⁡ y
24 23 imbi2d ⊢ k = i + 1 → φ → ∀ y ∈ 1 … k if y ∈ ℕ 1 0 ≤ F ⁡ y ↔ φ → ∀ y ∈ 1 … i + 1 if y ∈ ℕ 1 0 ≤ F ⁡ y
25 oveq2 ⊢ k = A → 1 … k = 1 … A
26 25 raleqdv ⊢ k = A → ∀ y ∈ 1 … k if y ∈ ℕ 1 0 ≤ F ⁡ y ↔ ∀ y ∈ 1 … A if y ∈ ℕ 1 0 ≤ F ⁡ y
27 26 imbi2d ⊢ k = A → φ → ∀ y ∈ 1 … k if y ∈ ℕ 1 0 ≤ F ⁡ y ↔ φ → ∀ y ∈ 1 … A if y ∈ ℕ 1 0 ≤ F ⁡ y
28 2prm ⊢ 2 ∈ ℙ
29 28 a1i ⊢ φ → 2 ∈ ℙ
30 0nn0 ⊢ 0 ∈ ℕ 0
31 30 a1i ⊢ φ → 0 ∈ ℕ 0
32 1 2 3 4 5 6 7 8 9 29 31 dchrisum0flblem1 ⊢ φ → if 2 0 ∈ ℕ 1 0 ≤ F ⁡ 2 0
33 elfz1eq ⊢ y ∈ 1 … 1 → y = 1
34 2nn0 ⊢ 2 ∈ ℕ 0
35 34 numexp0 ⊢ 2 0 = 1
36 33 35 eqtr4di ⊢ y ∈ 1 … 1 → y = 2 0
37 36 fveq2d ⊢ y ∈ 1 … 1 → y = 2 0
38 37 eleq1d ⊢ y ∈ 1 … 1 → y ∈ ℕ ↔ 2 0 ∈ ℕ
39 38 ifbid ⊢ y ∈ 1 … 1 → if y ∈ ℕ 1 0 = if 2 0 ∈ ℕ 1 0
40 36 fveq2d ⊢ y ∈ 1 … 1 → F ⁡ y = F ⁡ 2 0
41 39 40 breq12d ⊢ y ∈ 1 … 1 → if y ∈ ℕ 1 0 ≤ F ⁡ y ↔ if 2 0 ∈ ℕ 1 0 ≤ F ⁡ 2 0
42 41 biimprcd ⊢ if 2 0 ∈ ℕ 1 0 ≤ F ⁡ 2 0 → y ∈ 1 … 1 → if y ∈ ℕ 1 0 ≤ F ⁡ y
43 42 ralrimiv ⊢ if 2 0 ∈ ℕ 1 0 ≤ F ⁡ 2 0 → ∀ y ∈ 1 … 1 if y ∈ ℕ 1 0 ≤ F ⁡ y
44 32 43 syl ⊢ φ → ∀ y ∈ 1 … 1 if y ∈ ℕ 1 0 ≤ F ⁡ y
45 simpr ⊢ φ ∧ i ∈ ℕ → i ∈ ℕ
46 nnuz ⊢ ℕ = ℤ ≥ 1
47 45 46 eleqtrdi ⊢ φ ∧ i ∈ ℕ → i ∈ ℤ ≥ 1
48 47 adantrr ⊢ φ ∧ i ∈ ℕ ∧ ∀ y ∈ 1 … i if y ∈ ℕ 1 0 ≤ F ⁡ y → i ∈ ℤ ≥ 1
49 eluzp1p1 ⊢ i ∈ ℤ ≥ 1 → i + 1 ∈ ℤ ≥ 1 + 1
50 48 49 syl ⊢ φ ∧ i ∈ ℕ ∧ ∀ y ∈ 1 … i if y ∈ ℕ 1 0 ≤ F ⁡ y → i + 1 ∈ ℤ ≥ 1 + 1
51 df-2 ⊢ 2 = 1 + 1
52 51 fveq2i ⊢ ℤ ≥ 2 = ℤ ≥ 1 + 1
53 50 52 eleqtrrdi ⊢ φ ∧ i ∈ ℕ ∧ ∀ y ∈ 1 … i if y ∈ ℕ 1 0 ≤ F ⁡ y → i + 1 ∈ ℤ ≥ 2
54 exprmfct ⊢ i + 1 ∈ ℤ ≥ 2 → ∃ p ∈ ℙ p ∥ i + 1
55 53 54 syl ⊢ φ ∧ i ∈ ℕ ∧ ∀ y ∈ 1 … i if y ∈ ℕ 1 0 ≤ F ⁡ y → ∃ p ∈ ℙ p ∥ i + 1
56 3 ad2antrr ⊢ φ ∧ i ∈ ℕ ∧ ∀ y ∈ 1 … i if y ∈ ℕ 1 0 ≤ F ⁡ y ∧ p ∈ ℙ ∧ p ∥ i + 1 → N ∈ ℕ
57 8 ad2antrr ⊢ φ ∧ i ∈ ℕ ∧ ∀ y ∈ 1 … i if y ∈ ℕ 1 0 ≤ F ⁡ y ∧ p ∈ ℙ ∧ p ∥ i + 1 → X ∈ D
58 9 ad2antrr ⊢ φ ∧ i ∈ ℕ ∧ ∀ y ∈ 1 … i if y ∈ ℕ 1 0 ≤ F ⁡ y ∧ p ∈ ℙ ∧ p ∥ i + 1 → X : Base Z ⟶ ℝ
59 53 adantr ⊢ φ ∧ i ∈ ℕ ∧ ∀ y ∈ 1 … i if y ∈ ℕ 1 0 ≤ F ⁡ y ∧ p ∈ ℙ ∧ p ∥ i + 1 → i + 1 ∈ ℤ ≥ 2
60 simprl ⊢ φ ∧ i ∈ ℕ ∧ ∀ y ∈ 1 … i if y ∈ ℕ 1 0 ≤ F ⁡ y ∧ p ∈ ℙ ∧ p ∥ i + 1 → p ∈ ℙ
61 simprr ⊢ φ ∧ i ∈ ℕ ∧ ∀ y ∈ 1 … i if y ∈ ℕ 1 0 ≤ F ⁡ y ∧ p ∈ ℙ ∧ p ∥ i + 1 → p ∥ i + 1
62 simplrr ⊢ φ ∧ i ∈ ℕ ∧ ∀ y ∈ 1 … i if y ∈ ℕ 1 0 ≤ F ⁡ y ∧ p ∈ ℙ ∧ p ∥ i + 1 → ∀ y ∈ 1 … i if y ∈ ℕ 1 0 ≤ F ⁡ y
63 simplrl ⊢ φ ∧ i ∈ ℕ ∧ ∀ y ∈ 1 … i if y ∈ ℕ 1 0 ≤ F ⁡ y ∧ p ∈ ℙ ∧ p ∥ i + 1 → i ∈ ℕ
64 63 nnzd ⊢ φ ∧ i ∈ ℕ ∧ ∀ y ∈ 1 … i if y ∈ ℕ 1 0 ≤ F ⁡ y ∧ p ∈ ℙ ∧ p ∥ i + 1 → i ∈ ℤ
65 fzval3 ⊢ i ∈ ℤ → 1 … i = 1 ..^ i + 1
66 64 65 syl ⊢ φ ∧ i ∈ ℕ ∧ ∀ y ∈ 1 … i if y ∈ ℕ 1 0 ≤ F ⁡ y ∧ p ∈ ℙ ∧ p ∥ i + 1 → 1 … i = 1 ..^ i + 1
67 66 raleqdv ⊢ φ ∧ i ∈ ℕ ∧ ∀ y ∈ 1 … i if y ∈ ℕ 1 0 ≤ F ⁡ y ∧ p ∈ ℙ ∧ p ∥ i + 1 → ∀ y ∈ 1 … i if y ∈ ℕ 1 0 ≤ F ⁡ y ↔ ∀ y ∈ 1 ..^ i + 1 if y ∈ ℕ 1 0 ≤ F ⁡ y
68 62 67 mpbid ⊢ φ ∧ i ∈ ℕ ∧ ∀ y ∈ 1 … i if y ∈ ℕ 1 0 ≤ F ⁡ y ∧ p ∈ ℙ ∧ p ∥ i + 1 → ∀ y ∈ 1 ..^ i + 1 if y ∈ ℕ 1 0 ≤ F ⁡ y
69 1 2 56 4 5 6 7 57 58 59 60 61 68 dchrisum0flblem2 ⊢ φ ∧ i ∈ ℕ ∧ ∀ y ∈ 1 … i if y ∈ ℕ 1 0 ≤ F ⁡ y ∧ p ∈ ℙ ∧ p ∥ i + 1 → if i + 1 ∈ ℕ 1 0 ≤ F ⁡ i + 1
70 55 69 rexlimddv ⊢ φ ∧ i ∈ ℕ ∧ ∀ y ∈ 1 … i if y ∈ ℕ 1 0 ≤ F ⁡ y → if i + 1 ∈ ℕ 1 0 ≤ F ⁡ i + 1
71 ovex ⊢ i + 1 ∈ V
72 fveq2 ⊢ y = i + 1 → y = i + 1
73 72 eleq1d ⊢ y = i + 1 → y ∈ ℕ ↔ i + 1 ∈ ℕ
74 73 ifbid ⊢ y = i + 1 → if y ∈ ℕ 1 0 = if i + 1 ∈ ℕ 1 0
75 fveq2 ⊢ y = i + 1 → F ⁡ y = F ⁡ i + 1
76 74 75 breq12d ⊢ y = i + 1 → if y ∈ ℕ 1 0 ≤ F ⁡ y ↔ if i + 1 ∈ ℕ 1 0 ≤ F ⁡ i + 1
77 71 76 ralsn ⊢ ∀ y ∈ i + 1 if y ∈ ℕ 1 0 ≤ F ⁡ y ↔ if i + 1 ∈ ℕ 1 0 ≤ F ⁡ i + 1
78 70 77 sylibr ⊢ φ ∧ i ∈ ℕ ∧ ∀ y ∈ 1 … i if y ∈ ℕ 1 0 ≤ F ⁡ y → ∀ y ∈ i + 1 if y ∈ ℕ 1 0 ≤ F ⁡ y
79 78 expr ⊢ φ ∧ i ∈ ℕ → ∀ y ∈ 1 … i if y ∈ ℕ 1 0 ≤ F ⁡ y → ∀ y ∈ i + 1 if y ∈ ℕ 1 0 ≤ F ⁡ y
80 79 ancld ⊢ φ ∧ i ∈ ℕ → ∀ y ∈ 1 … i if y ∈ ℕ 1 0 ≤ F ⁡ y → ∀ y ∈ 1 … i if y ∈ ℕ 1 0 ≤ F ⁡ y ∧ ∀ y ∈ i + 1 if y ∈ ℕ 1 0 ≤ F ⁡ y
81 fzsuc ⊢ i ∈ ℤ ≥ 1 → 1 … i + 1 = 1 … i ∪ i + 1
82 47 81 syl ⊢ φ ∧ i ∈ ℕ → 1 … i + 1 = 1 … i ∪ i + 1
83 82 raleqdv ⊢ φ ∧ i ∈ ℕ → ∀ y ∈ 1 … i + 1 if y ∈ ℕ 1 0 ≤ F ⁡ y ↔ ∀ y ∈ 1 … i ∪ i + 1 if y ∈ ℕ 1 0 ≤ F ⁡ y
84 ralunb ⊢ ∀ y ∈ 1 … i ∪ i + 1 if y ∈ ℕ 1 0 ≤ F ⁡ y ↔ ∀ y ∈ 1 … i if y ∈ ℕ 1 0 ≤ F ⁡ y ∧ ∀ y ∈ i + 1 if y ∈ ℕ 1 0 ≤ F ⁡ y
85 83 84 bitrdi ⊢ φ ∧ i ∈ ℕ → ∀ y ∈ 1 … i + 1 if y ∈ ℕ 1 0 ≤ F ⁡ y ↔ ∀ y ∈ 1 … i if y ∈ ℕ 1 0 ≤ F ⁡ y ∧ ∀ y ∈ i + 1 if y ∈ ℕ 1 0 ≤ F ⁡ y
86 80 85 sylibrd ⊢ φ ∧ i ∈ ℕ → ∀ y ∈ 1 … i if y ∈ ℕ 1 0 ≤ F ⁡ y → ∀ y ∈ 1 … i + 1 if y ∈ ℕ 1 0 ≤ F ⁡ y
87 86 expcom ⊢ i ∈ ℕ → φ → ∀ y ∈ 1 … i if y ∈ ℕ 1 0 ≤ F ⁡ y → ∀ y ∈ 1 … i + 1 if y ∈ ℕ 1 0 ≤ F ⁡ y
88 87 a2d ⊢ i ∈ ℕ → φ → ∀ y ∈ 1 … i if y ∈ ℕ 1 0 ≤ F ⁡ y → φ → ∀ y ∈ 1 … i + 1 if y ∈ ℕ 1 0 ≤ F ⁡ y
89 18 21 24 27 44 88 nnind ⊢ A ∈ ℕ → φ → ∀ y ∈ 1 … A if y ∈ ℕ 1 0 ≤ F ⁡ y
90 10 89 mpcom ⊢ φ → ∀ y ∈ 1 … A if y ∈ ℕ 1 0 ≤ F ⁡ y
91 10 46 eleqtrdi ⊢ φ → A ∈ ℤ ≥ 1
92 eluzfz2 ⊢ A ∈ ℤ ≥ 1 → A ∈ 1 … A
93 91 92 syl ⊢ φ → A ∈ 1 … A
94 15 90 93 rspcdva ⊢ φ → if A ∈ ℕ 1 0 ≤ F ⁡ A