Theorem circlemethhgt 34641

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)(((((Λ ∘f · 𝐻)vts𝑁)‘𝑥) · ((((Λ ∘f · 𝐾)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 12272	. . . 4 ⊢ 3 ∈ ℕ
3	2	a1i 11	. . 3 ⊢ (𝜑 → 3 ∈ ℕ)
4		s3len 14867	. . . . . 6 ⊢ (♯‘⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩) = 3
5	4	eqcomi 2739	. . . . 5 ⊢ 3 = (♯‘⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩)
6	5	a1i 11	. . . 4 ⊢ (𝜑 → 3 = (♯‘⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩))
7		simprl 770	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → 𝑥 ∈ ℝ)
8		simprr 772	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → 𝑦 ∈ ℝ)
9	7, 8	remulcld 11211	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 · 𝑦) ∈ ℝ)
10	9	recnd 11209	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 · 𝑦) ∈ ℂ)
11		vmaf 27036	. . . . . . . 8 ⊢ Λ:ℕ⟶ℝ
12	11	a1i 11	. . . . . . 7 ⊢ (𝜑 → Λ:ℕ⟶ℝ)
13		circlemethhgt.h	. . . . . . 7 ⊢ (𝜑 → 𝐻:ℕ⟶ℝ)
14		nnex 12199	. . . . . . . 8 ⊢ ℕ ∈ V
15	14	a1i 11	. . . . . . 7 ⊢ (𝜑 → ℕ ∈ V)
16		inidm 4193	. . . . . . 7 ⊢ (ℕ ∩ ℕ) = ℕ
17	10, 12, 13, 15, 15, 16	off 7674	. . . . . 6 ⊢ (𝜑 → (Λ ∘f · 𝐻):ℕ⟶ℂ)
18		cnex 11156	. . . . . . 7 ⊢ ℂ ∈ V
19	18, 14	elmap 8847	. . . . . 6 ⊢ ((Λ ∘f · 𝐻) ∈ (ℂ ↑m ℕ) ↔ (Λ ∘f · 𝐻):ℕ⟶ℂ)
20	17, 19	sylibr 234	. . . . 5 ⊢ (𝜑 → (Λ ∘f · 𝐻) ∈ (ℂ ↑m ℕ))
21		circlemethhgt.k	. . . . . . 7 ⊢ (𝜑 → 𝐾:ℕ⟶ℝ)
22	10, 12, 21, 15, 15, 16	off 7674	. . . . . 6 ⊢ (𝜑 → (Λ ∘f · 𝐾):ℕ⟶ℂ)
23	18, 14	elmap 8847	. . . . . 6 ⊢ ((Λ ∘f · 𝐾) ∈ (ℂ ↑m ℕ) ↔ (Λ ∘f · 𝐾):ℕ⟶ℂ)
24	22, 23	sylibr 234	. . . . 5 ⊢ (𝜑 → (Λ ∘f · 𝐾) ∈ (ℂ ↑m ℕ))
25	20, 24, 24	s3cld 14845	. . . 4 ⊢ (𝜑 → ⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩ ∈ Word (ℂ ↑m ℕ))
26	6, 25	wrdfd 14491	. . 3 ⊢ (𝜑 → ⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩:(0..^3)⟶(ℂ ↑m ℕ))
27	1, 3, 26	circlemeth 34638	. 2 ⊢ (𝜑 → Σ𝑛 ∈ (ℕ(repr‘3)𝑁)∏𝑎 ∈ (0..^3)((⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘𝑎)‘(𝑛‘𝑎)) = ∫(0(,)1)(∏𝑎 ∈ (0..^3)(((⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) d𝑥)
28		fveq2 6861	. . . . . 6 ⊢ (𝑎 = 0 → (⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘𝑎) = (⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘0))
29		fveq2 6861	. . . . . 6 ⊢ (𝑎 = 0 → (𝑛‘𝑎) = (𝑛‘0))
30	28, 29	fveq12d 6868	. . . . 5 ⊢ (𝑎 = 0 → ((⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘𝑎)‘(𝑛‘𝑎)) = ((⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘0)‘(𝑛‘0)))
31		fveq2 6861	. . . . . 6 ⊢ (𝑎 = 1 → (⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘𝑎) = (⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘1))
32		fveq2 6861	. . . . . 6 ⊢ (𝑎 = 1 → (𝑛‘𝑎) = (𝑛‘1))
33	31, 32	fveq12d 6868	. . . . 5 ⊢ (𝑎 = 1 → ((⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘𝑎)‘(𝑛‘𝑎)) = ((⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘1)‘(𝑛‘1)))
34		fveq2 6861	. . . . . 6 ⊢ (𝑎 = 2 → (⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘𝑎) = (⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘2))
35		fveq2 6861	. . . . . 6 ⊢ (𝑎 = 2 → (𝑛‘𝑎) = (𝑛‘2))
36	34, 35	fveq12d 6868	. . . . 5 ⊢ (𝑎 = 2 → ((⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘𝑎)‘(𝑛‘𝑎)) = ((⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘2)‘(𝑛‘2)))
37	26	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → ⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩:(0..^3)⟶(ℂ ↑m ℕ))
38	37	ffvelcdmda 7059	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) ∧ 𝑎 ∈ (0..^3)) → (⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘𝑎) ∈ (ℂ ↑m ℕ))
39		elmapi 8825	. . . . . . 7 ⊢ ((⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘𝑎) ∈ (ℂ ↑m ℕ) → (⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘𝑎):ℕ⟶ℂ)
40	38, 39	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) ∧ 𝑎 ∈ (0..^3)) → (⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘𝑎):ℕ⟶ℂ)
41		ssidd 3973	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → ℕ ⊆ ℕ)
42	1	nn0zd 12562	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℤ)
43	42	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → 𝑁 ∈ ℤ)
44		3nn0 12467	. . . . . . . . 9 ⊢ 3 ∈ ℕ0
45	44	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → 3 ∈ ℕ0)
46		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → 𝑛 ∈ (ℕ(repr‘3)𝑁))
47	41, 43, 45, 46	reprf 34610	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → 𝑛:(0..^3)⟶ℕ)
48	47	ffvelcdmda 7059	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) ∧ 𝑎 ∈ (0..^3)) → (𝑛‘𝑎) ∈ ℕ)
49	40, 48	ffvelcdmd 7060	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) ∧ 𝑎 ∈ (0..^3)) → ((⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘𝑎)‘(𝑛‘𝑎)) ∈ ℂ)
50	30, 33, 36, 49	prodfzo03 34601	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → ∏𝑎 ∈ (0..^3)((⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘𝑎)‘(𝑛‘𝑎)) = (((⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘0)‘(𝑛‘0)) · (((⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘1)‘(𝑛‘1)) · ((⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘2)‘(𝑛‘2)))))
51		ovex 7423	. . . . . . . 8 ⊢ (Λ ∘f · 𝐻) ∈ V
52		s3fv0 14864	. . . . . . . 8 ⊢ ((Λ ∘f · 𝐻) ∈ V → (⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘0) = (Λ ∘f · 𝐻))
53	51, 52	mp1i 13	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → (⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘0) = (Λ ∘f · 𝐻))
54	53	fveq1d 6863	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → ((⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘0)‘(𝑛‘0)) = ((Λ ∘f · 𝐻)‘(𝑛‘0)))
55		simpl 482	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → 𝜑)
56		c0ex 11175	. . . . . . . . . . 11 ⊢ 0 ∈ V
57	56	tpid1 4735	. . . . . . . . . 10 ⊢ 0 ∈ {0, 1, 2}
58		fzo0to3tp 13720	. . . . . . . . . 10 ⊢ (0..^3) = {0, 1, 2}
59	57, 58	eleqtrri 2828	. . . . . . . . 9 ⊢ 0 ∈ (0..^3)
60	59	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → 0 ∈ (0..^3))
61	47, 60	ffvelcdmd 7060	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → (𝑛‘0) ∈ ℕ)
62		ffn 6691	. . . . . . . . . 10 ⊢ (Λ:ℕ⟶ℝ → Λ Fn ℕ)
63	11, 62	ax-mp 5	. . . . . . . . 9 ⊢ Λ Fn ℕ
64	63	a1i 11	. . . . . . . 8 ⊢ (𝜑 → Λ Fn ℕ)
65	13	ffnd 6692	. . . . . . . 8 ⊢ (𝜑 → 𝐻 Fn ℕ)
66		eqidd 2731	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛‘0) ∈ ℕ) → (Λ‘(𝑛‘0)) = (Λ‘(𝑛‘0)))
67		eqidd 2731	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛‘0) ∈ ℕ) → (𝐻‘(𝑛‘0)) = (𝐻‘(𝑛‘0)))
68	64, 65, 15, 15, 16, 66, 67	ofval 7667	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑛‘0) ∈ ℕ) → ((Λ ∘f · 𝐻)‘(𝑛‘0)) = ((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))))
69	55, 61, 68	syl2anc 584	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → ((Λ ∘f · 𝐻)‘(𝑛‘0)) = ((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))))
70	54, 69	eqtrd 2765	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → ((⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘0)‘(𝑛‘0)) = ((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))))
71		ovex 7423	. . . . . . . . 9 ⊢ (Λ ∘f · 𝐾) ∈ V
72		s3fv1 14865	. . . . . . . . 9 ⊢ ((Λ ∘f · 𝐾) ∈ V → (⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘1) = (Λ ∘f · 𝐾))
73	71, 72	mp1i 13	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → (⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘1) = (Λ ∘f · 𝐾))
74	73	fveq1d 6863	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → ((⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘1)‘(𝑛‘1)) = ((Λ ∘f · 𝐾)‘(𝑛‘1)))
75		1ex 11177	. . . . . . . . . . . 12 ⊢ 1 ∈ V
76	75	tpid2 4737	. . . . . . . . . . 11 ⊢ 1 ∈ {0, 1, 2}
77	76, 58	eleqtrri 2828	. . . . . . . . . 10 ⊢ 1 ∈ (0..^3)
78	77	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → 1 ∈ (0..^3))
79	47, 78	ffvelcdmd 7060	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → (𝑛‘1) ∈ ℕ)
80	21	ffnd 6692	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 Fn ℕ)
81		eqidd 2731	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛‘1) ∈ ℕ) → (Λ‘(𝑛‘1)) = (Λ‘(𝑛‘1)))
82		eqidd 2731	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛‘1) ∈ ℕ) → (𝐾‘(𝑛‘1)) = (𝐾‘(𝑛‘1)))
83	64, 80, 15, 15, 16, 81, 82	ofval 7667	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛‘1) ∈ ℕ) → ((Λ ∘f · 𝐾)‘(𝑛‘1)) = ((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))))
84	55, 79, 83	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → ((Λ ∘f · 𝐾)‘(𝑛‘1)) = ((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))))
85	74, 84	eqtrd 2765	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → ((⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘1)‘(𝑛‘1)) = ((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))))
86		s3fv2 14866	. . . . . . . . 9 ⊢ ((Λ ∘f · 𝐾) ∈ V → (⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘2) = (Λ ∘f · 𝐾))
87	71, 86	mp1i 13	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → (⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘2) = (Λ ∘f · 𝐾))
88	87	fveq1d 6863	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → ((⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘2)‘(𝑛‘2)) = ((Λ ∘f · 𝐾)‘(𝑛‘2)))
89		2ex 12270	. . . . . . . . . . . 12 ⊢ 2 ∈ V
90	89	tpid3 4740	. . . . . . . . . . 11 ⊢ 2 ∈ {0, 1, 2}
91	90, 58	eleqtrri 2828	. . . . . . . . . 10 ⊢ 2 ∈ (0..^3)
92	91	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → 2 ∈ (0..^3))
93	47, 92	ffvelcdmd 7060	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → (𝑛‘2) ∈ ℕ)
94		eqidd 2731	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛‘2) ∈ ℕ) → (Λ‘(𝑛‘2)) = (Λ‘(𝑛‘2)))
95		eqidd 2731	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛‘2) ∈ ℕ) → (𝐾‘(𝑛‘2)) = (𝐾‘(𝑛‘2)))
96	64, 80, 15, 15, 16, 94, 95	ofval 7667	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛‘2) ∈ ℕ) → ((Λ ∘f · 𝐾)‘(𝑛‘2)) = ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))
97	55, 93, 96	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → ((Λ ∘f · 𝐾)‘(𝑛‘2)) = ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))
98	88, 97	eqtrd 2765	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → ((⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘2)‘(𝑛‘2)) = ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))
99	85, 98	oveq12d 7408	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → (((⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘1)‘(𝑛‘1)) · ((⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘2)‘(𝑛‘2))) = (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2)))))
100	70, 99	oveq12d 7408	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(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 2765	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → ∏𝑎 ∈ (0..^3)((⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘𝑎)‘(𝑛‘𝑎)) = (((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))))
102	101	sumeq2dv 15675	. 2 ⊢ (𝜑 → Σ𝑛 ∈ (ℕ(repr‘3)𝑁)∏𝑎 ∈ (0..^3)((⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘𝑎)‘(𝑛‘𝑎)) = Σ𝑛 ∈ (ℕ(repr‘3)𝑁)(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))))
103		nfv 1914	. . . . . 6 ⊢ Ⅎ𝑎(𝜑 ∧ 𝑥 ∈ (0(,)1))
104		nfcv 2892	. . . . . 6 ⊢ Ⅎ𝑎(((Λ ∘f · 𝐻)vts𝑁)‘𝑥)
105		fzofi 13946	. . . . . . 7 ⊢ (1..^3) ∈ Fin
106	105	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → (1..^3) ∈ Fin)
107	56	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → 0 ∈ V)
108		eqid 2730	. . . . . . . . 9 ⊢ 0 = 0
109	108	orci 865	. . . . . . . 8 ⊢ (0 = 0 ∨ 0 = 3)
110		0elfz 13592	. . . . . . . . 9 ⊢ (3 ∈ ℕ0 → 0 ∈ (0...3))
111		elfznelfzob 13741	. . . . . . . . 9 ⊢ (0 ∈ (0...3) → (¬ 0 ∈ (1..^3) ↔ (0 = 0 ∨ 0 = 3)))
112	44, 110, 111	mp2b 10	. . . . . . . 8 ⊢ (¬ 0 ∈ (1..^3) ↔ (0 = 0 ∨ 0 = 3))
113	109, 112	mpbir 231	. . . . . . 7 ⊢ ¬ 0 ∈ (1..^3)
114	113	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → ¬ 0 ∈ (1..^3))
115	1	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑎 ∈ (1..^3)) → 𝑁 ∈ ℕ0)
116		ioossre 13375	. . . . . . . . . . 11 ⊢ (0(,)1) ⊆ ℝ
117		ax-resscn 11132	. . . . . . . . . . 11 ⊢ ℝ ⊆ ℂ
118	116, 117	sstri 3959	. . . . . . . . . 10 ⊢ (0(,)1) ⊆ ℂ
119	118	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (0(,)1) ⊆ ℂ)
120	119	sselda 3949	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → 𝑥 ∈ ℂ)
121	120	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑎 ∈ (1..^3)) → 𝑥 ∈ ℂ)
122	26	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑎 ∈ (1..^3)) → ⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩:(0..^3)⟶(ℂ ↑m ℕ))
123		fzo0ss1 13657	. . . . . . . . . . 11 ⊢ (1..^3) ⊆ (0..^3)
124	123	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → (1..^3) ⊆ (0..^3))
125	124	sselda 3949	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑎 ∈ (1..^3)) → 𝑎 ∈ (0..^3))
126	122, 125	ffvelcdmd 7060	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑎 ∈ (1..^3)) → (⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘𝑎) ∈ (ℂ ↑m ℕ))
127	126, 39	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑎 ∈ (1..^3)) → (⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘𝑎):ℕ⟶ℂ)
128	115, 121, 127	vtscl 34636	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑎 ∈ (1..^3)) → (((⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥) ∈ ℂ)
129	51, 52	ax-mp 5	. . . . . . . . 9 ⊢ (⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘0) = (Λ ∘f · 𝐻)
130	28, 129	eqtrdi 2781	. . . . . . . 8 ⊢ (𝑎 = 0 → (⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘𝑎) = (Λ ∘f · 𝐻))
131	130	oveq1d 7405	. . . . . . 7 ⊢ (𝑎 = 0 → ((⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘𝑎)vts𝑁) = ((Λ ∘f · 𝐻)vts𝑁))
132	131	fveq1d 6863	. . . . . 6 ⊢ (𝑎 = 0 → (((⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥) = (((Λ ∘f · 𝐻)vts𝑁)‘𝑥))
133	1	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → 𝑁 ∈ ℕ0)
134	17	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → (Λ ∘f · 𝐻):ℕ⟶ℂ)
135	133, 120, 134	vtscl 34636	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → (((Λ ∘f · 𝐻)vts𝑁)‘𝑥) ∈ ℂ)
136	103, 104, 106, 107, 114, 128, 132, 135	fprodsplitsn 15962	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → ∏𝑎 ∈ ((1..^3) ∪ {0})(((⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥) = (∏𝑎 ∈ (1..^3)(((⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥) · (((Λ ∘f · 𝐻)vts𝑁)‘𝑥)))
137		uncom 4124	. . . . . . . 8 ⊢ ((1..^3) ∪ {0}) = ({0} ∪ (1..^3))
138		fzo0sn0fzo1 13723	. . . . . . . . 9 ⊢ (3 ∈ ℕ → (0..^3) = ({0} ∪ (1..^3)))
139	2, 138	ax-mp 5	. . . . . . . 8 ⊢ (0..^3) = ({0} ∪ (1..^3))
140	137, 139	eqtr4i 2756	. . . . . . 7 ⊢ ((1..^3) ∪ {0}) = (0..^3)
141	140	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → ((1..^3) ∪ {0}) = (0..^3))
142	141	prodeq1d 15893	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → ∏𝑎 ∈ ((1..^3) ∪ {0})(((⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥) = ∏𝑎 ∈ (0..^3)(((⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥))
143		fzo13pr 13717	. . . . . . . . . . . . . . 15 ⊢ (1..^3) = {1, 2}
144	143	eleq2i 2821	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ (1..^3) ↔ 𝑎 ∈ {1, 2})
145		vex 3454	. . . . . . . . . . . . . . 15 ⊢ 𝑎 ∈ V
146	145	elpr 4617	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ {1, 2} ↔ (𝑎 = 1 ∨ 𝑎 = 2))
147	144, 146	bitri 275	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ (1..^3) ↔ (𝑎 = 1 ∨ 𝑎 = 2))
148	31	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑎 = 1) → (⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘𝑎) = (⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘1))
149	71, 72	mp1i 13	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑎 = 1) → (⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘1) = (Λ ∘f · 𝐾))
150	148, 149	eqtrd 2765	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 = 1) → (⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘𝑎) = (Λ ∘f · 𝐾))
151	34	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑎 = 2) → (⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘𝑎) = (⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘2))
152	71, 86	mp1i 13	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑎 = 2) → (⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘2) = (Λ ∘f · 𝐾))
153	151, 152	eqtrd 2765	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 = 2) → (⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘𝑎) = (Λ ∘f · 𝐾))
154	150, 153	jaodan 959	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 = 1 ∨ 𝑎 = 2)) → (⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘𝑎) = (Λ ∘f · 𝐾))
155	147, 154	sylan2b 594	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (1..^3)) → (⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘𝑎) = (Λ ∘f · 𝐾))
156	155	adantlr 715	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑎 ∈ (1..^3)) → (⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘𝑎) = (Λ ∘f · 𝐾))
157	156	oveq1d 7405	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑎 ∈ (1..^3)) → ((⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘𝑎)vts𝑁) = ((Λ ∘f · 𝐾)vts𝑁))
158	157	fveq1d 6863	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑎 ∈ (1..^3)) → (((⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥) = (((Λ ∘f · 𝐾)vts𝑁)‘𝑥))
159	158	prodeq2dv 15895	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → ∏𝑎 ∈ (1..^3)(((⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥) = ∏𝑎 ∈ (1..^3)(((Λ ∘f · 𝐾)vts𝑁)‘𝑥))
160	22	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → (Λ ∘f · 𝐾):ℕ⟶ℂ)
161	133, 120, 160	vtscl 34636	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → (((Λ ∘f · 𝐾)vts𝑁)‘𝑥) ∈ ℂ)
162		fprodconst 15951	. . . . . . . . 9 ⊢ (((1..^3) ∈ Fin ∧ (((Λ ∘f · 𝐾)vts𝑁)‘𝑥) ∈ ℂ) → ∏𝑎 ∈ (1..^3)(((Λ ∘f · 𝐾)vts𝑁)‘𝑥) = ((((Λ ∘f · 𝐾)vts𝑁)‘𝑥)↑(♯‘(1..^3))))
163	106, 161, 162	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → ∏𝑎 ∈ (1..^3)(((Λ ∘f · 𝐾)vts𝑁)‘𝑥) = ((((Λ ∘f · 𝐾)vts𝑁)‘𝑥)↑(♯‘(1..^3))))
164		nnuz 12843	. . . . . . . . . . . . 13 ⊢ ℕ = (ℤ≥‘1)
165	2, 164	eleqtri 2827	. . . . . . . . . . . 12 ⊢ 3 ∈ (ℤ≥‘1)
166		hashfzo 14401	. . . . . . . . . . . 12 ⊢ (3 ∈ (ℤ≥‘1) → (♯‘(1..^3)) = (3 − 1))
167	165, 166	ax-mp 5	. . . . . . . . . . 11 ⊢ (♯‘(1..^3)) = (3 − 1)
168		3m1e2 12316	. . . . . . . . . . 11 ⊢ (3 − 1) = 2
169	167, 168	eqtri 2753	. . . . . . . . . 10 ⊢ (♯‘(1..^3)) = 2
170	169	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → (♯‘(1..^3)) = 2)
171	170	oveq2d 7406	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → ((((Λ ∘f · 𝐾)vts𝑁)‘𝑥)↑(♯‘(1..^3))) = ((((Λ ∘f · 𝐾)vts𝑁)‘𝑥)↑2))
172	159, 163, 171	3eqtrd 2769	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → ∏𝑎 ∈ (1..^3)(((⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥) = ((((Λ ∘f · 𝐾)vts𝑁)‘𝑥)↑2))
173	172	oveq1d 7405	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → (∏𝑎 ∈ (1..^3)(((⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥) · (((Λ ∘f · 𝐻)vts𝑁)‘𝑥)) = (((((Λ ∘f · 𝐾)vts𝑁)‘𝑥)↑2) · (((Λ ∘f · 𝐻)vts𝑁)‘𝑥)))
174	161	sqcld 14116	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → ((((Λ ∘f · 𝐾)vts𝑁)‘𝑥)↑2) ∈ ℂ)
175	135, 174	mulcomd 11202	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → ((((Λ ∘f · 𝐻)vts𝑁)‘𝑥) · ((((Λ ∘f · 𝐾)vts𝑁)‘𝑥)↑2)) = (((((Λ ∘f · 𝐾)vts𝑁)‘𝑥)↑2) · (((Λ ∘f · 𝐻)vts𝑁)‘𝑥)))
176	173, 175	eqtr4d 2768	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → (∏𝑎 ∈ (1..^3)(((⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥) · (((Λ ∘f · 𝐻)vts𝑁)‘𝑥)) = ((((Λ ∘f · 𝐻)vts𝑁)‘𝑥) · ((((Λ ∘f · 𝐾)vts𝑁)‘𝑥)↑2)))
177	136, 142, 176	3eqtr3d 2773	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → ∏𝑎 ∈ (0..^3)(((⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥) = ((((Λ ∘f · 𝐻)vts𝑁)‘𝑥) · ((((Λ ∘f · 𝐾)vts𝑁)‘𝑥)↑2)))
178	177	oveq1d 7405	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → (∏𝑎 ∈ (0..^3)(((⟨“(Λ ∘f · 𝐻)(Λ ∘f · 𝐾)(Λ ∘f · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) = (((((Λ ∘f · 𝐻)vts𝑁)‘𝑥) · ((((Λ ∘f · 𝐾)vts𝑁)‘𝑥)↑2)) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))))
179	178	itgeq2dv 25690	. 2 ⊢ (𝜑 → ∫(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 2773	1 ⊢ (𝜑 → Σ𝑛 ∈ (ℕ(repr‘3)𝑁)(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) = ∫(0(,)1)(((((Λ ∘f · 𝐻)vts𝑁)‘𝑥) · ((((Λ ∘f · 𝐾)vts𝑁)‘𝑥)↑2)) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) d𝑥)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1540   ∈ wcel 2109  Vcvv 3450   ∪ cun 3915   ⊆ wss 3917  {csn 4592  {cpr 4594  {ctp 4596   Fn wfn 6509  ⟶wf 6510  ‘cfv 6514  (class class class)co 7390   ∘_f cof 7654   ↑_m cmap 8802  Fincfn 8921  ℂcc 11073  ℝcr 11074  0cc0 11075  1c1 11076  ici 11077   · cmul 11080   − cmin 11412  -cneg 11413  ℕcn 12193  2c2 12248  3c3 12249  ℕ₀cn0 12449  ℤcz 12536  ℤ_≥cuz 12800  (,)cioo 13313  ...cfz 13475  ..^cfzo 13622  ↑cexp 14033  ♯chash 14302  ⟨“cs3 14815  Σcsu 15659  ∏cprod 15876  expce 16034  πcpi 16039  ∫citg 25526  Λcvma 27009  reprcrepr 34606  vtscvts 34633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-inf2 9601  ax-cc 10395  ax-cnex 11131  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152  ax-pre-sup 11153  ax-addf 11154

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-symdif 4219  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-tp 4597  df-op 4599  df-uni 4875  df-int 4914  df-iun 4960  df-iin 4961  df-disj 5078  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-se 5595  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-isom 6523  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-of 7656  df-ofr 7657  df-om 7846  df-1st 7971  df-2nd 7972  df-supp 8143  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-1o 8437  df-2o 8438  df-oadd 8441  df-omul 8442  df-er 8674  df-map 8804  df-pm 8805  df-ixp 8874  df-en 8922  df-dom 8923  df-sdom 8924  df-fin 8925  df-fsupp 9320  df-fi 9369  df-sup 9400  df-inf 9401  df-oi 9470  df-dju 9861  df-card 9899  df-acn 9902  df-pnf 11217  df-mnf 11218  df-xr 11219  df-ltxr 11220  df-le 11221  df-sub 11414  df-neg 11415  df-div 11843  df-nn 12194  df-2 12256  df-3 12257  df-4 12258  df-5 12259  df-6 12260  df-7 12261  df-8 12262  df-9 12263  df-n0 12450  df-z 12537  df-dec 12657  df-uz 12801  df-q 12915  df-rp 12959  df-xneg 13079  df-xadd 13080  df-xmul 13081  df-ioo 13317  df-ioc 13318  df-ico 13319  df-icc 13320  df-fz 13476  df-fzo 13623  df-fl 13761  df-mod 13839  df-seq 13974  df-exp 14034  df-fac 14246  df-bc 14275  df-hash 14303  df-word 14486  df-concat 14543  df-s1 14568  df-s2 14821  df-s3 14822  df-shft 15040  df-cj 15072  df-re 15073  df-im 15074  df-sqrt 15208  df-abs 15209  df-limsup 15444  df-clim 15461  df-rlim 15462  df-sum 15660  df-prod 15877  df-ef 16040  df-sin 16042  df-cos 16043  df-pi 16045  df-dvds 16230  df-gcd 16472  df-prm 16649  df-pc 16815  df-struct 17124  df-sets 17141  df-slot 17159  df-ndx 17171  df-base 17187  df-ress 17208  df-plusg 17240  df-mulr 17241  df-starv 17242  df-sca 17243  df-vsca 17244  df-ip 17245  df-tset 17246  df-ple 17247  df-ds 17249  df-unif 17250  df-hom 17251  df-cco 17252  df-rest 17392  df-topn 17393  df-0g 17411  df-gsum 17412  df-topgen 17413  df-pt 17414  df-prds 17417  df-xrs 17472  df-qtop 17477  df-imas 17478  df-xps 17480  df-mre 17554  df-mrc 17555  df-acs 17557  df-mgm 18574  df-sgrp 18653  df-mnd 18669  df-submnd 18718  df-mulg 19007  df-cntz 19256  df-cmn 19719  df-psmet 21263  df-xmet 21264  df-met 21265  df-bl 21266  df-mopn 21267  df-fbas 21268  df-fg 21269  df-cnfld 21272  df-top 22788  df-topon 22805  df-topsp 22827  df-bases 22840  df-cld 22913  df-ntr 22914  df-cls 22915  df-nei 22992  df-lp 23030  df-perf 23031  df-cn 23121  df-cnp 23122  df-haus 23209  df-cmp 23281  df-tx 23456  df-hmeo 23649  df-fil 23740  df-fm 23832  df-flim 23833  df-flf 23834  df-xms 24215  df-ms 24216  df-tms 24217  df-cncf 24778  df-ovol 25372  df-vol 25373  df-mbf 25527  df-itg1 25528  df-itg2 25529  df-ibl 25530  df-itg 25531  df-0p 25578  df-limc 25774  df-dv 25775  df-log 26472  df-vma 27015  df-repr 34607  df-vts 34634

This theorem is referenced by:  tgoldbachgtde  34658