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=BaseG
rpvmasum2.1 ⊢1˙=0G
dchrisum0f.f ⊢F=b∈ℕ⟼∑v∈q∈ℕ|q∥bX⁡L⁡v
dchrisum0f.x ⊢φ→X∈D
dchrisum0flb.r ⊢φ→X:BaseZ⟶ℝ
dchrisum0flb.a ⊢φ→A∈ℕ
Assertion dchrisum0flb ⊢φ→ifA∈ℕ10≤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=BaseG
6 rpvmasum2.1 ⊢1˙=0G
7 dchrisum0f.f ⊢F=b∈ℕ⟼∑v∈q∈ℕ|q∥bX⁡L⁡v
8 dchrisum0f.x ⊢φ→X∈D
9 dchrisum0flb.r ⊢φ→X:BaseZ⟶ℝ
10 dchrisum0flb.a ⊢φ→A∈ℕ
11 fveq2 ⊢y=A→y=A
12 11 eleq1d ⊢y=A→y∈ℕ↔A∈ℕ
13 12 ifbid ⊢y=A→ify∈ℕ10=ifA∈ℕ10
14 fveq2 ⊢y=A→F⁡y=F⁡A
15 13 14 breq12d ⊢y=A→ify∈ℕ10≤F⁡y↔ifA∈ℕ10≤F⁡A
16 oveq2 ⊢k=1→1…k=1…1
17 16 raleqdv ⊢k=1→∀y∈1…kify∈ℕ10≤F⁡y↔∀y∈1…1ify∈ℕ10≤F⁡y
18 17 imbi2d ⊢k=1→φ→∀y∈1…kify∈ℕ10≤F⁡y↔φ→∀y∈1…1ify∈ℕ10≤F⁡y
19 oveq2 ⊢k=i→1…k=1…i
20 19 raleqdv ⊢k=i→∀y∈1…kify∈ℕ10≤F⁡y↔∀y∈1…iify∈ℕ10≤F⁡y
21 20 imbi2d ⊢k=i→φ→∀y∈1…kify∈ℕ10≤F⁡y↔φ→∀y∈1…iify∈ℕ10≤F⁡y
22 oveq2 ⊢k=i+1→1…k=1…i+1
23 22 raleqdv ⊢k=i+1→∀y∈1…kify∈ℕ10≤F⁡y↔∀y∈1…i+1ify∈ℕ10≤F⁡y
24 23 imbi2d ⊢k=i+1→φ→∀y∈1…kify∈ℕ10≤F⁡y↔φ→∀y∈1…i+1ify∈ℕ10≤F⁡y
25 oveq2 ⊢k=A→1…k=1…A
26 25 raleqdv ⊢k=A→∀y∈1…kify∈ℕ10≤F⁡y↔∀y∈1…Aify∈ℕ10≤F⁡y
27 26 imbi2d ⊢k=A→φ→∀y∈1…kify∈ℕ10≤F⁡y↔φ→∀y∈1…Aify∈ℕ10≤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 ⊢φ→if20∈ℕ10≤F⁡20
33 elfz1eq ⊢y∈1…1→y=1
34 2nn0 ⊢2∈ℕ0
35 34 numexp0 ⊢20=1
36 33 35 eqtr4di ⊢y∈1…1→y=20
37 36 fveq2d ⊢y∈1…1→y=20
38 37 eleq1d ⊢y∈1…1→y∈ℕ↔20∈ℕ
39 38 ifbid ⊢y∈1…1→ify∈ℕ10=if20∈ℕ10
40 36 fveq2d ⊢y∈1…1→F⁡y=F⁡20
41 39 40 breq12d ⊢y∈1…1→ify∈ℕ10≤F⁡y↔if20∈ℕ10≤F⁡20
42 41 biimprcd ⊢if20∈ℕ10≤F⁡20→y∈1…1→ify∈ℕ10≤F⁡y
43 42 ralrimiv ⊢if20∈ℕ10≤F⁡20→∀y∈1…1ify∈ℕ10≤F⁡y
44 32 43 syl ⊢φ→∀y∈1…1ify∈ℕ10≤F⁡y
45 simpr ⊢φ∧i∈ℕ→i∈ℕ
46 nnuz ⊢ℕ=ℤ≥1
47 45 46 eleqtrdi ⊢φ∧i∈ℕ→i∈ℤ≥1
48 47 adantrr ⊢φ∧i∈ℕ∧∀y∈1…iify∈ℕ10≤F⁡y→i∈ℤ≥1
49 eluzp1p1 ⊢i∈ℤ≥1→i+1∈ℤ≥1+1
50 48 49 syl ⊢φ∧i∈ℕ∧∀y∈1…iify∈ℕ10≤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…iify∈ℕ10≤F⁡y→i+1∈ℤ≥2
54 exprmfct ⊢i+1∈ℤ≥2→∃p∈ℙp∥i+1
55 53 54 syl ⊢φ∧i∈ℕ∧∀y∈1…iify∈ℕ10≤F⁡y→∃p∈ℙp∥i+1
56 3 ad2antrr ⊢φ∧i∈ℕ∧∀y∈1…iify∈ℕ10≤F⁡y∧p∈ℙ∧p∥i+1→N∈ℕ
57 8 ad2antrr ⊢φ∧i∈ℕ∧∀y∈1…iify∈ℕ10≤F⁡y∧p∈ℙ∧p∥i+1→X∈D
58 9 ad2antrr ⊢φ∧i∈ℕ∧∀y∈1…iify∈ℕ10≤F⁡y∧p∈ℙ∧p∥i+1→X:BaseZ⟶ℝ
59 53 adantr ⊢φ∧i∈ℕ∧∀y∈1…iify∈ℕ10≤F⁡y∧p∈ℙ∧p∥i+1→i+1∈ℤ≥2
60 simprl ⊢φ∧i∈ℕ∧∀y∈1…iify∈ℕ10≤F⁡y∧p∈ℙ∧p∥i+1→p∈ℙ
61 simprr ⊢φ∧i∈ℕ∧∀y∈1…iify∈ℕ10≤F⁡y∧p∈ℙ∧p∥i+1→p∥i+1
62 simplrr ⊢φ∧i∈ℕ∧∀y∈1…iify∈ℕ10≤F⁡y∧p∈ℙ∧p∥i+1→∀y∈1…iify∈ℕ10≤F⁡y
63 simplrl ⊢φ∧i∈ℕ∧∀y∈1…iify∈ℕ10≤F⁡y∧p∈ℙ∧p∥i+1→i∈ℕ
64 63 nnzd ⊢φ∧i∈ℕ∧∀y∈1…iify∈ℕ10≤F⁡y∧p∈ℙ∧p∥i+1→i∈ℤ
65 fzval3 ⊢i∈ℤ→1…i=1..^i+1
66 64 65 syl ⊢φ∧i∈ℕ∧∀y∈1…iify∈ℕ10≤F⁡y∧p∈ℙ∧p∥i+1→1…i=1..^i+1
67 66 raleqdv ⊢φ∧i∈ℕ∧∀y∈1…iify∈ℕ10≤F⁡y∧p∈ℙ∧p∥i+1→∀y∈1…iify∈ℕ10≤F⁡y↔∀y∈1..^i+1ify∈ℕ10≤F⁡y
68 62 67 mpbid ⊢φ∧i∈ℕ∧∀y∈1…iify∈ℕ10≤F⁡y∧p∈ℙ∧p∥i+1→∀y∈1..^i+1ify∈ℕ10≤F⁡y
69 1 2 56 4 5 6 7 57 58 59 60 61 68 dchrisum0flblem2 ⊢φ∧i∈ℕ∧∀y∈1…iify∈ℕ10≤F⁡y∧p∈ℙ∧p∥i+1→ifi+1∈ℕ10≤F⁡i+1
70 55 69 rexlimddv ⊢φ∧i∈ℕ∧∀y∈1…iify∈ℕ10≤F⁡y→ifi+1∈ℕ10≤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→ify∈ℕ10=ifi+1∈ℕ10
75 fveq2 ⊢y=i+1→F⁡y=F⁡i+1
76 74 75 breq12d ⊢y=i+1→ify∈ℕ10≤F⁡y↔ifi+1∈ℕ10≤F⁡i+1
77 71 76 ralsn ⊢∀y∈i+1ify∈ℕ10≤F⁡y↔ifi+1∈ℕ10≤F⁡i+1
78 70 77 sylibr ⊢φ∧i∈ℕ∧∀y∈1…iify∈ℕ10≤F⁡y→∀y∈i+1ify∈ℕ10≤F⁡y
79 78 expr ⊢φ∧i∈ℕ→∀y∈1…iify∈ℕ10≤F⁡y→∀y∈i+1ify∈ℕ10≤F⁡y
80 79 ancld ⊢φ∧i∈ℕ→∀y∈1…iify∈ℕ10≤F⁡y→∀y∈1…iify∈ℕ10≤F⁡y∧∀y∈i+1ify∈ℕ10≤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+1ify∈ℕ10≤F⁡y↔∀y∈1…i∪i+1ify∈ℕ10≤F⁡y
84 ralunb ⊢∀y∈1…i∪i+1ify∈ℕ10≤F⁡y↔∀y∈1…iify∈ℕ10≤F⁡y∧∀y∈i+1ify∈ℕ10≤F⁡y
85 83 84 bitrdi ⊢φ∧i∈ℕ→∀y∈1…i+1ify∈ℕ10≤F⁡y↔∀y∈1…iify∈ℕ10≤F⁡y∧∀y∈i+1ify∈ℕ10≤F⁡y
86 80 85 sylibrd ⊢φ∧i∈ℕ→∀y∈1…iify∈ℕ10≤F⁡y→∀y∈1…i+1ify∈ℕ10≤F⁡y
87 86 expcom ⊢i∈ℕ→φ→∀y∈1…iify∈ℕ10≤F⁡y→∀y∈1…i+1ify∈ℕ10≤F⁡y
88 87 a2d ⊢i∈ℕ→φ→∀y∈1…iify∈ℕ10≤F⁡y→φ→∀y∈1…i+1ify∈ℕ10≤F⁡y
89 18 21 24 27 44 88 nnind ⊢A∈ℕ→φ→∀y∈1…Aify∈ℕ10≤F⁡y
90 10 89 mpcom ⊢φ→∀y∈1…Aify∈ℕ10≤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 ⊢φ→ifA∈ℕ10≤F⁡A