fourierdlem111

Description: The fourier partial sum for F is the sum of two integrals, with the same integrand involving F and the Dirichlet Kernel D , but on two opposite intervals. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem111.a	$⊢ A = (n \in ℕ_{0} ⟼ \frac{\int_{(- π, π)} F (t) \cos n t d t}{π})$
	fourierdlem111.b	$⊢ B = (n \in ℕ ⟼ \frac{\int_{(- π, π)} F (t) \sin n t d t}{π})$
	fourierdlem111.s	$⊢ S = (m \in ℕ ⟼ (\frac{A (0)}{2}) + \sum_{n = 1}^{m} (A (n) \cos n X + B (n) \sin n X))$
	fourierdlem111.d	$⊢ D = (n \in ℕ ⟼ (y \in ℝ ⟼ if (y \mod 2 π = 0, \frac{2 n + 1}{2 π}, \frac{\sin (n + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})})))$
	fourierdlem111.p	$⊢ P = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = - π \land p (m) = π) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
	fourierdlem111.m	$⊢ φ \to M \in ℕ$
	fourierdlem111.q	$⊢ φ \to Q \in P (M)$
	fourierdlem111.x	$⊢ φ \to X \in ℝ$
	fourierdlem111.6	$⊢ φ \to F : ℝ ⟶ ℝ$
	fourierdlem111.fper	$⊢ (φ \land x \in ℝ) \to F (x + T) = F (x)$
	fourierdlem111.g	$⊢ G = (x \in ℝ ⟼ F (X + x) D (n) (x))$
	fourierdlem111.fcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
	fourierdlem111.r	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
	fourierdlem111.l	$⊢ (φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
	fourierdlem111.t	$⊢ T = 2 π$
	fourierdlem111.o	$⊢ O = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = - π - X \land p (m) = π - X) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
	fourierdlem111.14	$⊢ W = (i \in (0 \dots M) ⟼ Q (i) - X)$
