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 ⊢ ( 𝜑 → 𝐻 : ℕ ⟶ ℝ )
circlemethhgt.k ⊢ ( 𝜑 → 𝐾 : ℕ ⟶ ℝ )
circlemethhgt.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion circlemethhgt ( 𝜑 → Σ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) = ∫ ( 0 (,) 1 ) ( ( ( ( ( Λ ∘f · 𝐻 ) vts 𝑁 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝐾 ) vts 𝑁 ) ‘ 𝑥 ) ↑ 2 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) d 𝑥 )

Proof

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