Theorem circlemethhgt 30721

Description: The circle method, where the Vinogradov sums are weighted using the Von Mangoldt function and smoothed using functions 𝐻 and 𝐾. 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.)

Hypotheses

Ref	Expression
circlemethhgt.h	⊢ (𝜑 → 𝐻:ℕ⟶ℝ)
circlemethhgt.k	⊢ (𝜑 → 𝐾:ℕ⟶ℝ)
circlemethhgt.n	⊢ (𝜑 → 𝑁 ∈ ℕ0)

Assertion

Ref	Expression
circlemethhgt	⊢ (𝜑 → Σ𝑛 ∈ (ℕ(repr‘3)𝑁)(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) = ∫(0(,)1)(((((Λ ∘𝑓 · 𝐻)vts𝑁)‘𝑥) · ((((Λ ∘𝑓 · 𝐾)vts𝑁)‘𝑥)↑2)) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) d𝑥)

Distinct variable groups:   𝑛,𝐻,𝑥   𝑛,𝐾,𝑥   𝑛,𝑁,𝑥   𝜑,𝑛,𝑥

Proof of Theorem circlemethhgt

Dummy variables 𝑎 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		circlemethhgt.n	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℕ0)
2		3nn 11186	. . . 4 ⊢ 3 ∈ ℕ
3	2	a1i 11	. . 3 ⊢ (𝜑 → 3 ∈ ℕ)
4		s3len 13639	. . . . . 6 ⊢ (#‘⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩) = 3
5	4	eqcomi 2631	. . . . 5 ⊢ 3 = (#‘⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩)
6	5	a1i 11	. . . 4 ⊢ (𝜑 → 3 = (#‘⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩))
7		simprl 794	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → 𝑥 ∈ ℝ)
8		simprr 796	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → 𝑦 ∈ ℝ)
9	7, 8	remulcld 10070	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 · 𝑦) ∈ ℝ)
10	9	recnd 10068	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 · 𝑦) ∈ ℂ)
11		vmaf 24845	. . . . . . . 8 ⊢ Λ:ℕ⟶ℝ
12	11	a1i 11	. . . . . . 7 ⊢ (𝜑 → Λ:ℕ⟶ℝ)
13		circlemethhgt.h	. . . . . . 7 ⊢ (𝜑 → 𝐻:ℕ⟶ℝ)
14		nnex 11026	. . . . . . . 8 ⊢ ℕ ∈ V
15	14	a1i 11	. . . . . . 7 ⊢ (𝜑 → ℕ ∈ V)
16		inidm 3822	. . . . . . 7 ⊢ (ℕ ∩ ℕ) = ℕ
17	10, 12, 13, 15, 15, 16	off 6912	. . . . . 6 ⊢ (𝜑 → (Λ ∘𝑓 · 𝐻):ℕ⟶ℂ)
18		cnex 10017	. . . . . . 7 ⊢ ℂ ∈ V
19	18, 14	elmap 7886	. . . . . 6 ⊢ ((Λ ∘𝑓 · 𝐻) ∈ (ℂ ↑𝑚 ℕ) ↔ (Λ ∘𝑓 · 𝐻):ℕ⟶ℂ)
20	17, 19	sylibr 224	. . . . 5 ⊢ (𝜑 → (Λ ∘𝑓 · 𝐻) ∈ (ℂ ↑𝑚 ℕ))
21		circlemethhgt.k	. . . . . . 7 ⊢ (𝜑 → 𝐾:ℕ⟶ℝ)
22	10, 12, 21, 15, 15, 16	off 6912	. . . . . 6 ⊢ (𝜑 → (Λ ∘𝑓 · 𝐾):ℕ⟶ℂ)
23	18, 14	elmap 7886	. . . . . 6 ⊢ ((Λ ∘𝑓 · 𝐾) ∈ (ℂ ↑𝑚 ℕ) ↔ (Λ ∘𝑓 · 𝐾):ℕ⟶ℂ)
24	22, 23	sylibr 224	. . . . 5 ⊢ (𝜑 → (Λ ∘𝑓 · 𝐾) ∈ (ℂ ↑𝑚 ℕ))
25	20, 24, 24	s3cld 13617	. . . 4 ⊢ (𝜑 → ⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩ ∈ Word (ℂ ↑𝑚 ℕ))
26	6, 25	wrdfd 30616	. . 3 ⊢ (𝜑 → ⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩:(0..^3)⟶(ℂ ↑𝑚 ℕ))
27	1, 3, 26	circlemeth 30718	. 2 ⊢ (𝜑 → Σ𝑛 ∈ (ℕ(repr‘3)𝑁)∏𝑎 ∈ (0..^3)((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)‘(𝑛‘𝑎)) = ∫(0(,)1)(∏𝑎 ∈ (0..^3)(((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) d𝑥)
28		fveq2 6191	. . . . . 6 ⊢ (𝑎 = 0 → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎) = (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘0))
29		fveq2 6191	. . . . . 6 ⊢ (𝑎 = 0 → (𝑛‘𝑎) = (𝑛‘0))
30	28, 29	fveq12d 6197	. . . . 5 ⊢ (𝑎 = 0 → ((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)‘(𝑛‘𝑎)) = ((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘0)‘(𝑛‘0)))
31		fveq2 6191	. . . . . 6 ⊢ (𝑎 = 1 → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎) = (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘1))
32		fveq2 6191	. . . . . 6 ⊢ (𝑎 = 1 → (𝑛‘𝑎) = (𝑛‘1))
33	31, 32	fveq12d 6197	. . . . 5 ⊢ (𝑎 = 1 → ((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)‘(𝑛‘𝑎)) = ((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘1)‘(𝑛‘1)))
34		fveq2 6191	. . . . . 6 ⊢ (𝑎 = 2 → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎) = (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘2))
35		fveq2 6191	. . . . . 6 ⊢ (𝑎 = 2 → (𝑛‘𝑎) = (𝑛‘2))
36	34, 35	fveq12d 6197	. . . . 5 ⊢ (𝑎 = 2 → ((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)‘(𝑛‘𝑎)) = ((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘2)‘(𝑛‘2)))
37	26	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → ⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩:(0..^3)⟶(ℂ ↑𝑚 ℕ))
38	37	ffvelrnda 6359	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) ∧ 𝑎 ∈ (0..^3)) → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎) ∈ (ℂ ↑𝑚 ℕ))
39		elmapi 7879	. . . . . . 7 ⊢ ((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎) ∈ (ℂ ↑𝑚 ℕ) → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎):ℕ⟶ℂ)
40	38, 39	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) ∧ 𝑎 ∈ (0..^3)) → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎):ℕ⟶ℂ)
41		ssid 3624	. . . . . . . . 9 ⊢ ℕ ⊆ ℕ
42	41	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → ℕ ⊆ ℕ)
43	1	nn0zd 11480	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℤ)
44	43	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → 𝑁 ∈ ℤ)
45		3nn0 11310	. . . . . . . . 9 ⊢ 3 ∈ ℕ0
46	45	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → 3 ∈ ℕ0)
47		simpr 477	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → 𝑛 ∈ (ℕ(repr‘3)𝑁))
48	42, 44, 46, 47	reprf 30690	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → 𝑛:(0..^3)⟶ℕ)
49	48	ffvelrnda 6359	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) ∧ 𝑎 ∈ (0..^3)) → (𝑛‘𝑎) ∈ ℕ)
50	40, 49	ffvelrnd 6360	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) ∧ 𝑎 ∈ (0..^3)) → ((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)‘(𝑛‘𝑎)) ∈ ℂ)
51	30, 33, 36, 50	prodfzo03 30681	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → ∏𝑎 ∈ (0..^3)((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)‘(𝑛‘𝑎)) = (((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘0)‘(𝑛‘0)) · (((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘1)‘(𝑛‘1)) · ((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘2)‘(𝑛‘2)))))
52		ovex 6678	. . . . . . . 8 ⊢ (Λ ∘𝑓 · 𝐻) ∈ V
53		s3fv0 13636	. . . . . . . 8 ⊢ ((Λ ∘𝑓 · 𝐻) ∈ V → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘0) = (Λ ∘𝑓 · 𝐻))
54	52, 53	mp1i 13	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘0) = (Λ ∘𝑓 · 𝐻))
55	54	fveq1d 6193	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → ((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘0)‘(𝑛‘0)) = ((Λ ∘𝑓 · 𝐻)‘(𝑛‘0)))
56		simpl 473	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → 𝜑)
57		c0ex 10034	. . . . . . . . . . 11 ⊢ 0 ∈ V
58	57	tpid1 4303	. . . . . . . . . 10 ⊢ 0 ∈ {0, 1, 2}
59		fzo0to3tp 12554	. . . . . . . . . 10 ⊢ (0..^3) = {0, 1, 2}
60	58, 59	eleqtrri 2700	. . . . . . . . 9 ⊢ 0 ∈ (0..^3)
61	60	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → 0 ∈ (0..^3))
62	48, 61	ffvelrnd 6360	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → (𝑛‘0) ∈ ℕ)
63		ffn 6045	. . . . . . . . . 10 ⊢ (Λ:ℕ⟶ℝ → Λ Fn ℕ)
64	11, 63	ax-mp 5	. . . . . . . . 9 ⊢ Λ Fn ℕ
65	64	a1i 11	. . . . . . . 8 ⊢ (𝜑 → Λ Fn ℕ)
66	13	ffnd 6046	. . . . . . . 8 ⊢ (𝜑 → 𝐻 Fn ℕ)
67		eqidd 2623	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛‘0) ∈ ℕ) → (Λ‘(𝑛‘0)) = (Λ‘(𝑛‘0)))
68		eqidd 2623	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛‘0) ∈ ℕ) → (𝐻‘(𝑛‘0)) = (𝐻‘(𝑛‘0)))
69	65, 66, 15, 15, 16, 67, 68	ofval 6906	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑛‘0) ∈ ℕ) → ((Λ ∘𝑓 · 𝐻)‘(𝑛‘0)) = ((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))))
70	56, 62, 69	syl2anc 693	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → ((Λ ∘𝑓 · 𝐻)‘(𝑛‘0)) = ((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))))
71	55, 70	eqtrd 2656	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → ((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘0)‘(𝑛‘0)) = ((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))))
72		ovex 6678	. . . . . . . . 9 ⊢ (Λ ∘𝑓 · 𝐾) ∈ V
73		s3fv1 13637	. . . . . . . . 9 ⊢ ((Λ ∘𝑓 · 𝐾) ∈ V → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘1) = (Λ ∘𝑓 · 𝐾))
74	72, 73	mp1i 13	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘1) = (Λ ∘𝑓 · 𝐾))
75	74	fveq1d 6193	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → ((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘1)‘(𝑛‘1)) = ((Λ ∘𝑓 · 𝐾)‘(𝑛‘1)))
76		1ex 10035	. . . . . . . . . . . 12 ⊢ 1 ∈ V
77	76	tpid2 4304	. . . . . . . . . . 11 ⊢ 1 ∈ {0, 1, 2}
78	77, 59	eleqtrri 2700	. . . . . . . . . 10 ⊢ 1 ∈ (0..^3)
79	78	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → 1 ∈ (0..^3))
80	48, 79	ffvelrnd 6360	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → (𝑛‘1) ∈ ℕ)
81	21	ffnd 6046	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 Fn ℕ)
82		eqidd 2623	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛‘1) ∈ ℕ) → (Λ‘(𝑛‘1)) = (Λ‘(𝑛‘1)))
83		eqidd 2623	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛‘1) ∈ ℕ) → (𝐾‘(𝑛‘1)) = (𝐾‘(𝑛‘1)))
84	65, 81, 15, 15, 16, 82, 83	ofval 6906	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛‘1) ∈ ℕ) → ((Λ ∘𝑓 · 𝐾)‘(𝑛‘1)) = ((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))))
85	56, 80, 84	syl2anc 693	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → ((Λ ∘𝑓 · 𝐾)‘(𝑛‘1)) = ((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))))
86	75, 85	eqtrd 2656	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → ((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘1)‘(𝑛‘1)) = ((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))))
87		s3fv2 13638	. . . . . . . . 9 ⊢ ((Λ ∘𝑓 · 𝐾) ∈ V → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘2) = (Λ ∘𝑓 · 𝐾))
88	72, 87	mp1i 13	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘2) = (Λ ∘𝑓 · 𝐾))
89	88	fveq1d 6193	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → ((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘2)‘(𝑛‘2)) = ((Λ ∘𝑓 · 𝐾)‘(𝑛‘2)))
90		2ex 11092	. . . . . . . . . . . 12 ⊢ 2 ∈ V
91	90	tpid3 4307	. . . . . . . . . . 11 ⊢ 2 ∈ {0, 1, 2}
92	91, 59	eleqtrri 2700	. . . . . . . . . 10 ⊢ 2 ∈ (0..^3)
93	92	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → 2 ∈ (0..^3))
94	48, 93	ffvelrnd 6360	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → (𝑛‘2) ∈ ℕ)
95		eqidd 2623	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛‘2) ∈ ℕ) → (Λ‘(𝑛‘2)) = (Λ‘(𝑛‘2)))
96		eqidd 2623	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛‘2) ∈ ℕ) → (𝐾‘(𝑛‘2)) = (𝐾‘(𝑛‘2)))
97	65, 81, 15, 15, 16, 95, 96	ofval 6906	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛‘2) ∈ ℕ) → ((Λ ∘𝑓 · 𝐾)‘(𝑛‘2)) = ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))
98	56, 94, 97	syl2anc 693	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → ((Λ ∘𝑓 · 𝐾)‘(𝑛‘2)) = ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))
99	89, 98	eqtrd 2656	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → ((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘2)‘(𝑛‘2)) = ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))
100	86, 99	oveq12d 6668	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → (((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘1)‘(𝑛‘1)) · ((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘2)‘(𝑛‘2))) = (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2)))))
101	71, 100	oveq12d 6668	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → (((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘0)‘(𝑛‘0)) · (((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘1)‘(𝑛‘1)) · ((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘2)‘(𝑛‘2)))) = (((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))))
102	51, 101	eqtrd 2656	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → ∏𝑎 ∈ (0..^3)((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)‘(𝑛‘𝑎)) = (((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))))
103	102	sumeq2dv 14433	. 2 ⊢ (𝜑 → Σ𝑛 ∈ (ℕ(repr‘3)𝑁)∏𝑎 ∈ (0..^3)((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)‘(𝑛‘𝑎)) = Σ𝑛 ∈ (ℕ(repr‘3)𝑁)(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))))
104		nfv 1843	. . . . . 6 ⊢ Ⅎ𝑎(𝜑 ∧ 𝑥 ∈ (0(,)1))
105		nfcv 2764	. . . . . 6 ⊢ Ⅎ𝑎(((Λ ∘𝑓 · 𝐻)vts𝑁)‘𝑥)
106		fzofi 12773	. . . . . . 7 ⊢ (1..^3) ∈ Fin
107	106	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → (1..^3) ∈ Fin)
108	57	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → 0 ∈ V)
109		eqid 2622	. . . . . . . . 9 ⊢ 0 = 0
110	109	orci 405	. . . . . . . 8 ⊢ (0 = 0 ∨ 0 = 3)
111		0elfz 12436	. . . . . . . . 9 ⊢ (3 ∈ ℕ0 → 0 ∈ (0...3))
112		elfznelfzob 12574	. . . . . . . . 9 ⊢ (0 ∈ (0...3) → (¬ 0 ∈ (1..^3) ↔ (0 = 0 ∨ 0 = 3)))
113	45, 111, 112	mp2b 10	. . . . . . . 8 ⊢ (¬ 0 ∈ (1..^3) ↔ (0 = 0 ∨ 0 = 3))
114	110, 113	mpbir 221	. . . . . . 7 ⊢ ¬ 0 ∈ (1..^3)
115	114	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → ¬ 0 ∈ (1..^3))
116	1	ad2antrr 762	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑎 ∈ (1..^3)) → 𝑁 ∈ ℕ0)
117		ioossre 12235	. . . . . . . . . . 11 ⊢ (0(,)1) ⊆ ℝ
118		ax-resscn 9993	. . . . . . . . . . 11 ⊢ ℝ ⊆ ℂ
119	117, 118	sstri 3612	. . . . . . . . . 10 ⊢ (0(,)1) ⊆ ℂ
120	119	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (0(,)1) ⊆ ℂ)
121	120	sselda 3603	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → 𝑥 ∈ ℂ)
122	121	adantr 481	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑎 ∈ (1..^3)) → 𝑥 ∈ ℂ)
123	26	ad2antrr 762	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑎 ∈ (1..^3)) → ⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩:(0..^3)⟶(ℂ ↑𝑚 ℕ))
124		fzo0ss1 12498	. . . . . . . . . . 11 ⊢ (1..^3) ⊆ (0..^3)
125	124	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → (1..^3) ⊆ (0..^3))
126	125	sselda 3603	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑎 ∈ (1..^3)) → 𝑎 ∈ (0..^3))
127	123, 126	ffvelrnd 6360	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑎 ∈ (1..^3)) → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎) ∈ (ℂ ↑𝑚 ℕ))
128	127, 39	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑎 ∈ (1..^3)) → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎):ℕ⟶ℂ)
129	116, 122, 128	vtscl 30716	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑎 ∈ (1..^3)) → (((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥) ∈ ℂ)
130	52, 53	ax-mp 5	. . . . . . . . 9 ⊢ (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘0) = (Λ ∘𝑓 · 𝐻)
131	28, 130	syl6eq 2672	. . . . . . . 8 ⊢ (𝑎 = 0 → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎) = (Λ ∘𝑓 · 𝐻))
132	131	oveq1d 6665	. . . . . . 7 ⊢ (𝑎 = 0 → ((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)vts𝑁) = ((Λ ∘𝑓 · 𝐻)vts𝑁))
133	132	fveq1d 6193	. . . . . 6 ⊢ (𝑎 = 0 → (((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥) = (((Λ ∘𝑓 · 𝐻)vts𝑁)‘𝑥))
134	1	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → 𝑁 ∈ ℕ0)
135	17	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → (Λ ∘𝑓 · 𝐻):ℕ⟶ℂ)
136	134, 121, 135	vtscl 30716	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → (((Λ ∘𝑓 · 𝐻)vts𝑁)‘𝑥) ∈ ℂ)
137	104, 105, 107, 108, 115, 129, 133, 136	fprodsplitsn 14720	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → ∏𝑎 ∈ ((1..^3) ∪ {0})(((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥) = (∏𝑎 ∈ (1..^3)(((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥) · (((Λ ∘𝑓 · 𝐻)vts𝑁)‘𝑥)))
138		uncom 3757	. . . . . . . 8 ⊢ ((1..^3) ∪ {0}) = ({0} ∪ (1..^3))
139		fzo0sn0fzo1 12557	. . . . . . . . 9 ⊢ (3 ∈ ℕ → (0..^3) = ({0} ∪ (1..^3)))
140	2, 139	ax-mp 5	. . . . . . . 8 ⊢ (0..^3) = ({0} ∪ (1..^3))
141	138, 140	eqtr4i 2647	. . . . . . 7 ⊢ ((1..^3) ∪ {0}) = (0..^3)
142	141	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → ((1..^3) ∪ {0}) = (0..^3))
143	142	prodeq1d 14651	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → ∏𝑎 ∈ ((1..^3) ∪ {0})(((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥) = ∏𝑎 ∈ (0..^3)(((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥))
144		fzo13pr 12552	. . . . . . . . . . . . . . 15 ⊢ (1..^3) = {1, 2}
145	144	eleq2i 2693	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ (1..^3) ↔ 𝑎 ∈ {1, 2})
146		vex 3203	. . . . . . . . . . . . . . 15 ⊢ 𝑎 ∈ V
147	146	elpr 4198	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ {1, 2} ↔ (𝑎 = 1 ∨ 𝑎 = 2))
148	145, 147	bitri 264	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ (1..^3) ↔ (𝑎 = 1 ∨ 𝑎 = 2))
149	31	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑎 = 1) → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎) = (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘1))
150	72, 73	mp1i 13	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑎 = 1) → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘1) = (Λ ∘𝑓 · 𝐾))
151	149, 150	eqtrd 2656	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 = 1) → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎) = (Λ ∘𝑓 · 𝐾))
152	34	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑎 = 2) → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎) = (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘2))
153	72, 87	mp1i 13	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑎 = 2) → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘2) = (Λ ∘𝑓 · 𝐾))
154	152, 153	eqtrd 2656	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 = 2) → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎) = (Λ ∘𝑓 · 𝐾))
155	151, 154	jaodan 826	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 = 1 ∨ 𝑎 = 2)) → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎) = (Λ ∘𝑓 · 𝐾))
156	148, 155	sylan2b 492	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (1..^3)) → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎) = (Λ ∘𝑓 · 𝐾))
157	156	adantlr 751	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑎 ∈ (1..^3)) → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎) = (Λ ∘𝑓 · 𝐾))
158	157	oveq1d 6665	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑎 ∈ (1..^3)) → ((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)vts𝑁) = ((Λ ∘𝑓 · 𝐾)vts𝑁))
159	158	fveq1d 6193	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑎 ∈ (1..^3)) → (((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥) = (((Λ ∘𝑓 · 𝐾)vts𝑁)‘𝑥))
160	159	prodeq2dv 14653	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → ∏𝑎 ∈ (1..^3)(((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥) = ∏𝑎 ∈ (1..^3)(((Λ ∘𝑓 · 𝐾)vts𝑁)‘𝑥))
161	22	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → (Λ ∘𝑓 · 𝐾):ℕ⟶ℂ)
162	134, 121, 161	vtscl 30716	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → (((Λ ∘𝑓 · 𝐾)vts𝑁)‘𝑥) ∈ ℂ)
163		fprodconst 14708	. . . . . . . . 9 ⊢ (((1..^3) ∈ Fin ∧ (((Λ ∘𝑓 · 𝐾)vts𝑁)‘𝑥) ∈ ℂ) → ∏𝑎 ∈ (1..^3)(((Λ ∘𝑓 · 𝐾)vts𝑁)‘𝑥) = ((((Λ ∘𝑓 · 𝐾)vts𝑁)‘𝑥)↑(#‘(1..^3))))
164	107, 162, 163	syl2anc 693	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → ∏𝑎 ∈ (1..^3)(((Λ ∘𝑓 · 𝐾)vts𝑁)‘𝑥) = ((((Λ ∘𝑓 · 𝐾)vts𝑁)‘𝑥)↑(#‘(1..^3))))
165		nnuz 11723	. . . . . . . . . . . . 13 ⊢ ℕ = (ℤ≥‘1)
166	2, 165	eleqtri 2699	. . . . . . . . . . . 12 ⊢ 3 ∈ (ℤ≥‘1)
167		hashfzo 13216	. . . . . . . . . . . 12 ⊢ (3 ∈ (ℤ≥‘1) → (#‘(1..^3)) = (3 − 1))
168	166, 167	ax-mp 5	. . . . . . . . . . 11 ⊢ (#‘(1..^3)) = (3 − 1)
169		3m1e2 11137	. . . . . . . . . . 11 ⊢ (3 − 1) = 2
170	168, 169	eqtri 2644	. . . . . . . . . 10 ⊢ (#‘(1..^3)) = 2
171	170	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → (#‘(1..^3)) = 2)
172	171	oveq2d 6666	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → ((((Λ ∘𝑓 · 𝐾)vts𝑁)‘𝑥)↑(#‘(1..^3))) = ((((Λ ∘𝑓 · 𝐾)vts𝑁)‘𝑥)↑2))
173	160, 164, 172	3eqtrd 2660	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → ∏𝑎 ∈ (1..^3)(((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥) = ((((Λ ∘𝑓 · 𝐾)vts𝑁)‘𝑥)↑2))
174	173	oveq1d 6665	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → (∏𝑎 ∈ (1..^3)(((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥) · (((Λ ∘𝑓 · 𝐻)vts𝑁)‘𝑥)) = (((((Λ ∘𝑓 · 𝐾)vts𝑁)‘𝑥)↑2) · (((Λ ∘𝑓 · 𝐻)vts𝑁)‘𝑥)))
175	162	sqcld 13006	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → ((((Λ ∘𝑓 · 𝐾)vts𝑁)‘𝑥)↑2) ∈ ℂ)
176	136, 175	mulcomd 10061	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → ((((Λ ∘𝑓 · 𝐻)vts𝑁)‘𝑥) · ((((Λ ∘𝑓 · 𝐾)vts𝑁)‘𝑥)↑2)) = (((((Λ ∘𝑓 · 𝐾)vts𝑁)‘𝑥)↑2) · (((Λ ∘𝑓 · 𝐻)vts𝑁)‘𝑥)))
177	174, 176	eqtr4d 2659	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → (∏𝑎 ∈ (1..^3)(((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥) · (((Λ ∘𝑓 · 𝐻)vts𝑁)‘𝑥)) = ((((Λ ∘𝑓 · 𝐻)vts𝑁)‘𝑥) · ((((Λ ∘𝑓 · 𝐾)vts𝑁)‘𝑥)↑2)))
178	137, 143, 177	3eqtr3d 2664	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → ∏𝑎 ∈ (0..^3)(((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥) = ((((Λ ∘𝑓 · 𝐻)vts𝑁)‘𝑥) · ((((Λ ∘𝑓 · 𝐾)vts𝑁)‘𝑥)↑2)))
179	178	oveq1d 6665	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → (∏𝑎 ∈ (0..^3)(((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) = (((((Λ ∘𝑓 · 𝐻)vts𝑁)‘𝑥) · ((((Λ ∘𝑓 · 𝐾)vts𝑁)‘𝑥)↑2)) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))))
180	179	itgeq2dv 23548	. 2 ⊢ (𝜑 → ∫(0(,)1)(∏𝑎 ∈ (0..^3)(((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) d𝑥 = ∫(0(,)1)(((((Λ ∘𝑓 · 𝐻)vts𝑁)‘𝑥) · ((((Λ ∘𝑓 · 𝐾)vts𝑁)‘𝑥)↑2)) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) d𝑥)
181	27, 103, 180	3eqtr3d 2664	1 ⊢ (𝜑 → Σ𝑛 ∈ (ℕ(repr‘3)𝑁)(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) = ∫(0(,)1)(((((Λ ∘𝑓 · 𝐻)vts𝑁)‘𝑥) · ((((Λ ∘𝑓 · 𝐾)vts𝑁)‘𝑥)↑2)) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) d𝑥)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 383   ∧ wa 384   = wceq 1483   ∈ wcel 1990  Vcvv 3200   ∪ cun 3572   ⊆ wss 3574  {csn 4177  {cpr 4179  {ctp 4181   Fn wfn 5883  ⟶wf 5884  ‘cfv 5888  (class class class)co 6650   ∘_𝑓 cof 6895   ↑_𝑚 cmap 7857  Fincfn 7955  ℂcc 9934  ℝcr 9935  0cc0 9936  1c1 9937  ici 9938   · cmul 9941   − cmin 10266  -cneg 10267  ℕcn 11020  2c2 11070  3c3 11071  ℕ₀cn0 11292  ℤcz 11377  ℤ_≥cuz 11687  (,)cioo 12175  ...cfz 12326  ..^cfzo 12465  ↑cexp 12860  #chash 13117  ⟨“cs3 13587  Σcsu 14416  ∏cprod 14635  expce 14792  πcpi 14797  ∫citg 23387  Λcvma 24818  reprcrepr 30686  vtscvts 30713

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cc 9257  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014  ax-addf 10015  ax-mulf 10016

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-disj 4621  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-of 6897  df-ofr 6898  df-om 7066  df-1st 7168  df-2nd 7169  df-supp 7296  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-oadd 7564  df-omul 7565  df-er 7742  df-map 7859  df-pm 7860  df-ixp 7909  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fsupp 8276  df-fi 8317  df-sup 8348  df-inf 8349  df-oi 8415  df-card 8765  df-acn 8768  df-cda 8990  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-z 11378  df-dec 11494  df-uz 11688  df-q 11789  df-rp 11833  df-xneg 11946  df-xadd 11947  df-xmul 11948  df-ioo 12179  df-ioc 12180  df-ico 12181  df-icc 12182  df-fz 12327  df-fzo 12466  df-fl 12593  df-mod 12669  df-seq 12802  df-exp 12861  df-fac 13061  df-bc 13090  df-hash 13118  df-word 13299  df-concat 13301  df-s1 13302  df-s2 13593  df-s3 13594  df-shft 13807  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-limsup 14202  df-clim 14219  df-rlim 14220  df-sum 14417  df-prod 14636  df-ef 14798  df-sin 14800  df-cos 14801  df-pi 14803  df-dvds 14984  df-gcd 15217  df-prm 15386  df-pc 15542  df-struct 15859  df-ndx 15860  df-slot 15861  df-base 15863  df-sets 15864  df-ress 15865  df-plusg 15954  df-mulr 15955  df-starv 15956  df-sca 15957  df-vsca 15958  df-ip 15959  df-tset 15960  df-ple 15961  df-ds 15964  df-unif 15965  df-hom 15966  df-cco 15967  df-rest 16083  df-topn 16084  df-0g 16102  df-gsum 16103  df-topgen 16104  df-pt 16105  df-prds 16108  df-xrs 16162  df-qtop 16167  df-imas 16168  df-xps 16170  df-mre 16246  df-mrc 16247  df-acs 16249  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-submnd 17336  df-mulg 17541  df-cntz 17750  df-cmn 18195  df-psmet 19738  df-xmet 19739  df-met 19740  df-bl 19741  df-mopn 19742  df-fbas 19743  df-fg 19744  df-cnfld 19747  df-top 20699  df-topon 20716  df-topsp 20737  df-bases 20750  df-cld 20823  df-ntr 20824  df-cls 20825  df-nei 20902  df-lp 20940  df-perf 20941  df-cn 21031  df-cnp 21032  df-haus 21119  df-cmp 21190  df-tx 21365  df-hmeo 21558  df-fil 21650  df-fm 21742  df-flim 21743  df-flf 21744  df-xms 22125  df-ms 22126  df-tms 22127  df-cncf 22681  df-ovol 23233  df-vol 23234  df-mbf 23388  df-itg1 23389  df-itg2 23390  df-ibl 23391  df-itg 23392  df-0p 23437  df-limc 23630  df-dv 23631  df-log 24303  df-vma 24824  df-repr 30687  df-vts 30714

This theorem is referenced by:  tgoldbachgtde  30738