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	⊢ ∀ 𝑛 ∈ { 𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧 } ( ( ; 1 0 ↑ ; 2 7 ) ≤ 𝑛 → ∃ ℎ ∈ ( ( 0 [,) +∞ ) ↑m ℕ ) ∃ 𝑘 ∈ ( ( 0 [,) +∞ ) ↑m ℕ ) ( ∀ 𝑚 ∈ ℕ ( 𝑘 ‘ 𝑚 ) ≤ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ∧ ∀ 𝑚 ∈ ℕ ( ℎ ‘ 𝑚 ) ≤ ( 1 . _ 4 _ 1 4 ) ∧ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) · ( 𝑛 ↑ 2 ) ) ≤ ∫ ( 0 (,) 1 ) ( ( ( ( ( Λ ∘f · ℎ ) vts 𝑛 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑛 ) ‘ 𝑥 ) ↑ 2 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑛 · 𝑥 ) ) ) ) d 𝑥 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vn	⊢ 𝑛
1		vz	⊢ 𝑧
2		cz	⊢ ℤ
3		c2	⊢ 2
4		cdvds	⊢ ∥
5	1	cv	⊢ 𝑧
6	3 5 4	wbr	⊢ 2 ∥ 𝑧
7	6	wn	⊢ ¬ 2 ∥ 𝑧
8	7 1 2	crab	⊢ { 𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧 }
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	⊢ 𝑛
18	15 17 16	wbr	⊢ ( ; 1 0 ↑ ; 2 7 ) ≤ 𝑛
19		vh	⊢ ℎ
20		cico	⊢ [,)
21		cpnf	⊢ +∞
22	10 21 20	co	⊢ ( 0 [,) +∞ )
23		cmap	⊢ ↑m
24		cn	⊢ ℕ
25	22 24 23	co	⊢ ( ( 0 [,) +∞ ) ↑m ℕ )
26		vk	⊢ 𝑘
27		vm	⊢ 𝑚
28	26	cv	⊢ 𝑘
29	27	cv	⊢ 𝑚
30	29 28	cfv	⊢ ( 𝑘 ‘ 𝑚 )
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	⊢ ( 𝑘 ‘ 𝑚 ) ≤ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 )
41	40 27 24	wral	⊢ ∀ 𝑚 ∈ ℕ ( 𝑘 ‘ 𝑚 ) ≤ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 )
42	19	cv	⊢ ℎ
43	29 42	cfv	⊢ ( ℎ ‘ 𝑚 )
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	⊢ ( ℎ ‘ 𝑚 ) ≤ ( 1 . _ 4 _ 1 4 )
49	48 27 24	wral	⊢ ∀ 𝑚 ∈ ℕ ( ℎ ‘ 𝑚 ) ≤ ( 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	⊢ ·
60	17 3 12	co	⊢ ( 𝑛 ↑ 2 )
61	58 60 59	co	⊢ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) · ( 𝑛 ↑ 2 ) )
62		cioo	⊢ (,)
63	10 9 62	co	⊢ ( 0 (,) 1 )
64		cvma	⊢ Λ
65	59	cof	⊢ ∘f ·
66	64 42 65	co	⊢ ( Λ ∘f · ℎ )
67		cvts	⊢ vts
68	66 17 67	co	⊢ ( ( Λ ∘f · ℎ ) vts 𝑛 )
69		vx	⊢ 𝑥
70	69	cv	⊢ 𝑥
71	70 68	cfv	⊢ ( ( ( Λ ∘f · ℎ ) vts 𝑛 ) ‘ 𝑥 )
72	64 28 65	co	⊢ ( Λ ∘f · 𝑘 )
73	72 17 67	co	⊢ ( ( Λ ∘f · 𝑘 ) vts 𝑛 )
74	70 73	cfv	⊢ ( ( ( Λ ∘f · 𝑘 ) vts 𝑛 ) ‘ 𝑥 )
75	74 3 12	co	⊢ ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑛 ) ‘ 𝑥 ) ↑ 2 )
76	71 75 59	co	⊢ ( ( ( ( Λ ∘f · ℎ ) vts 𝑛 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑛 ) ‘ 𝑥 ) ↑ 2 ) )
77		ce	⊢ exp
78		ci	⊢ i
79		cpi	⊢ π
80	3 79 59	co	⊢ ( 2 · π )
81	78 80 59	co	⊢ ( i · ( 2 · π ) )
82	17	cneg	⊢ - 𝑛
83	82 70 59	co	⊢ ( - 𝑛 · 𝑥 )
84	81 83 59	co	⊢ ( ( i · ( 2 · π ) ) · ( - 𝑛 · 𝑥 ) )
85	84 77	cfv	⊢ ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑛 · 𝑥 ) ) )
86	76 85 59	co	⊢ ( ( ( ( ( Λ ∘f · ℎ ) vts 𝑛 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑛 ) ‘ 𝑥 ) ↑ 2 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑛 · 𝑥 ) ) ) )
87	69 63 86	citg	⊢ ∫ ( 0 (,) 1 ) ( ( ( ( ( Λ ∘f · ℎ ) vts 𝑛 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑛 ) ‘ 𝑥 ) ↑ 2 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑛 · 𝑥 ) ) ) ) d 𝑥
88	61 87 16	wbr	⊢ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) · ( 𝑛 ↑ 2 ) ) ≤ ∫ ( 0 (,) 1 ) ( ( ( ( ( Λ ∘f · ℎ ) vts 𝑛 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑛 ) ‘ 𝑥 ) ↑ 2 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑛 · 𝑥 ) ) ) ) d 𝑥
89	41 49 88	w3a	⊢ ( ∀ 𝑚 ∈ ℕ ( 𝑘 ‘ 𝑚 ) ≤ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ∧ ∀ 𝑚 ∈ ℕ ( ℎ ‘ 𝑚 ) ≤ ( 1 . _ 4 _ 1 4 ) ∧ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) · ( 𝑛 ↑ 2 ) ) ≤ ∫ ( 0 (,) 1 ) ( ( ( ( ( Λ ∘f · ℎ ) vts 𝑛 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑛 ) ‘ 𝑥 ) ↑ 2 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑛 · 𝑥 ) ) ) ) d 𝑥 )
90	89 26 25	wrex	⊢ ∃ 𝑘 ∈ ( ( 0 [,) +∞ ) ↑m ℕ ) ( ∀ 𝑚 ∈ ℕ ( 𝑘 ‘ 𝑚 ) ≤ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ∧ ∀ 𝑚 ∈ ℕ ( ℎ ‘ 𝑚 ) ≤ ( 1 . _ 4 _ 1 4 ) ∧ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) · ( 𝑛 ↑ 2 ) ) ≤ ∫ ( 0 (,) 1 ) ( ( ( ( ( Λ ∘f · ℎ ) vts 𝑛 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑛 ) ‘ 𝑥 ) ↑ 2 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑛 · 𝑥 ) ) ) ) d 𝑥 )
91	90 19 25	wrex	⊢ ∃ ℎ ∈ ( ( 0 [,) +∞ ) ↑m ℕ ) ∃ 𝑘 ∈ ( ( 0 [,) +∞ ) ↑m ℕ ) ( ∀ 𝑚 ∈ ℕ ( 𝑘 ‘ 𝑚 ) ≤ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ∧ ∀ 𝑚 ∈ ℕ ( ℎ ‘ 𝑚 ) ≤ ( 1 . _ 4 _ 1 4 ) ∧ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) · ( 𝑛 ↑ 2 ) ) ≤ ∫ ( 0 (,) 1 ) ( ( ( ( ( Λ ∘f · ℎ ) vts 𝑛 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑛 ) ‘ 𝑥 ) ↑ 2 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑛 · 𝑥 ) ) ) ) d 𝑥 )
92	18 91	wi	⊢ ( ( ; 1 0 ↑ ; 2 7 ) ≤ 𝑛 → ∃ ℎ ∈ ( ( 0 [,) +∞ ) ↑m ℕ ) ∃ 𝑘 ∈ ( ( 0 [,) +∞ ) ↑m ℕ ) ( ∀ 𝑚 ∈ ℕ ( 𝑘 ‘ 𝑚 ) ≤ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ∧ ∀ 𝑚 ∈ ℕ ( ℎ ‘ 𝑚 ) ≤ ( 1 . _ 4 _ 1 4 ) ∧ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) · ( 𝑛 ↑ 2 ) ) ≤ ∫ ( 0 (,) 1 ) ( ( ( ( ( Λ ∘f · ℎ ) vts 𝑛 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑛 ) ‘ 𝑥 ) ↑ 2 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑛 · 𝑥 ) ) ) ) d 𝑥 ) )
93	92 0 8	wral	⊢ ∀ 𝑛 ∈ { 𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧 } ( ( ; 1 0 ↑ ; 2 7 ) ≤ 𝑛 → ∃ ℎ ∈ ( ( 0 [,) +∞ ) ↑m ℕ ) ∃ 𝑘 ∈ ( ( 0 [,) +∞ ) ↑m ℕ ) ( ∀ 𝑚 ∈ ℕ ( 𝑘 ‘ 𝑚 ) ≤ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ∧ ∀ 𝑚 ∈ ℕ ( ℎ ‘ 𝑚 ) ≤ ( 1 . _ 4 _ 1 4 ) ∧ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) · ( 𝑛 ↑ 2 ) ) ≤ ∫ ( 0 (,) 1 ) ( ( ( ( ( Λ ∘f · ℎ ) vts 𝑛 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑛 ) ‘ 𝑥 ) ↑ 2 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑛 · 𝑥 ) ) ) ) d 𝑥 ) )