Metamath Proof Explorer


Axiom ax-hgt749

Description: Statement 7.49 of Helfgott p. 70. For a sufficiently big odd N , this postulates the existence of smoothing functions h (eta star) and k (eta plus) such that the lower bound for the circle integral is big enough. (Contributed by Thierry Arnoux, 15-Dec-2021)

Ref Expression
Assertion ax-hgt749
|- A. n e. { z e. ZZ | -. 2 || z } ( ( ; 1 0 ^ ; 2 7 ) <_ n -> E. h e. ( ( 0 [,) +oo ) ^m NN ) E. k e. ( ( 0 [,) +oo ) ^m NN ) ( A. m e. NN ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) /\ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( n ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts n ) ` x ) x. ( ( ( ( Lam oF x. k ) vts n ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u n x. x ) ) ) ) _d x ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 vn
 |-  n
1 vz
 |-  z
2 cz
 |-  ZZ
3 c2
 |-  2
4 cdvds
 |-  ||
5 1 cv
 |-  z
6 3 5 4 wbr
 |-  2 || z
7 6 wn
 |-  -. 2 || z
8 7 1 2 crab
 |-  { z e. ZZ | -. 2 || z }
9 c1
 |-  1
10 cc0
 |-  0
11 9 10 cdc
 |-  ; 1 0
12 cexp
 |-  ^
13 c7
 |-  7
14 3 13 cdc
 |-  ; 2 7
15 11 14 12 co
 |-  ( ; 1 0 ^ ; 2 7 )
16 cle
 |-  <_
17 0 cv
 |-  n
18 15 17 16 wbr
 |-  ( ; 1 0 ^ ; 2 7 ) <_ n
19 vh
 |-  h
20 cico
 |-  [,)
21 cpnf
 |-  +oo
22 10 21 20 co
 |-  ( 0 [,) +oo )
23 cmap
 |-  ^m
24 cn
 |-  NN
25 22 24 23 co
 |-  ( ( 0 [,) +oo ) ^m NN )
26 vk
 |-  k
27 vm
 |-  m
28 26 cv
 |-  k
29 27 cv
 |-  m
30 29 28 cfv
 |-  ( k ` m )
31 cdp
 |-  .
32 c9
 |-  9
33 c5
 |-  5
34 33 33 cdp2
 |-  _ 5 5
35 32 34 cdp2
 |-  _ 9 _ 5 5
36 32 35 cdp2
 |-  _ 9 _ 9 _ 5 5
37 13 36 cdp2
 |-  _ 7 _ 9 _ 9 _ 5 5
38 10 37 cdp2
 |-  _ 0 _ 7 _ 9 _ 9 _ 5 5
39 9 38 31 co
 |-  ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 )
40 30 39 16 wbr
 |-  ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 )
41 40 27 24 wral
 |-  A. m e. NN ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 )
42 19 cv
 |-  h
43 29 42 cfv
 |-  ( h ` m )
44 c4
 |-  4
45 9 44 cdp2
 |-  _ 1 4
46 44 45 cdp2
 |-  _ 4 _ 1 4
47 9 46 31 co
 |-  ( 1 . _ 4 _ 1 4 )
48 43 47 16 wbr
 |-  ( h ` m ) <_ ( 1 . _ 4 _ 1 4 )
49 48 27 24 wral
 |-  A. m e. NN ( h ` m ) <_ ( 1 . _ 4 _ 1 4 )
50 c8
 |-  8
51 44 50 cdp2
 |-  _ 4 8
52 3 51 cdp2
 |-  _ 2 _ 4 8
53 3 52 cdp2
 |-  _ 2 _ 2 _ 4 8
54 44 53 cdp2
 |-  _ 4 _ 2 _ 2 _ 4 8
55 10 54 cdp2
 |-  _ 0 _ 4 _ 2 _ 2 _ 4 8
56 10 55 cdp2
 |-  _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8
57 10 56 cdp2
 |-  _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8
58 10 57 31 co
 |-  ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 )
59 cmul
 |-  x.
60 17 3 12 co
 |-  ( n ^ 2 )
61 58 60 59 co
 |-  ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( n ^ 2 ) )
62 cioo
 |-  (,)
63 10 9 62 co
 |-  ( 0 (,) 1 )
64 cvma
 |-  Lam
65 59 cof
 |-  oF x.
66 64 42 65 co
 |-  ( Lam oF x. h )
67 cvts
 |-  vts
68 66 17 67 co
 |-  ( ( Lam oF x. h ) vts n )
69 vx
 |-  x
70 69 cv
 |-  x
71 70 68 cfv
 |-  ( ( ( Lam oF x. h ) vts n ) ` x )
