Axiom ax-hgt749 30722

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

Assertion

Ref

Expression

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 period_ 0_ 7_ 9_ 9_ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 period_ 4_ 1 4 ) /\ ( ( 0 period_ 0_ 0_ 0_ 4_ 2_ 2_ 4 8 ) x. ( n ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( (Λ oF x. h )vts n ) ` x ) x. ( ( ( (Λ oF x. k )vts n ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. pi ) ) x. ( -u n x. x ) ) ) ) _d x ) )

Distinct variable group:   h, k, m, n, x, z

Detailed syntax breakdown of Axiom ax-hgt749

Step	Hyp	Ref	Expression
1		c1 9937	. . . . . 6 class 1
2		cc0 9936	. . . . . 6 class 0
3	1, 2	cdc 11493	. . . . 5 class ; 1 0
4		c2 11070	. . . . . 6 class 2
5		c7 11075	. . . . . 6 class 7
6	4, 5	cdc 11493	. . . . 5 class ; 2 7
7		cexp 12860	. . . . 5 class ^
8	3, 6, 7	co 6650	. . . 4 class (; 1 0 ^; 2 7 )
9		vn	. . . . 5 setvar n
10	9	cv 1482	. . . 4 class n
11		cle 10075	. . . 4 class <_
12	8, 10, 11	wbr 4653	. . 3 wff (; 1 0 ^; 2 7 ) <_ n
13		vm	. . . . . . . . . 10 setvar m
14	13	cv 1482	. . . . . . . . 9 class m
15		vk	. . . . . . . . . 10 setvar k
16	15	cv 1482	. . . . . . . . 9 class k
17	14, 16	cfv 5888	. . . . . . . 8 class ( k ` m )
18		c9 11077	. . . . . . . . . . . 12 class 9
19		c5 11073	. . . . . . . . . . . . . 14 class 5
20	19, 19	cdp2 29577	. . . . . . . . . . . . 13 class _ 5 5
21	18, 20	cdp2 29577	. . . . . . . . . . . 12 class _ 9_ 5 5
22	18, 21	cdp2 29577	. . . . . . . . . . 11 class _ 9_ 9_ 5 5
23	5, 22	cdp2 29577	. . . . . . . . . 10 class _ 7_ 9_ 9_ 5 5
24	2, 23	cdp2 29577	. . . . . . . . 9 class _ 0_ 7_ 9_ 9_ 5 5
25		cdp 29595	. . . . . . . . 9 class period
26	1, 24, 25	co 6650	. . . . . . . 8 class ( 1 period_ 0_ 7_ 9_ 9_ 5 5 )
27	17, 26, 11	wbr 4653	. . . . . . 7 wff ( k ` m ) <_ ( 1 period_ 0_ 7_ 9_ 9_ 5 5 )
28		cn 11020	. . . . . . 7 class NN
29	27, 13, 28	wral 2912	. . . . . 6 wff A. m e. NN ( k ` m ) <_ ( 1 period_ 0_ 7_ 9_ 9_ 5 5 )
30		vh	. . . . . . . . . 10 setvar h
31	30	cv 1482	. . . . . . . . 9 class h
32	14, 31	cfv 5888	. . . . . . . 8 class ( h ` m )
33		c4 11072	. . . . . . . . . 10 class 4
34	1, 33	cdp2 29577	. . . . . . . . . 10 class _ 1 4
35	33, 34	cdp2 29577	. . . . . . . . 9 class _ 4_ 1 4
36	1, 35, 25	co 6650	. . . . . . . 8 class ( 1 period_ 4_ 1 4 )
37	32, 36, 11	wbr 4653	. . . . . . 7 wff ( h ` m ) <_ ( 1 period_ 4_ 1 4 )
38	37, 13, 28	wral 2912	. . . . . 6 wff A. m e. NN ( h ` m ) <_ ( 1 period_ 4_ 1 4 )
39		c8 11076	. . . . . . . . . . . . . . . 16 class 8
40	33, 39	cdp2 29577	. . . . . . . . . . . . . . 15 class _ 4 8
41	4, 40	cdp2 29577	. . . . . . . . . . . . . 14 class _ 2_ 4 8
42	4, 41	cdp2 29577	. . . . . . . . . . . . 13 class _ 2_ 2_ 4 8
43	33, 42	cdp2 29577	. . . . . . . . . . . 12 class _ 4_ 2_ 2_ 4 8
44	2, 43	cdp2 29577	. . . . . . . . . . 11 class _ 0_ 4_ 2_ 2_ 4 8
45	2, 44	cdp2 29577	. . . . . . . . . 10 class _ 0_ 0_ 4_ 2_ 2_ 4 8
46	2, 45	cdp2 29577	. . . . . . . . 9 class _ 0_ 0_ 0_ 4_ 2_ 2_ 4 8
47	2, 46, 25	co 6650	. . . . . . . 8 class ( 0 period_ 0_ 0_ 0_ 4_ 2_ 2_ 4 8 )
48	10, 4, 7	co 6650	. . . . . . . 8 class ( n ^ 2 )
49		cmul 9941	. . . . . . . 8 class x.
50	47, 48, 49	co 6650	. . . . . . 7 class ( ( 0 period_ 0_ 0_ 0_ 4_ 2_ 2_ 4 8 ) x. ( n ^ 2 ) )
51		vx	. . . . . . . 8 setvar x
52		cioo 12175	. . . . . . . . 9 class (,)
53	2, 1, 52	co 6650	. . . . . . . 8 class ( 0 (,) 1 )
54	51	cv 1482	. . . . . . . . . . 11 class x
55		cvma 24818	. . . . . . . . . . . . 13 class Λ
56	49	cof 6895	. . . . . . . . . . . . 13 class oF x.
57	55, 31, 56	co 6650	. . . . . . . . . . . 12 class (Λ oF x. h )
58		cvts 30713	. . . . . . . . . . . 12 class vts
59	57, 10, 58	co 6650	. . . . . . . . . . 11 class ( (Λ oF x. h )vts n )
60	54, 59	cfv 5888	. . . . . . . . . 10 class ( ( (Λ oF x. h )vts n ) ` x )
61	55, 16, 56	co 6650	. . . . . . . . . . . . 13 class (Λ oF x. k )
62	61, 10, 58	co 6650	. . . . . . . . . . . 12 class ( (Λ oF x. k )vts n )
63	54, 62	cfv 5888	. . . . . . . . . . 11 class ( ( (Λ oF x. k )vts n ) ` x )
64	63, 4, 7	co 6650	. . . . . . . . . 10 class ( ( ( (Λ oF x. k )vts n ) ` x ) ^ 2 )
65	60, 64, 49	co 6650	. . . . . . . . 9 class ( ( ( (Λ oF x. h )vts n ) ` x ) x. ( ( ( (Λ oF x. k )vts n ) ` x ) ^ 2 ) )
66		ci 9938	. . . . . . . . . . . 12 class _i
67		cpi 14797	. . . . . . . . . . . . 13 class pi
68	4, 67, 49	co 6650	. . . . . . . . . . . 12 class ( 2 x. pi )
69	66, 68, 49	co 6650	. . . . . . . . . . 11 class ( _i x. ( 2 x. pi ) )
70	10	cneg 10267	. . . . . . . . . . . 12 class -u n
71	70, 54, 49	co 6650	. . . . . . . . . . 11 class ( -u n x. x )
72	69, 71, 49	co 6650	. . . . . . . . . 10 class ( ( _i x. ( 2 x. pi ) ) x. ( -u n x. x ) )
73		ce 14792	. . . . . . . . . 10 class exp
74	72, 73	cfv 5888	. . . . . . . . 9 class ( exp ` ( ( _i x. ( 2 x. pi ) ) x. ( -u n x. x ) ) )
75	65, 74, 49	co 6650	. . . . . . . 8 class ( ( ( ( (Λ oF x. h )vts n ) ` x ) x. ( ( ( (Λ oF x. k )vts n ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. pi ) ) x. ( -u n x. x ) ) ) )
76	51, 53, 75	citg 23387	. . . . . . 7 class S. ( 0 (,) 1 ) ( ( ( ( (Λ oF x. h )vts n ) ` x ) x. ( ( ( (Λ oF x. k )vts n ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. pi ) ) x. ( -u n x. x ) ) ) ) _d x
77	50, 76, 11	wbr 4653	. . . . . 6 wff ( ( 0 period_ 0_ 0_ 0_ 4_ 2_ 2_ 4 8 ) x. ( n ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( (Λ oF x. h )vts n ) ` x ) x. ( ( ( (Λ oF x. k )vts n ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. pi ) ) x. ( -u n x. x ) ) ) ) _d x
78	29, 38, 77	w3a 1037	. . . . 5 wff ( A. m e. NN ( k ` m ) <_ ( 1 period_ 0_ 7_ 9_ 9_ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 period_ 4_ 1 4 ) /\ ( ( 0 period_ 0_ 0_ 0_ 4_ 2_ 2_ 4 8 ) x. ( n ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( (Λ oF x. h )vts n ) ` x ) x. ( ( ( (Λ oF x. k )vts n ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. pi ) ) x. ( -u n x. x ) ) ) ) _d x )
79		cpnf 10071	. . . . . . 7 class +oo
80		cico 12177	. . . . . . 7 class [,)
81	2, 79, 80	co 6650	. . . . . 6 class ( 0 [,) +oo )
82		cmap 7857	. . . . . 6 class ^m
83	81, 28, 82	co 6650	. . . . 5 class ( ( 0 [,) +oo ) ^m NN )
84	78, 15, 83	wrex 2913	. . . 4 wff E. k e. ( ( 0 [,) +oo ) ^m NN ) ( A. m e. NN ( k ` m ) <_ ( 1 period_ 0_ 7_ 9_ 9_ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 period_ 4_ 1 4 ) /\ ( ( 0 period_ 0_ 0_ 0_ 4_ 2_ 2_ 4 8 ) x. ( n ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( (Λ oF x. h )vts n ) ` x ) x. ( ( ( (Λ oF x. k )vts n ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. pi ) ) x. ( -u n x. x ) ) ) ) _d x )
85	84, 30, 83	wrex 2913	. . 3 wff E. h e. ( ( 0 [,) +oo ) ^m NN ) E. k e. ( ( 0 [,) +oo ) ^m NN ) ( A. m e. NN ( k ` m ) <_ ( 1 period_ 0_ 7_ 9_ 9_ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 period_ 4_ 1 4 ) /\ ( ( 0 period_ 0_ 0_ 0_ 4_ 2_ 2_ 4 8 ) x. ( n ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( (Λ oF x. h )vts n ) ` x ) x. ( ( ( (Λ oF x. k )vts n ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. pi ) ) x. ( -u n x. x ) ) ) ) _d x )
86	12, 85	wi 4	. 2 wff ( (; 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 period_ 0_ 7_ 9_ 9_ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 period_ 4_ 1 4 ) /\ ( ( 0 period_ 0_ 0_ 0_ 4_ 2_ 2_ 4 8 ) x. ( n ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( (Λ oF x. h )vts n ) ` x ) x. ( ( ( (Λ oF x. k )vts n ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. pi ) ) x. ( -u n x. x ) ) ) ) _d x ) )
87		vz	. . . . . 6 setvar z
88	87	cv 1482	. . . . 5 class z
89		cdvds 14983	. . . . 5 class ||
90	4, 88, 89	wbr 4653	. . . 4 wff 2 || z
91	90	wn 3	. . 3 wff -. 2 || z
92		cz 11377	. . 3 class ZZ
93	91, 87, 92	crab 2916	. 2 class { z e. ZZ | -. 2 || z }
94	86, 9, 93	wral 2912	1 wff 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 period_ 0_ 7_ 9_ 9_ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 period_ 4_ 1 4 ) /\ ( ( 0 period_ 0_ 0_ 0_ 4_ 2_ 2_ 4 8 ) x. ( n ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( (Λ oF x. h )vts n ) ` x ) x. ( ( ( (Λ oF x. k )vts n ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. pi ) ) x. ( -u n x. x ) ) ) ) _d x ) )

This axiom is referenced by:  hgt749d  30727