Metamath Proof Explorer


Theorem circlemethhgt

Description: The circle method, where the Vinogradov sums are weighted using the Von Mangoldt function and smoothed using functions H and K . Statement 7.49 of Helfgott p. 69. At this point there is no further constraint on the smoothing functions. (Contributed by Thierry Arnoux, 22-Dec-2021)

Ref Expression
Hypotheses circlemethhgt.h φ H :
circlemethhgt.k φ K :
circlemethhgt.n φ N 0
Assertion circlemethhgt φ n repr 3 N Λ n 0 H n 0 Λ n 1 K n 1 Λ n 2 K n 2 = 0 1 Λ × f H vts N x Λ × f K vts N x 2 e i 2 π -N x dx

Proof

Step Hyp Ref Expression
1 circlemethhgt.h φ H :
2 circlemethhgt.k φ K :
3 circlemethhgt.n φ N 0
4 3nn 3
5 4 a1i φ 3
6 s3len ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ = 3
7 6 eqcomi 3 = ⟨“ Λ × f HΛ × f KΛ × f K ”⟩
8 7 a1i φ 3 = ⟨“ Λ × f HΛ × f KΛ × f K ”⟩
9 simprl φ x y x
10 simprr φ x y y
11 9 10 remulcld φ x y x y
12 11 recnd φ x y x y
13 vmaf Λ :
14 13 a1i φ Λ :
15 nnex V
16 15 a1i φ V
17 inidm =
18 12 14 1 16 16 17 off φ Λ × f H :
19 cnex V
20 19 15 elmap Λ × f H Λ × f H :
21 18 20 sylibr φ Λ × f H
22 12 14 2 16 16 17 off φ Λ × f K :
23 19 15 elmap Λ × f K Λ × f K :
24 22 23 sylibr φ Λ × f K
25 21 24 24 s3cld φ ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ Word
26 8 25 wrdfd φ ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ : 0 ..^ 3
27 3 5 26 circlemeth φ n repr 3 N a 0 ..^ 3 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ a n a = 0 1 a 0 ..^ 3 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ a vts N x e i 2 π -N x dx
28 fveq2 a = 0 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ a = ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ 0
29 fveq2 a = 0 n a = n 0
30 28 29 fveq12d a = 0 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ a n a = ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ 0 n 0
31 fveq2 a = 1 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ a = ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ 1
32 fveq2 a = 1 n a = n 1
33 31 32 fveq12d a = 1 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ a n a = ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ 1 n 1
34 fveq2 a = 2 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ a = ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ 2
35 fveq2 a = 2 n a = n 2
36 34 35 fveq12d a = 2 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ a n a = ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ 2 n 2
37 26 adantr φ n repr 3 N ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ : 0 ..^ 3
38 37 ffvelrnda φ n repr 3 N a 0 ..^ 3 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ a
39 elmapi ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ a ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ a :
40 38 39 syl φ n repr 3 N a 0 ..^ 3 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ a :
41 ssidd φ n repr 3 N
42 3 nn0zd φ N
43 42 adantr φ n repr 3 N N
44 3nn0 3 0
45 44 a1i φ n repr 3 N 3 0
46 simpr φ n repr 3 N n repr 3 N
47 41 43 45 46 reprf φ n repr 3 N n : 0 ..^ 3
48 47 ffvelrnda φ n repr 3 N a 0 ..^ 3 n a
49 40 48 ffvelrnd φ n repr 3 N a 0 ..^ 3 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ a n a
50 30 33 36 49 prodfzo03 φ n repr 3 N a 0 ..^ 3 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ a n a = ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ 0 n 0 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ 1 n 1 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ 2 n 2
51 ovex Λ × f H V
52 s3fv0 Λ × f H V ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ 0 = Λ × f H
53 51 52 mp1i φ n repr 3 N ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ 0 = Λ × f H
54 53 fveq1d φ n repr 3 N ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ 0 n 0 = Λ × f H n 0
55 simpl φ n repr 3 N φ
56 c0ex 0 V
57 56 tpid1 0 0 1 2
58 fzo0to3tp 0 ..^ 3 = 0 1 2
59 57 58 eleqtrri 0 0 ..^ 3
60 59 a1i φ n repr 3 N 0 0 ..^ 3
61 47 60 ffvelrnd φ n repr 3 N n 0
62 ffn Λ : Λ Fn
63 13 62 ax-mp Λ Fn
64 63 a1i φ Λ Fn
65 1 ffnd φ H Fn
66 eqidd φ n 0 Λ n 0 = Λ n 0
67 eqidd φ n 0 H n 0 = H n 0
68 64 65 16 16 17 66 67 ofval φ n 0 Λ × f H n 0 = Λ n 0 H n 0
69 55 61 68 syl2anc φ n repr 3 N Λ × f H n 0 = Λ n 0 H n 0
70 54 69 eqtrd φ n repr 3 N ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ 0 n 0 = Λ n 0 H n 0
71 ovex Λ × f K V
72 s3fv1 Λ × f K V ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ 1 = Λ × f K
73 71 72 mp1i φ n repr 3 N ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ 1 = Λ × f K
74 73 fveq1d φ n repr 3 N ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ 1 n 1 = Λ × f K n 1
75 1ex 1 V
76 75 tpid2 1 0 1 2
77 76 58 eleqtrri 1 0 ..^ 3
78 77 a1i φ n repr 3 N 1 0 ..^ 3
79 47 78 ffvelrnd φ n repr 3 N n 1
80 2 ffnd φ K Fn
81 eqidd φ n 1 Λ n 1 = Λ n 1
82 eqidd φ n 1 K n 1 = K n 1
83 64 80 16 16 17 81 82 ofval φ n 1 Λ × f K n 1 = Λ n 1 K n 1
84 55 79 83 syl2anc φ n repr 3 N Λ × f K n 1 = Λ n 1 K n 1
85 74 84 eqtrd φ n repr 3 N ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ 1 n 1 = Λ n 1 K n 1
86 s3fv2 Λ × f K V ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ 2 = Λ × f K
87 71 86 mp1i φ n repr 3 N ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ 2 = Λ × f K
88 87 fveq1d φ n repr 3 N ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ 2 n 2 = Λ × f K n 2
89 2ex 2 V
90 89 tpid3 2 0 1 2
91 90 58 eleqtrri 2 0 ..^ 3
92 91 a1i φ n repr 3 N 2 0 ..^ 3
93 47 92 ffvelrnd φ n repr 3 N n 2
94 eqidd φ n 2 Λ n 2 = Λ n 2
95 eqidd φ n 2 K n 2 = K n 2
96 64 80 16 16 17 94 95 ofval φ n 2 Λ × f K n 2 = Λ n 2 K n 2
97 55 93 96 syl2anc φ n repr 3 N Λ × f K n 2 = Λ n 2 K n 2
98 88 97 eqtrd φ n repr 3 N ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ 2 n 2 = Λ n 2 K n 2
99 85 98 oveq12d φ n repr 3 N ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ 1 n 1 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ 2 n 2 = Λ n 1 K n 1 Λ n 2 K n 2
100 70 99 oveq12d φ n repr 3 N ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ 0 n 0 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ 1 n 1 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ 2 n 2 = Λ n 0 H n 0 Λ n 1 K n 1 Λ n 2 K n 2
101 50 100 eqtrd φ n repr 3 N a 0 ..^ 3 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ a n a = Λ n 0 H n 0 Λ n 1 K n 1 Λ n 2 K n 2
102 101 sumeq2dv φ n repr 3 N a 0 ..^ 3 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ a n a = n repr 3 N Λ n 0 H n 0 Λ n 1 K n 1 Λ n 2 K n 2
103 nfv a φ x 0 1
104 nfcv _ a Λ × f H vts N x
105 fzofi 1 ..^ 3 Fin
106 105 a1i φ x 0 1 1 ..^ 3 Fin
107 56 a1i φ x 0 1 0 V
108 eqid 0 = 0
109 108 orci 0 = 0 0 = 3
110 0elfz 3 0 0 0 3
111 elfznelfzob 0 0 3 ¬ 0 1 ..^ 3 0 = 0 0 = 3
112 44 110 111 mp2b ¬ 0 1 ..^ 3 0 = 0 0 = 3
113 109 112 mpbir ¬ 0 1 ..^ 3
114 113 a1i φ x 0 1 ¬ 0 1 ..^ 3
115 3 ad2antrr φ x 0 1 a 1 ..^ 3 N 0
116 ioossre 0 1
117 ax-resscn
118 116 117 sstri 0 1
119 118 a1i φ 0 1
120 119 sselda φ x 0 1 x
121 120 adantr φ x 0 1 a 1 ..^ 3 x
122 26 ad2antrr φ x 0 1 a 1 ..^ 3 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ : 0 ..^ 3
123 fzo0ss1 1 ..^ 3 0 ..^ 3
124 123 a1i φ x 0 1 1 ..^ 3 0 ..^ 3
125 124 sselda φ x 0 1 a 1 ..^ 3 a 0 ..^ 3
126 122 125 ffvelrnd φ x 0 1 a 1 ..^ 3 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ a
127 126 39 syl φ x 0 1 a 1 ..^ 3 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ a :
128 115 121 127 vtscl φ x 0 1 a 1 ..^ 3 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ a vts N x
129 51 52 ax-mp ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ 0 = Λ × f H
130 28 129 eqtrdi a = 0 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ a = Λ × f H
131 130 oveq1d a = 0 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ a vts N = Λ × f H vts N
132 131 fveq1d a = 0 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ a vts N x = Λ × f H vts N x
133 3 adantr φ x 0 1 N 0
134 18 adantr φ x 0 1 Λ × f H :
135 133 120 134 vtscl φ x 0 1 Λ × f H vts N x
136 103 104 106 107 114 128 132 135 fprodsplitsn φ x 0 1 a 1 ..^ 3 0 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ a vts N x = a 1 ..^ 3 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ a vts N x Λ × f H vts N x
137 uncom 1 ..^ 3 0 = 0 1 ..^ 3
138 fzo0sn0fzo1 3 0 ..^ 3 = 0 1 ..^ 3
139 4 138 ax-mp 0 ..^ 3 = 0 1 ..^ 3
140 137 139 eqtr4i 1 ..^ 3 0 = 0 ..^ 3
141 140 a1i φ x 0 1 1 ..^ 3 0 = 0 ..^ 3
142 141 prodeq1d φ x 0 1 a 1 ..^ 3 0 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ a vts N x = a 0 ..^ 3 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ a vts N x
143 fzo13pr 1 ..^ 3 = 1 2
144 143 eleq2i a 1 ..^ 3 a 1 2
145 vex a V
146 145 elpr a 1 2 a = 1 a = 2
147 144 146 bitri a 1 ..^ 3 a = 1 a = 2
148 31 adantl φ a = 1 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ a = ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ 1
149 71 72 mp1i φ a = 1 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ 1 = Λ × f K
150 148 149 eqtrd φ a = 1 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ a = Λ × f K
151 34 adantl φ a = 2 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ a = ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ 2
152 71 86 mp1i φ a = 2 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ 2 = Λ × f K
153 151 152 eqtrd φ a = 2 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ a = Λ × f K
154 150 153 jaodan φ a = 1 a = 2 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ a = Λ × f K
155 147 154 sylan2b φ a 1 ..^ 3 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ a = Λ × f K
156 155 adantlr φ x 0 1 a 1 ..^ 3 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ a = Λ × f K
157 156 oveq1d φ x 0 1 a 1 ..^ 3 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ a vts N = Λ × f K vts N
158 157 fveq1d φ x 0 1 a 1 ..^ 3 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ a vts N x = Λ × f K vts N x
159 158 prodeq2dv φ x 0 1 a 1 ..^ 3 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ a vts N x = a 1 ..^ 3 Λ × f K vts N x
160 22 adantr φ x 0 1 Λ × f K :
161 133 120 160 vtscl φ x 0 1 Λ × f K vts N x
162 fprodconst 1 ..^ 3 Fin Λ × f K vts N x a 1 ..^ 3 Λ × f K vts N x = Λ × f K vts N x 1 ..^ 3
163 106 161 162 syl2anc φ x 0 1 a 1 ..^ 3 Λ × f K vts N x = Λ × f K vts N x 1 ..^ 3
164 nnuz = 1
165 4 164 eleqtri 3 1
166 hashfzo 3 1 1 ..^ 3 = 3 1
167 165 166 ax-mp 1 ..^ 3 = 3 1
168 3m1e2 3 1 = 2
169 167 168 eqtri 1 ..^ 3 = 2
170 169 a1i φ x 0 1 1 ..^ 3 = 2
171 170 oveq2d φ x 0 1 Λ × f K vts N x 1 ..^ 3 = Λ × f K vts N x 2
172 159 163 171 3eqtrd φ x 0 1 a 1 ..^ 3 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ a vts N x = Λ × f K vts N x 2
173 172 oveq1d φ x 0 1 a 1 ..^ 3 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ a vts N x Λ × f H vts N x = Λ × f K vts N x 2 Λ × f H vts N x
174 161 sqcld φ x 0 1 Λ × f K vts N x 2
175 135 174 mulcomd φ x 0 1 Λ × f H vts N x Λ × f K vts N x 2 = Λ × f K vts N x 2 Λ × f H vts N x
176 173 175 eqtr4d φ x 0 1 a 1 ..^ 3 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ a vts N x Λ × f H vts N x = Λ × f H vts N x Λ × f K vts N x 2
177 136 142 176 3eqtr3d φ x 0 1 a 0 ..^ 3 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ a vts N x = Λ × f H vts N x Λ × f K vts N x 2
178 177 oveq1d φ x 0 1 a 0 ..^ 3 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ a vts N x e i 2 π -N x = Λ × f H vts N x Λ × f K vts N x 2 e i 2 π -N x
179 178 itgeq2dv φ 0 1 a 0 ..^ 3 ⟨“ Λ × f HΛ × f KΛ × f K ”⟩ a vts N x e i 2 π -N x dx = 0 1 Λ × f H vts N x Λ × f K vts N x 2 e i 2 π -N x dx
180 27 102 179 3eqtr3d φ n repr 3 N Λ n 0 H n 0 Λ n 1 K n 1 Λ n 2 K n 2 = 0 1 Λ × f H vts N x Λ × f K vts N x 2 e i 2 π -N x dx