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	$⊢ φ \to H : ℕ ⟶ ℝ$
	circlemethhgt.k	$⊢ φ \to K : ℕ ⟶ ℝ$
	circlemethhgt.n	$⊢ φ \to N \in ℕ_{0}$
Assertion	circlemethhgt	$⊢ φ \to \sum_{n \in ℕ repr (3) N} Λ (n (0)) H (n (0)) Λ (n (1)) K (n (1)) Λ (n (2)) K (n (2)) = \int_{(0, 1)} ((Λ \times_{f} H) vts N) (x) {((Λ \times_{f} K) vts N) (x)}^{2} e^{i 2 π -N x} d x$

Proof

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

Metamath Proof Explorer

Theorem circlemethhgt

Proof