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		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	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( 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	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( 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	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 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 𝑥 )