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 ⊢ ∀ n ∈ z ∈ ℤ | ¬ 2 ∥ z 10 27 ≤ n → ∃ h ∈ 0 +∞ ℕ ∃ k ∈ 0 +∞ ℕ ∀ m ∈ ℕ k ⁡ m ≤ 1.079955 ∧ ∀ m ∈ ℕ h ⁡ m ≤ 1.414 ∧ 0.00042248 ⁢ n 2 ≤ ∫ 0 1 Λ × f h vts n ⁡ x ⁢ Λ × f k vts n ⁡ x 2 ⁢ e i ⁢ 2 ⁢ π ⁢ − n ⁢ x dx

Detailed syntax breakdown

Step Hyp Ref Expression
0 vn setvar n
1 vz setvar z
2 cz class ℤ
3 c2 class 2
4 cdvds class ∥
5 1 cv setvar z
6 3 5 4 wbr wff 2 ∥ z
7 6 wn wff ¬ 2 ∥ z
8 7 1 2 crab class z ∈ ℤ | ¬ 2 ∥ z
9 c1 class 1
10 cc0 class 0
11 9 10 cdc class 10
12 cexp class ^
13 c7 class 7
14 3 13 cdc class 27
15 11 14 12 co class 10 27
16 cle class ≤
17 0 cv setvar n
18 15 17 16 wbr wff 10 27 ≤ n
19 vh setvar h
20 cico class .
21 cpnf class +∞
22 10 21 20 co class 0 +∞
23 cmap class ↑ 𝑚
24 cn class ℕ
25 22 24 23 co class 0 +∞ ℕ
26 vk setvar k
27 vm setvar m
28 26 cv setvar k
29 27 cv setvar m
30 29 28 cfv class k ⁡ m
31 cdp class .
32 c9 class 9
33 c5 class 5
34 33 33 cdp2 class 55
35 32 34 cdp2 class 955
36 32 35 cdp2 class 9955
37 13 36 cdp2 class 79955
38 10 37 cdp2 class 079955
39 9 38 31 co class 1.079955
40 30 39 16 wbr wff k ⁡ m ≤ 1.079955
41 40 27 24 wral wff ∀ m ∈ ℕ k ⁡ m ≤ 1.079955
42 19 cv setvar h
43 29 42 cfv class h ⁡ m
44 c4 class 4
45 9 44 cdp2 class 14
46 44 45 cdp2 class 414
47 9 46 31 co class 1.414
48 43 47 16 wbr wff h ⁡ m ≤ 1.414
49 48 27 24 wral wff ∀ m ∈ ℕ h ⁡ m ≤ 1.414
50 c8 class 8
51 44 50 cdp2 class 48
52 3 51 cdp2 class 248
53 3 52 cdp2 class 2248
54 44 53 cdp2 class 42248
55 10 54 cdp2 class 042248
56 10 55 cdp2 class 0042248
57 10 56 cdp2 class 00042248
58 10 57 31 co class 0.00042248
59 cmul class ×
60 17 3 12 co class n 2
61 58 60 59 co class 0.00042248 ⁢ n 2
62 cioo class .
63 10 9 62 co class 0 1
64 cvma class Λ
65 59 cof class ∘ f ⁡ ×
66 64 42 65 co class Λ × f h
67 cvts class vts
68 66 17 67 co class Λ × f h vts n
69 vx setvar x
70 69 cv setvar x
71 70 68 cfv class Λ × f h vts n ⁡ x
72 64 28 65 co class Λ × f k
73 72 17 67 co class Λ × f k vts n
74 70 73 cfv class Λ × f k vts n ⁡ x
75 74 3 12 co class Λ × f k vts n ⁡ x 2
76 71 75 59 co class Λ × f h vts n ⁡ x ⁢ Λ × f k vts n ⁡ x 2
77 ce class exp
78 ci class i
79 cpi class π
80 3 79 59 co class 2 ⁢ π
81 78 80 59 co class i ⁢ 2 ⁢ π
82 17 cneg class − n
83 82 70 59 co class − n ⁢ x
84 81 83 59 co class i ⁢ 2 ⁢ π ⁢ − n ⁢ x
85 84 77 cfv class e i ⁢ 2 ⁢ π ⁢ − n ⁢ x
86 76 85 59 co class Λ × f h vts n ⁡ x ⁢ Λ × f k vts n ⁡ x 2 ⁢ e i ⁢ 2 ⁢ π ⁢ − n ⁢ x
87 69 63 86 citg class ∫ 0 1 Λ × f h vts n ⁡ x ⁢ Λ × f k vts n ⁡ x 2 ⁢ e i ⁢ 2 ⁢ π ⁢ − n ⁢ x dx
88 61 87 16 wbr wff 0.00042248 ⁢ n 2 ≤ ∫ 0 1 Λ × f h vts n ⁡ x ⁢ Λ × f k vts n ⁡ x 2 ⁢ e i ⁢ 2 ⁢ π ⁢ − n ⁢ x dx
89 41 49 88 w3a wff ∀ m ∈ ℕ k ⁡ m ≤ 1.079955 ∧ ∀ m ∈ ℕ h ⁡ m ≤ 1.414 ∧ 0.00042248 ⁢ n 2 ≤ ∫ 0 1 Λ × f h vts n ⁡ x ⁢ Λ × f k vts n ⁡ x 2 ⁢ e i ⁢ 2 ⁢ π ⁢ − n ⁢ x dx
90 89 26 25 wrex wff ∃ k ∈ 0 +∞ ℕ ∀ m ∈ ℕ k ⁡ m ≤ 1.079955 ∧ ∀ m ∈ ℕ h ⁡ m ≤ 1.414 ∧ 0.00042248 ⁢ n 2 ≤ ∫ 0 1 Λ × f h vts n ⁡ x ⁢ Λ × f k vts n ⁡ x 2 ⁢ e i ⁢ 2 ⁢ π ⁢ − n ⁢ x dx
91 90 19 25 wrex wff ∃ h ∈ 0 +∞ ℕ ∃ k ∈ 0 +∞ ℕ ∀ m ∈ ℕ k ⁡ m ≤ 1.079955 ∧ ∀ m ∈ ℕ h ⁡ m ≤ 1.414 ∧ 0.00042248 ⁢ n 2 ≤ ∫ 0 1 Λ × f h vts n ⁡ x ⁢ Λ × f k vts n ⁡ x 2 ⁢ e i ⁢ 2 ⁢ π ⁢ − n ⁢ x dx
92 18 91 wi wff 10 27 ≤ n → ∃ h ∈ 0 +∞ ℕ ∃ k ∈ 0 +∞ ℕ ∀ m ∈ ℕ k ⁡ m ≤ 1.079955 ∧ ∀ m ∈ ℕ h ⁡ m ≤ 1.414 ∧ 0.00042248 ⁢ n 2 ≤ ∫ 0 1 Λ × f h vts n ⁡ x ⁢ Λ × f k vts n ⁡ x 2 ⁢ e i ⁢ 2 ⁢ π ⁢ − n ⁢ x dx
93 92 0 8 wral wff ∀ n ∈ z ∈ ℤ | ¬ 2 ∥ z 10 27 ≤ n → ∃ h ∈ 0 +∞ ℕ ∃ k ∈ 0 +∞ ℕ ∀ m ∈ ℕ k ⁡ m ≤ 1.079955 ∧ ∀ m ∈ ℕ h ⁡ m ≤ 1.414 ∧ 0.00042248 ⁢ n 2 ≤ ∫ 0 1 Λ × f h vts n ⁡ x ⁢ Λ × f k vts n ⁡ x 2 ⁢ e i ⁢ 2 ⁢ π ⁢ − n ⁢ x dx