Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ax-hgt749 Structured version   Visualization version   GIF version

Axiom ax-hgt749 31989
 Description: Statement 7.49 of [Helfgott] p. 70. For a sufficiently big odd 𝑁, this postulates the existence of smoothing functions ℎ (eta star) and 𝑘 (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 𝑛 ∈ {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧} ((10↑27) ≤ 𝑛 → ∃ ∈ ((0[,)+∞) ↑m ℕ)∃𝑘 ∈ ((0[,)+∞) ↑m ℕ)(∀𝑚 ∈ ℕ (𝑘𝑚) ≤ (1.079955) ∧ ∀𝑚 ∈ ℕ (𝑚) ≤ (1.414) ∧ ((0.00042248) · (𝑛↑2)) ≤ ∫(0(,)1)(((((Λ ∘f · )vts𝑛)‘𝑥) · ((((Λ ∘f · 𝑘)vts𝑛)‘𝑥)↑2)) · (exp‘((i · (2 · π)) · (-𝑛 · 𝑥)))) d𝑥))
Distinct variable group:   ,𝑘,𝑚,𝑛,𝑥,𝑧

Detailed syntax breakdown of Axiom ax-hgt749
StepHypRef Expression
1 c1 10527 . . . . . 6 class 1
2 cc0 10526 . . . . . 6 class 0
31, 2cdc 12086 . . . . 5 class 10
4 c2 11680 . . . . . 6 class 2
5 c7 11685 . . . . . 6 class 7
64, 5cdc 12086 . . . . 5 class 27
7 cexp 13425 . . . . 5 class
83, 6, 7co 7140 . . . 4 class (10↑27)
9 vn . . . . 5 setvar 𝑛
109cv 1537 . . . 4 class 𝑛
11 cle 10665 . . . 4 class
128, 10, 11wbr 5042 . . 3 wff (10↑27) ≤ 𝑛
13 vm . . . . . . . . . 10 setvar 𝑚
1413cv 1537 . . . . . . . . 9 class 𝑚
15 vk . . . . . . . . . 10 setvar 𝑘
1615cv 1537 . . . . . . . . 9 class 𝑘
1714, 16cfv 6334 . . . . . . . 8 class (𝑘𝑚)
18 c9 11687 . . . . . . . . . . . 12 class 9
19 c5 11683 . . . . . . . . . . . . . 14 class 5
2019, 19cdp2 30557 . . . . . . . . . . . . 13 class 55
2118, 20cdp2 30557 . . . . . . . . . . . 12 class 955
2218, 21cdp2 30557 . . . . . . . . . . 11 class 9955
235, 22cdp2 30557 . . . . . . . . . 10 class 79955
242, 23cdp2 30557 . . . . . . . . 9 class 079955
25 cdp 30574 . . . . . . . . 9 class .
261, 24, 25co 7140 . . . . . . . 8 class (1.079955)
2717, 26, 11wbr 5042 . . . . . . 7 wff (𝑘𝑚) ≤ (1.079955)
28 cn 11625 . . . . . . 7 class
2927, 13, 28wral 3130 . . . . . 6 wff 𝑚 ∈ ℕ (𝑘𝑚) ≤ (1.079955)
30 vh . . . . . . . . . 10 setvar
3130cv 1537 . . . . . . . . 9 class
3214, 31cfv 6334 . . . . . . . 8 class (𝑚)
33 c4 11682 . . . . . . . . . 10 class 4
341, 33cdp2 30557 . . . . . . . . . 10 class 14
3533, 34cdp2 30557 . . . . . . . . 9 class 414
361, 35, 25co 7140 . . . . . . . 8 class (1.414)
3732, 36, 11wbr 5042 . . . . . . 7 wff (𝑚) ≤ (1.414)
3837, 13, 28wral 3130 . . . . . 6 wff 𝑚 ∈ ℕ (𝑚) ≤ (1.414)
39 c8 11686 . . . . . . . . . . . . . . . 16 class 8
4033, 39cdp2 30557 . . . . . . . . . . . . . . 15 class 48
414, 40cdp2 30557 . . . . . . . . . . . . . 14 class 248
424, 41cdp2 30557 . . . . . . . . . . . . 13 class 2248
4333, 42cdp2 30557 . . . . . . . . . . . 12 class 42248
442, 43cdp2 30557 . . . . . . . . . . 11 class 042248
452, 44cdp2 30557 . . . . . . . . . 10 class 0042248
462, 45cdp2 30557 . . . . . . . . 9 class 00042248
472, 46, 25co 7140 . . . . . . . 8 class (0.00042248)
4810, 4, 7co 7140 . . . . . . . 8 class (𝑛↑2)
49 cmul 10531 . . . . . . . 8 class ·
5047, 48, 49co 7140 . . . . . . 7 class ((0.00042248) · (𝑛↑2))
51 vx . . . . . . . 8 setvar 𝑥
52 cioo 12726 . . . . . . . . 9 class (,)
532, 1, 52co 7140 . . . . . . . 8 class (0(,)1)
5451cv 1537 . . . . . . . . . . 11 class 𝑥
55 cvma 25675 . . . . . . . . . . . . 13 class Λ
5649cof 7392 . . . . . . . . . . . . 13 class f ·
5755, 31, 56co 7140 . . . . . . . . . . . 12 class (Λ ∘f · )
58 cvts 31980 . . . . . . . . . . . 12 class vts
5957, 10, 58co 7140 . . . . . . . . . . 11 class ((Λ ∘f · )vts𝑛)
6054, 59cfv 6334 . . . . . . . . . 10 class (((Λ ∘f · )vts𝑛)‘𝑥)
6155, 16, 56co 7140 . . . . . . . . . . . . 13 class (Λ ∘f · 𝑘)
6261, 10, 58co 7140 . . . . . . . . . . . 12 class ((Λ ∘f · 𝑘)vts𝑛)
6354, 62cfv 6334 . . . . . . . . . . 11 class (((Λ ∘f · 𝑘)vts𝑛)‘𝑥)
6463, 4, 7co 7140 . . . . . . . . . 10 class ((((Λ ∘f · 𝑘)vts𝑛)‘𝑥)↑2)
6560, 64, 49co 7140 . . . . . . . . 9 class ((((Λ ∘f · )vts𝑛)‘𝑥) · ((((Λ ∘f · 𝑘)vts𝑛)‘𝑥)↑2))
66 ci 10528 . . . . . . . . . . . 12 class i
67 cpi 15411 . . . . . . . . . . . . 13 class π
684, 67, 49co 7140 . . . . . . . . . . . 12 class (2 · π)
6966, 68, 49co 7140 . . . . . . . . . . 11 class (i · (2 · π))
7010cneg 10860 . . . . . . . . . . . 12 class -𝑛
7170, 54, 49co 7140 . . . . . . . . . . 11 class (-𝑛 · 𝑥)
7269, 71, 49co 7140 . . . . . . . . . 10 class ((i · (2 · π)) · (-𝑛 · 𝑥))
73 ce 15406 . . . . . . . . . 10 class exp
7472, 73cfv 6334 . . . . . . . . 9 class (exp‘((i · (2 · π)) · (-𝑛 · 𝑥)))
7565, 74, 49co 7140 . . . . . . . 8 class (((((Λ ∘f · )vts𝑛)‘𝑥) · ((((Λ ∘f · 𝑘)vts𝑛)‘𝑥)↑2)) · (exp‘((i · (2 · π)) · (-𝑛 · 𝑥))))
7651, 53, 75citg 24220 . . . . . . 7 class ∫(0(,)1)(((((Λ ∘f · )vts𝑛)‘𝑥) · ((((Λ ∘f · 𝑘)vts𝑛)‘𝑥)↑2)) · (exp‘((i · (2 · π)) · (-𝑛 · 𝑥)))) d𝑥
7750, 76, 11wbr 5042 . . . . . 6 wff ((0.00042248) · (𝑛↑2)) ≤ ∫(0(,)1)(((((Λ ∘f · )vts𝑛)‘𝑥) · ((((Λ ∘f · 𝑘)vts𝑛)‘𝑥)↑2)) · (exp‘((i · (2 · π)) · (-𝑛 · 𝑥)))) d𝑥
7829, 38, 77w3a 1084 . . . . 5 wff (∀𝑚 ∈ ℕ (𝑘𝑚) ≤ (1.079955) ∧ ∀𝑚 ∈ ℕ (𝑚) ≤ (1.414) ∧ ((0.00042248) · (𝑛↑2)) ≤ ∫(0(,)1)(((((Λ ∘f · )vts𝑛)‘𝑥) · ((((Λ ∘f · 𝑘)vts𝑛)‘𝑥)↑2)) · (exp‘((i · (2 · π)) · (-𝑛 · 𝑥)))) d𝑥)
79 cpnf 10661 . . . . . . 7 class +∞
80 cico 12728 . . . . . . 7 class [,)
812, 79, 80co 7140 . . . . . 6 class (0[,)+∞)
82 cmap 8393 . . . . . 6 class m
8381, 28, 82co 7140 . . . . 5 class ((0[,)+∞) ↑m ℕ)
8478, 15, 83wrex 3131 . . . 4 wff 𝑘 ∈ ((0[,)+∞) ↑m ℕ)(∀𝑚 ∈ ℕ (𝑘𝑚) ≤ (1.079955) ∧ ∀𝑚 ∈ ℕ (𝑚) ≤ (1.414) ∧ ((0.00042248) · (𝑛↑2)) ≤ ∫(0(,)1)(((((Λ ∘f · )vts𝑛)‘𝑥) · ((((Λ ∘f · 𝑘)vts𝑛)‘𝑥)↑2)) · (exp‘((i · (2 · π)) · (-𝑛 · 𝑥)))) d𝑥)
8584, 30, 83wrex 3131 . . 3 wff ∈ ((0[,)+∞) ↑m ℕ)∃𝑘 ∈ ((0[,)+∞) ↑m ℕ)(∀𝑚 ∈ ℕ (𝑘𝑚) ≤ (1.079955) ∧ ∀𝑚 ∈ ℕ (𝑚) ≤ (1.414) ∧ ((0.00042248) · (𝑛↑2)) ≤ ∫(0(,)1)(((((Λ ∘f · )vts𝑛)‘𝑥) · ((((Λ ∘f · 𝑘)vts𝑛)‘𝑥)↑2)) · (exp‘((i · (2 · π)) · (-𝑛 · 𝑥)))) d𝑥)
8612, 85wi 4 . 2 wff ((10↑27) ≤ 𝑛 → ∃ ∈ ((0[,)+∞) ↑m ℕ)∃𝑘 ∈ ((0[,)+∞) ↑m ℕ)(∀𝑚 ∈ ℕ (𝑘𝑚) ≤ (1.079955) ∧ ∀𝑚 ∈ ℕ (𝑚) ≤ (1.414) ∧ ((0.00042248) · (𝑛↑2)) ≤ ∫(0(,)1)(((((Λ ∘f · )vts𝑛)‘𝑥) · ((((Λ ∘f · 𝑘)vts𝑛)‘𝑥)↑2)) · (exp‘((i · (2 · π)) · (-𝑛 · 𝑥)))) d𝑥))
87 vz . . . . . 6 setvar 𝑧
8887cv 1537 . . . . 5 class 𝑧
89 cdvds 15598 . . . . 5 class
904, 88, 89wbr 5042 . . . 4 wff 2 ∥ 𝑧
9190wn 3 . . 3 wff ¬ 2 ∥ 𝑧
92 cz 11969 . . 3 class
9391, 87, 92crab 3134 . 2 class {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧}
9486, 9, 93wral 3130 1 wff 𝑛 ∈ {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧} ((10↑27) ≤ 𝑛 → ∃ ∈ ((0[,)+∞) ↑m ℕ)∃𝑘 ∈ ((0[,)+∞) ↑m ℕ)(∀𝑚 ∈ ℕ (𝑘𝑚) ≤ (1.079955) ∧ ∀𝑚 ∈ ℕ (𝑚) ≤ (1.414) ∧ ((0.00042248) · (𝑛↑2)) ≤ ∫(0(,)1)(((((Λ ∘f · )vts𝑛)‘𝑥) · ((((Λ ∘f · 𝑘)vts𝑛)‘𝑥)↑2)) · (exp‘((i · (2 · π)) · (-𝑛 · 𝑥)))) d𝑥))
 Colors of variables: wff setvar class This axiom is referenced by:  hgt749d  31994
 Copyright terms: Public domain W3C validator