Metamath Proof Explorer

Theorem circlevma

Description: The Circle Method, where the Vinogradov sums are weighted using the von Mangoldt function, as it appears as proposition 1.1 of Helfgott p. 5. (Contributed by Thierry Arnoux, 13-Dec-2021)

Ref Expression
Hypothesis circlevma.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion circlevma ( 𝜑 → Σ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) = ∫ ( 0 (,) 1 ) ( ( ( ( Λ vts 𝑁 ) ‘ 𝑥 ) ↑ 3 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) d 𝑥 )

Proof

Step Hyp Ref Expression
1 circlevma.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
2 3nn ⊢ 3 ∈ ℕ
3 2 a1i ⊢ ( 𝜑 → 3 ∈ ℕ )
4 vmaf ⊢ Λ : ℕ ⟶ ℝ
5 ax-resscn ⊢ ℝ ⊆ ℂ
6 fss ⊢ ( ( Λ : ℕ ⟶ ℝ ∧ ℝ ⊆ ℂ ) → Λ : ℕ ⟶ ℂ )
7 4 5 6 mp2an ⊢ Λ : ℕ ⟶ ℂ
8 cnex ⊢ ℂ ∈ V
9 nnex ⊢ ℕ ∈ V
10 elmapg ⊢ ( ( ℂ ∈ V ∧ ℕ ∈ V ) → ( Λ ∈ ( ℂ ↑m ℕ ) ↔ Λ : ℕ ⟶ ℂ ) )
11 8 9 10 mp2an ⊢ ( Λ ∈ ( ℂ ↑m ℕ ) ↔ Λ : ℕ ⟶ ℂ )
12 7 11 mpbir ⊢ Λ ∈ ( ℂ ↑m ℕ )
13 12 fconst6 ⊢ ( ( 0 ..^ 3 ) × { Λ } ) : ( 0 ..^ 3 ) ⟶ ( ℂ ↑m ℕ )
14 13 a1i ⊢ ( 𝜑 → ( ( 0 ..^ 3 ) × { Λ } ) : ( 0 ..^ 3 ) ⟶ ( ℂ ↑m ℕ ) )
15 1 3 14 circlemeth ⊢ ( 𝜑 → Σ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∏ 𝑎 ∈ ( 0 ..^ 3 ) ( ( ( ( 0 ..^ 3 ) × { Λ } ) ‘ 𝑎 ) ‘ ( 𝑛 ‘ 𝑎 ) ) = ∫ ( 0 (,) 1 ) ( ∏ 𝑎 ∈ ( 0 ..^ 3 ) ( ( ( ( ( 0 ..^ 3 ) × { Λ } ) ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑥 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) d 𝑥 )
16 c0ex ⊢ 0 ∈ V
17 16 tpid1 ⊢ 0 ∈ { 0 , 1 , 2 }
18 fzo0to3tp ⊢ ( 0 ..^ 3 ) = { 0 , 1 , 2 }
19 17 18 eleqtrri ⊢ 0 ∈ ( 0 ..^ 3 )
20 eleq1 ⊢ ( 𝑎 = 0 → ( 𝑎 ∈ ( 0 ..^ 3 ) ↔ 0 ∈ ( 0 ..^ 3 ) ) )
21 19 20 mpbiri ⊢ ( 𝑎 = 0 → 𝑎 ∈ ( 0 ..^ 3 ) )
22 12 elexi ⊢ Λ ∈ V
23 22 fvconst2 ⊢ ( 𝑎 ∈ ( 0 ..^ 3 ) → ( ( ( 0 ..^ 3 ) × { Λ } ) ‘ 𝑎 ) = Λ )
24 21 23 syl ⊢ ( 𝑎 = 0 → ( ( ( 0 ..^ 3 ) × { Λ } ) ‘ 𝑎 ) = Λ )
25 fveq2 ⊢ ( 𝑎 = 0 → ( 𝑛 ‘ 𝑎 ) = ( 𝑛 ‘ 0 ) )
26 24 25 fveq12d ⊢ ( 𝑎 = 0 → ( ( ( ( 0 ..^ 3 ) × { Λ } ) ‘ 𝑎 ) ‘ ( 𝑛 ‘ 𝑎 ) ) = ( Λ ‘ ( 𝑛 ‘ 0 ) ) )
27 1eltp012 ⊢ 1 ∈ { 0 , 1 , 2 }
28 27 18 eleqtrri ⊢ 1 ∈ ( 0 ..^ 3 )
29 eleq1 ⊢ ( 𝑎 = 1 → ( 𝑎 ∈ ( 0 ..^ 3 ) ↔ 1 ∈ ( 0 ..^ 3 ) ) )
30 28 29 mpbiri ⊢ ( 𝑎 = 1 → 𝑎 ∈ ( 0 ..^ 3 ) )
31 30 23 syl ⊢ ( 𝑎 = 1 → ( ( ( 0 ..^ 3 ) × { Λ } ) ‘ 𝑎 ) = Λ )
32 fveq2 ⊢ ( 𝑎 = 1 → ( 𝑛 ‘ 𝑎 ) = ( 𝑛 ‘ 1 ) )
33 31 32 fveq12d ⊢ ( 𝑎 = 1 → ( ( ( ( 0 ..^ 3 ) × { Λ } ) ‘ 𝑎 ) ‘ ( 𝑛 ‘ 𝑎 ) ) = ( Λ ‘ ( 𝑛 ‘ 1 ) ) )
34 2ex ⊢ 2 ∈ V
35 34 tpid3 ⊢ 2 ∈ { 0 , 1 , 2 }
36 35 18 eleqtrri ⊢ 2 ∈ ( 0 ..^ 3 )
37 eleq1 ⊢ ( 𝑎 = 2 → ( 𝑎 ∈ ( 0 ..^ 3 ) ↔ 2 ∈ ( 0 ..^ 3 ) ) )
38 36 37 mpbiri ⊢ ( 𝑎 = 2 → 𝑎 ∈ ( 0 ..^ 3 ) )
39 38 23 syl ⊢ ( 𝑎 = 2 → ( ( ( 0 ..^ 3 ) × { Λ } ) ‘ 𝑎 ) = Λ )
40 fveq2 ⊢ ( 𝑎 = 2 → ( 𝑛 ‘ 𝑎 ) = ( 𝑛 ‘ 2 ) )
41 39 40 fveq12d ⊢ ( 𝑎 = 2 → ( ( ( ( 0 ..^ 3 ) × { Λ } ) ‘ 𝑎 ) ‘ ( 𝑛 ‘ 𝑎 ) ) = ( Λ ‘ ( 𝑛 ‘ 2 ) ) )
42 23 fveq1d ⊢ ( 𝑎 ∈ ( 0 ..^ 3 ) → ( ( ( ( 0 ..^ 3 ) × { Λ } ) ‘ 𝑎 ) ‘ ( 𝑛 ‘ 𝑎 ) ) = ( Λ ‘ ( 𝑛 ‘ 𝑎 ) ) )
43 42 adantl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) → ( ( ( ( 0 ..^ 3 ) × { Λ } ) ‘ 𝑎 ) ‘ ( 𝑛 ‘ 𝑎 ) ) = ( Λ ‘ ( 𝑛 ‘ 𝑎 ) ) )
44 7 a1i ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) → Λ : ℕ ⟶ ℂ )
45 ssidd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → ℕ ⊆ ℕ )
46 1 nn0zd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
47 46 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → 𝑁 ∈ ℤ )
48 2 nnnn0i ⊢ 3 ∈ ℕ0
49 48 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → 3 ∈ ℕ0 )
50 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) )
51 45 47 49 50 reprf ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → 𝑛 : ( 0 ..^ 3 ) ⟶ ℕ )
52 51 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) → ( 𝑛 ‘ 𝑎 ) ∈ ℕ )
53 44 52 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) → ( Λ ‘ ( 𝑛 ‘ 𝑎 ) ) ∈ ℂ )
54 43 53 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) → ( ( ( ( 0 ..^ 3 ) × { Λ } ) ‘ 𝑎 ) ‘ ( 𝑛 ‘ 𝑎 ) ) ∈ ℂ )
55 26 33 41 54 prodfzo03 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → ∏ 𝑎 ∈ ( 0 ..^ 3 ) ( ( ( ( 0 ..^ 3 ) × { Λ } ) ‘ 𝑎 ) ‘ ( 𝑛 ‘ 𝑎 ) ) = ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) )
56 55 sumeq2dv ⊢ ( 𝜑 → Σ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∏ 𝑎 ∈ ( 0 ..^ 3 ) ( ( ( ( 0 ..^ 3 ) × { Λ } ) ‘ 𝑎 ) ‘ ( 𝑛 ‘ 𝑎 ) ) = Σ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) )
57 23 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) → ( ( ( 0 ..^ 3 ) × { Λ } ) ‘ 𝑎 ) = Λ )
58 57 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) → ( ( ( ( 0 ..^ 3 ) × { Λ } ) ‘ 𝑎 ) vts 𝑁 ) = ( Λ vts 𝑁 ) )
59 58 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) → ( ( ( ( ( 0 ..^ 3 ) × { Λ } ) ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑥 ) = ( ( Λ vts 𝑁 ) ‘ 𝑥 ) )
60 59 prodeq2dv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ∏ 𝑎 ∈ ( 0 ..^ 3 ) ( ( ( ( ( 0 ..^ 3 ) × { Λ } ) ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑥 ) = ∏ 𝑎 ∈ ( 0 ..^ 3 ) ( ( Λ vts 𝑁 ) ‘ 𝑥 ) )
61 fzofi ⊢ ( 0 ..^ 3 ) ∈ Fin
62 61 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( 0 ..^ 3 ) ∈ Fin )
63 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → 𝑁 ∈ ℕ0 )
64 ioossre ⊢ ( 0 (,) 1 ) ⊆ ℝ
65 64 5 sstri ⊢ ( 0 (,) 1 ) ⊆ ℂ
66 65 a1i ⊢ ( 𝜑 → ( 0 (,) 1 ) ⊆ ℂ )
67 66 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → 𝑥 ∈ ℂ )
68 7 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → Λ : ℕ ⟶ ℂ )
69 63 67 68 vtscl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( ( Λ vts 𝑁 ) ‘ 𝑥 ) ∈ ℂ )
70 fprodconst ⊢ ( ( ( 0 ..^ 3 ) ∈ Fin ∧ ( ( Λ vts 𝑁 ) ‘ 𝑥 ) ∈ ℂ ) → ∏ 𝑎 ∈ ( 0 ..^ 3 ) ( ( Λ vts 𝑁 ) ‘ 𝑥 ) = ( ( ( Λ vts 𝑁 ) ‘ 𝑥 ) ↑ ( ♯ ‘ ( 0 ..^ 3 ) ) ) )
71 62 69 70 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ∏ 𝑎 ∈ ( 0 ..^ 3 ) ( ( Λ vts 𝑁 ) ‘ 𝑥 ) = ( ( ( Λ vts 𝑁 ) ‘ 𝑥 ) ↑ ( ♯ ‘ ( 0 ..^ 3 ) ) ) )
72 hashfzo0 ⊢ ( 3 ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ 3 ) ) = 3 )
73 48 72 ax-mp ⊢ ( ♯ ‘ ( 0 ..^ 3 ) ) = 3
74 73 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( ♯ ‘ ( 0 ..^ 3 ) ) = 3 )
75 74 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( ( ( Λ vts 𝑁 ) ‘ 𝑥 ) ↑ ( ♯ ‘ ( 0 ..^ 3 ) ) ) = ( ( ( Λ vts 𝑁 ) ‘ 𝑥 ) ↑ 3 ) )
76 60 71 75 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ∏ 𝑎 ∈ ( 0 ..^ 3 ) ( ( ( ( ( 0 ..^ 3 ) × { Λ } ) ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑥 ) = ( ( ( Λ vts 𝑁 ) ‘ 𝑥 ) ↑ 3 ) )
77 76 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( ∏ 𝑎 ∈ ( 0 ..^ 3 ) ( ( ( ( ( 0 ..^ 3 ) × { Λ } ) ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑥 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) = ( ( ( ( Λ vts 𝑁 ) ‘ 𝑥 ) ↑ 3 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) )
78 77 itgeq2dv ⊢ ( 𝜑 → ∫ ( 0 (,) 1 ) ( ∏ 𝑎 ∈ ( 0 ..^ 3 ) ( ( ( ( ( 0 ..^ 3 ) × { Λ } ) ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑥 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) d 𝑥 = ∫ ( 0 (,) 1 ) ( ( ( ( Λ vts 𝑁 ) ‘ 𝑥 ) ↑ 3 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) d 𝑥 )
79 15 56 78 3eqtr3d ⊢ ( 𝜑 → Σ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) = ∫ ( 0 (,) 1 ) ( ( ( ( Λ vts 𝑁 ) ‘ 𝑥 ) ↑ 3 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) d 𝑥 )