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