Axiom ax-hgt749 33725

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._0_7_9_9_55) ∧ ∀𝑚 ∈ ℕ (ℎ‘𝑚) ≤ (1._4_14) ∧ ((0._0_0_0_4_2_2_48) · (𝑛↑2)) ≤ ∫(0(,)1)(((((Λ ∘f · ℎ)vts𝑛)‘𝑥) · ((((Λ ∘f · 𝑘)vts𝑛)‘𝑥)↑2)) · (exp‘((i · (2 · π)) · (-𝑛 · 𝑥)))) d𝑥))

Distinct variable group:   ℎ,𝑘,𝑚,𝑛,𝑥,𝑧

Detailed syntax breakdown of Axiom ax-hgt749

Step	Hyp	Ref	Expression
1		c1 11113	. . . . . 6 class 1
2		cc0 11112	. . . . . 6 class 0
3	1, 2	cdc 12679	. . . . 5 class ;10
4		c2 12269	. . . . . 6 class 2
5		c7 12274	. . . . . 6 class 7
6	4, 5	cdc 12679	. . . . 5 class ;27
7		cexp 14029	. . . . 5 class ↑
8	3, 6, 7	co 7411	. . . 4 class (;10↑;27)
9		vn	. . . . 5 setvar 𝑛
10	9	cv 1540	. . . 4 class 𝑛
11		cle 11251	. . . 4 class ≤
12	8, 10, 11	wbr 5148	. . 3 wff (;10↑;27) ≤ 𝑛
13		vm	. . . . . . . . . 10 setvar 𝑚
14	13	cv 1540	. . . . . . . . 9 class 𝑚
15		vk	. . . . . . . . . 10 setvar 𝑘
16	15	cv 1540	. . . . . . . . 9 class 𝑘
17	14, 16	cfv 6543	. . . . . . . 8 class (𝑘‘𝑚)
18		c9 12276	. . . . . . . . . . . 12 class 9
19		c5 12272	. . . . . . . . . . . . . 14 class 5
20	19, 19	cdp2 32075	. . . . . . . . . . . . 13 class _55
21	18, 20	cdp2 32075	. . . . . . . . . . . 12 class _9_55
22	18, 21	cdp2 32075	. . . . . . . . . . 11 class _9_9_55
23	5, 22	cdp2 32075	. . . . . . . . . 10 class _7_9_9_55
24	2, 23	cdp2 32075	. . . . . . . . 9 class _0_7_9_9_55
25		cdp 32092	. . . . . . . . 9 class .
26	1, 24, 25	co 7411	. . . . . . . 8 class (1._0_7_9_9_55)
27	17, 26, 11	wbr 5148	. . . . . . 7 wff (𝑘‘𝑚) ≤ (1._0_7_9_9_55)
28		cn 12214	. . . . . . 7 class ℕ
29	27, 13, 28	wral 3061	. . . . . 6 wff ∀𝑚 ∈ ℕ (𝑘‘𝑚) ≤ (1._0_7_9_9_55)
30		vh	. . . . . . . . . 10 setvar ℎ
31	30	cv 1540	. . . . . . . . 9 class ℎ
32	14, 31	cfv 6543	. . . . . . . 8 class (ℎ‘𝑚)
33		c4 12271	. . . . . . . . . 10 class 4
34	1, 33	cdp2 32075	. . . . . . . . . 10 class _14
35	33, 34	cdp2 32075	. . . . . . . . 9 class _4_14
36	1, 35, 25	co 7411	. . . . . . . 8 class (1._4_14)
37	32, 36, 11	wbr 5148	. . . . . . 7 wff (ℎ‘𝑚) ≤ (1._4_14)
38	37, 13, 28	wral 3061	. . . . . 6 wff ∀𝑚 ∈ ℕ (ℎ‘𝑚) ≤ (1._4_14)
39		c8 12275	. . . . . . . . . . . . . . . 16 class 8
40	33, 39	cdp2 32075	. . . . . . . . . . . . . . 15 class _48
41	4, 40	cdp2 32075	. . . . . . . . . . . . . 14 class _2_48
42	4, 41	cdp2 32075	. . . . . . . . . . . . 13 class _2_2_48
43	33, 42	cdp2 32075	. . . . . . . . . . . 12 class _4_2_2_48
44	2, 43	cdp2 32075	. . . . . . . . . . 11 class _0_4_2_2_48
45	2, 44	cdp2 32075	. . . . . . . . . 10 class _0_0_4_2_2_48
46	2, 45	cdp2 32075	. . . . . . . . 9 class _0_0_0_4_2_2_48
47	2, 46, 25	co 7411	. . . . . . . 8 class (0._0_0_0_4_2_2_48)
48	10, 4, 7	co 7411	. . . . . . . 8 class (𝑛↑2)
49		cmul 11117	. . . . . . . 8 class ·
50	47, 48, 49	co 7411	. . . . . . 7 class ((0._0_0_0_4_2_2_48) · (𝑛↑2))
51		vx	. . . . . . . 8 setvar 𝑥
52		cioo 13326	. . . . . . . . 9 class (,)
53	2, 1, 52	co 7411	. . . . . . . 8 class (0(,)1)
54	51	cv 1540	. . . . . . . . . . 11 class 𝑥
55		cvma 26603	. . . . . . . . . . . . 13 class Λ
56	49	cof 7670	. . . . . . . . . . . . 13 class ∘f ·
57	55, 31, 56	co 7411	. . . . . . . . . . . 12 class (Λ ∘f · ℎ)
58		cvts 33716	. . . . . . . . . . . 12 class vts
59	57, 10, 58	co 7411	. . . . . . . . . . 11 class ((Λ ∘f · ℎ)vts𝑛)
60	54, 59	cfv 6543	. . . . . . . . . 10 class (((Λ ∘f · ℎ)vts𝑛)‘𝑥)
61	55, 16, 56	co 7411	. . . . . . . . . . . . 13 class (Λ ∘f · 𝑘)
62	61, 10, 58	co 7411	. . . . . . . . . . . 12 class ((Λ ∘f · 𝑘)vts𝑛)
63	54, 62	cfv 6543	. . . . . . . . . . 11 class (((Λ ∘f · 𝑘)vts𝑛)‘𝑥)
64	63, 4, 7	co 7411	. . . . . . . . . 10 class ((((Λ ∘f · 𝑘)vts𝑛)‘𝑥)↑2)
65	60, 64, 49	co 7411	. . . . . . . . 9 class ((((Λ ∘f · ℎ)vts𝑛)‘𝑥) · ((((Λ ∘f · 𝑘)vts𝑛)‘𝑥)↑2))
66		ci 11114	. . . . . . . . . . . 12 class i
67		cpi 16012	. . . . . . . . . . . . 13 class π
68	4, 67, 49	co 7411	. . . . . . . . . . . 12 class (2 · π)
69	66, 68, 49	co 7411	. . . . . . . . . . 11 class (i · (2 · π))
70	10	cneg 11447	. . . . . . . . . . . 12 class -𝑛
71	70, 54, 49	co 7411	. . . . . . . . . . 11 class (-𝑛 · 𝑥)
72	69, 71, 49	co 7411	. . . . . . . . . 10 class ((i · (2 · π)) · (-𝑛 · 𝑥))
73		ce 16007	. . . . . . . . . 10 class exp
74	72, 73	cfv 6543	. . . . . . . . 9 class (exp‘((i · (2 · π)) · (-𝑛 · 𝑥)))
75	65, 74, 49	co 7411	. . . . . . . 8 class (((((Λ ∘f · ℎ)vts𝑛)‘𝑥) · ((((Λ ∘f · 𝑘)vts𝑛)‘𝑥)↑2)) · (exp‘((i · (2 · π)) · (-𝑛 · 𝑥))))
76	51, 53, 75	citg 25142	. . . . . . 7 class ∫(0(,)1)(((((Λ ∘f · ℎ)vts𝑛)‘𝑥) · ((((Λ ∘f · 𝑘)vts𝑛)‘𝑥)↑2)) · (exp‘((i · (2 · π)) · (-𝑛 · 𝑥)))) d𝑥
77	50, 76, 11	wbr 5148	. . . . . 6 wff ((0._0_0_0_4_2_2_48) · (𝑛↑2)) ≤ ∫(0(,)1)(((((Λ ∘f · ℎ)vts𝑛)‘𝑥) · ((((Λ ∘f · 𝑘)vts𝑛)‘𝑥)↑2)) · (exp‘((i · (2 · π)) · (-𝑛 · 𝑥)))) d𝑥
78	29, 38, 77	w3a 1087	. . . . 5 wff (∀𝑚 ∈ ℕ (𝑘‘𝑚) ≤ (1._0_7_9_9_55) ∧ ∀𝑚 ∈ ℕ (ℎ‘𝑚) ≤ (1._4_14) ∧ ((0._0_0_0_4_2_2_48) · (𝑛↑2)) ≤ ∫(0(,)1)(((((Λ ∘f · ℎ)vts𝑛)‘𝑥) · ((((Λ ∘f · 𝑘)vts𝑛)‘𝑥)↑2)) · (exp‘((i · (2 · π)) · (-𝑛 · 𝑥)))) d𝑥)
79		cpnf 11247	. . . . . . 7 class +∞
80		cico 13328	. . . . . . 7 class [,)
81	2, 79, 80	co 7411	. . . . . 6 class (0[,)+∞)
82		cmap 8822	. . . . . 6 class ↑m
83	81, 28, 82	co 7411	. . . . 5 class ((0[,)+∞) ↑m ℕ)
84	78, 15, 83	wrex 3070	. . . 4 wff ∃𝑘 ∈ ((0[,)+∞) ↑m ℕ)(∀𝑚 ∈ ℕ (𝑘‘𝑚) ≤ (1._0_7_9_9_55) ∧ ∀𝑚 ∈ ℕ (ℎ‘𝑚) ≤ (1._4_14) ∧ ((0._0_0_0_4_2_2_48) · (𝑛↑2)) ≤ ∫(0(,)1)(((((Λ ∘f · ℎ)vts𝑛)‘𝑥) · ((((Λ ∘f · 𝑘)vts𝑛)‘𝑥)↑2)) · (exp‘((i · (2 · π)) · (-𝑛 · 𝑥)))) d𝑥)
85	84, 30, 83	wrex 3070	. . 3 wff ∃ℎ ∈ ((0[,)+∞) ↑m ℕ)∃𝑘 ∈ ((0[,)+∞) ↑m ℕ)(∀𝑚 ∈ ℕ (𝑘‘𝑚) ≤ (1._0_7_9_9_55) ∧ ∀𝑚 ∈ ℕ (ℎ‘𝑚) ≤ (1._4_14) ∧ ((0._0_0_0_4_2_2_48) · (𝑛↑2)) ≤ ∫(0(,)1)(((((Λ ∘f · ℎ)vts𝑛)‘𝑥) · ((((Λ ∘f · 𝑘)vts𝑛)‘𝑥)↑2)) · (exp‘((i · (2 · π)) · (-𝑛 · 𝑥)))) d𝑥)
86	12, 85	wi 4	. 2 wff ((;10↑;27) ≤ 𝑛 → ∃ℎ ∈ ((0[,)+∞) ↑m ℕ)∃𝑘 ∈ ((0[,)+∞) ↑m ℕ)(∀𝑚 ∈ ℕ (𝑘‘𝑚) ≤ (1._0_7_9_9_55) ∧ ∀𝑚 ∈ ℕ (ℎ‘𝑚) ≤ (1._4_14) ∧ ((0._0_0_0_4_2_2_48) · (𝑛↑2)) ≤ ∫(0(,)1)(((((Λ ∘f · ℎ)vts𝑛)‘𝑥) · ((((Λ ∘f · 𝑘)vts𝑛)‘𝑥)↑2)) · (exp‘((i · (2 · π)) · (-𝑛 · 𝑥)))) d𝑥))
87		vz	. . . . . 6 setvar 𝑧
88	87	cv 1540	. . . . 5 class 𝑧
89		cdvds 16199	. . . . 5 class ∥
90	4, 88, 89	wbr 5148	. . . 4 wff 2 ∥ 𝑧
91	90	wn 3	. . 3 wff ¬ 2 ∥ 𝑧
92		cz 12560	. . 3 class ℤ
93	91, 87, 92	crab 3432	. 2 class {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧}
94	86, 9, 93	wral 3061	1 wff ∀𝑛 ∈ {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧} ((;10↑;27) ≤ 𝑛 → ∃ℎ ∈ ((0[,)+∞) ↑m ℕ)∃𝑘 ∈ ((0[,)+∞) ↑m ℕ)(∀𝑚 ∈ ℕ (𝑘‘𝑚) ≤ (1._0_7_9_9_55) ∧ ∀𝑚 ∈ ℕ (ℎ‘𝑚) ≤ (1._4_14) ∧ ((0._0_0_0_4_2_2_48) · (𝑛↑2)) ≤ ∫(0(,)1)(((((Λ ∘f · ℎ)vts𝑛)‘𝑥) · ((((Λ ∘f · 𝑘)vts𝑛)‘𝑥)↑2)) · (exp‘((i · (2 · π)) · (-𝑛 · 𝑥)))) d𝑥))

This axiom is referenced by:  hgt749d  33730