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	ffvelcdmda	$⊢ ((φ \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	ffvelcdmda	$⊢ ((φ \land n \in (ℕ repr (3) N)) \land a \in (0 ..^3)) \to n (a) \in ℕ$
49	40 48	ffvelcdmd	$⊢ ((φ \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	ffvelcdmd	$⊢ (φ \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		1eltp012	$⊢ 1 \in \{0, 1, 2\}$
76	75 58	eleqtrri	$⊢ 1 \in (0 ..^3)$
77	76	a1i	$⊢ (φ \land n \in (ℕ repr (3) N)) \to 1 \in (0 ..^3)$
78	47 77	ffvelcdmd	$⊢ (φ \land n \in (ℕ repr (3) N)) \to n (1) \in ℕ$
79	2	ffnd	$⊢ φ \to K Fn ℕ$
80		eqidd	$⊢ (φ \land n (1) \in ℕ) \to Λ (n (1)) = Λ (n (1))$
81		eqidd	$⊢ (φ \land n (1) \in ℕ) \to K (n (1)) = K (n (1))$
82	64 79 16 16 17 80 81	ofval	$⊢ (φ \land n (1) \in ℕ) \to (Λ \times_{f} K) (n (1)) = Λ (n (1)) K (n (1))$
83	55 78 82	syl2anc	$⊢ (φ \land n \in (ℕ repr (3) N)) \to (Λ \times_{f} K) (n (1)) = Λ (n (1)) K (n (1))$
84	74 83	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))$
85		s3fv2	$⊢ Λ \times_{f} K \in V \to ⟨“ (Λ \times_{f} H) (Λ \times_{f} K) (Λ \times_{f} K) ”⟩ (2) = Λ \times_{f} K$
86	71 85	mp1i	$⊢ (φ \land n \in (ℕ repr (3) N)) \to ⟨“ (Λ \times_{f} H) (Λ \times_{f} K) (Λ \times_{f} K) ”⟩ (2) = Λ \times_{f} K$
87	86	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))$
88		2ex	$⊢ 2 \in V$
89	88	tpid3	$⊢ 2 \in \{0, 1, 2\}$
90	89 58	eleqtrri	$⊢ 2 \in (0 ..^3)$
91	90	a1i	$⊢ (φ \land n \in (ℕ repr (3) N)) \to 2 \in (0 ..^3)$
92	47 91	ffvelcdmd	$⊢ (φ \land n \in (ℕ repr (3) N)) \to n (2) \in ℕ$
93		eqidd	$⊢ (φ \land n (2) \in ℕ) \to Λ (n (2)) = Λ (n (2))$
94		eqidd	$⊢ (φ \land n (2) \in ℕ) \to K (n (2)) = K (n (2))$
95	64 79 16 16 17 93 94	ofval	$⊢ (φ \land n (2) \in ℕ) \to (Λ \times_{f} K) (n (2)) = Λ (n (2)) K (n (2))$
96	55 92 95	syl2anc	$⊢ (φ \land n \in (ℕ repr (3) N)) \to (Λ \times_{f} K) (n (2)) = Λ (n (2)) K (n (2))$
97	87 96	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))$
98	84 97	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))$
99	70 98	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))$
100	50 99	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))$
101	100	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))$
102		nfv	$⊢ Ⅎ a (φ \land x \in (0, 1))$
103		nfcv	$⊢ \underline{Ⅎ} a ((Λ \times_{f} H) vts N) (x)$
104		fzofi	$⊢ (1 ..^3) \in Fin$
105	104	a1i	$⊢ (φ \land x \in (0, 1)) \to (1 ..^3) \in Fin$
106	56	a1i	$⊢ (φ \land x \in (0, 1)) \to 0 \in V$
107		eqid	$⊢ 0 = 0$
108	107	orci	$⊢ (0 = 0 \lor 0 = 3)$
109		0elfz	$⊢ 3 \in ℕ_{0} \to 0 \in (0 \dots 3)$
110		elfznelfzob	$⊢ 0 \in (0 \dots 3) \to (\neg 0 \in (1 ..^3) \leftrightarrow (0 = 0 \lor 0 = 3))$
111	44 109 110	mp2b	$⊢ \neg 0 \in (1 ..^3) \leftrightarrow (0 = 0 \lor 0 = 3)$
112	108 111	mpbir	$⊢ \neg 0 \in (1 ..^3)$
113	112	a1i	$⊢ (φ \land x \in (0, 1)) \to \neg 0 \in (1 ..^3)$
114	3	ad2antrr	$⊢ ((φ \land x \in (0, 1)) \land a \in (1 ..^3)) \to N \in ℕ_{0}$
115		ioossre	$⊢ (0, 1) \subseteq ℝ$
116		ax-resscn	$⊢ ℝ \subseteq ℂ$
117	115 116	sstri	$⊢ (0, 1) \subseteq ℂ$
118	117	a1i	$⊢ φ \to (0, 1) \subseteq ℂ$
119	118	sselda	$⊢ (φ \land x \in (0, 1)) \to x \in ℂ$
120	119	adantr	$⊢ ((φ \land x \in (0, 1)) \land a \in (1 ..^3)) \to x \in ℂ$
121	26	ad2antrr	$⊢ ((φ \land x \in (0, 1)) \land a \in (1 ..^3)) \to ⟨“ (Λ \times_{f} H) (Λ \times_{f} K) (Λ \times_{f} K) ”⟩ : (0 ..^3) ⟶ ℂ^{ℕ}$
122		fzo0ss1	$⊢ (1 ..^3) \subseteq (0 ..^3)$
123	122	a1i	$⊢ (φ \land x \in (0, 1)) \to (1 ..^3) \subseteq (0 ..^3)$
124	123	sselda	$⊢ ((φ \land x \in (0, 1)) \land a \in (1 ..^3)) \to a \in (0 ..^3)$
125	121 124	ffvelcdmd	$⊢ ((φ \land x \in (0, 1)) \land a \in (1 ..^3)) \to ⟨“ (Λ \times_{f} H) (Λ \times_{f} K) (Λ \times_{f} K) ”⟩ (a) \in (ℂ^{ℕ})$
126	125 39	syl	$⊢ ((φ \land x \in (0, 1)) \land a \in (1 ..^3)) \to ⟨“ (Λ \times_{f} H) (Λ \times_{f} K) (Λ \times_{f} K) ”⟩ (a) : ℕ ⟶ ℂ$
127	114 120 126	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 ℂ$
128	51 52	ax-mp	$⊢ ⟨“ (Λ \times_{f} H) (Λ \times_{f} K) (Λ \times_{f} K) ”⟩ (0) = Λ \times_{f} H$
129	28 128	eqtrdi	$⊢ a = 0 \to ⟨“ (Λ \times_{f} H) (Λ \times_{f} K) (Λ \times_{f} K) ”⟩ (a) = Λ \times_{f} H$
130	129	oveq1d	$⊢ a = 0 \to ⟨“ (Λ \times_{f} H) (Λ \times_{f} K) (Λ \times_{f} K) ”⟩ (a) vts N = (Λ \times_{f} H) vts N$
131	130	fveq1d	$⊢ a = 0 \to (⟨“ (Λ \times_{f} H) (Λ \times_{f} K) (Λ \times_{f} K) ”⟩ (a) vts N) (x) = ((Λ \times_{f} H) vts N) (x)$
132	3	adantr	$⊢ (φ \land x \in (0, 1)) \to N \in ℕ_{0}$
133	18	adantr	$⊢ (φ \land x \in (0, 1)) \to (Λ \times_{f} H) : ℕ ⟶ ℂ$
134	132 119 133	vtscl	$⊢ (φ \land x \in (0, 1)) \to ((Λ \times_{f} H) vts N) (x) \in ℂ$
135	102 103 105 106 113 127 131 134	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)$
136		uncom	$⊢ (1 ..^3) \cup \{0\} = \{0\} \cup (1 ..^3)$
137		fzo0sn0fzo1	$⊢ 3 \in ℕ \to (0 ..^3) = \{0\} \cup (1 ..^3)$
138	4 137	ax-mp	$⊢ (0 ..^3) = \{0\} \cup (1 ..^3)$
139	136 138	eqtr4i	$⊢ (1 ..^3) \cup \{0\} = (0 ..^3)$
140	139	a1i	$⊢ (φ \land x \in (0, 1)) \to (1 ..^3) \cup \{0\} = (0 ..^3)$
141	140	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)$
142		fzo13pr	$⊢ (1 ..^3) = \{1, 2\}$
143	142	eleq2i	$⊢ a \in (1 ..^3) \leftrightarrow a \in \{1, 2\}$
144		vex	$⊢ a \in V$
145	144	elpr	$⊢ a \in \{1, 2\} \leftrightarrow (a = 1 \lor a = 2)$
146	143 145	bitri	$⊢ a \in (1 ..^3) \leftrightarrow (a = 1 \lor a = 2)$
147	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)$
148	71 72	mp1i	$⊢ (φ \land a = 1) \to ⟨“ (Λ \times_{f} H) (Λ \times_{f} K) (Λ \times_{f} K) ”⟩ (1) = Λ \times_{f} K$
149	147 148	eqtrd	$⊢ (φ \land a = 1) \to ⟨“ (Λ \times_{f} H) (Λ \times_{f} K) (Λ \times_{f} K) ”⟩ (a) = Λ \times_{f} K$
150	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)$
151	71 85	mp1i	$⊢ (φ \land a = 2) \to ⟨“ (Λ \times_{f} H) (Λ \times_{f} K) (Λ \times_{f} K) ”⟩ (2) = Λ \times_{f} K$
152	150 151	eqtrd	$⊢ (φ \land a = 2) \to ⟨“ (Λ \times_{f} H) (Λ \times_{f} K) (Λ \times_{f} K) ”⟩ (a) = Λ \times_{f} K$
153	149 152	jaodan	$⊢ (φ \land (a = 1 \lor a = 2)) \to ⟨“ (Λ \times_{f} H) (Λ \times_{f} K) (Λ \times_{f} K) ”⟩ (a) = Λ \times_{f} K$
154	146 153	sylan2b	$⊢ (φ \land a \in (1 ..^3)) \to ⟨“ (Λ \times_{f} H) (Λ \times_{f} K) (Λ \times_{f} K) ”⟩ (a) = Λ \times_{f} K$
155	154	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$
156	155	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$
157	156	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)$
158	157	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)$
159	22	adantr	$⊢ (φ \land x \in (0, 1)) \to (Λ \times_{f} K) : ℕ ⟶ ℂ$
160	132 119 159	vtscl	$⊢ (φ \land x \in (0, 1)) \to ((Λ \times_{f} K) vts N) (x) \in ℂ$
161		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)\|}$
162	105 160 161	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)\|}$
163		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
164	4 163	eleqtri	$⊢ 3 \in ℤ_{\geq 1}$
165		hashfzo	$⊢ 3 \in ℤ_{\geq 1} \to \|(1 ..^3)\| = 3 - 1$
166	164 165	ax-mp	$⊢ \|(1 ..^3)\| = 3 - 1$
167		3m1e2	$⊢ 3 - 1 = 2$
168	166 167	eqtri	$⊢ \|(1 ..^3)\| = 2$
169	168	a1i	$⊢ (φ \land x \in (0, 1)) \to \|(1 ..^3)\| = 2$
170	169	oveq2d	$⊢ (φ \land x \in (0, 1)) \to {((Λ \times_{f} K) vts N) (x)}^{\|(1 ..^3)\|} = {((Λ \times_{f} K) vts N) (x)}^{2}$
171	158 162 170	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}$
172	171	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)$
173	160	sqcld	$⊢ (φ \land x \in (0, 1)) \to {((Λ \times_{f} K) vts N) (x)}^{2} \in ℂ$
174	134 173	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)$
175	172 174	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}$
176	135 141 175	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}$
177	176	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}$
178	177	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$
179	27 101 178	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