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 = ( Z/nZ ` N )
rpvmasum.l 
|- L = ( ZRHom ` Z )
rpvmasum.a 
|- ( ph -> N e. NN )
rpvmasum2.g 
|- G = ( DChr ` N )
rpvmasum2.d 
|- D = ( Base ` G )
rpvmasum2.1 
|- .1. = ( 0g ` G )
dchrisum0f.f 
|- F = ( b e. NN |-> sum_ v e. { q e. NN | q || b } ( X ` ( L ` v ) ) )
dchrisum0f.x 
|- ( ph -> X e. D )
dchrisum0flb.r 
|- ( ph -> X : ( Base ` Z ) --> RR )
dchrisum0flb.a 
|- ( ph -> A e. NN )
Assertion dchrisum0flb 
|- ( ph -> if ( ( sqrt ` A ) e. NN , 1 , 0 ) <_ ( F ` A ) )

Proof

Step Hyp Ref Expression
1 rpvmasum.z 
 |-  Z = ( Z/nZ ` N )
2 rpvmasum.l 
 |-  L = ( ZRHom ` Z )
3 rpvmasum.a 
 |-  ( ph -> N e. NN )
4 rpvmasum2.g 
 |-  G = ( DChr ` N )
5 rpvmasum2.d 
 |-  D = ( Base ` G )
6 rpvmasum2.1 
 |-  .1. = ( 0g ` G )
7 dchrisum0f.f 
 |-  F = ( b e. NN |-> sum_ v e. { q e. NN | q || b } ( X ` ( L ` v ) ) )
8 dchrisum0f.x 
 |-  ( ph -> X e. D )
9 dchrisum0flb.r 
 |-  ( ph -> X : ( Base ` Z ) --> RR )
10 dchrisum0flb.a 
 |-  ( ph -> A e. NN )
11 fveq2 
 |-  ( y = A -> ( sqrt ` y ) = ( sqrt ` A ) )
12 11 eleq1d 
 |-  ( y = A -> ( ( sqrt ` y ) e. NN <-> ( sqrt ` A ) e. NN ) )
13 12 ifbid 
 |-  ( y = A -> if ( ( sqrt ` y ) e. NN , 1 , 0 ) = if ( ( sqrt ` A ) e. NN , 1 , 0 ) )
14 fveq2 
 |-  ( y = A -> ( F ` y ) = ( F ` A ) )
15 13 14 breq12d 
 |-  ( y = A -> ( if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) <-> if ( ( sqrt ` A ) e. NN , 1 , 0 ) <_ ( F ` A ) ) )
16 oveq2 
 |-  ( k = 1 -> ( 1 ... k ) = ( 1 ... 1 ) )
17 16 raleqdv 
 |-  ( k = 1 -> ( A. y e. ( 1 ... k ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) <-> A. y e. ( 1 ... 1 ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) )
18 17 imbi2d 
 |-  ( k = 1 -> ( ( ph -> A. y e. ( 1 ... k ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) <-> ( ph -> A. y e. ( 1 ... 1 ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) ) )
19 oveq2 
 |-  ( k = i -> ( 1 ... k ) = ( 1 ... i ) )
20 19 raleqdv 
 |-  ( k = i -> ( A. y e. ( 1 ... k ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) <-> A. y e. ( 1 ... i ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) )
21 20 imbi2d 
 |-  ( k = i -> ( ( ph -> A. y e. ( 1 ... k ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) <-> ( ph -> A. y e. ( 1 ... i ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) ) )
22 oveq2 
 |-  ( k = ( i + 1 ) -> ( 1 ... k ) = ( 1 ... ( i + 1 ) ) )
23 22 raleqdv 
 |-  ( k = ( i + 1 ) -> ( A. y e. ( 1 ... k ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) <-> A. y e. ( 1 ... ( i + 1 ) ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) )
24 23 imbi2d 
 |-  ( k = ( i + 1 ) -> ( ( ph -> A. y e. ( 1 ... k ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) <-> ( ph -> A. y e. ( 1 ... ( i + 1 ) ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) ) )
25 oveq2 
 |-  ( k = A -> ( 1 ... k ) = ( 1 ... A ) )
26 25 raleqdv 
 |-  ( k = A -> ( A. y e. ( 1 ... k ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) <-> A. y e. ( 1 ... A ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) )
27 26 imbi2d 
 |-  ( k = A -> ( ( ph -> A. y e. ( 1 ... k ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) <-> ( ph -> A. y e. ( 1 ... A ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) ) )
28 2prm 
 |-  2 e. Prime
29 28 a1i 
 |-  ( ph -> 2 e. Prime )
30 0nn0 
 |-  0 e. NN0
31 30 a1i 
 |-  ( ph -> 0 e. NN0 )
32 1 2 3 4 5 6 7 8 9 29 31 dchrisum0flblem1 
 |-  ( ph -> if ( ( sqrt ` ( 2 ^ 0 ) ) e. NN , 1 , 0 ) <_ ( F ` ( 2 ^ 0 ) ) )
33 elfz1eq 
 |-  ( y e. ( 1 ... 1 ) -> y = 1 )
34 2nn0 
 |-  2 e. NN0
35 34 numexp0 
 |-  ( 2 ^ 0 ) = 1
36 33 35 eqtr4di 
 |-  ( y e. ( 1 ... 1 ) -> y = ( 2 ^ 0 ) )
37 36 fveq2d 
 |-  ( y e. ( 1 ... 1 ) -> ( sqrt ` y ) = ( sqrt ` ( 2 ^ 0 ) ) )
38 37 eleq1d 
 |-  ( y e. ( 1 ... 1 ) -> ( ( sqrt ` y ) e. NN <-> ( sqrt ` ( 2 ^ 0 ) ) e. NN ) )
39 38 ifbid 
 |-  ( y e. ( 1 ... 1 ) -> if ( ( sqrt ` y ) e. NN , 1 , 0 ) = if ( ( sqrt ` ( 2 ^ 0 ) ) e. NN , 1 , 0 ) )
40 36 fveq2d 
 |-  ( y e. ( 1 ... 1 ) -> ( F ` y ) = ( F ` ( 2 ^ 0 ) ) )
41 39 40 breq12d 
 |-  ( y e. ( 1 ... 1 ) -> ( if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) <-> if ( ( sqrt ` ( 2 ^ 0 ) ) e. NN , 1 , 0 ) <_ ( F ` ( 2 ^ 0 ) ) ) )
42 41 biimprcd 
 |-  ( if ( ( sqrt ` ( 2 ^ 0 ) ) e. NN , 1 , 0 ) <_ ( F ` ( 2 ^ 0 ) ) -> ( y e. ( 1 ... 1 ) -> if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) )
43 42 ralrimiv 
 |-  ( if ( ( sqrt ` ( 2 ^ 0 ) ) e. NN , 1 , 0 ) <_ ( F ` ( 2 ^ 0 ) ) -> A. y e. ( 1 ... 1 ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) )
44 32 43 syl 
 |-  ( ph -> A. y e. ( 1 ... 1 ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) )
45 simpr 
 |-  ( ( ph /\ i e. NN ) -> i e. NN )
46 nnuz 
 |-  NN = ( ZZ>= ` 1 )
47 45 46 eleqtrdi 
 |-  ( ( ph /\ i e. NN ) -> i e. ( ZZ>= ` 1 ) )
48 47 adantrr 
 |-  ( ( ph /\ ( i e. NN /\ A. y e. ( 1 ... i ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) ) -> i e. ( ZZ>= ` 1 ) )
49 eluzp1p1 
 |-  ( i e. ( ZZ>= ` 1 ) -> ( i + 1 ) e. ( ZZ>= ` ( 1 + 1 ) ) )
50 48 49 syl 
 |-  ( ( ph /\ ( i e. NN /\ A. y e. ( 1 ... i ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) ) -> ( i + 1 ) e. ( ZZ>= ` ( 1 + 1 ) ) )
51 df-2 
 |-  2 = ( 1 + 1 )
52 51 fveq2i 
 |-  ( ZZ>= ` 2 ) = ( ZZ>= ` ( 1 + 1 ) )
53 50 52 eleqtrrdi 
 |-  ( ( ph /\ ( i e. NN /\ A. y e. ( 1 ... i ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) ) -> ( i + 1 ) e. ( ZZ>= ` 2 ) )
54 exprmfct 
 |-  ( ( i + 1 ) e. ( ZZ>= ` 2 ) -> E. p e. Prime p || ( i + 1 ) )
55 53 54 syl 
 |-  ( ( ph /\ ( i e. NN /\ A. y e. ( 1 ... i ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) ) -> E. p e. Prime p || ( i + 1 ) )
56 3 ad2antrr 
 |-  ( ( ( ph /\ ( i e. NN /\ A. y e. ( 1 ... i ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) ) /\ ( p e. Prime /\ p || ( i + 1 ) ) ) -> N e. NN )
57 8 ad2antrr 
 |-  ( ( ( ph /\ ( i e. NN /\ A. y e. ( 1 ... i ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) ) /\ ( p e. Prime /\ p || ( i + 1 ) ) ) -> X e. D )
58 9 ad2antrr 
 |-  ( ( ( ph /\ ( i e. NN /\ A. y e. ( 1 ... i ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) ) /\ ( p e. Prime /\ p || ( i + 1 ) ) ) -> X : ( Base ` Z ) --> RR )
59 53 adantr 
 |-  ( ( ( ph /\ ( i e. NN /\ A. y e. ( 1 ... i ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) ) /\ ( p e. Prime /\ p || ( i + 1 ) ) ) -> ( i + 1 ) e. ( ZZ>= ` 2 ) )
60 simprl 
 |-  ( ( ( ph /\ ( i e. NN /\ A. y e. ( 1 ... i ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) ) /\ ( p e. Prime /\ p || ( i + 1 ) ) ) -> p e. Prime )
61 simprr 
 |-  ( ( ( ph /\ ( i e. NN /\ A. y e. ( 1 ... i ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) ) /\ ( p e. Prime /\ p || ( i + 1 ) ) ) -> p || ( i + 1 ) )
62 simplrr 
 |-  ( ( ( ph /\ ( i e. NN /\ A. y e. ( 1 ... i ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) ) /\ ( p e. Prime /\ p || ( i + 1 ) ) ) -> A. y e. ( 1 ... i ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) )
63 simplrl 
 |-  ( ( ( ph /\ ( i e. NN /\ A. y e. ( 1 ... i ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) ) /\ ( p e. Prime /\ p || ( i + 1 ) ) ) -> i e. NN )
64 63 nnzd 
 |-  ( ( ( ph /\ ( i e. NN /\ A. y e. ( 1 ... i ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) ) /\ ( p e. Prime /\ p || ( i + 1 ) ) ) -> i e. ZZ )
65 fzval3 
 |-  ( i e. ZZ -> ( 1 ... i ) = ( 1 ..^ ( i + 1 ) ) )
66 64 65 syl 
 |-  ( ( ( ph /\ ( i e. NN /\ A. y e. ( 1 ... i ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) ) /\ ( p e. Prime /\ p || ( i + 1 ) ) ) -> ( 1 ... i ) = ( 1 ..^ ( i + 1 ) ) )
67 66 raleqdv 
 |-  ( ( ( ph /\ ( i e. NN /\ A. y e. ( 1 ... i ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) ) /\ ( p e. Prime /\ p || ( i + 1 ) ) ) -> ( A. y e. ( 1 ... i ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) <-> A. y e. ( 1 ..^ ( i + 1 ) ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) )
68 62 67 mpbid 
 |-  ( ( ( ph /\ ( i e. NN /\ A. y e. ( 1 ... i ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) ) /\ ( p e. Prime /\ p || ( i + 1 ) ) ) -> A. y e. ( 1 ..^ ( i + 1 ) ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) )
69 1 2 56 4 5 6 7 57 58 59 60 61 68 dchrisum0flblem2 
 |-  ( ( ( ph /\ ( i e. NN /\ A. y e. ( 1 ... i ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) ) /\ ( p e. Prime /\ p || ( i + 1 ) ) ) -> if ( ( sqrt ` ( i + 1 ) ) e. NN , 1 , 0 ) <_ ( F ` ( i + 1 ) ) )
70 55 69 rexlimddv 
 |-  ( ( ph /\ ( i e. NN /\ A. y e. ( 1 ... i ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) ) -> if ( ( sqrt ` ( i + 1 ) ) e. NN , 1 , 0 ) <_ ( F ` ( i + 1 ) ) )
71 ovex 
 |-  ( i + 1 ) e. _V
72 fveq2 
 |-  ( y = ( i + 1 ) -> ( sqrt ` y ) = ( sqrt ` ( i + 1 ) ) )
73 72 eleq1d 
 |-  ( y = ( i + 1 ) -> ( ( sqrt ` y ) e. NN <-> ( sqrt ` ( i + 1 ) ) e. NN ) )
74 73 ifbid 
 |-  ( y = ( i + 1 ) -> if ( ( sqrt ` y ) e. NN , 1 , 0 ) = if ( ( sqrt ` ( i + 1 ) ) e. NN , 1 , 0 ) )
75 fveq2 
 |-  ( y = ( i + 1 ) -> ( F ` y ) = ( F ` ( i + 1 ) ) )
76 74 75 breq12d 
 |-  ( y = ( i + 1 ) -> ( if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) <-> if ( ( sqrt ` ( i + 1 ) ) e. NN , 1 , 0 ) <_ ( F ` ( i + 1 ) ) ) )
77 71 76 ralsn 
 |-  ( A. y e. { ( i + 1 ) } if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) <-> if ( ( sqrt ` ( i + 1 ) ) e. NN , 1 , 0 ) <_ ( F ` ( i + 1 ) ) )
78 70 77 sylibr 
 |-  ( ( ph /\ ( i e. NN /\ A. y e. ( 1 ... i ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) ) -> A. y e. { ( i + 1 ) } if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) )
79 78 expr 
 |-  ( ( ph /\ i e. NN ) -> ( A. y e. ( 1 ... i ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) -> A. y e. { ( i + 1 ) } if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) )
80 79 ancld 
 |-  ( ( ph /\ i e. NN ) -> ( A. y e. ( 1 ... i ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) -> ( A. y e. ( 1 ... i ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) /\ A. y e. { ( i + 1 ) } if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) ) )
81 fzsuc 
 |-  ( i e. ( ZZ>= ` 1 ) -> ( 1 ... ( i + 1 ) ) = ( ( 1 ... i ) u. { ( i + 1 ) } ) )
82 47 81 syl 
 |-  ( ( ph /\ i e. NN ) -> ( 1 ... ( i + 1 ) ) = ( ( 1 ... i ) u. { ( i + 1 ) } ) )
83 82 raleqdv 
 |-  ( ( ph /\ i e. NN ) -> ( A. y e. ( 1 ... ( i + 1 ) ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) <-> A. y e. ( ( 1 ... i ) u. { ( i + 1 ) } ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) )
84 ralunb 
 |-  ( A. y e. ( ( 1 ... i ) u. { ( i + 1 ) } ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) <-> ( A. y e. ( 1 ... i ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) /\ A. y e. { ( i + 1 ) } if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) )
85 83 84 bitrdi 
 |-  ( ( ph /\ i e. NN ) -> ( A. y e. ( 1 ... ( i + 1 ) ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) <-> ( A. y e. ( 1 ... i ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) /\ A. y e. { ( i + 1 ) } if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) ) )
86 80 85 sylibrd 
 |-  ( ( ph /\ i e. NN ) -> ( A. y e. ( 1 ... i ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) -> A. y e. ( 1 ... ( i + 1 ) ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) )
87 86 expcom 
 |-  ( i e. NN -> ( ph -> ( A. y e. ( 1 ... i ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) -> A. y e. ( 1 ... ( i + 1 ) ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) ) )
88 87 a2d 
 |-  ( i e. NN -> ( ( ph -> A. y e. ( 1 ... i ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) -> ( ph -> A. y e. ( 1 ... ( i + 1 ) ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) ) )
89 18 21 24 27 44 88 nnind 
 |-  ( A e. NN -> ( ph -> A. y e. ( 1 ... A ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) ) )
90 10 89 mpcom 
 |-  ( ph -> A. y e. ( 1 ... A ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) )
91 10 46 eleqtrdi 
 |-  ( ph -> A e. ( ZZ>= ` 1 ) )
92 eluzfz2 
 |-  ( A e. ( ZZ>= ` 1 ) -> A e. ( 1 ... A ) )
93 91 92 syl 
 |-  ( ph -> A e. ( 1 ... A ) )
94 15 90 93 rspcdva 
 |-  ( ph -> if ( ( sqrt ` A ) e. NN , 1 , 0 ) <_ ( F ` A ) )