This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )