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 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( 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 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) → ( 𝑛 ‘ 𝑎 ) ∈ ℕ )
49 40 48 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( 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 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( 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 1ex ⊢ 1 ∈ V
76 75 tpid2 ⊢ 1 ∈ { 0 , 1 , 2 }
77 76 58 eleqtrri ⊢ 1 ∈ ( 0 ..^ 3 )
78 77 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → 1 ∈ ( 0 ..^ 3 ) )
79 47 78 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → ( 𝑛 ‘ 1 ) ∈ ℕ )
80 2 ffnd ⊢ ( 𝜑 → 𝐾 Fn ℕ )
81 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑛 ‘ 1 ) ∈ ℕ ) → ( Λ ‘ ( 𝑛 ‘ 1 ) ) = ( Λ ‘ ( 𝑛 ‘ 1 ) ) )
82 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑛 ‘ 1 ) ∈ ℕ ) → ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) = ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) )
83 64 80 16 16 17 81 82 ofval ⊢ ( ( 𝜑 ∧ ( 𝑛 ‘ 1 ) ∈ ℕ ) → ( ( Λ ∘f · 𝐾 ) ‘ ( 𝑛 ‘ 1 ) ) = ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) )
84 55 79 83 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → ( ( Λ ∘f · 𝐾 ) ‘ ( 𝑛 ‘ 1 ) ) = ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) )
85 74 84 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → ( ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 1 ) ‘ ( 𝑛 ‘ 1 ) ) = ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) )
86 s3fv2 ⊢ ( ( Λ ∘f · 𝐾 ) ∈ V → ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 2 ) = ( Λ ∘f · 𝐾 ) )
87 71 86 mp1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 2 ) = ( Λ ∘f · 𝐾 ) )
88 87 fveq1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → ( ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 2 ) ‘ ( 𝑛 ‘ 2 ) ) = ( ( Λ ∘f · 𝐾 ) ‘ ( 𝑛 ‘ 2 ) ) )
89 2ex ⊢ 2 ∈ V
90 89 tpid3 ⊢ 2 ∈ { 0 , 1 , 2 }
91 90 58 eleqtrri ⊢ 2 ∈ ( 0 ..^ 3 )
92 91 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → 2 ∈ ( 0 ..^ 3 ) )
93 47 92 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → ( 𝑛 ‘ 2 ) ∈ ℕ )
94 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑛 ‘ 2 ) ∈ ℕ ) → ( Λ ‘ ( 𝑛 ‘ 2 ) ) = ( Λ ‘ ( 𝑛 ‘ 2 ) ) )
95 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑛 ‘ 2 ) ∈ ℕ ) → ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) = ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) )
96 64 80 16 16 17 94 95 ofval ⊢ ( ( 𝜑 ∧ ( 𝑛 ‘ 2 ) ∈ ℕ ) → ( ( Λ ∘f · 𝐾 ) ‘ ( 𝑛 ‘ 2 ) ) = ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) )
97 55 93 96 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → ( ( Λ ∘f · 𝐾 ) ‘ ( 𝑛 ‘ 2 ) ) = ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) )
98 88 97 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → ( ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 2 ) ‘ ( 𝑛 ‘ 2 ) ) = ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) )
99 85 98 oveq12d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → ( ( ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 1 ) ‘ ( 𝑛 ‘ 1 ) ) · ( ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 2 ) ‘ ( 𝑛 ‘ 2 ) ) ) = ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) )
100 70 99 oveq12d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → ( ( ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 0 ) ‘ ( 𝑛 ‘ 0 ) ) · ( ( ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 1 ) ‘ ( 𝑛 ‘ 1 ) ) · ( ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 2 ) ‘ ( 𝑛 ‘ 2 ) ) ) ) = ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) )
101 50 100 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → ∏ 𝑎 ∈ ( 0 ..^ 3 ) ( ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 𝑎 ) ‘ ( 𝑛 ‘ 𝑎 ) ) = ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) )
102 101 sumeq2dv ⊢ ( 𝜑 → Σ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∏ 𝑎 ∈ ( 0 ..^ 3 ) ( ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 𝑎 ) ‘ ( 𝑛 ‘ 𝑎 ) ) = Σ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) )
103 nfv ⊢ Ⅎ 𝑎 ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) )
104 nfcv ⊢ Ⅎ 𝑎 ( ( ( Λ ∘f · 𝐻 ) vts 𝑁 ) ‘ 𝑥 )
105 fzofi ⊢ ( 1 ..^ 3 ) ∈ Fin
106 105 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( 1 ..^ 3 ) ∈ Fin )
107 56 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 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 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ¬ 0 ∈ ( 1 ..^ 3 ) )
115 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑎 ∈ ( 1 ..^ 3 ) ) → 𝑁 ∈ ℕ0 )
116 ioossre ⊢ ( 0 (,) 1 ) ⊆ ℝ
117 ax-resscn ⊢ ℝ ⊆ ℂ
118 116 117 sstri ⊢ ( 0 (,) 1 ) ⊆ ℂ
119 118 a1i ⊢ ( 𝜑 → ( 0 (,) 1 ) ⊆ ℂ )
120 119 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → 𝑥 ∈ ℂ )
121 120 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑎 ∈ ( 1 ..^ 3 ) ) → 𝑥 ∈ ℂ )
122 26 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑎 ∈ ( 1 ..^ 3 ) ) → ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ : ( 0 ..^ 3 ) ⟶ ( ℂ ↑m ℕ ) )
123 fzo0ss1 ⊢ ( 1 ..^ 3 ) ⊆ ( 0 ..^ 3 )
124 123 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( 1 ..^ 3 ) ⊆ ( 0 ..^ 3 ) )
125 124 sselda ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑎 ∈ ( 1 ..^ 3 ) ) → 𝑎 ∈ ( 0 ..^ 3 ) )
126 122 125 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑎 ∈ ( 1 ..^ 3 ) ) → ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 𝑎 ) ∈ ( ℂ ↑m ℕ ) )
127 126 39 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑎 ∈ ( 1 ..^ 3 ) ) → ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 𝑎 ) : ℕ ⟶ ℂ )
128 115 121 127 vtscl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑎 ∈ ( 1 ..^ 3 ) ) → ( ( ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑥 ) ∈ ℂ )
129 51 52 ax-mp ⊢ ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 0 ) = ( Λ ∘f · 𝐻 )
130 28 129 eqtrdi ⊢ ( 𝑎 = 0 → ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 𝑎 ) = ( Λ ∘f · 𝐻 ) )
131 130 oveq1d ⊢ ( 𝑎 = 0 → ( ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 𝑎 ) vts 𝑁 ) = ( ( Λ ∘f · 𝐻 ) vts 𝑁 ) )
132 131 fveq1d ⊢ ( 𝑎 = 0 → ( ( ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑥 ) = ( ( ( Λ ∘f · 𝐻 ) vts 𝑁 ) ‘ 𝑥 ) )
133 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → 𝑁 ∈ ℕ0 )
134 18 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( Λ ∘f · 𝐻 ) : ℕ ⟶ ℂ )
135 133 120 134 vtscl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( ( ( Λ ∘f · 𝐻 ) vts 𝑁 ) ‘ 𝑥 ) ∈ ℂ )
136 103 104 106 107 114 128 132 135 fprodsplitsn ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ∏ 𝑎 ∈ ( ( 1 ..^ 3 ) ∪ { 0 } ) ( ( ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑥 ) = ( ∏ 𝑎 ∈ ( 1 ..^ 3 ) ( ( ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑥 ) · ( ( ( Λ ∘f · 𝐻 ) vts 𝑁 ) ‘ 𝑥 ) ) )
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 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( ( 1 ..^ 3 ) ∪ { 0 } ) = ( 0 ..^ 3 ) )
142 141 prodeq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ∏ 𝑎 ∈ ( ( 1 ..^ 3 ) ∪ { 0 } ) ( ( ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑥 ) = ∏ 𝑎 ∈ ( 0 ..^ 3 ) ( ( ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑥 ) )
143 fzo13pr ⊢ ( 1 ..^ 3 ) = { 1 , 2 }
144 143 eleq2i ⊢ ( 𝑎 ∈ ( 1 ..^ 3 ) ↔ 𝑎 ∈ { 1 , 2 } )
145 vex ⊢ 𝑎 ∈ V
146 145 elpr ⊢ ( 𝑎 ∈ { 1 , 2 } ↔ ( 𝑎 = 1 ∨ 𝑎 = 2 ) )
147 144 146 bitri ⊢ ( 𝑎 ∈ ( 1 ..^ 3 ) ↔ ( 𝑎 = 1 ∨ 𝑎 = 2 ) )
148 31 adantl ⊢ ( ( 𝜑 ∧ 𝑎 = 1 ) → ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 𝑎 ) = ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 1 ) )
149 71 72 mp1i ⊢ ( ( 𝜑 ∧ 𝑎 = 1 ) → ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 1 ) = ( Λ ∘f · 𝐾 ) )
150 148 149 eqtrd ⊢ ( ( 𝜑 ∧ 𝑎 = 1 ) → ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 𝑎 ) = ( Λ ∘f · 𝐾 ) )
151 34 adantl ⊢ ( ( 𝜑 ∧ 𝑎 = 2 ) → ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 𝑎 ) = ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 2 ) )
152 71 86 mp1i ⊢ ( ( 𝜑 ∧ 𝑎 = 2 ) → ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 2 ) = ( Λ ∘f · 𝐾 ) )
153 151 152 eqtrd ⊢ ( ( 𝜑 ∧ 𝑎 = 2 ) → ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 𝑎 ) = ( Λ ∘f · 𝐾 ) )
154 150 153 jaodan ⊢ ( ( 𝜑 ∧ ( 𝑎 = 1 ∨ 𝑎 = 2 ) ) → ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 𝑎 ) = ( Λ ∘f · 𝐾 ) )
155 147 154 sylan2b ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ..^ 3 ) ) → ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 𝑎 ) = ( Λ ∘f · 𝐾 ) )
156 155 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑎 ∈ ( 1 ..^ 3 ) ) → ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 𝑎 ) = ( Λ ∘f · 𝐾 ) )
157 156 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑎 ∈ ( 1 ..^ 3 ) ) → ( ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 𝑎 ) vts 𝑁 ) = ( ( Λ ∘f · 𝐾 ) vts 𝑁 ) )
158 157 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑎 ∈ ( 1 ..^ 3 ) ) → ( ( ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑥 ) = ( ( ( Λ ∘f · 𝐾 ) vts 𝑁 ) ‘ 𝑥 ) )
159 158 prodeq2dv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ∏ 𝑎 ∈ ( 1 ..^ 3 ) ( ( ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑥 ) = ∏ 𝑎 ∈ ( 1 ..^ 3 ) ( ( ( Λ ∘f · 𝐾 ) vts 𝑁 ) ‘ 𝑥 ) )
160 22 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( Λ ∘f · 𝐾 ) : ℕ ⟶ ℂ )
161 133 120 160 vtscl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( ( ( Λ ∘f · 𝐾 ) vts 𝑁 ) ‘ 𝑥 ) ∈ ℂ )
162 fprodconst ⊢ ( ( ( 1 ..^ 3 ) ∈ Fin ∧ ( ( ( Λ ∘f · 𝐾 ) vts 𝑁 ) ‘ 𝑥 ) ∈ ℂ ) → ∏ 𝑎 ∈ ( 1 ..^ 3 ) ( ( ( Λ ∘f · 𝐾 ) vts 𝑁 ) ‘ 𝑥 ) = ( ( ( ( Λ ∘f · 𝐾 ) vts 𝑁 ) ‘ 𝑥 ) ↑ ( ♯ ‘ ( 1 ..^ 3 ) ) ) )
163 106 161 162 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ∏ 𝑎 ∈ ( 1 ..^ 3 ) ( ( ( Λ ∘f · 𝐾 ) vts 𝑁 ) ‘ 𝑥 ) = ( ( ( ( Λ ∘f · 𝐾 ) vts 𝑁 ) ‘ 𝑥 ) ↑ ( ♯ ‘ ( 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 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( ♯ ‘ ( 1 ..^ 3 ) ) = 2 )
171 170 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( ( ( ( Λ ∘f · 𝐾 ) vts 𝑁 ) ‘ 𝑥 ) ↑ ( ♯ ‘ ( 1 ..^ 3 ) ) ) = ( ( ( ( Λ ∘f · 𝐾 ) vts 𝑁 ) ‘ 𝑥 ) ↑ 2 ) )
172 159 163 171 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ∏ 𝑎 ∈ ( 1 ..^ 3 ) ( ( ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑥 ) = ( ( ( ( Λ ∘f · 𝐾 ) vts 𝑁 ) ‘ 𝑥 ) ↑ 2 ) )
173 172 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( ∏ 𝑎 ∈ ( 1 ..^ 3 ) ( ( ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑥 ) · ( ( ( Λ ∘f · 𝐻 ) vts 𝑁 ) ‘ 𝑥 ) ) = ( ( ( ( ( Λ ∘f · 𝐾 ) vts 𝑁 ) ‘ 𝑥 ) ↑ 2 ) · ( ( ( Λ ∘f · 𝐻 ) vts 𝑁 ) ‘ 𝑥 ) ) )
174 161 sqcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( ( ( ( Λ ∘f · 𝐾 ) vts 𝑁 ) ‘ 𝑥 ) ↑ 2 ) ∈ ℂ )
175 135 174 mulcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( ( ( ( Λ ∘f · 𝐻 ) vts 𝑁 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝐾 ) vts 𝑁 ) ‘ 𝑥 ) ↑ 2 ) ) = ( ( ( ( ( Λ ∘f · 𝐾 ) vts 𝑁 ) ‘ 𝑥 ) ↑ 2 ) · ( ( ( Λ ∘f · 𝐻 ) vts 𝑁 ) ‘ 𝑥 ) ) )
176 173 175 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( ∏ 𝑎 ∈ ( 1 ..^ 3 ) ( ( ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑥 ) · ( ( ( Λ ∘f · 𝐻 ) vts 𝑁 ) ‘ 𝑥 ) ) = ( ( ( ( Λ ∘f · 𝐻 ) vts 𝑁 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝐾 ) vts 𝑁 ) ‘ 𝑥 ) ↑ 2 ) ) )
177 136 142 176 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ∏ 𝑎 ∈ ( 0 ..^ 3 ) ( ( ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑥 ) = ( ( ( ( Λ ∘f · 𝐻 ) vts 𝑁 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝐾 ) vts 𝑁 ) ‘ 𝑥 ) ↑ 2 ) ) )
178 177 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( ∏ 𝑎 ∈ ( 0 ..^ 3 ) ( ( ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑥 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) = ( ( ( ( ( Λ ∘f · 𝐻 ) vts 𝑁 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝐾 ) vts 𝑁 ) ‘ 𝑥 ) ↑ 2 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) )
179 178 itgeq2dv ⊢ ( 𝜑 → ∫ ( 0 (,) 1 ) ( ∏ 𝑎 ∈ ( 0 ..^ 3 ) ( ( ( ⟨“ ( Λ ∘f · 𝐻 ) ( Λ ∘f · 𝐾 ) ( Λ ∘f · 𝐾 ) ”⟩ ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑥 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) d 𝑥 = ∫ ( 0 (,) 1 ) ( ( ( ( ( Λ ∘f · 𝐻 ) vts 𝑁 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝐾 ) vts 𝑁 ) ‘ 𝑥 ) ↑ 2 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) d 𝑥 )
180 27 102 179 3eqtr3d ⊢ ( 𝜑 → Σ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) = ∫ ( 0 (,) 1 ) ( ( ( ( ( Λ ∘f · 𝐻 ) vts 𝑁 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝐾 ) vts 𝑁 ) ‘ 𝑥 ) ↑ 2 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) d 𝑥 )