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 1ex ⊢ 1 ∈ V
28 27 tpid2 ⊢ 1 ∈ { 0 , 1 , 2 }
29 28 18 eleqtrri ⊢ 1 ∈ ( 0 ..^ 3 )
30 eleq1 ⊢ ( 𝑎 = 1 → ( 𝑎 ∈ ( 0 ..^ 3 ) ↔ 1 ∈ ( 0 ..^ 3 ) ) )
31 29 30 mpbiri ⊢ ( 𝑎 = 1 → 𝑎 ∈ ( 0 ..^ 3 ) )
32 31 23 syl ⊢ ( 𝑎 = 1 → ( ( ( 0 ..^ 3 ) × { Λ } ) ‘ 𝑎 ) = Λ )
33 fveq2 ⊢ ( 𝑎 = 1 → ( 𝑛 ‘ 𝑎 ) = ( 𝑛 ‘ 1 ) )
34 32 33 fveq12d ⊢ ( 𝑎 = 1 → ( ( ( ( 0 ..^ 3 ) × { Λ } ) ‘ 𝑎 ) ‘ ( 𝑛 ‘ 𝑎 ) ) = ( Λ ‘ ( 𝑛 ‘ 1 ) ) )
35 2ex ⊢ 2 ∈ V
36 35 tpid3 ⊢ 2 ∈ { 0 , 1 , 2 }
37 36 18 eleqtrri ⊢ 2 ∈ ( 0 ..^ 3 )
38 eleq1 ⊢ ( 𝑎 = 2 → ( 𝑎 ∈ ( 0 ..^ 3 ) ↔ 2 ∈ ( 0 ..^ 3 ) ) )
39 37 38 mpbiri ⊢ ( 𝑎 = 2 → 𝑎 ∈ ( 0 ..^ 3 ) )
40 39 23 syl ⊢ ( 𝑎 = 2 → ( ( ( 0 ..^ 3 ) × { Λ } ) ‘ 𝑎 ) = Λ )
41 fveq2 ⊢ ( 𝑎 = 2 → ( 𝑛 ‘ 𝑎 ) = ( 𝑛 ‘ 2 ) )
42 40 41 fveq12d ⊢ ( 𝑎 = 2 → ( ( ( ( 0 ..^ 3 ) × { Λ } ) ‘ 𝑎 ) ‘ ( 𝑛 ‘ 𝑎 ) ) = ( Λ ‘ ( 𝑛 ‘ 2 ) ) )
43 23 fveq1d ⊢ ( 𝑎 ∈ ( 0 ..^ 3 ) → ( ( ( ( 0 ..^ 3 ) × { Λ } ) ‘ 𝑎 ) ‘ ( 𝑛 ‘ 𝑎 ) ) = ( Λ ‘ ( 𝑛 ‘ 𝑎 ) ) )
44 43 adantl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) → ( ( ( ( 0 ..^ 3 ) × { Λ } ) ‘ 𝑎 ) ‘ ( 𝑛 ‘ 𝑎 ) ) = ( Λ ‘ ( 𝑛 ‘ 𝑎 ) ) )
45 7 a1i ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) → Λ : ℕ ⟶ ℂ )
46 ssidd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → ℕ ⊆ ℕ )
47 1 nn0zd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
48 47 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → 𝑁 ∈ ℤ )
49 2 nnnn0i ⊢ 3 ∈ ℕ0
50 49 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → 3 ∈ ℕ0 )
51 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) )
52 46 48 50 51 reprf ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → 𝑛 : ( 0 ..^ 3 ) ⟶ ℕ )
53 52 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) → ( 𝑛 ‘ 𝑎 ) ∈ ℕ )
54 45 53 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) → ( Λ ‘ ( 𝑛 ‘ 𝑎 ) ) ∈ ℂ )
55 44 54 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) → ( ( ( ( 0 ..^ 3 ) × { Λ } ) ‘ 𝑎 ) ‘ ( 𝑛 ‘ 𝑎 ) ) ∈ ℂ )
56 26 34 42 55 prodfzo03 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → ∏ 𝑎 ∈ ( 0 ..^ 3 ) ( ( ( ( 0 ..^ 3 ) × { Λ } ) ‘ 𝑎 ) ‘ ( 𝑛 ‘ 𝑎 ) ) = ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) )
57 56 sumeq2dv ⊢ ( 𝜑 → Σ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∏ 𝑎 ∈ ( 0 ..^ 3 ) ( ( ( ( 0 ..^ 3 ) × { Λ } ) ‘ 𝑎 ) ‘ ( 𝑛 ‘ 𝑎 ) ) = Σ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) )
58 23 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) → ( ( ( 0 ..^ 3 ) × { Λ } ) ‘ 𝑎 ) = Λ )
59 58 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) → ( ( ( ( 0 ..^ 3 ) × { Λ } ) ‘ 𝑎 ) vts 𝑁 ) = ( Λ vts 𝑁 ) )
60 59 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) → ( ( ( ( ( 0 ..^ 3 ) × { Λ } ) ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑥 ) = ( ( Λ vts 𝑁 ) ‘ 𝑥 ) )
61 60 prodeq2dv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ∏ 𝑎 ∈ ( 0 ..^ 3 ) ( ( ( ( ( 0 ..^ 3 ) × { Λ } ) ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑥 ) = ∏ 𝑎 ∈ ( 0 ..^ 3 ) ( ( Λ vts 𝑁 ) ‘ 𝑥 ) )
62 fzofi ⊢ ( 0 ..^ 3 ) ∈ Fin
63 62 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( 0 ..^ 3 ) ∈ Fin )
64 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → 𝑁 ∈ ℕ0 )
65 ioossre ⊢ ( 0 (,) 1 ) ⊆ ℝ
66 65 5 sstri ⊢ ( 0 (,) 1 ) ⊆ ℂ
67 66 a1i ⊢ ( 𝜑 → ( 0 (,) 1 ) ⊆ ℂ )
68 67 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → 𝑥 ∈ ℂ )
69 7 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → Λ : ℕ ⟶ ℂ )
70 64 68 69 vtscl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( ( Λ vts 𝑁 ) ‘ 𝑥 ) ∈ ℂ )
71 fprodconst ⊢ ( ( ( 0 ..^ 3 ) ∈ Fin ∧ ( ( Λ vts 𝑁 ) ‘ 𝑥 ) ∈ ℂ ) → ∏ 𝑎 ∈ ( 0 ..^ 3 ) ( ( Λ vts 𝑁 ) ‘ 𝑥 ) = ( ( ( Λ vts 𝑁 ) ‘ 𝑥 ) ↑ ( ♯ ‘ ( 0 ..^ 3 ) ) ) )
72 63 70 71 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ∏ 𝑎 ∈ ( 0 ..^ 3 ) ( ( Λ vts 𝑁 ) ‘ 𝑥 ) = ( ( ( Λ vts 𝑁 ) ‘ 𝑥 ) ↑ ( ♯ ‘ ( 0 ..^ 3 ) ) ) )
73 hashfzo0 ⊢ ( 3 ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ 3 ) ) = 3 )
74 49 73 ax-mp ⊢ ( ♯ ‘ ( 0 ..^ 3 ) ) = 3
75 74 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( ♯ ‘ ( 0 ..^ 3 ) ) = 3 )
76 75 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( ( ( Λ vts 𝑁 ) ‘ 𝑥 ) ↑ ( ♯ ‘ ( 0 ..^ 3 ) ) ) = ( ( ( Λ vts 𝑁 ) ‘ 𝑥 ) ↑ 3 ) )
77 61 72 76 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ∏ 𝑎 ∈ ( 0 ..^ 3 ) ( ( ( ( ( 0 ..^ 3 ) × { Λ } ) ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑥 ) = ( ( ( Λ vts 𝑁 ) ‘ 𝑥 ) ↑ 3 ) )
78 77 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( ∏ 𝑎 ∈ ( 0 ..^ 3 ) ( ( ( ( ( 0 ..^ 3 ) × { Λ } ) ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑥 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) = ( ( ( ( Λ vts 𝑁 ) ‘ 𝑥 ) ↑ 3 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) )
79 78 itgeq2dv ⊢ ( 𝜑 → ∫ ( 0 (,) 1 ) ( ∏ 𝑎 ∈ ( 0 ..^ 3 ) ( ( ( ( ( 0 ..^ 3 ) × { Λ } ) ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑥 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) d 𝑥 = ∫ ( 0 (,) 1 ) ( ( ( ( Λ vts 𝑁 ) ‘ 𝑥 ) ↑ 3 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) d 𝑥 )
80 15 57 79 3eqtr3d ⊢ ( 𝜑 → Σ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) = ∫ ( 0 (,) 1 ) ( ( ( ( Λ vts 𝑁 ) ‘ 𝑥 ) ↑ 3 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) d 𝑥 )