72 64 28 65 co
 |-  ( Lam oF x. k )
73 72 17 67 co
 |-  ( ( Lam oF x. k ) vts n )
74 70 73 cfv
 |-  ( ( ( Lam oF x. k ) vts n ) ` x )
75 74 3 12 co
 |-  ( ( ( ( Lam oF x. k ) vts n ) ` x ) ^ 2 )
76 71 75 59 co
 |-  ( ( ( ( Lam oF x. h ) vts n ) ` x ) x. ( ( ( ( Lam oF x. k ) vts n ) ` x ) ^ 2 ) )
77 ce
 |-  exp
78 ci
 |-  _i
79 cpi
 |-  _pi
80 3 79 59 co
 |-  ( 2 x. _pi )
81 78 80 59 co
 |-  ( _i x. ( 2 x. _pi ) )
82 17 cneg
 |-  -u n
83 82 70 59 co
 |-  ( -u n x. x )
84 81 83 59 co
 |-  ( ( _i x. ( 2 x. _pi ) ) x. ( -u n x. x ) )
85 84 77 cfv
 |-  ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u n x. x ) ) )
86 76 85 59 co
 |-  ( ( ( ( ( Lam oF x. h ) vts n ) ` x ) x. ( ( ( ( Lam oF x. k ) vts n ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u n x. x ) ) ) )
87 69 63 86 citg
 |-  S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts n ) ` x ) x. ( ( ( ( Lam oF x. k ) vts n ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u n x. x ) ) ) ) _d x
88 61 87 16 wbr
 |-  ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( n ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts n ) ` x ) x. ( ( ( ( Lam oF x. k ) vts n ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u n x. x ) ) ) ) _d x
89 41 49 88 w3a
 |-  ( A. m e. NN ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) /\ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( n ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts n ) ` x ) x. ( ( ( ( Lam oF x. k ) vts n ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u n x. x ) ) ) ) _d x )
90 89 26 25 wrex
 |-  E. k e. ( ( 0 [,) +oo ) ^m NN ) ( A. m e. NN ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) /\ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( n ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts n ) ` x ) x. ( ( ( ( Lam oF x. k ) vts n ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u n x. x ) ) ) ) _d x )
91 90 19 25 wrex
 |-  E. h e. ( ( 0 [,) +oo ) ^m NN ) E. k e. ( ( 0 [,) +oo ) ^m NN ) ( A. m e. NN ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) /\ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( n ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts n ) ` x ) x. ( ( ( ( Lam oF x. k ) vts n ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u n x. x ) ) ) ) _d x )
92 18 91 wi
 |-  ( ( ; 1 0 ^ ; 2 7 ) <_ n -> E. h e. ( ( 0 [,) +oo ) ^m NN ) E. k e. ( ( 0 [,) +oo ) ^m NN ) ( A. m e. NN ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) /\ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( n ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts n ) ` x ) x. ( ( ( ( Lam oF x. k ) vts n ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u n x. x ) ) ) ) _d x ) )
93 92 0 8 wral
 |-  A. n e. { z e. ZZ | -. 2 || z } ( ( ; 1 0 ^ ; 2 7 ) <_ n -> E. h e. ( ( 0 [,) +oo ) ^m NN ) E. k e. ( ( 0 [,) +oo ) ^m NN ) ( A. m e. NN ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) /\ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( n ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts n ) ` x ) x. ( ( ( ( Lam oF x. k ) vts n ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u n x. x ) ) ) ) _d x ) )