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 ∀ 𝑛 ∈ { 𝑧 ∈ ℤ ∣ ¬ 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 𝑥 ) )