Assertion	fourierdlem111	$⊢ (φ \land n \in ℕ) \to S (n) = \int_{(- π, 0)} F (X + s) D (n) (s) d s + \int_{(0, π)} F (X + s) D (n) (s) d s$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem111.a	$⊢ A = (n \in ℕ_{0} ⟼ \frac{\int_{(- π, π)} F (t) \cos n t d t}{π})$
2		fourierdlem111.b	$⊢ B = (n \in ℕ ⟼ \frac{\int_{(- π, π)} F (t) \sin n t d t}{π})$
3		fourierdlem111.s	$⊢ S = (m \in ℕ ⟼ (\frac{A (0)}{2}) + \sum_{n = 1}^{m} (A (n) \cos n X + B (n) \sin n X))$
4		fourierdlem111.d	$⊢ D = (n \in ℕ ⟼ (y \in ℝ ⟼ if (y \mod 2 π = 0, \frac{2 n + 1}{2 π}, \frac{\sin (n + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})})))$
5		fourierdlem111.p	$⊢ P = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = - π \land p (m) = π) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
6		fourierdlem111.m	$⊢ φ \to M \in ℕ$
7		fourierdlem111.q	$⊢ φ \to Q \in P (M)$
8		fourierdlem111.x	$⊢ φ \to X \in ℝ$
9		fourierdlem111.6	$⊢ φ \to F : ℝ ⟶ ℝ$
10		fourierdlem111.fper	$⊢ (φ \land x \in ℝ) \to F (x + T) = F (x)$
11		fourierdlem111.g	$⊢ G = (x \in ℝ ⟼ F (X + x) D (n) (x))$
12		fourierdlem111.fcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
13		fourierdlem111.r	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
14		fourierdlem111.l	$⊢ (φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
15		fourierdlem111.t	$⊢ T = 2 π$
16		fourierdlem111.o	$⊢ O = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = - π - X \land p (m) = π - X) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
17		fourierdlem111.14	$⊢ W = (i \in (0 \dots M) ⟼ Q (i) - X)$
18		eleq1	$⊢ k = n \to (k \in ℕ \leftrightarrow n \in ℕ)$
19	18	anbi2d	$⊢ k = n \to ((φ \land k \in ℕ) \leftrightarrow (φ \land n \in ℕ))$
20		fveq2	$⊢ k = n \to S (k) = S (n)$
21		fveq2	$⊢ k = n \to D (k) = D (n)$
22	21	fveq1d	$⊢ k = n \to D (k) (t - X) = D (n) (t - X)$
23	22	oveq2d	$⊢ k = n \to F (t) D (k) (t - X) = F (t) D (n) (t - X)$
24	23	adantr	$⊢ (k = n \land t \in (- π, π)) \to F (t) D (k) (t - X) = F (t) D (n) (t - X)$
25	24	itgeq2dv	$⊢ k = n \to \int_{(- π, π)} F (t) D (k) (t - X) d t = \int_{(- π, π)} F (t) D (n) (t - X) d t$
26	20 25	eqeq12d	$⊢ k = n \to (S (k) = \int_{(- π, π)} F (t) D (k) (t - X) d t \leftrightarrow S (n) = \int_{(- π, π)} F (t) D (n) (t - X) d t)$
27	19 26	imbi12d	$⊢ k = n \to (((φ \land k \in ℕ) \to S (k) = \int_{(- π, π)} F (t) D (k) (t - X) d t) \leftrightarrow ((φ \land n \in ℕ) \to S (n) = \int_{(- π, π)} F (t) D (n) (t - X) d t))$
28	9	adantr	$⊢ (φ \land k \in ℕ) \to F : ℝ ⟶ ℝ$
29		eqid	$⊢ (- π, π) = (- π, π)$
30		ioossre	$⊢ (- π, π) \subseteq ℝ$
31	30	a1i	$⊢ φ \to (- π, π) \subseteq ℝ$
32	9 31	feqresmpt	$⊢ φ \to {F ↾}_{(- π, π)} = (x \in (- π, π) ⟼ F (x))$
33		ioossicc	$⊢ (- π, π) \subseteq [- π, π]$
34	33	a1i	$⊢ φ \to (- π, π) \subseteq [- π, π]$
35		ioombl	$⊢ (- π, π) \in dom vol$
36	35	a1i	$⊢ φ \to (- π, π) \in dom vol$
37	9	adantr	$⊢ (φ \land x \in [- π, π]) \to F : ℝ ⟶ ℝ$
38		pire	$⊢ π \in ℝ$
39	38	renegcli	$⊢ - π \in ℝ$
40	39 38	elicc2i	$⊢ t \in [- π, π] \leftrightarrow (t \in ℝ \land - π \leq t \land t \leq π)$
41	40	simp1bi	$⊢ t \in [- π, π] \to t \in ℝ$
42	41	ssriv	$⊢ [- π, π] \subseteq ℝ$
43	42	a1i	$⊢ φ \to [- π, π] \subseteq ℝ$
44	43	sselda	$⊢ (φ \land x \in [- π, π]) \to x \in ℝ$
45	37 44	ffvelrnd	$⊢ (φ \land x \in [- π, π]) \to F (x) \in ℝ$
46	9 43	feqresmpt	$⊢ φ \to {F ↾}_{[- π, π]} = (x \in [- π, π] ⟼ F (x))$
47		ax-resscn	$⊢ ℝ \subseteq ℂ$
48	47	a1i	$⊢ φ \to ℝ \subseteq ℂ$
49	9 48	fssd	$⊢ φ \to F : ℝ ⟶ ℂ$
50	49 43	fssresd	$⊢ φ \to ({F ↾}_{[- π, π]}) : [- π, π] ⟶ ℂ$
51		ioossicc	$⊢ (Q (i), Q (i + 1)) \subseteq [Q (i), Q (i + 1)]$
52	39	rexri	$⊢ - π \in ℝ^{*}$
53	52	a1i	$⊢ (φ \land i \in (0 ..^M)) \to - π \in ℝ^{*}$
54	38	rexri	$⊢ π \in ℝ^{*}$
55	54	a1i	$⊢ (φ \land i \in (0 ..^M)) \to π \in ℝ^{*}$
56	5 6 7	fourierdlem15	$⊢ φ \to Q : (0 \dots M) ⟶ [- π, π]$
57	56	adantr	$⊢ (φ \land i \in (0 ..^M)) \to Q : (0 \dots M) ⟶ [- π, π]$
58		simpr	$⊢ (φ \land i \in (0 ..^M)) \to i \in (0 ..^M)$
59	53 55 57 58	fourierdlem8	$⊢ (φ \land i \in (0 ..^M)) \to [Q (i), Q (i + 1)] \subseteq [- π, π]$
60	51 59	sstrid	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq [- π, π]$
61	60	resabs1d	$⊢ (φ \land i \in (0 ..^M)) \to {({F ↾}_{[- π, π]}) ↾}_{(Q (i), Q (i + 1))} = {F ↾}_{(Q (i), Q (i + 1))}$
62	61 12	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to ({({F ↾}_{[- π, π]}) ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
63	61	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to ({({F ↾}_{[- π, π]}) ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i) = ({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i)$
64	13 63	eleqtrrd	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({({F ↾}_{[- π, π]}) ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
65	61	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to ({({F ↾}_{[- π, π]}) ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1) = ({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1)$
66	14 65	eleqtrrd	$⊢ (φ \land i \in (0 ..^M)) \to L \in (({({F ↾}_{[- π, π]}) ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
67	5 6 7 50 62 64 66	fourierdlem69	$⊢ φ \to {F ↾}_{[- π, π]} \in 𝐿^{1}$
68	46 67	eqeltrrd	$⊢ φ \to (x \in [- π, π] ⟼ F (x)) \in 𝐿^{1}$
69	34 36 45 68	iblss	$⊢ φ \to (x \in (- π, π) ⟼ F (x)) \in 𝐿^{1}$
70	32 69	eqeltrd	$⊢ φ \to {F ↾}_{(- π, π)} \in 𝐿^{1}$
71	70	adantr	$⊢ (φ \land k \in ℕ) \to {F ↾}_{(- π, π)} \in 𝐿^{1}$
72	8	adantr	$⊢ (φ \land k \in ℕ) \to X \in ℝ$
73		simpr	$⊢ (φ \land k \in ℕ) \to k \in ℕ$
74	28 29 71 1 2 72 3 4 73	fourierdlem83	$⊢ (φ \land k \in ℕ) \to S (k) = \int_{(- π, π)} F (t) D (k) (t - X) d t$
75	27 74	chvarvv	$⊢ (φ \land n \in ℕ) \to S (n) = \int_{(- π, π)} F (t) D (n) (t - X) d t$
76	39	a1i	$⊢ (φ \land n \in ℕ) \to - π \in ℝ$
77	38	a1i	$⊢ (φ \land n \in ℕ) \to π \in ℝ$
78	49	adantr	$⊢ (φ \land t \in [- π, π]) \to F : ℝ ⟶ ℂ$
79	41	adantl	$⊢ (φ \land t \in [- π, π]) \to t \in ℝ$
80	78 79	ffvelrnd	$⊢ (φ \land t \in [- π, π]) \to F (t) \in ℂ$
81	80	adantlr	$⊢ ((φ \land n \in ℕ) \land t \in [- π, π]) \to F (t) \in ℂ$
82	4	dirkerf	$⊢ n \in ℕ \to D (n) : ℝ ⟶ ℝ$
83	82	ad2antlr	$⊢ ((φ \land n \in ℕ) \land t \in [- π, π]) \to D (n) : ℝ ⟶ ℝ$
84	8	adantr	$⊢ (φ \land t \in [- π, π]) \to X \in ℝ$
85	79 84	resubcld	$⊢ (φ \land t \in [- π, π]) \to t - X \in ℝ$
86	85	adantlr	$⊢ ((φ \land n \in ℕ) \land t \in [- π, π]) \to t - X \in ℝ$
87	83 86	ffvelrnd	$⊢ ((φ \land n \in ℕ) \land t \in [- π, π]) \to D (n) (t - X) \in ℝ$
88	87	recnd	$⊢ ((φ \land n \in ℕ) \land t \in [- π, π]) \to D (n) (t - X) \in ℂ$
89	81 88	mulcld	$⊢ ((φ \land n \in ℕ) \land t \in [- π, π]) \to F (t) D (n) (t - X) \in ℂ$
90	76 77 89	itgioo	$⊢ (φ \land n \in ℕ) \to \int_{(- π, π)} F (t) D (n) (t - X) d t = \int_{[- π, π]} F (t) D (n) (t - X) d t$
91		fvres	$⊢ t \in [- π, π] \to ({F ↾}_{[- π, π]}) (t) = F (t)$
92	91	eqcomd	$⊢ t \in [- π, π] \to F (t) = ({F ↾}_{[- π, π]}) (t)$
93	92	oveq1d	$⊢ t \in [- π, π] \to F (t) D (n) (t - X) = ({F ↾}_{[- π, π]}) (t) D (n) (t - X)$
94	93	adantl	$⊢ ((φ \land n \in ℕ) \land t \in [- π, π]) \to F (t) D (n) (t - X) = ({F ↾}_{[- π, π]}) (t) D (n) (t - X)$
95	94	itgeq2dv	$⊢ (φ \land n \in ℕ) \to \int_{[- π, π]} F (t) D (n) (t - X) d t = \int_{[- π, π]} ({F ↾}_{[- π, π]}) (t) D (n) (t - X) d t$
96		simpl	$⊢ (n = m \land y \in ℝ) \to n = m$
97	96	oveq2d	$⊢ (n = m \land y \in ℝ) \to 2 n = 2 m$
98	97	oveq1d	$⊢ (n = m \land y \in ℝ) \to 2 n + 1 = 2 m + 1$
99	98	oveq1d	$⊢ (n = m \land y \in ℝ) \to \frac{2 n + 1}{2 π} = \frac{2 m + 1}{2 π}$
100	96	oveq1d	$⊢ (n = m \land y \in ℝ) \to n + (\frac{1}{2}) = m + (\frac{1}{2})$
101	100	oveq1d	$⊢ (n = m \land y \in ℝ) \to (n + (\frac{1}{2})) y = (m + (\frac{1}{2})) y$
102	101	fveq2d	$⊢ (n = m \land y \in ℝ) \to \sin (n + (\frac{1}{2})) y = \sin (m + (\frac{1}{2})) y$
103	102	oveq1d	$⊢ (n = m \land y \in ℝ) \to \frac{\sin (n + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})} = \frac{\sin (m + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})}$
104	99 103	ifeq12d	$⊢ (n = m \land y \in ℝ) \to if (y \mod 2 π = 0, \frac{2 n + 1}{2 π}, \frac{\sin (n + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})}) = if (y \mod 2 π = 0, \frac{2 m + 1}{2 π}, \frac{\sin (m + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})})$
105	104	mpteq2dva	$⊢ n = m \to (y \in ℝ ⟼ if (y \mod 2 π = 0, \frac{2 n + 1}{2 π}, \frac{\sin (n + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})})) = (y \in ℝ ⟼ if (y \mod 2 π = 0, \frac{2 m + 1}{2 π}, \frac{\sin (m + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})}))$
106	105	cbvmptv	$⊢ (n \in ℕ ⟼ (y \in ℝ ⟼ if (y \mod 2 π = 0, \frac{2 n + 1}{2 π}, \frac{\sin (n + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})}))) = (m \in ℕ ⟼ (y \in ℝ ⟼ if (y \mod 2 π = 0, \frac{2 m + 1}{2 π}, \frac{\sin (m + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})})))$
107	4 106	eqtri	$⊢ D = (m \in ℕ ⟼ (y \in ℝ ⟼ if (y \mod 2 π = 0, \frac{2 m + 1}{2 π}, \frac{\sin (m + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})})))$
108		fveq2	$⊢ s = t \to ({F ↾}_{[- π, π]}) (s) = ({F ↾}_{[- π, π]}) (t)$
109		oveq1	$⊢ s = t \to s - X = t - X$
110	109	fveq2d	$⊢ s = t \to D (n) (s - X) = D (n) (t - X)$
111	108 110	oveq12d	$⊢ s = t \to ({F ↾}_{[- π, π]}) (s) D (n) (s - X) = ({F ↾}_{[- π, π]}) (t) D (n) (t - X)$
112	111	cbvmptv	$⊢ (s \in [- π, π] ⟼ ({F ↾}_{[- π, π]}) (s) D (n) (s - X)) = (t \in [- π, π] ⟼ ({F ↾}_{[- π, π]}) (t) D (n) (t - X))$
113	7	adantr	$⊢ (φ \land n \in ℕ) \to Q \in P (M)$
114	6	adantr	$⊢ (φ \land n \in ℕ) \to M \in ℕ$
115		simpr	$⊢ (φ \land n \in ℕ) \to n \in ℕ$
116	8	adantr	$⊢ (φ \land n \in ℕ) \to X \in ℝ$
117	50	adantr	$⊢ (φ \land n \in ℕ) \to ({F ↾}_{[- π, π]}) : [- π, π] ⟶ ℂ$
118	62	adantlr	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to ({({F ↾}_{[- π, π]}) ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
119	64	adantlr	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to R \in (({({F ↾}_{[- π, π]}) ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
120	66	adantlr	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to L \in (({({F ↾}_{[- π, π]}) ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
121	107 5 112 113 114 115 116 117 118 119 120	fourierdlem101	$⊢ (φ \land n \in ℕ) \to \int_{[- π, π]} ({F ↾}_{[- π, π]}) (t) D (n) (t - X) d t = \int_{[- π - X, π - X]} ({F ↾}_{[- π, π]}) (X + y) D (n) (y) d y$
122		oveq2	$⊢ s = y \to X + s = X + y$
123	122	fveq2d	$⊢ s = y \to F (X + s) = F (X + y)$
124		fveq2	$⊢ s = y \to D (n) (s) = D (n) (y)$
125	123 124	oveq12d	$⊢ s = y \to F (X + s) D (n) (s) = F (X + y) D (n) (y)$
126	125	cbvitgv	$⊢ \int_{(- π - X, π - X)} F (X + s) D (n) (s) d s = \int_{(- π - X, π - X)} F (X + y) D (n) (y) d y$
127	126	a1i	$⊢ (φ \land n \in ℕ) \to \int_{(- π - X, π - X)} F (X + s) D (n) (s) d s = \int_{(- π - X, π - X)} F (X + y) D (n) (y) d y$
128	39	a1i	$⊢ φ \to - π \in ℝ$
129	128 8	resubcld	$⊢ φ \to - π - X \in ℝ$
130	129	adantr	$⊢ (φ \land n \in ℕ) \to - π - X \in ℝ$
131	38	a1i	$⊢ φ \to π \in ℝ$
132	131 8	resubcld	$⊢ φ \to π - X \in ℝ$
133	132	adantr	$⊢ (φ \land n \in ℕ) \to π - X \in ℝ$
134	49	adantr	$⊢ (φ \land y \in [- π - X, π - X]) \to F : ℝ ⟶ ℂ$
135	8	adantr	$⊢ (φ \land y \in [- π - X, π - X]) \to X \in ℝ$
136		simpr	$⊢ (φ \land y \in [- π - X, π - X]) \to y \in [- π - X, π - X]$
137	129	adantr	$⊢ (φ \land y \in [- π - X, π - X]) \to - π - X \in ℝ$
138	132	adantr	$⊢ (φ \land y \in [- π - X, π - X]) \to π - X \in ℝ$
139		elicc2	$⊢ (- π - X \in ℝ \land π - X \in ℝ) \to (y \in [- π - X, π - X] \leftrightarrow (y \in ℝ \land - π - X \leq y \land y \leq π - X))$
140	137 138 139	syl2anc	$⊢ (φ \land y \in [- π - X, π - X]) \to (y \in [- π - X, π - X] \leftrightarrow (y \in ℝ \land - π - X \leq y \land y \leq π - X))$
141	136 140	mpbid	$⊢ (φ \land y \in [- π - X, π - X]) \to (y \in ℝ \land - π - X \leq y \land y \leq π - X)$
142	141	simp1d	$⊢ (φ \land y \in [- π - X, π - X]) \to y \in ℝ$
143	135 142	readdcld	$⊢ (φ \land y \in [- π - X, π - X]) \to X + y \in ℝ$
144	134 143	ffvelrnd	$⊢ (φ \land y \in [- π - X, π - X]) \to F (X + y) \in ℂ$
145	144	adantlr	$⊢ ((φ \land n \in ℕ) \land y \in [- π - X, π - X]) \to F (X + y) \in ℂ$
146	82	ad2antlr	$⊢ ((φ \land n \in ℕ) \land y \in [- π - X, π - X]) \to D (n) : ℝ ⟶ ℝ$
147	142	adantlr	$⊢ ((φ \land n \in ℕ) \land y \in [- π - X, π - X]) \to y \in ℝ$
148	146 147	ffvelrnd	$⊢ ((φ \land n \in ℕ) \land y \in [- π - X, π - X]) \to D (n) (y) \in ℝ$
149	148	recnd	$⊢ ((φ \land n \in ℕ) \land y \in [- π - X, π - X]) \to D (n) (y) \in ℂ$
150	145 149	mulcld	$⊢ ((φ \land n \in ℕ) \land y \in [- π - X, π - X]) \to F (X + y) D (n) (y) \in ℂ$
151	130 133 150	itgioo	$⊢ (φ \land n \in ℕ) \to \int_{(- π - X, π - X)} F (X + y) D (n) (y) d y = \int_{[- π - X, π - X]} F (X + y) D (n) (y) d y$
152	39	a1i	$⊢ (φ \land y \in [- π - X, π - X]) \to - π \in ℝ$
153	38	a1i	$⊢ (φ \land y \in [- π - X, π - X]) \to π \in ℝ$
154	8	recnd	$⊢ φ \to X \in ℂ$
155	131	recnd	$⊢ φ \to π \in ℂ$
156	155	negcld	$⊢ φ \to - π \in ℂ$
157	154 156	pncan3d	$⊢ φ \to X + (- π) - X = - π$
158	157	eqcomd	$⊢ φ \to - π = X + (- π) - X$
159	158	adantr	$⊢ (φ \land y \in [- π - X, π - X]) \to - π = X + (- π) - X$
160	141	simp2d	$⊢ (φ \land y \in [- π - X, π - X]) \to - π - X \leq y$
161	137 142 135 160	leadd2dd	$⊢ (φ \land y \in [- π - X, π - X]) \to X + (- π) - X \leq X + y$
162	159 161	eqbrtrd	$⊢ (φ \land y \in [- π - X, π - X]) \to - π \leq X + y$
163	141	simp3d	$⊢ (φ \land y \in [- π - X, π - X]) \to y \leq π - X$
164	142 138 135 163	leadd2dd	$⊢ (φ \land y \in [- π - X, π - X]) \to X + y \leq X + π - X$
165	154	adantr	$⊢ (φ \land y \in [- π - X, π - X]) \to X \in ℂ$
166	155	adantr	$⊢ (φ \land y \in [- π - X, π - X]) \to π \in ℂ$
167	165 166	pncan3d	$⊢ (φ \land y \in [- π - X, π - X]) \to X + π - X = π$
168	164 167	breqtrd	$⊢ (φ \land y \in [- π - X, π - X]) \to X + y \leq π$
169	152 153 143 162 168	eliccd	$⊢ (φ \land y \in [- π - X, π - X]) \to X + y \in [- π, π]$
170		fvres	$⊢ X + y \in [- π, π] \to ({F ↾}_{[- π, π]}) (X + y) = F (X + y)$
171	169 170	syl	$⊢ (φ \land y \in [- π - X, π - X]) \to ({F ↾}_{[- π, π]}) (X + y) = F (X + y)$
172	171	eqcomd	$⊢ (φ \land y \in [- π - X, π - X]) \to F (X + y) = ({F ↾}_{[- π, π]}) (X + y)$
173	172	adantlr	$⊢ ((φ \land n \in ℕ) \land y \in [- π - X, π - X]) \to F (X + y) = ({F ↾}_{[- π, π]}) (X + y)$
174	173	oveq1d	$⊢ ((φ \land n \in ℕ) \land y \in [- π - X, π - X]) \to F (X + y) D (n) (y) = ({F ↾}_{[- π, π]}) (X + y) D (n) (y)$
175	174	itgeq2dv	$⊢ (φ \land n \in ℕ) \to \int_{[- π - X, π - X]} F (X + y) D (n) (y) d y = \int_{[- π - X, π - X]} ({F ↾}_{[- π, π]}) (X + y) D (n) (y) d y$
176	127 151 175	3eqtrrd	$⊢ (φ \land n \in ℕ) \to \int_{[- π - X, π - X]} ({F ↾}_{[- π, π]}) (X + y) D (n) (y) d y = \int_{(- π - X, π - X)} F (X + s) D (n) (s) d s$
177	121 176	eqtrd	$⊢ (φ \land n \in ℕ) \to \int_{[- π, π]} ({F ↾}_{[- π, π]}) (t) D (n) (t - X) d t = \int_{(- π - X, π - X)} F (X + s) D (n) (s) d s$
178	90 95 177	3eqtrd	$⊢ (φ \land n \in ℕ) \to \int_{(- π, π)} F (t) D (n) (t - X) d t = \int_{(- π - X, π - X)} F (X + s) D (n) (s) d s$
179		elioore	$⊢ s \in (- π - X, π - X) \to s \in ℝ$
180	179	adantl	$⊢ ((φ \land n \in ℕ) \land s \in (- π - X, π - X)) \to s \in ℝ$
181	49	adantr	$⊢ (φ \land s \in (- π - X, π - X)) \to F : ℝ ⟶ ℂ$
182	8	adantr	$⊢ (φ \land s \in (- π - X, π - X)) \to X \in ℝ$
183	179	adantl	$⊢ (φ \land s \in (- π - X, π - X)) \to s \in ℝ$
184	182 183	readdcld	$⊢ (φ \land s \in (- π - X, π - X)) \to X + s \in ℝ$
185	181 184	ffvelrnd	$⊢ (φ \land s \in (- π - X, π - X)) \to F (X + s) \in ℂ$
186	185	adantlr	$⊢ ((φ \land n \in ℕ) \land s \in (- π - X, π - X)) \to F (X + s) \in ℂ$
187	82	ad2antlr	$⊢ ((φ \land n \in ℕ) \land s \in (- π - X, π - X)) \to D (n) : ℝ ⟶ ℝ$
188	187 180	ffvelrnd	$⊢ ((φ \land n \in ℕ) \land s \in (- π - X, π - X)) \to D (n) (s) \in ℝ$
189	188	recnd	$⊢ ((φ \land n \in ℕ) \land s \in (- π - X, π - X)) \to D (n) (s) \in ℂ$
190	186 189	mulcld	$⊢ ((φ \land n \in ℕ) \land s \in (- π - X, π - X)) \to F (X + s) D (n) (s) \in ℂ$
191		oveq2	$⊢ x = s \to X + x = X + s$
192	191	fveq2d	$⊢ x = s \to F (X + x) = F (X + s)$
193		fveq2	$⊢ x = s \to D (n) (x) = D (n) (s)$
194	192 193	oveq12d	$⊢ x = s \to F (X + x) D (n) (x) = F (X + s) D (n) (s)$
195	194	cbvmptv	$⊢ (x \in ℝ ⟼ F (X + x) D (n) (x)) = (s \in ℝ ⟼ F (X + s) D (n) (s))$
196	11 195	eqtri	$⊢ G = (s \in ℝ ⟼ F (X + s) D (n) (s))$
197	196	fvmpt2	$⊢ (s \in ℝ \land F (X + s) D (n) (s) \in ℂ) \to G (s) = F (X + s) D (n) (s)$
198	180 190 197	syl2anc	$⊢ ((φ \land n \in ℕ) \land s \in (- π - X, π - X)) \to G (s) = F (X + s) D (n) (s)$
199	198	eqcomd	$⊢ ((φ \land n \in ℕ) \land s \in (- π - X, π - X)) \to F (X + s) D (n) (s) = G (s)$
200	199	itgeq2dv	$⊢ (φ \land n \in ℕ) \to \int_{(- π - X, π - X)} F (X + s) D (n) (s) d s = \int_{(- π - X, π - X)} G (s) d s$
201	49	adantr	$⊢ (φ \land x \in ℝ) \to F : ℝ ⟶ ℂ$
202	8	adantr	$⊢ (φ \land x \in ℝ) \to X \in ℝ$
203		simpr	$⊢ (φ \land x \in ℝ) \to x \in ℝ$
204	202 203	readdcld	$⊢ (φ \land x \in ℝ) \to X + x \in ℝ$
205	201 204	ffvelrnd	$⊢ (φ \land x \in ℝ) \to F (X + x) \in ℂ$
206	205	adantlr	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to F (X + x) \in ℂ$
207	82	adantl	$⊢ (φ \land n \in ℕ) \to D (n) : ℝ ⟶ ℝ$
208	207	ffvelrnda	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to D (n) (x) \in ℝ$
209	208	recnd	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to D (n) (x) \in ℂ$
210	206 209	mulcld	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to F (X + x) D (n) (x) \in ℂ$
211	210 11	fmptd	$⊢ (φ \land n \in ℕ) \to G : ℝ ⟶ ℂ$
212	211	adantr	$⊢ ((φ \land n \in ℕ) \land s \in [- π - X, π - X]) \to G : ℝ ⟶ ℂ$
213	129	adantr	$⊢ (φ \land s \in [- π - X, π - X]) \to - π - X \in ℝ$
214	132	adantr	$⊢ (φ \land s \in [- π - X, π - X]) \to π - X \in ℝ$
215		simpr	$⊢ (φ \land s \in [- π - X, π - X]) \to s \in [- π - X, π - X]$
216		eliccre	$⊢ (- π - X \in ℝ \land π - X \in ℝ \land s \in [- π - X, π - X]) \to s \in ℝ$
217	213 214 215 216	syl3anc	$⊢ (φ \land s \in [- π - X, π - X]) \to s \in ℝ$
218	217	adantlr	$⊢ ((φ \land n \in ℕ) \land s \in [- π - X, π - X]) \to s \in ℝ$
219	212 218	ffvelrnd	$⊢ ((φ \land n \in ℕ) \land s \in [- π - X, π - X]) \to G (s) \in ℂ$
220	130 133 219	itgioo	$⊢ (φ \land n \in ℕ) \to \int_{(- π - X, π - X)} G (s) d s = \int_{[- π - X, π - X]} G (s) d s$
221		fveq2	$⊢ s = x \to G (s) = G (x)$
222	221	cbvitgv	$⊢ \int_{[- π - X, π - X]} G (s) d s = \int_{[- π - X, π - X]} G (x) d x$
223	220 222	eqtrdi	$⊢ (φ \land n \in ℕ) \to \int_{(- π - X, π - X)} G (s) d s = \int_{[- π - X, π - X]} G (x) d x$
224	200 223	eqtrd	$⊢ (φ \land n \in ℕ) \to \int_{(- π - X, π - X)} F (X + s) D (n) (s) d s = \int_{[- π - X, π - X]} G (x) d x$
225		eqid	$⊢ π - X - (- π - X) = π - X - (- π - X)$
226	116	renegcld	$⊢ (φ \land n \in ℕ) \to - X \in ℝ$
227	5	fourierdlem2	$⊢ M \in ℕ \to (Q \in P (M) \leftrightarrow (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = - π \land Q (M) = π) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))))$
228	6 227	syl	$⊢ φ \to (Q \in P (M) \leftrightarrow (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = - π \land Q (M) = π) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))))$
229	7 228	mpbid	$⊢ φ \to (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = - π \land Q (M) = π) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1)))$
230	229	simpld	$⊢ φ \to Q \in (ℝ^{(0 \dots M)})$
231		elmapi	$⊢ Q \in (ℝ^{(0 \dots M)}) \to Q : (0 \dots M) ⟶ ℝ$
232	230 231	syl	$⊢ φ \to Q : (0 \dots M) ⟶ ℝ$
233	232	ffvelrnda	$⊢ (φ \land i \in (0 \dots M)) \to Q (i) \in ℝ$
234	8	adantr	$⊢ (φ \land i \in (0 \dots M)) \to X \in ℝ$
235	233 234	resubcld	$⊢ (φ \land i \in (0 \dots M)) \to Q (i) - X \in ℝ$
236	235 17	fmptd	$⊢ φ \to W : (0 \dots M) ⟶ ℝ$
237		reex	$⊢ ℝ \in V$
238		ovex	$⊢ (0 \dots M) \in V$
239	237 238	pm3.2i	$⊢ (ℝ \in V \land (0 \dots M) \in V)$
240		elmapg	$⊢ (ℝ \in V \land (0 \dots M) \in V) \to (W \in (ℝ^{(0 \dots M)}) \leftrightarrow W : (0 \dots M) ⟶ ℝ)$
241	239 240	mp1i	$⊢ φ \to (W \in (ℝ^{(0 \dots M)}) \leftrightarrow W : (0 \dots M) ⟶ ℝ)$
242	236 241	mpbird	$⊢ φ \to W \in (ℝ^{(0 \dots M)})$
243	17	a1i	$⊢ φ \to W = (i \in (0 \dots M) ⟼ Q (i) - X)$
244		fveq2	$⊢ i = 0 \to Q (i) = Q (0)$
245	229	simprd	$⊢ φ \to ((Q (0) = - π \land Q (M) = π) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))$
246	245	simpld	$⊢ φ \to (Q (0) = - π \land Q (M) = π)$
247	246	simpld	$⊢ φ \to Q (0) = - π$
248	244 247	sylan9eqr	$⊢ (φ \land i = 0) \to Q (i) = - π$
249	248	oveq1d	$⊢ (φ \land i = 0) \to Q (i) - X = - π - X$
250		0zd	$⊢ φ \to 0 \in ℤ$
251	6	nnzd	$⊢ φ \to M \in ℤ$
252		0red	$⊢ M \in ℕ \to 0 \in ℝ$
253		nnre	$⊢ M \in ℕ \to M \in ℝ$
254		nngt0	$⊢ M \in ℕ \to 0 < M$
255	252 253 254	ltled	$⊢ M \in ℕ \to 0 \leq M$
256	6 255	syl	$⊢ φ \to 0 \leq M$
257		eluz2	$⊢ M \in ℤ_{\geq 0} \leftrightarrow (0 \in ℤ \land M \in ℤ \land 0 \leq M)$
258	250 251 256 257	syl3anbrc	$⊢ φ \to M \in ℤ_{\geq 0}$
259		eluzfz1	$⊢ M \in ℤ_{\geq 0} \to 0 \in (0 \dots M)$
260	258 259	syl	$⊢ φ \to 0 \in (0 \dots M)$
261	243 249 260 129	fvmptd	$⊢ φ \to W (0) = - π - X$
262		fveq2	$⊢ i = M \to Q (i) = Q (M)$
263	246	simprd	$⊢ φ \to Q (M) = π$
264	262 263	sylan9eqr	$⊢ (φ \land i = M) \to Q (i) = π$
265	264	oveq1d	$⊢ (φ \land i = M) \to Q (i) - X = π - X$
266		eluzfz2	$⊢ M \in ℤ_{\geq 0} \to M \in (0 \dots M)$
267	258 266	syl	$⊢ φ \to M \in (0 \dots M)$
268	243 265 267 132	fvmptd	$⊢ φ \to W (M) = π - X$
269	261 268	jca	$⊢ φ \to (W (0) = - π - X \land W (M) = π - X)$
270	232	adantr	$⊢ (φ \land i \in (0 ..^M)) \to Q : (0 \dots M) ⟶ ℝ$
271		elfzofz	$⊢ i \in (0 ..^M) \to i \in (0 \dots M)$
272	271	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i \in (0 \dots M)$
273	270 272	ffvelrnd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ℝ$
274		fzofzp1	$⊢ i \in (0 ..^M) \to i + 1 \in (0 \dots M)$
275	274	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i + 1 \in (0 \dots M)$
276	270 275	ffvelrnd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ℝ$
277	8	adantr	$⊢ (φ \land i \in (0 ..^M)) \to X \in ℝ$
278	245	simprd	$⊢ φ \to \forall i \in (0 ..^M) Q (i) < Q (i + 1)$
279	278	r19.21bi	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) < Q (i + 1)$
280	273 276 277 279	ltsub1dd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) - X < Q (i + 1) - X$
281	272 235	syldan	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) - X \in ℝ$
282	17	fvmpt2	$⊢ (i \in (0 \dots M) \land Q (i) - X \in ℝ) \to W (i) = Q (i) - X$
283	272 281 282	syl2anc	$⊢ (φ \land i \in (0 ..^M)) \to W (i) = Q (i) - X$
284		fveq2	$⊢ i = j \to Q (i) = Q (j)$
285	284	oveq1d	$⊢ i = j \to Q (i) - X = Q (j) - X$
286	285	cbvmptv	$⊢ (i \in (0 \dots M) ⟼ Q (i) - X) = (j \in (0 \dots M) ⟼ Q (j) - X)$
287	17 286	eqtri	$⊢ W = (j \in (0 \dots M) ⟼ Q (j) - X)$
288	287	a1i	$⊢ (φ \land i \in (0 ..^M)) \to W = (j \in (0 \dots M) ⟼ Q (j) - X)$
289		fveq2	$⊢ j = i + 1 \to Q (j) = Q (i + 1)$
290	289	oveq1d	$⊢ j = i + 1 \to Q (j) - X = Q (i + 1) - X$
291	290	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land j = i + 1) \to Q (j) - X = Q (i + 1) - X$
292	276 277	resubcld	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) - X \in ℝ$
293	288 291 275 292	fvmptd	$⊢ (φ \land i \in (0 ..^M)) \to W (i + 1) = Q (i + 1) - X$
294	280 283 293	3brtr4d	$⊢ (φ \land i \in (0 ..^M)) \to W (i) < W (i + 1)$
295	294	ralrimiva	$⊢ φ \to \forall i \in (0 ..^M) W (i) < W (i + 1)$
296	242 269 295	jca32	$⊢ φ \to (W \in (ℝ^{(0 \dots M)}) \land ((W (0) = - π - X \land W (M) = π - X) \land \forall i \in (0 ..^M) W (i) < W (i + 1)))$
297	16	fourierdlem2	$⊢ M \in ℕ \to (W \in O (M) \leftrightarrow (W \in (ℝ^{(0 \dots M)}) \land ((W (0) = - π - X \land W (M) = π - X) \land \forall i \in (0 ..^M) W (i) < W (i + 1))))$
298	6 297	syl	$⊢ φ \to (W \in O (M) \leftrightarrow (W \in (ℝ^{(0 \dots M)}) \land ((W (0) = - π - X \land W (M) = π - X) \land \forall i \in (0 ..^M) W (i) < W (i + 1))))$
299	296 298	mpbird	$⊢ φ \to W \in O (M)$
300	299	adantr	$⊢ (φ \land n \in ℕ) \to W \in O (M)$
301	155 156 154	nnncan2d	$⊢ φ \to π - X - (- π - X) = π - (- π)$
302		picn	$⊢ π \in ℂ$
303	302	2timesi	$⊢ 2 π = π + π$
304	302 302	subnegi	$⊢ π - (- π) = π + π$
305	303 15 304	3eqtr4i	$⊢ T = π - (- π)$
306	301 305	eqtr4di	$⊢ φ \to π - X - (- π - X) = T$
307	306	oveq2d	$⊢ φ \to x + (π - X) - (- π - X) = x + T$
308	307	fveq2d	$⊢ φ \to G (x + (π - X) - (- π - X)) = G (x + T)$
309	308	ad2antrr	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to G (x + (π - X) - (- π - X)) = G (x + T)$
310		simpr	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to x \in ℝ$
311	11	fvmpt2	$⊢ (x \in ℝ \land F (X + x) D (n) (x) \in ℂ) \to G (x) = F (X + x) D (n) (x)$
312	310 210 311	syl2anc	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to G (x) = F (X + x) D (n) (x)$
313	154	adantr	$⊢ (φ \land x \in ℝ) \to X \in ℂ$
314	203	recnd	$⊢ (φ \land x \in ℝ) \to x \in ℂ$
315		2re	$⊢ 2 \in ℝ$
316	315 38	remulcli	$⊢ 2 π \in ℝ$
317	15 316	eqeltri	$⊢ T \in ℝ$
318	317	a1i	$⊢ φ \to T \in ℝ$
319	318	recnd	$⊢ φ \to T \in ℂ$
320	319	adantr	$⊢ (φ \land x \in ℝ) \to T \in ℂ$
321	313 314 320	addassd	$⊢ (φ \land x \in ℝ) \to X + x + T = X + x + T$
322	321	eqcomd	$⊢ (φ \land x \in ℝ) \to X + x + T = X + x + T$
323	322	fveq2d	$⊢ (φ \land x \in ℝ) \to F (X + x + T) = F (X + x + T)$
324		simpl	$⊢ (φ \land x \in ℝ) \to φ$
325	324 204	jca	$⊢ (φ \land x \in ℝ) \to (φ \land X + x \in ℝ)$
326		eleq1	$⊢ s = X + x \to (s \in ℝ \leftrightarrow X + x \in ℝ)$
327	326	anbi2d	$⊢ s = X + x \to ((φ \land s \in ℝ) \leftrightarrow (φ \land X + x \in ℝ))$
328		oveq1	$⊢ s = X + x \to s + T = X + x + T$
329	328	fveq2d	$⊢ s = X + x \to F (s + T) = F (X + x + T)$
330		fveq2	$⊢ s = X + x \to F (s) = F (X + x)$
331	329 330	eqeq12d	$⊢ s = X + x \to (F (s + T) = F (s) \leftrightarrow F (X + x + T) = F (X + x))$
332	327 331	imbi12d	$⊢ s = X + x \to (((φ \land s \in ℝ) \to F (s + T) = F (s)) \leftrightarrow ((φ \land X + x \in ℝ) \to F (X + x + T) = F (X + x)))$
333		eleq1	$⊢ x = s \to (x \in ℝ \leftrightarrow s \in ℝ)$
334	333	anbi2d	$⊢ x = s \to ((φ \land x \in ℝ) \leftrightarrow (φ \land s \in ℝ))$
335		oveq1	$⊢ x = s \to x + T = s + T$
336	335	fveq2d	$⊢ x = s \to F (x + T) = F (s + T)$
337		fveq2	$⊢ x = s \to F (x) = F (s)$
338	336 337	eqeq12d	$⊢ x = s \to (F (x + T) = F (x) \leftrightarrow F (s + T) = F (s))$
339	334 338	imbi12d	$⊢ x = s \to (((φ \land x \in ℝ) \to F (x + T) = F (x)) \leftrightarrow ((φ \land s \in ℝ) \to F (s + T) = F (s)))$
340	339 10	chvarvv	$⊢ (φ \land s \in ℝ) \to F (s + T) = F (s)$
341	332 340	vtoclg	$⊢ X + x \in ℝ \to ((φ \land X + x \in ℝ) \to F (X + x + T) = F (X + x))$
342	204 325 341	sylc	$⊢ (φ \land x \in ℝ) \to F (X + x + T) = F (X + x)$
343	323 342	eqtr2d	$⊢ (φ \land x \in ℝ) \to F (X + x) = F (X + x + T)$
344	343	adantlr	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to F (X + x) = F (X + x + T)$
345	4 15	dirkerper	$⊢ (n \in ℕ \land x \in ℝ) \to D (n) (x + T) = D (n) (x)$
346	345	eqcomd	$⊢ (n \in ℕ \land x \in ℝ) \to D (n) (x) = D (n) (x + T)$
347	346	adantll	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to D (n) (x) = D (n) (x + T)$
348	344 347	oveq12d	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to F (X + x) D (n) (x) = F (X + x + T) D (n) (x + T)$
349	196	a1i	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to G = (s \in ℝ ⟼ F (X + s) D (n) (s))$
350		oveq2	$⊢ s = x + T \to X + s = X + x + T$
351	350	fveq2d	$⊢ s = x + T \to F (X + s) = F (X + x + T)$
352		fveq2	$⊢ s = x + T \to D (n) (s) = D (n) (x + T)$
353	351 352	oveq12d	$⊢ s = x + T \to F (X + s) D (n) (s) = F (X + x + T) D (n) (x + T)$
354	353	adantl	$⊢ (((φ \land n \in ℕ) \land x \in ℝ) \land s = x + T) \to F (X + s) D (n) (s) = F (X + x + T) D (n) (x + T)$
355	317	a1i	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to T \in ℝ$
356	310 355	readdcld	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to x + T \in ℝ$
357	317	a1i	$⊢ (φ \land x \in ℝ) \to T \in ℝ$
358	203 357	readdcld	$⊢ (φ \land x \in ℝ) \to x + T \in ℝ$
359	202 358	readdcld	$⊢ (φ \land x \in ℝ) \to X + x + T \in ℝ$
360	201 359	ffvelrnd	$⊢ (φ \land x \in ℝ) \to F (X + x + T) \in ℂ$
361	360	adantlr	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to F (X + x + T) \in ℂ$
362	82	ad2antlr	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to D (n) : ℝ ⟶ ℝ$
363	362 356	ffvelrnd	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to D (n) (x + T) \in ℝ$
364	363	recnd	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to D (n) (x + T) \in ℂ$
365	361 364	mulcld	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to F (X + x + T) D (n) (x + T) \in ℂ$
366	349 354 356 365	fvmptd	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to G (x + T) = F (X + x + T) D (n) (x + T)$
367	366	eqcomd	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to F (X + x + T) D (n) (x + T) = G (x + T)$
368	312 348 367	3eqtrrd	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to G (x + T) = G (x)$
369	309 368	eqtrd	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to G (x + (π - X) - (- π - X)) = G (x)$
370	196	reseq1i	$⊢ {G ↾}_{(W (i), W (i + 1))} = {(s \in ℝ ⟼ F (X + s) D (n) (s)) ↾}_{(W (i), W (i + 1))}$
371	370	a1i	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to {G ↾}_{(W (i), W (i + 1))} = {(s \in ℝ ⟼ F (X + s) D (n) (s)) ↾}_{(W (i), W (i + 1))}$
372		ioossre	$⊢ (W (i), W (i + 1)) \subseteq ℝ$
373		resmpt	$⊢ (W (i), W (i + 1)) \subseteq ℝ \to {(s \in ℝ ⟼ F (X + s) D (n) (s)) ↾}_{(W (i), W (i + 1))} = (s \in (W (i), W (i + 1)) ⟼ F (X + s) D (n) (s))$
374	372 373	ax-mp	$⊢ {(s \in ℝ ⟼ F (X + s) D (n) (s)) ↾}_{(W (i), W (i + 1))} = (s \in (W (i), W (i + 1)) ⟼ F (X + s) D (n) (s))$
375	371 374	eqtrdi	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to {G ↾}_{(W (i), W (i + 1))} = (s \in (W (i), W (i + 1)) ⟼ F (X + s) D (n) (s))$
376	273	rexrd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ℝ^{*}$
377	376	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (W (i), W (i + 1))) \to Q (i) \in ℝ^{*}$
378	276	rexrd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ℝ^{*}$
379	378	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (W (i), W (i + 1))) \to Q (i + 1) \in ℝ^{*}$
380	8	adantr	$⊢ (φ \land s \in (W (i), W (i + 1))) \to X \in ℝ$
381		elioore	$⊢ s \in (W (i), W (i + 1)) \to s \in ℝ$
382	381	adantl	$⊢ (φ \land s \in (W (i), W (i + 1))) \to s \in ℝ$
383	380 382	readdcld	$⊢ (φ \land s \in (W (i), W (i + 1))) \to X + s \in ℝ$
384	383	adantlr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (W (i), W (i + 1))) \to X + s \in ℝ$
385		eleq1	$⊢ x = s \to (x \in (W (i), W (i + 1)) \leftrightarrow s \in (W (i), W (i + 1)))$
386	385	anbi2d	$⊢ x = s \to (((φ \land i \in (0 ..^M)) \land x \in (W (i), W (i + 1))) \leftrightarrow ((φ \land i \in (0 ..^M)) \land s \in (W (i), W (i + 1))))$
387	191	breq2d	$⊢ x = s \to (Q (i) < X + x \leftrightarrow Q (i) < X + s)$
388	386 387	imbi12d	$⊢ x = s \to ((((φ \land i \in (0 ..^M)) \land x \in (W (i), W (i + 1))) \to Q (i) < X + x) \leftrightarrow (((φ \land i \in (0 ..^M)) \land s \in (W (i), W (i + 1))) \to Q (i) < X + s))$
389	154	adantr	$⊢ (φ \land i \in (0 ..^M)) \to X \in ℂ$
390	283 281	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to W (i) \in ℝ$
391	390	recnd	$⊢ (φ \land i \in (0 ..^M)) \to W (i) \in ℂ$
392	389 391	addcomd	$⊢ (φ \land i \in (0 ..^M)) \to X + W (i) = W (i) + X$
393	283	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to W (i) + X = Q (i) - X + X$
394	273	recnd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ℂ$
395	394 389	npcand	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) - X + X = Q (i)$
396	392 393 395	3eqtrrd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) = X + W (i)$
397	396	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (W (i), W (i + 1))) \to Q (i) = X + W (i)$
398	390	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (W (i), W (i + 1))) \to W (i) \in ℝ$
399		elioore	$⊢ x \in (W (i), W (i + 1)) \to x \in ℝ$
400	399	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (W (i), W (i + 1))) \to x \in ℝ$
401	8	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (W (i), W (i + 1))) \to X \in ℝ$
402	390	rexrd	$⊢ (φ \land i \in (0 ..^M)) \to W (i) \in ℝ^{*}$
403	402	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (W (i), W (i + 1))) \to W (i) \in ℝ^{*}$
404	293 292	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to W (i + 1) \in ℝ$
405	404	rexrd	$⊢ (φ \land i \in (0 ..^M)) \to W (i + 1) \in ℝ^{*}$
406	405	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (W (i), W (i + 1))) \to W (i + 1) \in ℝ^{*}$
407		simpr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (W (i), W (i + 1))) \to x \in (W (i), W (i + 1))$
408		ioogtlb	$⊢ (W (i) \in ℝ^{} \land W (i + 1) \in ℝ^{} \land x \in (W (i), W (i + 1))) \to W (i) < x$
409	403 406 407 408	syl3anc	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (W (i), W (i + 1))) \to W (i) < x$
410	398 400 401 409	ltadd2dd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (W (i), W (i + 1))) \to X + W (i) < X + x$
411	397 410	eqbrtrd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (W (i), W (i + 1))) \to Q (i) < X + x$
412	388 411	chvarvv	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (W (i), W (i + 1))) \to Q (i) < X + s$
413	191	breq1d	$⊢ x = s \to (X + x < Q (i + 1) \leftrightarrow X + s < Q (i + 1))$
414	386 413	imbi12d	$⊢ x = s \to ((((φ \land i \in (0 ..^M)) \land x \in (W (i), W (i + 1))) \to X + x < Q (i + 1)) \leftrightarrow (((φ \land i \in (0 ..^M)) \land s \in (W (i), W (i + 1))) \to X + s < Q (i + 1)))$
415	404	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (W (i), W (i + 1))) \to W (i + 1) \in ℝ$
416		iooltub	$⊢ (W (i) \in ℝ^{} \land W (i + 1) \in ℝ^{} \land x \in (W (i), W (i + 1))) \to x < W (i + 1)$
417	403 406 407 416	syl3anc	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (W (i), W (i + 1))) \to x < W (i + 1)$
418	400 415 401 417	ltadd2dd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (W (i), W (i + 1))) \to X + x < X + W (i + 1)$
419	404	recnd	$⊢ (φ \land i \in (0 ..^M)) \to W (i + 1) \in ℂ$
420	389 419	addcomd	$⊢ (φ \land i \in (0 ..^M)) \to X + W (i + 1) = W (i + 1) + X$
421	293	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to W (i + 1) + X = Q (i + 1) - X + X$
422	276	recnd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ℂ$
423	422 389	npcand	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) - X + X = Q (i + 1)$
424	420 421 423	3eqtrd	$⊢ (φ \land i \in (0 ..^M)) \to X + W (i + 1) = Q (i + 1)$
425	424	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (W (i), W (i + 1))) \to X + W (i + 1) = Q (i + 1)$
426	418 425	breqtrd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (W (i), W (i + 1))) \to X + x < Q (i + 1)$
427	414 426	chvarvv	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (W (i), W (i + 1))) \to X + s < Q (i + 1)$
428	377 379 384 412 427	eliood	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (W (i), W (i + 1))) \to X + s \in (Q (i), Q (i + 1))$
429	191	cbvmptv	$⊢ (x \in (W (i), W (i + 1)) ⟼ X + x) = (s \in (W (i), W (i + 1)) ⟼ X + s)$
430	429	a1i	$⊢ (φ \land i \in (0 ..^M)) \to (x \in (W (i), W (i + 1)) ⟼ X + x) = (s \in (W (i), W (i + 1)) ⟼ X + s)$
431		ioossre	$⊢ (Q (i), Q (i + 1)) \subseteq ℝ$
432	431	a1i	$⊢ φ \to (Q (i), Q (i + 1)) \subseteq ℝ$
433	9 432	feqresmpt	$⊢ φ \to {F ↾}_{(Q (i), Q (i + 1))} = (x \in (Q (i), Q (i + 1)) ⟼ F (x))$
434	433	adantr	$⊢ (φ \land i \in (0 ..^M)) \to {F ↾}_{(Q (i), Q (i + 1))} = (x \in (Q (i), Q (i + 1)) ⟼ F (x))$
435		fveq2	$⊢ x = X + s \to F (x) = F (X + s)$
436	428 430 434 435	fmptco	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) \circ (x \in (W (i), W (i + 1)) ⟼ X + x) = (s \in (W (i), W (i + 1)) ⟼ F (X + s))$
437		eqid	$⊢ (x \in ℂ ⟼ X + x) = (x \in ℂ ⟼ X + x)$
438		ssid	$⊢ ℂ \subseteq ℂ$
439	438	a1i	$⊢ φ \to ℂ \subseteq ℂ$
440	439 154 439	constcncfg	$⊢ φ \to (x \in ℂ ⟼ X) : ℂ \underset{cn}{⟶} ℂ$
441		cncfmptid	$⊢ (ℂ \subseteq ℂ \land ℂ \subseteq ℂ) \to (x \in ℂ ⟼ x) : ℂ \underset{cn}{⟶} ℂ$
442	438 438 441	mp2an	$⊢ (x \in ℂ ⟼ x) : ℂ \underset{cn}{⟶} ℂ$
443	442	a1i	$⊢ φ \to (x \in ℂ ⟼ x) : ℂ \underset{cn}{⟶} ℂ$
444	440 443	addcncf	$⊢ φ \to (x \in ℂ ⟼ X + x) : ℂ \underset{cn}{⟶} ℂ$
445	444	adantr	$⊢ (φ \land i \in (0 ..^M)) \to (x \in ℂ ⟼ X + x) : ℂ \underset{cn}{⟶} ℂ$
446		ioosscn	$⊢ (W (i), W (i + 1)) \subseteq ℂ$
447	446	a1i	$⊢ (φ \land i \in (0 ..^M)) \to (W (i), W (i + 1)) \subseteq ℂ$
448		ioosscn	$⊢ (Q (i), Q (i + 1)) \subseteq ℂ$
449	448	a1i	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq ℂ$
450	376	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (W (i), W (i + 1))) \to Q (i) \in ℝ^{*}$
451	378	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (W (i), W (i + 1))) \to Q (i + 1) \in ℝ^{*}$
452	8	adantr	$⊢ (φ \land x \in (W (i), W (i + 1))) \to X \in ℝ$
453	399	adantl	$⊢ (φ \land x \in (W (i), W (i + 1))) \to x \in ℝ$
454	452 453	readdcld	$⊢ (φ \land x \in (W (i), W (i + 1))) \to X + x \in ℝ$
455	454	adantlr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (W (i), W (i + 1))) \to X + x \in ℝ$
456	450 451 455 411 426	eliood	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (W (i), W (i + 1))) \to X + x \in (Q (i), Q (i + 1))$
457	437 445 447 449 456	cncfmptssg	$⊢ (φ \land i \in (0 ..^M)) \to (x \in (W (i), W (i + 1)) ⟼ X + x) : (W (i), W (i + 1)) \underset{cn}{⟶} (Q (i), Q (i + 1))$
458	457 12	cncfco	$⊢ (φ \land i \in (0 ..^M)) \to (({F ↾}_{(Q (i), Q (i + 1))}) \circ (x \in (W (i), W (i + 1)) ⟼ X + x)) : (W (i), W (i + 1)) \underset{cn}{⟶} ℂ$
459	436 458	eqeltrrd	$⊢ (φ \land i \in (0 ..^M)) \to (s \in (W (i), W (i + 1)) ⟼ F (X + s)) : (W (i), W (i + 1)) \underset{cn}{⟶} ℂ$
460	459	adantlr	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to (s \in (W (i), W (i + 1)) ⟼ F (X + s)) : (W (i), W (i + 1)) \underset{cn}{⟶} ℂ$
461		eqid	$⊢ (s \in ℝ ⟼ D (n) (s)) = (s \in ℝ ⟼ D (n) (s))$
462	82	feqmptd	$⊢ n \in ℕ \to D (n) = (s \in ℝ ⟼ D (n) (s))$
463		cncfss	$⊢ (ℝ \subseteq ℂ \land ℂ \subseteq ℂ) \to ℝ \underset{cn}{⟶} ℝ \subseteq ℝ \underset{cn}{⟶} ℂ$
464	47 438 463	mp2an	$⊢ ℝ \underset{cn}{⟶} ℝ \subseteq ℝ \underset{cn}{⟶} ℂ$
465	4	dirkercncf	$⊢ n \in ℕ \to D (n) : ℝ \underset{cn}{⟶} ℝ$
466	464 465	sselid	$⊢ n \in ℕ \to D (n) : ℝ \underset{cn}{⟶} ℂ$
467	462 466	eqeltrrd	$⊢ n \in ℕ \to (s \in ℝ ⟼ D (n) (s)) : ℝ \underset{cn}{⟶} ℂ$
468	372	a1i	$⊢ n \in ℕ \to (W (i), W (i + 1)) \subseteq ℝ$
469	438	a1i	$⊢ n \in ℕ \to ℂ \subseteq ℂ$
470		cncff	$⊢ D (n) : ℝ \underset{cn}{⟶} ℂ \to D (n) : ℝ ⟶ ℂ$
471	466 470	syl	$⊢ n \in ℕ \to D (n) : ℝ ⟶ ℂ$
472	471	adantr	$⊢ (n \in ℕ \land s \in (W (i), W (i + 1))) \to D (n) : ℝ ⟶ ℂ$
473	381	adantl	$⊢ (n \in ℕ \land s \in (W (i), W (i + 1))) \to s \in ℝ$
474	472 473	ffvelrnd	$⊢ (n \in ℕ \land s \in (W (i), W (i + 1))) \to D (n) (s) \in ℂ$
475	461 467 468 469 474	cncfmptssg	$⊢ n \in ℕ \to (s \in (W (i), W (i + 1)) ⟼ D (n) (s)) : (W (i), W (i + 1)) \underset{cn}{⟶} ℂ$
476	475	ad2antlr	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to (s \in (W (i), W (i + 1)) ⟼ D (n) (s)) : (W (i), W (i + 1)) \underset{cn}{⟶} ℂ$
477	460 476	mulcncf	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to (s \in (W (i), W (i + 1)) ⟼ F (X + s) D (n) (s)) : (W (i), W (i + 1)) \underset{cn}{⟶} ℂ$
478	375 477	eqeltrd	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to ({G ↾}_{(W (i), W (i + 1))}) : (W (i), W (i + 1)) \underset{cn}{⟶} ℂ$
479	453 205	syldan	$⊢ (φ \land x \in (W (i), W (i + 1))) \to F (X + x) \in ℂ$
480	479	adantlr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (W (i), W (i + 1))) \to F (X + x) \in ℂ$
481		eqid	$⊢ (x \in (W (i), W (i + 1)) ⟼ F (X + x)) = (x \in (W (i), W (i + 1)) ⟼ F (X + x))$
482	480 481	fmptd	$⊢ (φ \land i \in (0 ..^M)) \to (x \in (W (i), W (i + 1)) ⟼ F (X + x)) : (W (i), W (i + 1)) ⟶ ℂ$
483	482	adantlr	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to (x \in (W (i), W (i + 1)) ⟼ F (X + x)) : (W (i), W (i + 1)) ⟶ ℂ$
484	82	ad2antlr	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to D (n) : ℝ ⟶ ℝ$
485	372	a1i	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to (W (i), W (i + 1)) \subseteq ℝ$
486	484 485	fssresd	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to ({D (n) ↾}_{(W (i), W (i + 1))}) : (W (i), W (i + 1)) ⟶ ℝ$
487	47	a1i	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to ℝ \subseteq ℂ$
488	486 487	fssd	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to ({D (n) ↾}_{(W (i), W (i + 1))}) : (W (i), W (i + 1)) ⟶ ℂ$
489		eqid	$⊢ (s \in (W (i), W (i + 1)) ⟼ (x \in (W (i), W (i + 1)) ⟼ F (X + x)) (s) ({D (n) ↾}_{(W (i), W (i + 1))}) (s)) = (s \in (W (i), W (i + 1)) ⟼ (x \in (W (i), W (i + 1)) ⟼ F (X + x)) (s) ({D (n) ↾}_{(W (i), W (i + 1))}) (s))$
490		fdm	$⊢ F : ℝ ⟶ ℂ \to dom F = ℝ$
491	49 490	syl	$⊢ φ \to dom F = ℝ$
492	431 491	sseqtrrid	$⊢ φ \to (Q (i), Q (i + 1)) \subseteq dom F$
493		ssdmres	$⊢ (Q (i), Q (i + 1)) \subseteq dom F \leftrightarrow dom ({F ↾}_{(Q (i), Q (i + 1))}) = (Q (i), Q (i + 1))$
494	492 493	sylib	$⊢ φ \to dom ({F ↾}_{(Q (i), Q (i + 1))}) = (Q (i), Q (i + 1))$
495	494	eqcomd	$⊢ φ \to (Q (i), Q (i + 1)) = dom ({F ↾}_{(Q (i), Q (i + 1))})$
496	495	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (W (i), W (i + 1))) \to (Q (i), Q (i + 1)) = dom ({F ↾}_{(Q (i), Q (i + 1))})$
497	456 496	eleqtrd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (W (i), W (i + 1))) \to X + x \in dom ({F ↾}_{(Q (i), Q (i + 1))})$
498	273	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (W (i), W (i + 1))) \to Q (i) \in ℝ$
499	498 411	gtned	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (W (i), W (i + 1))) \to X + x \neq Q (i)$
500		eldifsn	$⊢ X + x \in (dom ({F ↾}_{(Q (i), Q (i + 1))}) ∖ \{Q (i)\}) \leftrightarrow (X + x \in dom ({F ↾}_{(Q (i), Q (i + 1))}) \land X + x \neq Q (i))$
501	497 499 500	sylanbrc	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (W (i), W (i + 1))) \to X + x \in (dom ({F ↾}_{(Q (i), Q (i + 1))}) ∖ \{Q (i)\})$
502	501	ralrimiva	$⊢ (φ \land i \in (0 ..^M)) \to \forall x \in (W (i), W (i + 1)) X + x \in (dom ({F ↾}_{(Q (i), Q (i + 1))}) ∖ \{Q (i)\})$
503		eqid	$⊢ (x \in (W (i), W (i + 1)) ⟼ X + x) = (x \in (W (i), W (i + 1)) ⟼ X + x)$
504	503	rnmptss	$⊢ \forall x \in (W (i), W (i + 1)) X + x \in (dom ({F ↾}_{(Q (i), Q (i + 1))}) ∖ \{Q (i)\}) \to ran (x \in (W (i), W (i + 1)) ⟼ X + x) \subseteq dom ({F ↾}_{(Q (i), Q (i + 1))}) ∖ \{Q (i)\}$
505	502 504	syl	$⊢ (φ \land i \in (0 ..^M)) \to ran (x \in (W (i), W (i + 1)) ⟼ X + x) \subseteq dom ({F ↾}_{(Q (i), Q (i + 1))}) ∖ \{Q (i)\}$
506		eqidd	$⊢ (φ \land i \in (0 ..^M)) \to (x \in [W (i), W (i + 1)] ⟼ X + x) = (x \in [W (i), W (i + 1)] ⟼ X + x)$
507		oveq2	$⊢ x = W (i) \to X + x = X + W (i)$
508	507	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land x = W (i)) \to X + x = X + W (i)$
509	390	leidd	$⊢ (φ \land i \in (0 ..^M)) \to W (i) \leq W (i)$
510	390 404 294	ltled	$⊢ (φ \land i \in (0 ..^M)) \to W (i) \leq W (i + 1)$
511	390 404 390 509 510	eliccd	$⊢ (φ \land i \in (0 ..^M)) \to W (i) \in [W (i), W (i + 1)]$
512	396 273	eqeltrrd	$⊢ (φ \land i \in (0 ..^M)) \to X + W (i) \in ℝ$
513	506 508 511 512	fvmptd	$⊢ (φ \land i \in (0 ..^M)) \to (x \in [W (i), W (i + 1)] ⟼ X + x) (W (i)) = X + W (i)$
514	396	eqcomd	$⊢ (φ \land i \in (0 ..^M)) \to X + W (i) = Q (i)$
515	513 514	eqtr2d	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) = (x \in [W (i), W (i + 1)] ⟼ X + x) (W (i))$
516	390 404	iccssred	$⊢ (φ \land i \in (0 ..^M)) \to [W (i), W (i + 1)] \subseteq ℝ$
517	516 47	sstrdi	$⊢ (φ \land i \in (0 ..^M)) \to [W (i), W (i + 1)] \subseteq ℂ$
518	517	resmptd	$⊢ (φ \land i \in (0 ..^M)) \to {(x \in ℂ ⟼ X + x) ↾}_{[W (i), W (i + 1)]} = (x \in [W (i), W (i + 1)] ⟼ X + x)$
519		rescncf	$⊢ [W (i), W (i + 1)] \subseteq ℂ \to ((x \in ℂ ⟼ X + x) : ℂ \underset{cn}{⟶} ℂ \to ({(x \in ℂ ⟼ X + x) ↾}_{[W (i), W (i + 1)]}) : [W (i), W (i + 1)] \underset{cn}{⟶} ℂ)$
520	517 445 519	sylc	$⊢ (φ \land i \in (0 ..^M)) \to ({(x \in ℂ ⟼ X + x) ↾}_{[W (i), W (i + 1)]}) : [W (i), W (i + 1)] \underset{cn}{⟶} ℂ$
521	518 520	eqeltrrd	$⊢ (φ \land i \in (0 ..^M)) \to (x \in [W (i), W (i + 1)] ⟼ X + x) : [W (i), W (i + 1)] \underset{cn}{⟶} ℂ$
522	521 511	cnlimci	$⊢ (φ \land i \in (0 ..^M)) \to (x \in [W (i), W (i + 1)] ⟼ X + x) (W (i)) \in ((x \in [W (i), W (i + 1)] ⟼ X + x) {lim}_{ℂ} W (i))$
523	515 522	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ((x \in [W (i), W (i + 1)] ⟼ X + x) {lim}_{ℂ} W (i))$
524		ioossicc	$⊢ (W (i), W (i + 1)) \subseteq [W (i), W (i + 1)]$
525		resmpt	$⊢ (W (i), W (i + 1)) \subseteq [W (i), W (i + 1)] \to {(x \in [W (i), W (i + 1)] ⟼ X + x) ↾}_{(W (i), W (i + 1))} = (x \in (W (i), W (i + 1)) ⟼ X + x)$
526	524 525	ax-mp	$⊢ {(x \in [W (i), W (i + 1)] ⟼ X + x) ↾}_{(W (i), W (i + 1))} = (x \in (W (i), W (i + 1)) ⟼ X + x)$
527	526	eqcomi	$⊢ (x \in (W (i), W (i + 1)) ⟼ X + x) = {(x \in [W (i), W (i + 1)] ⟼ X + x) ↾}_{(W (i), W (i + 1))}$
528	527	a1i	$⊢ (φ \land i \in (0 ..^M)) \to (x \in (W (i), W (i + 1)) ⟼ X + x) = {(x \in [W (i), W (i + 1)] ⟼ X + x) ↾}_{(W (i), W (i + 1))}$
529	528	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to (x \in (W (i), W (i + 1)) ⟼ X + x) {lim}_{ℂ} W (i) = ({(x \in [W (i), W (i + 1)] ⟼ X + x) ↾}_{(W (i), W (i + 1))}) {lim}_{ℂ} W (i)$
530	154	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [W (i), W (i + 1)]) \to X \in ℂ$
531	390	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [W (i), W (i + 1)]) \to W (i) \in ℝ$
532	404	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [W (i), W (i + 1)]) \to W (i + 1) \in ℝ$
533		simpr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [W (i), W (i + 1)]) \to x \in [W (i), W (i + 1)]$
534		eliccre	$⊢ (W (i) \in ℝ \land W (i + 1) \in ℝ \land x \in [W (i), W (i + 1)]) \to x \in ℝ$
535	531 532 533 534	syl3anc	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [W (i), W (i + 1)]) \to x \in ℝ$
536	535	recnd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [W (i), W (i + 1)]) \to x \in ℂ$
537	530 536	addcld	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [W (i), W (i + 1)]) \to X + x \in ℂ$
538		eqid	$⊢ (x \in [W (i), W (i + 1)] ⟼ X + x) = (x \in [W (i), W (i + 1)] ⟼ X + x)$
539	537 538	fmptd	$⊢ (φ \land i \in (0 ..^M)) \to (x \in [W (i), W (i + 1)] ⟼ X + x) : [W (i), W (i + 1)] ⟶ ℂ$
540	390 404 294 539	limciccioolb	$⊢ (φ \land i \in (0 ..^M)) \to ({(x \in [W (i), W (i + 1)] ⟼ X + x) ↾}_{(W (i), W (i + 1))}) {lim}_{ℂ} W (i) = (x \in [W (i), W (i + 1)] ⟼ X + x) {lim}_{ℂ} W (i)$
541	529 540	eqtr2d	$⊢ (φ \land i \in (0 ..^M)) \to (x \in [W (i), W (i + 1)] ⟼ X + x) {lim}_{ℂ} W (i) = (x \in (W (i), W (i + 1)) ⟼ X + x) {lim}_{ℂ} W (i)$
542	523 541	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ((x \in (W (i), W (i + 1)) ⟼ X + x) {lim}_{ℂ} W (i))$
543	505 542 13	limccog	$⊢ (φ \land i \in (0 ..^M)) \to R \in ((({F ↾}_{(Q (i), Q (i + 1))}) \circ (x \in (W (i), W (i + 1)) ⟼ X + x)) {lim}_{ℂ} W (i))$
544	49 432	fssresd	$⊢ φ \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) ⟶ ℂ$
545	544	adantr	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) ⟶ ℂ$
546	456 503	fmptd	$⊢ (φ \land i \in (0 ..^M)) \to (x \in (W (i), W (i + 1)) ⟼ X + x) : (W (i), W (i + 1)) ⟶ (Q (i), Q (i + 1))$
547		fcompt	$⊢ (({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) ⟶ ℂ \land (x \in (W (i), W (i + 1)) ⟼ X + x) : (W (i), W (i + 1)) ⟶ (Q (i), Q (i + 1))) \to ({F ↾}_{(Q (i), Q (i + 1))}) \circ (x \in (W (i), W (i + 1)) ⟼ X + x) = (y \in (W (i), W (i + 1)) ⟼ ({F ↾}_{(Q (i), Q (i + 1))}) ((x \in (W (i), W (i + 1)) ⟼ X + x) (y)))$
548	545 546 547	syl2anc	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) \circ (x \in (W (i), W (i + 1)) ⟼ X + x) = (y \in (W (i), W (i + 1)) ⟼ ({F ↾}_{(Q (i), Q (i + 1))}) ((x \in (W (i), W (i + 1)) ⟼ X + x) (y)))$
549		eqidd	$⊢ (φ \land y \in (W (i), W (i + 1))) \to (x \in (W (i), W (i + 1)) ⟼ X + x) = (x \in (W (i), W (i + 1)) ⟼ X + x)$
550		oveq2	$⊢ x = y \to X + x = X + y$
551	550	adantl	$⊢ ((φ \land y \in (W (i), W (i + 1))) \land x = y) \to X + x = X + y$
552		simpr	$⊢ (φ \land y \in (W (i), W (i + 1))) \to y \in (W (i), W (i + 1))$
553	8	adantr	$⊢ (φ \land y \in (W (i), W (i + 1))) \to X \in ℝ$
554	372 552	sselid	$⊢ (φ \land y \in (W (i), W (i + 1))) \to y \in ℝ$
555	553 554	readdcld	$⊢ (φ \land y \in (W (i), W (i + 1))) \to X + y \in ℝ$
556	549 551 552 555	fvmptd	$⊢ (φ \land y \in (W (i), W (i + 1))) \to (x \in (W (i), W (i + 1)) ⟼ X + x) (y) = X + y$
557	556	fveq2d	$⊢ (φ \land y \in (W (i), W (i + 1))) \to ({F ↾}_{(Q (i), Q (i + 1))}) ((x \in (W (i), W (i + 1)) ⟼ X + x) (y)) = ({F ↾}_{(Q (i), Q (i + 1))}) (X + y)$
558	557	adantlr	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (W (i), W (i + 1))) \to ({F ↾}_{(Q (i), Q (i + 1))}) ((x \in (W (i), W (i + 1)) ⟼ X + x) (y)) = ({F ↾}_{(Q (i), Q (i + 1))}) (X + y)$
559	376	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (W (i), W (i + 1))) \to Q (i) \in ℝ^{*}$
560	378	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (W (i), W (i + 1))) \to Q (i + 1) \in ℝ^{*}$
561	555	adantlr	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (W (i), W (i + 1))) \to X + y \in ℝ$
562	396	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (W (i), W (i + 1))) \to Q (i) = X + W (i)$
563	390	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (W (i), W (i + 1))) \to W (i) \in ℝ$
564	554	adantlr	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (W (i), W (i + 1))) \to y \in ℝ$
565	8	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (W (i), W (i + 1))) \to X \in ℝ$
566	402	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (W (i), W (i + 1))) \to W (i) \in ℝ^{*}$
567	405	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (W (i), W (i + 1))) \to W (i + 1) \in ℝ^{*}$
568		simpr	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (W (i), W (i + 1))) \to y \in (W (i), W (i + 1))$
569		ioogtlb	$⊢ (W (i) \in ℝ^{} \land W (i + 1) \in ℝ^{} \land y \in (W (i), W (i + 1))) \to W (i) < y$
570	566 567 568 569	syl3anc	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (W (i), W (i + 1))) \to W (i) < y$
571	563 564 565 570	ltadd2dd	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (W (i), W (i + 1))) \to X + W (i) < X + y$
572	562 571	eqbrtrd	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (W (i), W (i + 1))) \to Q (i) < X + y$
573	404	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (W (i), W (i + 1))) \to W (i + 1) \in ℝ$
574		iooltub	$⊢ (W (i) \in ℝ^{} \land W (i + 1) \in ℝ^{} \land y \in (W (i), W (i + 1))) \to y < W (i + 1)$
575	566 567 568 574	syl3anc	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (W (i), W (i + 1))) \to y < W (i + 1)$
576	564 573 565 575	ltadd2dd	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (W (i), W (i + 1))) \to X + y < X + W (i + 1)$
577	424	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (W (i), W (i + 1))) \to X + W (i + 1) = Q (i + 1)$
578	576 577	breqtrd	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (W (i), W (i + 1))) \to X + y < Q (i + 1)$
579	559 560 561 572 578	eliood	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (W (i), W (i + 1))) \to X + y \in (Q (i), Q (i + 1))$
580		fvres	$⊢ X + y \in (Q (i), Q (i + 1)) \to ({F ↾}_{(Q (i), Q (i + 1))}) (X + y) = F (X + y)$
581	579 580	syl	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (W (i), W (i + 1))) \to ({F ↾}_{(Q (i), Q (i + 1))}) (X + y) = F (X + y)$
582	558 581	eqtrd	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (W (i), W (i + 1))) \to ({F ↾}_{(Q (i), Q (i + 1))}) ((x \in (W (i), W (i + 1)) ⟼ X + x) (y)) = F (X + y)$
583	582	mpteq2dva	$⊢ (φ \land i \in (0 ..^M)) \to (y \in (W (i), W (i + 1)) ⟼ ({F ↾}_{(Q (i), Q (i + 1))}) ((x \in (W (i), W (i + 1)) ⟼ X + x) (y))) = (y \in (W (i), W (i + 1)) ⟼ F (X + y))$
584	550	fveq2d	$⊢ x = y \to F (X + x) = F (X + y)$
585	584	cbvmptv	$⊢ (x \in (W (i), W (i + 1)) ⟼ F (X + x)) = (y \in (W (i), W (i + 1)) ⟼ F (X + y))$
586	583 585	eqtr4di	$⊢ (φ \land i \in (0 ..^M)) \to (y \in (W (i), W (i + 1)) ⟼ ({F ↾}_{(Q (i), Q (i + 1))}) ((x \in (W (i), W (i + 1)) ⟼ X + x) (y))) = (x \in (W (i), W (i + 1)) ⟼ F (X + x))$
587	548 586	eqtrd	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) \circ (x \in (W (i), W (i + 1)) ⟼ X + x) = (x \in (W (i), W (i + 1)) ⟼ F (X + x))$
588	587	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to (({F ↾}_{(Q (i), Q (i + 1))}) \circ (x \in (W (i), W (i + 1)) ⟼ X + x)) {lim}_{ℂ} W (i) = (x \in (W (i), W (i + 1)) ⟼ F (X + x)) {lim}_{ℂ} W (i)$
589	543 588	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to R \in ((x \in (W (i), W (i + 1)) ⟼ F (X + x)) {lim}_{ℂ} W (i))$
590	589	adantlr	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to R \in ((x \in (W (i), W (i + 1)) ⟼ F (X + x)) {lim}_{ℂ} W (i))$
591		fvres	$⊢ W (i) \in [W (i), W (i + 1)] \to ({D (n) ↾}_{[W (i), W (i + 1)]}) (W (i)) = D (n) (W (i))$
592	511 591	syl	$⊢ (φ \land i \in (0 ..^M)) \to ({D (n) ↾}_{[W (i), W (i + 1)]}) (W (i)) = D (n) (W (i))$
593	592	eqcomd	$⊢ (φ \land i \in (0 ..^M)) \to D (n) (W (i)) = ({D (n) ↾}_{[W (i), W (i + 1)]}) (W (i))$
594	593	adantlr	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to D (n) (W (i)) = ({D (n) ↾}_{[W (i), W (i + 1)]}) (W (i))$
595	516	adantlr	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to [W (i), W (i + 1)] \subseteq ℝ$
596	465	ad2antlr	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to D (n) : ℝ \underset{cn}{⟶} ℝ$
597		rescncf	$⊢ [W (i), W (i + 1)] \subseteq ℝ \to (D (n) : ℝ \underset{cn}{⟶} ℝ \to ({D (n) ↾}_{[W (i), W (i + 1)]}) : [W (i), W (i + 1)] \underset{cn}{⟶} ℝ)$
598	595 596 597	sylc	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to ({D (n) ↾}_{[W (i), W (i + 1)]}) : [W (i), W (i + 1)] \underset{cn}{⟶} ℝ$
599	511	adantlr	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to W (i) \in [W (i), W (i + 1)]$
600	598 599	cnlimci	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to ({D (n) ↾}_{[W (i), W (i + 1)]}) (W (i)) \in (({D (n) ↾}_{[W (i), W (i + 1)]}) {lim}_{ℂ} W (i))$
601	594 600	eqeltrd	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to D (n) (W (i)) \in (({D (n) ↾}_{[W (i), W (i + 1)]}) {lim}_{ℂ} W (i))$
602	524	a1i	$⊢ (φ \land i \in (0 ..^M)) \to (W (i), W (i + 1)) \subseteq [W (i), W (i + 1)]$
603	602	resabs1d	$⊢ (φ \land i \in (0 ..^M)) \to {({D (n) ↾}_{[W (i), W (i + 1)]}) ↾}_{(W (i), W (i + 1))} = {D (n) ↾}_{(W (i), W (i + 1))}$
604	603	eqcomd	$⊢ (φ \land i \in (0 ..^M)) \to {D (n) ↾}_{(W (i), W (i + 1))} = {({D (n) ↾}_{[W (i), W (i + 1)]}) ↾}_{(W (i), W (i + 1))}$
605	604	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to ({D (n) ↾}_{(W (i), W (i + 1))}) {lim}_{ℂ} W (i) = ({({D (n) ↾}_{[W (i), W (i + 1)]}) ↾}_{(W (i), W (i + 1))}) {lim}_{ℂ} W (i)$
606	605	adantlr	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to ({D (n) ↾}_{(W (i), W (i + 1))}) {lim}_{ℂ} W (i) = ({({D (n) ↾}_{[W (i), W (i + 1)]}) ↾}_{(W (i), W (i + 1))}) {lim}_{ℂ} W (i)$
607	390	adantlr	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to W (i) \in ℝ$
608	404	adantlr	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to W (i + 1) \in ℝ$
609	294	adantlr	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to W (i) < W (i + 1)$
610	471	ad2antlr	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to D (n) : ℝ ⟶ ℂ$
611	610 595	fssresd	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to ({D (n) ↾}_{[W (i), W (i + 1)]}) : [W (i), W (i + 1)] ⟶ ℂ$
612	607 608 609 611	limciccioolb	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to ({({D (n) ↾}_{[W (i), W (i + 1)]}) ↾}_{(W (i), W (i + 1))}) {lim}_{ℂ} W (i) = ({D (n) ↾}_{[W (i), W (i + 1)]}) {lim}_{ℂ} W (i)$
613	606 612	eqtr2d	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to ({D (n) ↾}_{[W (i), W (i + 1)]}) {lim}_{ℂ} W (i) = ({D (n) ↾}_{(W (i), W (i + 1))}) {lim}_{ℂ} W (i)$
614	601 613	eleqtrd	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to D (n) (W (i)) \in (({D (n) ↾}_{(W (i), W (i + 1))}) {lim}_{ℂ} W (i))$
615	483 488 489 590 614	mullimcf	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to R D (n) (W (i)) \in ((s \in (W (i), W (i + 1)) ⟼ (x \in (W (i), W (i + 1)) ⟼ F (X + x)) (s) ({D (n) ↾}_{(W (i), W (i + 1))}) (s)) {lim}_{ℂ} W (i))$
616		eqidd	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (W (i), W (i + 1))) \to (x \in (W (i), W (i + 1)) ⟼ F (X + x)) = (x \in (W (i), W (i + 1)) ⟼ F (X + x))$
617	192	adantl	$⊢ (((φ \land i \in (0 ..^M)) \land s \in (W (i), W (i + 1))) \land x = s) \to F (X + x) = F (X + s)$
618		simpr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (W (i), W (i + 1))) \to s \in (W (i), W (i + 1))$
619	49	adantr	$⊢ (φ \land s \in (W (i), W (i + 1))) \to F : ℝ ⟶ ℂ$
620	619 383	ffvelrnd	$⊢ (φ \land s \in (W (i), W (i + 1))) \to F (X + s) \in ℂ$
621	620	adantlr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (W (i), W (i + 1))) \to F (X + s) \in ℂ$
622	616 617 618 621	fvmptd	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (W (i), W (i + 1))) \to (x \in (W (i), W (i + 1)) ⟼ F (X + x)) (s) = F (X + s)$
623	622	adantllr	$⊢ (((φ \land n \in ℕ) \land i \in (0 ..^M)) \land s \in (W (i), W (i + 1))) \to (x \in (W (i), W (i + 1)) ⟼ F (X + x)) (s) = F (X + s)$
624		fvres	$⊢ s \in (W (i), W (i + 1)) \to ({D (n) ↾}_{(W (i), W (i + 1))}) (s) = D (n) (s)$
625	624	adantl	$⊢ (((φ \land n \in ℕ) \land i \in (0 ..^M)) \land s \in (W (i), W (i + 1))) \to ({D (n) ↾}_{(W (i), W (i + 1))}) (s) = D (n) (s)$
626	623 625	oveq12d	$⊢ (((φ \land n \in ℕ) \land i \in (0 ..^M)) \land s \in (W (i), W (i + 1))) \to (x \in (W (i), W (i + 1)) ⟼ F (X + x)) (s) ({D (n) ↾}_{(W (i), W (i + 1))}) (s) = F (X + s) D (n) (s)$
627	626	eqcomd	$⊢ (((φ \land n \in ℕ) \land i \in (0 ..^M)) \land s \in (W (i), W (i + 1))) \to F (X + s) D (n) (s) = (x \in (W (i), W (i + 1)) ⟼ F (X + x)) (s) ({D (n) ↾}_{(W (i), W (i + 1))}) (s)$
628	627	mpteq2dva	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to (s \in (W (i), W (i + 1)) ⟼ F (X + s) D (n) (s)) = (s \in (W (i), W (i + 1)) ⟼ (x \in (W (i), W (i + 1)) ⟼ F (X + x)) (s) ({D (n) ↾}_{(W (i), W (i + 1))}) (s))$
629	375 628	eqtr2d	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to (s \in (W (i), W (i + 1)) ⟼ (x \in (W (i), W (i + 1)) ⟼ F (X + x)) (s) ({D (n) ↾}_{(W (i), W (i + 1))}) (s)) = {G ↾}_{(W (i), W (i + 1))}$
630	629	oveq1d	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to (s \in (W (i), W (i + 1)) ⟼ (x \in (W (i), W (i + 1)) ⟼ F (X + x)) (s) ({D (n) ↾}_{(W (i), W (i + 1))}) (s)) {lim}_{ℂ} W (i) = ({G ↾}_{(W (i), W (i + 1))}) {lim}_{ℂ} W (i)$
631	615 630	eleqtrd	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to R D (n) (W (i)) \in (({G ↾}_{(W (i), W (i + 1))}) {lim}_{ℂ} W (i))$
632	455 426	ltned	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (W (i), W (i + 1))) \to X + x \neq Q (i + 1)$
633		eldifsn	$⊢ X + x \in (dom ({F ↾}_{(Q (i), Q (i + 1))}) ∖ \{Q (i + 1)\}) \leftrightarrow (X + x \in dom ({F ↾}_{(Q (i), Q (i + 1))}) \land X + x \neq Q (i + 1))$
634	497 632 633	sylanbrc	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (W (i), W (i + 1))) \to X + x \in (dom ({F ↾}_{(Q (i), Q (i + 1))}) ∖ \{Q (i + 1)\})$
635	634	ralrimiva	$⊢ (φ \land i \in (0 ..^M)) \to \forall x \in (W (i), W (i + 1)) X + x \in (dom ({F ↾}_{(Q (i), Q (i + 1))}) ∖ \{Q (i + 1)\})$
636	503	rnmptss	$⊢ \forall x \in (W (i), W (i + 1)) X + x \in (dom ({F ↾}_{(Q (i), Q (i + 1))}) ∖ \{Q (i + 1)\}) \to ran (x \in (W (i), W (i + 1)) ⟼ X + x) \subseteq dom ({F ↾}_{(Q (i), Q (i + 1))}) ∖ \{Q (i + 1)\}$
637	635 636	syl	$⊢ (φ \land i \in (0 ..^M)) \to ran (x \in (W (i), W (i + 1)) ⟼ X + x) \subseteq dom ({F ↾}_{(Q (i), Q (i + 1))}) ∖ \{Q (i + 1)\}$
638	404	leidd	$⊢ (φ \land i \in (0 ..^M)) \to W (i + 1) \leq W (i + 1)$
639	390 404 404 510 638	eliccd	$⊢ (φ \land i \in (0 ..^M)) \to W (i + 1) \in [W (i), W (i + 1)]$
640	521 639	cnlimci	$⊢ (φ \land i \in (0 ..^M)) \to (x \in [W (i), W (i + 1)] ⟼ X + x) (W (i + 1)) \in ((x \in [W (i), W (i + 1)] ⟼ X + x) {lim}_{ℂ} W (i + 1))$
641		oveq2	$⊢ x = W (i + 1) \to X + x = X + W (i + 1)$
642	641	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land x = W (i + 1)) \to X + x = X + W (i + 1)$
643	277 404	readdcld	$⊢ (φ \land i \in (0 ..^M)) \to X + W (i + 1) \in ℝ$
644	506 642 639 643	fvmptd	$⊢ (φ \land i \in (0 ..^M)) \to (x \in [W (i), W (i + 1)] ⟼ X + x) (W (i + 1)) = X + W (i + 1)$
645	644 424	eqtrd	$⊢ (φ \land i \in (0 ..^M)) \to (x \in [W (i), W (i + 1)] ⟼ X + x) (W (i + 1)) = Q (i + 1)$
646	528	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to (x \in (W (i), W (i + 1)) ⟼ X + x) {lim}_{ℂ} W (i + 1) = ({(x \in [W (i), W (i + 1)] ⟼ X + x) ↾}_{(W (i), W (i + 1))}) {lim}_{ℂ} W (i + 1)$
647	390 404 294 539	limcicciooub	$⊢ (φ \land i \in (0 ..^M)) \to ({(x \in [W (i), W (i + 1)] ⟼ X + x) ↾}_{(W (i), W (i + 1))}) {lim}_{ℂ} W (i + 1) = (x \in [W (i), W (i + 1)] ⟼ X + x) {lim}_{ℂ} W (i + 1)$
648	646 647	eqtr2d	$⊢ (φ \land i \in (0 ..^M)) \to (x \in [W (i), W (i + 1)] ⟼ X + x) {lim}_{ℂ} W (i + 1) = (x \in (W (i), W (i + 1)) ⟼ X + x) {lim}_{ℂ} W (i + 1)$
649	640 645 648	3eltr3d	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ((x \in (W (i), W (i + 1)) ⟼ X + x) {lim}_{ℂ} W (i + 1))$
650	637 649 14	limccog	$⊢ (φ \land i \in (0 ..^M)) \to L \in ((({F ↾}_{(Q (i), Q (i + 1))}) \circ (x \in (W (i), W (i + 1)) ⟼ X + x)) {lim}_{ℂ} W (i + 1))$
651	587	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to (({F ↾}_{(Q (i), Q (i + 1))}) \circ (x \in (W (i), W (i + 1)) ⟼ X + x)) {lim}_{ℂ} W (i + 1) = (x \in (W (i), W (i + 1)) ⟼ F (X + x)) {lim}_{ℂ} W (i + 1)$
652	650 651	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to L \in ((x \in (W (i), W (i + 1)) ⟼ F (X + x)) {lim}_{ℂ} W (i + 1))$
653	652	adantlr	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to L \in ((x \in (W (i), W (i + 1)) ⟼ F (X + x)) {lim}_{ℂ} W (i + 1))$
654	639	adantlr	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to W (i + 1) \in [W (i), W (i + 1)]$
655	598 654	cnlimci	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to ({D (n) ↾}_{[W (i), W (i + 1)]}) (W (i + 1)) \in (({D (n) ↾}_{[W (i), W (i + 1)]}) {lim}_{ℂ} W (i + 1))$
656		fvres	$⊢ W (i + 1) \in [W (i), W (i + 1)] \to ({D (n) ↾}_{[W (i), W (i + 1)]}) (W (i + 1)) = D (n) (W (i + 1))$
657	654 656	syl	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to ({D (n) ↾}_{[W (i), W (i + 1)]}) (W (i + 1)) = D (n) (W (i + 1))$
658	607 608 609 611	limcicciooub	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to ({({D (n) ↾}_{[W (i), W (i + 1)]}) ↾}_{(W (i), W (i + 1))}) {lim}_{ℂ} W (i + 1) = ({D (n) ↾}_{[W (i), W (i + 1)]}) {lim}_{ℂ} W (i + 1)$
659	658	eqcomd	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to ({D (n) ↾}_{[W (i), W (i + 1)]}) {lim}_{ℂ} W (i + 1) = ({({D (n) ↾}_{[W (i), W (i + 1)]}) ↾}_{(W (i), W (i + 1))}) {lim}_{ℂ} W (i + 1)$
660		resabs1	$⊢ (W (i), W (i + 1)) \subseteq [W (i), W (i + 1)] \to {({D (n) ↾}_{[W (i), W (i + 1)]}) ↾}_{(W (i), W (i + 1))} = {D (n) ↾}_{(W (i), W (i + 1))}$
661	524 660	mp1i	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to {({D (n) ↾}_{[W (i), W (i + 1)]}) ↾}_{(W (i), W (i + 1))} = {D (n) ↾}_{(W (i), W (i + 1))}$
662	661	oveq1d	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to ({({D (n) ↾}_{[W (i), W (i + 1)]}) ↾}_{(W (i), W (i + 1))}) {lim}_{ℂ} W (i + 1) = ({D (n) ↾}_{(W (i), W (i + 1))}) {lim}_{ℂ} W (i + 1)$
663	659 662	eqtrd	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to ({D (n) ↾}_{[W (i), W (i + 1)]}) {lim}_{ℂ} W (i + 1) = ({D (n) ↾}_{(W (i), W (i + 1))}) {lim}_{ℂ} W (i + 1)$
664	655 657 663	3eltr3d	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to D (n) (W (i + 1)) \in (({D (n) ↾}_{(W (i), W (i + 1))}) {lim}_{ℂ} W (i + 1))$
665	483 488 489 653 664	mullimcf	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to L D (n) (W (i + 1)) \in ((s \in (W (i), W (i + 1)) ⟼ (x \in (W (i), W (i + 1)) ⟼ F (X + x)) (s) ({D (n) ↾}_{(W (i), W (i + 1))}) (s)) {lim}_{ℂ} W (i + 1))$
666	629	oveq1d	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to (s \in (W (i), W (i + 1)) ⟼ (x \in (W (i), W (i + 1)) ⟼ F (X + x)) (s) ({D (n) ↾}_{(W (i), W (i + 1))}) (s)) {lim}_{ℂ} W (i + 1) = ({G ↾}_{(W (i), W (i + 1))}) {lim}_{ℂ} W (i + 1)$
667	665 666	eleqtrd	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to L D (n) (W (i + 1)) \in (({G ↾}_{(W (i), W (i + 1))}) {lim}_{ℂ} W (i + 1))$
668	130 133 225 226 16 114 300 211 369 478 631 667	fourierdlem110	$⊢ (φ \land n \in ℕ) \to \int_{[(- π) - X - (- X), π - X - (- X)]} G (x) d x = \int_{[- π - X, π - X]} G (x) d x$
669	668	eqcomd	$⊢ (φ \land n \in ℕ) \to \int_{[- π - X, π - X]} G (x) d x = \int_{[(- π) - X - (- X), π - X - (- X)]} G (x) d x$
670	129	recnd	$⊢ φ \to - π - X \in ℂ$
671	670 154	subnegd	$⊢ φ \to (- π) - X - (- X) = (- π) - X + X$
672	156 154	npcand	$⊢ φ \to (- π) - X + X = - π$
673	671 672	eqtrd	$⊢ φ \to (- π) - X - (- X) = - π$
674	132	recnd	$⊢ φ \to π - X \in ℂ$
675	674 154	subnegd	$⊢ φ \to π - X - (- X) = π - X + X$
676	155 154	npcand	$⊢ φ \to π - X + X = π$
677	675 676	eqtrd	$⊢ φ \to π - X - (- X) = π$
678	673 677	oveq12d	$⊢ φ \to [(- π) - X - (- X), π - X - (- X)] = [- π, π]$
679	678	itgeq1d	$⊢ φ \to \int_{[(- π) - X - (- X), π - X - (- X)]} G (x) d x = \int_{[- π, π]} G (x) d x$
680	679	adantr	$⊢ (φ \land n \in ℕ) \to \int_{[(- π) - X - (- X), π - X - (- X)]} G (x) d x = \int_{[- π, π]} G (x) d x$
681	669 680	eqtrd	$⊢ (φ \land n \in ℕ) \to \int_{[- π - X, π - X]} G (x) d x = \int_{[- π, π]} G (x) d x$
682		fveq2	$⊢ x = s \to G (x) = G (s)$
683	682	cbvitgv	$⊢ \int_{(- π, π)} G (x) d x = \int_{(- π, π)} G (s) d s$
684	211	adantr	$⊢ ((φ \land n \in ℕ) \land x \in [- π, π]) \to G : ℝ ⟶ ℂ$
685	44	adantlr	$⊢ ((φ \land n \in ℕ) \land x \in [- π, π]) \to x \in ℝ$
686	684 685	ffvelrnd	$⊢ ((φ \land n \in ℕ) \land x \in [- π, π]) \to G (x) \in ℂ$
687	76 77 686	itgioo	$⊢ (φ \land n \in ℕ) \to \int_{(- π, π)} G (x) d x = \int_{[- π, π]} G (x) d x$
688		elioore	$⊢ s \in (- π, π) \to s \in ℝ$
689	688	adantl	$⊢ ((φ \land n \in ℕ) \land s \in (- π, π)) \to s \in ℝ$
690	49	adantr	$⊢ (φ \land s \in (- π, π)) \to F : ℝ ⟶ ℂ$
691	8	adantr	$⊢ (φ \land s \in (- π, π)) \to X \in ℝ$
692	688	adantl	$⊢ (φ \land s \in (- π, π)) \to s \in ℝ$
693	691 692	readdcld	$⊢ (φ \land s \in (- π, π)) \to X + s \in ℝ$
694	690 693	ffvelrnd	$⊢ (φ \land s \in (- π, π)) \to F (X + s) \in ℂ$
695	694	adantlr	$⊢ ((φ \land n \in ℕ) \land s \in (- π, π)) \to F (X + s) \in ℂ$
696	82	ad2antlr	$⊢ ((φ \land n \in ℕ) \land s \in (- π, π)) \to D (n) : ℝ ⟶ ℝ$
697	696 689	ffvelrnd	$⊢ ((φ \land n \in ℕ) \land s \in (- π, π)) \to D (n) (s) \in ℝ$
698	697	recnd	$⊢ ((φ \land n \in ℕ) \land s \in (- π, π)) \to D (n) (s) \in ℂ$
699	695 698	mulcld	$⊢ ((φ \land n \in ℕ) \land s \in (- π, π)) \to F (X + s) D (n) (s) \in ℂ$
700	689 699 197	syl2anc	$⊢ ((φ \land n \in ℕ) \land s \in (- π, π)) \to G (s) = F (X + s) D (n) (s)$
701	700	itgeq2dv	$⊢ (φ \land n \in ℕ) \to \int_{(- π, π)} G (s) d s = \int_{(- π, π)} F (X + s) D (n) (s) d s$
702	683 687 701	3eqtr3a	$⊢ (φ \land n \in ℕ) \to \int_{[- π, π]} G (x) d x = \int_{(- π, π)} F (X + s) D (n) (s) d s$
703	224 681 702	3eqtrd	$⊢ (φ \land n \in ℕ) \to \int_{(- π - X, π - X)} F (X + s) D (n) (s) d s = \int_{(- π, π)} F (X + s) D (n) (s) d s$
704	75 178 703	3eqtrd	$⊢ (φ \land n \in ℕ) \to S (n) = \int_{(- π, π)} F (X + s) D (n) (s) d s$
705	77	renegcld	$⊢ (φ \land n \in ℕ) \to - π \in ℝ$
706		0red	$⊢ (φ \land n \in ℕ) \to 0 \in ℝ$
707		0re	$⊢ 0 \in ℝ$
708		negpilt0	$⊢ - π < 0$
709	39 707 708	ltleii	$⊢ - π \leq 0$
710	709	a1i	$⊢ (φ \land n \in ℕ) \to - π \leq 0$
711		pipos	$⊢ 0 < π$
712	707 38 711	ltleii	$⊢ 0 \leq π$
713	712	a1i	$⊢ (φ \land n \in ℕ) \to 0 \leq π$
714	76 77 706 710 713	eliccd	$⊢ (φ \land n \in ℕ) \to 0 \in [- π, π]$
715		ioossicc	$⊢ (- π, 0) \subseteq [- π, 0]$
716	715	a1i	$⊢ (φ \land n \in ℕ) \to (- π, 0) \subseteq [- π, 0]$
717		ioombl	$⊢ (- π, 0) \in dom vol$
718	717	a1i	$⊢ (φ \land n \in ℕ) \to (- π, 0) \in dom vol$
719	49	adantr	$⊢ (φ \land s \in [- π, 0]) \to F : ℝ ⟶ ℂ$
720	8	adantr	$⊢ (φ \land s \in [- π, 0]) \to X \in ℝ$
721	39	a1i	$⊢ s \in [- π, 0] \to - π \in ℝ$
722		0red	$⊢ s \in [- π, 0] \to 0 \in ℝ$
723		id	$⊢ s \in [- π, 0] \to s \in [- π, 0]$
724		eliccre	$⊢ (- π \in ℝ \land 0 \in ℝ \land s \in [- π, 0]) \to s \in ℝ$
725	721 722 723 724	syl3anc	$⊢ s \in [- π, 0] \to s \in ℝ$
726	725	adantl	$⊢ (φ \land s \in [- π, 0]) \to s \in ℝ$
727	720 726	readdcld	$⊢ (φ \land s \in [- π, 0]) \to X + s \in ℝ$
728	719 727	ffvelrnd	$⊢ (φ \land s \in [- π, 0]) \to F (X + s) \in ℂ$
729	728	adantlr	$⊢ ((φ \land n \in ℕ) \land s \in [- π, 0]) \to F (X + s) \in ℂ$
730	82	ad2antlr	$⊢ ((φ \land n \in ℕ) \land s \in [- π, 0]) \to D (n) : ℝ ⟶ ℝ$
731	725	adantl	$⊢ ((φ \land n \in ℕ) \land s \in [- π, 0]) \to s \in ℝ$
732	730 731	ffvelrnd	$⊢ ((φ \land n \in ℕ) \land s \in [- π, 0]) \to D (n) (s) \in ℝ$
733	732	recnd	$⊢ ((φ \land n \in ℕ) \land s \in [- π, 0]) \to D (n) (s) \in ℂ$
734	729 733	mulcld	$⊢ ((φ \land n \in ℕ) \land s \in [- π, 0]) \to F (X + s) D (n) (s) \in ℂ$
735	731 734 197	syl2anc	$⊢ ((φ \land n \in ℕ) \land s \in [- π, 0]) \to G (s) = F (X + s) D (n) (s)$
736	735	eqcomd	$⊢ ((φ \land n \in ℕ) \land s \in [- π, 0]) \to F (X + s) D (n) (s) = G (s)$
737	736	mpteq2dva	$⊢ (φ \land n \in ℕ) \to (s \in [- π, 0] ⟼ F (X + s) D (n) (s)) = (s \in [- π, 0] ⟼ G (s))$
738	306	oveq2d	$⊢ φ \to s + (π - X) - (- π - X) = s + T$
739	738	ad2antrr	$⊢ ((φ \land n \in ℕ) \land s \in ℝ) \to s + (π - X) - (- π - X) = s + T$
740	739	fveq2d	$⊢ ((φ \land n \in ℕ) \land s \in ℝ) \to G (s + (π - X) - (- π - X)) = G (s + T)$
741	11	a1i	$⊢ ((φ \land n \in ℕ) \land s \in ℝ) \to G = (x \in ℝ ⟼ F (X + x) D (n) (x))$
742		oveq2	$⊢ x = s + T \to X + x = X + s + T$
743	742	fveq2d	$⊢ x = s + T \to F (X + x) = F (X + s + T)$
744		fveq2	$⊢ x = s + T \to D (n) (x) = D (n) (s + T)$
745	743 744	oveq12d	$⊢ x = s + T \to F (X + x) D (n) (x) = F (X + s + T) D (n) (s + T)$
746	745	adantl	$⊢ (((φ \land n \in ℕ) \land s \in ℝ) \land x = s + T) \to F (X + x) D (n) (x) = F (X + s + T) D (n) (s + T)$
747		simpr	$⊢ (φ \land s \in ℝ) \to s \in ℝ$
748	317	a1i	$⊢ (φ \land s \in ℝ) \to T \in ℝ$
749	747 748	readdcld	$⊢ (φ \land s \in ℝ) \to s + T \in ℝ$
750	749	adantlr	$⊢ ((φ \land n \in ℕ) \land s \in ℝ) \to s + T \in ℝ$
751	49	adantr	$⊢ (φ \land s \in ℝ) \to F : ℝ ⟶ ℂ$
752	8	adantr	$⊢ (φ \land s \in ℝ) \to X \in ℝ$
753	752 749	readdcld	$⊢ (φ \land s \in ℝ) \to X + s + T \in ℝ$
754	751 753	ffvelrnd	$⊢ (φ \land s \in ℝ) \to F (X + s + T) \in ℂ$
755	754	adantlr	$⊢ ((φ \land n \in ℕ) \land s \in ℝ) \to F (X + s + T) \in ℂ$
756	82	ad2antlr	$⊢ ((φ \land n \in ℕ) \land s \in ℝ) \to D (n) : ℝ ⟶ ℝ$
757	756 750	ffvelrnd	$⊢ ((φ \land n \in ℕ) \land s \in ℝ) \to D (n) (s + T) \in ℝ$
758	757	recnd	$⊢ ((φ \land n \in ℕ) \land s \in ℝ) \to D (n) (s + T) \in ℂ$
759	755 758	mulcld	$⊢ ((φ \land n \in ℕ) \land s \in ℝ) \to F (X + s + T) D (n) (s + T) \in ℂ$
760	741 746 750 759	fvmptd	$⊢ ((φ \land n \in ℕ) \land s \in ℝ) \to G (s + T) = F (X + s + T) D (n) (s + T)$
761	154	adantr	$⊢ (φ \land s \in ℝ) \to X \in ℂ$
762	747	recnd	$⊢ (φ \land s \in ℝ) \to s \in ℂ$
763	319	adantr	$⊢ (φ \land s \in ℝ) \to T \in ℂ$
764	761 762 763	addassd	$⊢ (φ \land s \in ℝ) \to X + s + T = X + s + T$
765	764	eqcomd	$⊢ (φ \land s \in ℝ) \to X + s + T = X + s + T$
766	765	fveq2d	$⊢ (φ \land s \in ℝ) \to F (X + s + T) = F (X + s + T)$
767	752 747	readdcld	$⊢ (φ \land s \in ℝ) \to X + s \in ℝ$
768		simpl	$⊢ (φ \land s \in ℝ) \to φ$
769	768 767	jca	$⊢ (φ \land s \in ℝ) \to (φ \land X + s \in ℝ)$
770		eleq1	$⊢ x = X + s \to (x \in ℝ \leftrightarrow X + s \in ℝ)$
771	770	anbi2d	$⊢ x = X + s \to ((φ \land x \in ℝ) \leftrightarrow (φ \land X + s \in ℝ))$
772		oveq1	$⊢ x = X + s \to x + T = X + s + T$
773	772	fveq2d	$⊢ x = X + s \to F (x + T) = F (X + s + T)$
774	773 435	eqeq12d	$⊢ x = X + s \to (F (x + T) = F (x) \leftrightarrow F (X + s + T) = F (X + s))$
775	771 774	imbi12d	$⊢ x = X + s \to (((φ \land x \in ℝ) \to F (x + T) = F (x)) \leftrightarrow ((φ \land X + s \in ℝ) \to F (X + s + T) = F (X + s)))$
776	775 10	vtoclg	$⊢ X + s \in ℝ \to ((φ \land X + s \in ℝ) \to F (X + s + T) = F (X + s))$
777	767 769 776	sylc	$⊢ (φ \land s \in ℝ) \to F (X + s + T) = F (X + s)$
778	766 777	eqtrd	$⊢ (φ \land s \in ℝ) \to F (X + s + T) = F (X + s)$
779	778	adantlr	$⊢ ((φ \land n \in ℕ) \land s \in ℝ) \to F (X + s + T) = F (X + s)$
780	4 15	dirkerper	$⊢ (n \in ℕ \land s \in ℝ) \to D (n) (s + T) = D (n) (s)$
781	780	adantll	$⊢ ((φ \land n \in ℕ) \land s \in ℝ) \to D (n) (s + T) = D (n) (s)$
782	779 781	oveq12d	$⊢ ((φ \land n \in ℕ) \land s \in ℝ) \to F (X + s + T) D (n) (s + T) = F (X + s) D (n) (s)$
783		simpr	$⊢ ((φ \land n \in ℕ) \land s \in ℝ) \to s \in ℝ$
784	782 759	eqeltrrd	$⊢ ((φ \land n \in ℕ) \land s \in ℝ) \to F (X + s) D (n) (s) \in ℂ$
785	783 784 197	syl2anc	$⊢ ((φ \land n \in ℕ) \land s \in ℝ) \to G (s) = F (X + s) D (n) (s)$
786	785	eqcomd	$⊢ ((φ \land n \in ℕ) \land s \in ℝ) \to F (X + s) D (n) (s) = G (s)$
787	782 786	eqtrd	$⊢ ((φ \land n \in ℕ) \land s \in ℝ) \to F (X + s + T) D (n) (s + T) = G (s)$
788	740 760 787	3eqtrd	$⊢ ((φ \land n \in ℕ) \land s \in ℝ) \to G (s + (π - X) - (- π - X)) = G (s)$
789		0ltpnf	$⊢ 0 < +∞$
790		pnfxr	$⊢ +∞ \in ℝ^{*}$
791		elioo2	$⊢ (- π \in ℝ^{} \land +∞ \in ℝ^{}) \to (0 \in (- π, +∞) \leftrightarrow (0 \in ℝ \land - π < 0 \land 0 < +∞))$
792	52 790 791	mp2an	$⊢ 0 \in (- π, +∞) \leftrightarrow (0 \in ℝ \land - π < 0 \land 0 < +∞)$
793	707 708 789 792	mpbir3an	$⊢ 0 \in (- π, +∞)$
794	793	a1i	$⊢ (φ \land n \in ℕ) \to 0 \in (- π, +∞)$
795	16 225 114 300 211 788 478 631 667 76 794	fourierdlem105	$⊢ (φ \land n \in ℕ) \to (s \in [- π, 0] ⟼ G (s)) \in 𝐿^{1}$
796	737 795	eqeltrd	$⊢ (φ \land n \in ℕ) \to (s \in [- π, 0] ⟼ F (X + s) D (n) (s)) \in 𝐿^{1}$
797	716 718 734 796	iblss	$⊢ (φ \land n \in ℕ) \to (s \in (- π, 0) ⟼ F (X + s) D (n) (s)) \in 𝐿^{1}$
798		elioore	$⊢ s \in (0, π) \to s \in ℝ$
799	798	adantl	$⊢ ((φ \land n \in ℕ) \land s \in (0, π)) \to s \in ℝ$
800	799 784	syldan	$⊢ ((φ \land n \in ℕ) \land s \in (0, π)) \to F (X + s) D (n) (s) \in ℂ$
801	799 800 197	syl2anc	$⊢ ((φ \land n \in ℕ) \land s \in (0, π)) \to G (s) = F (X + s) D (n) (s)$
802	801	eqcomd	$⊢ ((φ \land n \in ℕ) \land s \in (0, π)) \to F (X + s) D (n) (s) = G (s)$
803	802	mpteq2dva	$⊢ (φ \land n \in ℕ) \to (s \in (0, π) ⟼ F (X + s) D (n) (s)) = (s \in (0, π) ⟼ G (s))$
804		ioossicc	$⊢ (0, π) \subseteq [0, π]$
805	804	a1i	$⊢ (φ \land n \in ℕ) \to (0, π) \subseteq [0, π]$
806		ioombl	$⊢ (0, π) \in dom vol$
807	806	a1i	$⊢ (φ \land n \in ℕ) \to (0, π) \in dom vol$
808	211	adantr	$⊢ ((φ \land n \in ℕ) \land s \in [0, π]) \to G : ℝ ⟶ ℂ$
809		0red	$⊢ (φ \land s \in [0, π]) \to 0 \in ℝ$
810	38	a1i	$⊢ (φ \land s \in [0, π]) \to π \in ℝ$
811		simpr	$⊢ (φ \land s \in [0, π]) \to s \in [0, π]$
812		eliccre	$⊢ (0 \in ℝ \land π \in ℝ \land s \in [0, π]) \to s \in ℝ$
813	809 810 811 812	syl3anc	$⊢ (φ \land s \in [0, π]) \to s \in ℝ$
814	813	adantlr	$⊢ ((φ \land n \in ℕ) \land s \in [0, π]) \to s \in ℝ$
815	808 814	ffvelrnd	$⊢ ((φ \land n \in ℕ) \land s \in [0, π]) \to G (s) \in ℂ$
816		0xr	$⊢ 0 \in ℝ^{*}$
817	816	a1i	$⊢ (φ \land n \in ℕ) \to 0 \in ℝ^{*}$
818	790	a1i	$⊢ (φ \land n \in ℕ) \to +∞ \in ℝ^{*}$
819	711	a1i	$⊢ (φ \land n \in ℕ) \to 0 < π$
820		ltpnf	$⊢ π \in ℝ \to π < +∞$
821	38 820	mp1i	$⊢ (φ \land n \in ℕ) \to π < +∞$
822	817 818 77 819 821	eliood	$⊢ (φ \land n \in ℕ) \to π \in (0, +∞)$
823	16 225 114 300 211 788 478 631 667 706 822	fourierdlem105	$⊢ (φ \land n \in ℕ) \to (s \in [0, π] ⟼ G (s)) \in 𝐿^{1}$
824	805 807 815 823	iblss	$⊢ (φ \land n \in ℕ) \to (s \in (0, π) ⟼ G (s)) \in 𝐿^{1}$
825	803 824	eqeltrd	$⊢ (φ \land n \in ℕ) \to (s \in (0, π) ⟼ F (X + s) D (n) (s)) \in 𝐿^{1}$
826	705 77 714 699 797 825	itgsplitioo	$⊢ (φ \land n \in ℕ) \to \int_{(- π, π)} F (X + s) D (n) (s) d s = \int_{(- π, 0)} F (X + s) D (n) (s) d s + \int_{(0, π)} F (X + s) D (n) (s) d s$
827	704 826	eqtrd	$⊢ (φ \land n \in ℕ) \to S (n) = \int_{(- π, 0)} F (X + s) D (n) (s) d s + \int_{(0, π)} F (X + s) D (n) (s) d s$

Metamath Proof Explorer

Theorem fourierdlem111

Proof