fourierdlem92

Description: The integral of a piecewise continuous periodic function F is unchanged if the domain is shifted by its period T . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem92.a	$⊢ φ \to A \in ℝ$
	fourierdlem92.b	$⊢ φ \to B \in ℝ$
	fourierdlem92.p	$⊢ P = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A \land p (m) = B) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
	fourierdlem92.m	$⊢ φ \to M \in ℕ$
	fourierdlem92.t	$⊢ φ \to T \in ℝ$
	fourierdlem92.q	$⊢ φ \to Q \in P (M)$
	fourierdlem92.fper	$⊢ (φ \land x \in [A, B]) \to F (x + T) = F (x)$
	fourierdlem92.s	$⊢ S = (i \in (0 \dots M) ⟼ Q (i) + T)$
	fourierdlem92.h	$⊢ H = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A + T \land p (m) = B + T) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
	fourierdlem92.f	$⊢ φ \to F : ℝ ⟶ ℂ$
	fourierdlem92.cncf	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
	fourierdlem92.r	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
	fourierdlem92.l	$⊢ (φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
Assertion	fourierdlem92	$⊢ φ \to \int_{[A + T, B + T]} F (x) d x = \int_{[A, B]} F (x) d x$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem92.a	$⊢ φ \to A \in ℝ$
2		fourierdlem92.b	$⊢ φ \to B \in ℝ$
3		fourierdlem92.p	$⊢ P = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A \land p (m) = B) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
4		fourierdlem92.m	$⊢ φ \to M \in ℕ$
5		fourierdlem92.t	$⊢ φ \to T \in ℝ$
6		fourierdlem92.q	$⊢ φ \to Q \in P (M)$
7		fourierdlem92.fper	$⊢ (φ \land x \in [A, B]) \to F (x + T) = F (x)$
8		fourierdlem92.s	$⊢ S = (i \in (0 \dots M) ⟼ Q (i) + T)$
9		fourierdlem92.h	$⊢ H = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A + T \land p (m) = B + T) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
10		fourierdlem92.f	$⊢ φ \to F : ℝ ⟶ ℂ$
11		fourierdlem92.cncf	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
12		fourierdlem92.r	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
13		fourierdlem92.l	$⊢ (φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
14	1	adantr	$⊢ (φ \land 0 < T) \to A \in ℝ$
15	2	adantr	$⊢ (φ \land 0 < T) \to B \in ℝ$
16	4	adantr	$⊢ (φ \land 0 < T) \to M \in ℕ$
17	5	adantr	$⊢ (φ \land 0 < T) \to T \in ℝ$
18		simpr	$⊢ (φ \land 0 < T) \to 0 < T$
19	17 18	elrpd	$⊢ (φ \land 0 < T) \to T \in ℝ^{+}$
20	6	adantr	$⊢ (φ \land 0 < T) \to Q \in P (M)$
21	7	adantlr	$⊢ ((φ \land 0 < T) \land x \in [A, B]) \to F (x + T) = F (x)$
22		fveq2	$⊢ j = i \to Q (j) = Q (i)$
23	22	oveq1d	$⊢ j = i \to Q (j) + T = Q (i) + T$
24	23	cbvmptv	$⊢ (j \in (0 \dots M) ⟼ Q (j) + T) = (i \in (0 \dots M) ⟼ Q (i) + T)$
25	10	adantr	$⊢ (φ \land 0 < T) \to F : ℝ ⟶ ℂ$
26	11	adantlr	$⊢ ((φ \land 0 < T) \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
27	12	adantlr	$⊢ ((φ \land 0 < T) \land i \in (0 ..^M)) \to R \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
28	13	adantlr	$⊢ ((φ \land 0 < T) \land i \in (0 ..^M)) \to L \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
29		eqeq1	$⊢ y = x \to (y = Q (i) \leftrightarrow x = Q (i))$
30		eqeq1	$⊢ y = x \to (y = Q (i + 1) \leftrightarrow x = Q (i + 1))$
31		fveq2	$⊢ y = x \to F (y) = F (x)$
32	30 31	ifbieq2d	$⊢ y = x \to if (y = Q (i + 1), L, F (y)) = if (x = Q (i + 1), L, F (x))$
33	29 32	ifbieq2d	$⊢ y = x \to if (y = Q (i), R, if (y = Q (i + 1), L, F (y))) = if (x = Q (i), R, if (x = Q (i + 1), L, F (x)))$
34	33	cbvmptv	$⊢ (y \in [Q (i), Q (i + 1)] ⟼ if (y = Q (i), R, if (y = Q (i + 1), L, F (y)))) = (x \in [Q (i), Q (i + 1)] ⟼ if (x = Q (i), R, if (x = Q (i + 1), L, F (x))))$
35		eqid	$⊢ (x \in [(j \in (0 \dots M) ⟼ Q (j) + T) (i), (j \in (0 \dots M) ⟼ Q (j) + T) (i + 1)] ⟼ (y \in [Q (i), Q (i + 1)] ⟼ if (y = Q (i), R, if (y = Q (i + 1), L, F (y)))) (x - T)) = (x \in [(j \in (0 \dots M) ⟼ Q (j) + T) (i), (j \in (0 \dots M) ⟼ Q (j) + T) (i + 1)] ⟼ (y \in [Q (i), Q (i + 1)] ⟼ if (y = Q (i), R, if (y = Q (i + 1), L, F (y)))) (x - T))$
36	14 15 3 16 19 20 21 24 25 26 27 28 34 35	fourierdlem81	$⊢ (φ \land 0 < T) \to \int_{[A + T, B + T]} F (x) d x = \int_{[A, B]} F (x) d x$
37		simpr	$⊢ (φ \land T = 0) \to T = 0$
38	37	oveq2d	$⊢ (φ \land T = 0) \to A + T = A + 0$
39	1	recnd	$⊢ φ \to A \in ℂ$
40	39	adantr	$⊢ (φ \land T = 0) \to A \in ℂ$
41	40	addridd	$⊢ (φ \land T = 0) \to A + 0 = A$
42	38 41	eqtrd	$⊢ (φ \land T = 0) \to A + T = A$
43	37	oveq2d	$⊢ (φ \land T = 0) \to B + T = B + 0$
44	2	recnd	$⊢ φ \to B \in ℂ$
45	44	adantr	$⊢ (φ \land T = 0) \to B \in ℂ$
46	45	addridd	$⊢ (φ \land T = 0) \to B + 0 = B$
47	43 46	eqtrd	$⊢ (φ \land T = 0) \to B + T = B$
48	42 47	oveq12d	$⊢ (φ \land T = 0) \to [A + T, B + T] = [A, B]$
49	48	itgeq1d	$⊢ (φ \land T = 0) \to \int_{[A + T, B + T]} F (x) d x = \int_{[A, B]} F (x) d x$
50	49	adantlr	$⊢ ((φ \land \neg 0 < T) \land T = 0) \to \int_{[A + T, B + T]} F (x) d x = \int_{[A, B]} F (x) d x$
51		simpll	$⊢ ((φ \land \neg 0 < T) \land \neg T = 0) \to φ$
52		simpr	$⊢ ((φ \land \neg 0 < T) \land \neg T = 0) \to \neg T = 0$
53		simplr	$⊢ ((φ \land \neg 0 < T) \land \neg T = 0) \to \neg 0 < T$
54		ioran	$⊢ \neg (T = 0 \lor 0 < T) \leftrightarrow (\neg T = 0 \land \neg 0 < T)$
55	52 53 54	sylanbrc	$⊢ ((φ \land \neg 0 < T) \land \neg T = 0) \to \neg (T = 0 \lor 0 < T)$
56	51 5	syl	$⊢ ((φ \land \neg 0 < T) \land \neg T = 0) \to T \in ℝ$
57		0red	$⊢ ((φ \land \neg 0 < T) \land \neg T = 0) \to 0 \in ℝ$
58	56 57	lttrid	$⊢ ((φ \land \neg 0 < T) \land \neg T = 0) \to (T < 0 \leftrightarrow \neg (T = 0 \lor 0 < T))$
59	55 58	mpbird	$⊢ ((φ \land \neg 0 < T) \land \neg T = 0) \to T < 0$
60	56	lt0neg1d	$⊢ ((φ \land \neg 0 < T) \land \neg T = 0) \to (T < 0 \leftrightarrow 0 < - T)$
61	59 60	mpbid	$⊢ ((φ \land \neg 0 < T) \land \neg T = 0) \to 0 < - T$
62	1 5	readdcld	$⊢ φ \to A + T \in ℝ$
63	62	recnd	$⊢ φ \to A + T \in ℂ$
64	5	recnd	$⊢ φ \to T \in ℂ$
65	63 64	negsubd	$⊢ φ \to A + T + (- T) = A + T - T$
66	39 64	pncand	$⊢ φ \to A + T - T = A$
67	65 66	eqtrd	$⊢ φ \to A + T + (- T) = A$
68	2 5	readdcld	$⊢ φ \to B + T \in ℝ$
69	68	recnd	$⊢ φ \to B + T \in ℂ$
70	69 64	negsubd	$⊢ φ \to B + T + (- T) = B + T - T$
71	44 64	pncand	$⊢ φ \to B + T - T = B$
72	70 71	eqtrd	$⊢ φ \to B + T + (- T) = B$
73	67 72	oveq12d	$⊢ φ \to [A + T + (- T), B + T + (- T)] = [A, B]$
74	73	eqcomd	$⊢ φ \to [A, B] = [A + T + (- T), B + T + (- T)]$
75	74	itgeq1d	$⊢ φ \to \int_{[A, B]} F (x) d x = \int_{[A + T + (- T), B + T + (- T)]} F (x) d x$
76	75	adantr	$⊢ (φ \land 0 < - T) \to \int_{[A, B]} F (x) d x = \int_{[A + T + (- T), B + T + (- T)]} F (x) d x$
77	1	adantr	$⊢ (φ \land 0 < - T) \to A \in ℝ$
78	5	adantr	$⊢ (φ \land 0 < - T) \to T \in ℝ$
79	77 78	readdcld	$⊢ (φ \land 0 < - T) \to A + T \in ℝ$
80	2	adantr	$⊢ (φ \land 0 < - T) \to B \in ℝ$
81	80 78	readdcld	$⊢ (φ \land 0 < - T) \to B + T \in ℝ$
82		eqid	$⊢ (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A + T \land p (m) = B + T) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\}) = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A + T \land p (m) = B + T) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
83	4	adantr	$⊢ (φ \land 0 < - T) \to M \in ℕ$
84	78	renegcld	$⊢ (φ \land 0 < - T) \to - T \in ℝ$
85		simpr	$⊢ (φ \land 0 < - T) \to 0 < - T$
86	84 85	elrpd	$⊢ (φ \land 0 < - T) \to - T \in ℝ^{+}$
87	3	fourierdlem2	$⊢ M \in ℕ \to (Q \in P (M) \leftrightarrow (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))))$
88	4 87	syl	$⊢ φ \to (Q \in P (M) \leftrightarrow (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))))$
89	6 88	mpbid	$⊢ φ \to (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1)))$
90	89	simpld	$⊢ φ \to Q \in (ℝ^{(0 \dots M)})$
91		elmapi	$⊢ Q \in (ℝ^{(0 \dots M)}) \to Q : (0 \dots M) ⟶ ℝ$
92	90 91	syl	$⊢ φ \to Q : (0 \dots M) ⟶ ℝ$
93	92	ffvelcdmda	$⊢ (φ \land i \in (0 \dots M)) \to Q (i) \in ℝ$
94	5	adantr	$⊢ (φ \land i \in (0 \dots M)) \to T \in ℝ$
95	93 94	readdcld	$⊢ (φ \land i \in (0 \dots M)) \to Q (i) + T \in ℝ$
96	95 8	fmptd	$⊢ φ \to S : (0 \dots M) ⟶ ℝ$
97		reex	$⊢ ℝ \in V$
98	97	a1i	$⊢ φ \to ℝ \in V$
99		ovex	$⊢ (0 \dots M) \in V$
100	99	a1i	$⊢ φ \to (0 \dots M) \in V$
101	98 100	elmapd	$⊢ φ \to (S \in (ℝ^{(0 \dots M)}) \leftrightarrow S : (0 \dots M) ⟶ ℝ)$
102	96 101	mpbird	$⊢ φ \to S \in (ℝ^{(0 \dots M)})$
103	8	a1i	$⊢ φ \to S = (i \in (0 \dots M) ⟼ Q (i) + T)$
104		fveq2	$⊢ i = 0 \to Q (i) = Q (0)$
105	104	oveq1d	$⊢ i = 0 \to Q (i) + T = Q (0) + T$
106	105	adantl	$⊢ (φ \land i = 0) \to Q (i) + T = Q (0) + T$
107		0zd	$⊢ φ \to 0 \in ℤ$
108	4	nnzd	$⊢ φ \to M \in ℤ$
109		0le0	$⊢ 0 \leq 0$
110	109	a1i	$⊢ φ \to 0 \leq 0$
111		nnnn0	$⊢ M \in ℕ \to M \in ℕ_{0}$
112	111	nn0ge0d	$⊢ M \in ℕ \to 0 \leq M$
113	4 112	syl	$⊢ φ \to 0 \leq M$
114	107 108 107 110 113	elfzd	$⊢ φ \to 0 \in (0 \dots M)$
115	92 114	ffvelcdmd	$⊢ φ \to Q (0) \in ℝ$
116	115 5	readdcld	$⊢ φ \to Q (0) + T \in ℝ$
117	103 106 114 116	fvmptd	$⊢ φ \to S (0) = Q (0) + T$
118		simprll	$⊢ (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))) \to Q (0) = A$
119	89 118	syl	$⊢ φ \to Q (0) = A$
120	119	oveq1d	$⊢ φ \to Q (0) + T = A + T$
121	117 120	eqtrd	$⊢ φ \to S (0) = A + T$
122		fveq2	$⊢ i = M \to Q (i) = Q (M)$
123	122	oveq1d	$⊢ i = M \to Q (i) + T = Q (M) + T$
124	123	adantl	$⊢ (φ \land i = M) \to Q (i) + T = Q (M) + T$
125	4	nnnn0d	$⊢ φ \to M \in ℕ_{0}$
126		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
127	125 126	eleqtrdi	$⊢ φ \to M \in ℤ_{\geq 0}$
128		eluzfz2	$⊢ M \in ℤ_{\geq 0} \to M \in (0 \dots M)$
129	127 128	syl	$⊢ φ \to M \in (0 \dots M)$
130	92 129	ffvelcdmd	$⊢ φ \to Q (M) \in ℝ$
131	130 5	readdcld	$⊢ φ \to Q (M) + T \in ℝ$
132	103 124 129 131	fvmptd	$⊢ φ \to S (M) = Q (M) + T$
133		simprlr	$⊢ (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))) \to Q (M) = B$
134	89 133	syl	$⊢ φ \to Q (M) = B$
135	134	oveq1d	$⊢ φ \to Q (M) + T = B + T$
136	132 135	eqtrd	$⊢ φ \to S (M) = B + T$
137	121 136	jca	$⊢ φ \to (S (0) = A + T \land S (M) = B + T)$
138	92	adantr	$⊢ (φ \land i \in (0 ..^M)) \to Q : (0 \dots M) ⟶ ℝ$
139		elfzofz	$⊢ i \in (0 ..^M) \to i \in (0 \dots M)$
140	139	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i \in (0 \dots M)$
141	138 140	ffvelcdmd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ℝ$
142		fzofzp1	$⊢ i \in (0 ..^M) \to i + 1 \in (0 \dots M)$
143	142	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i + 1 \in (0 \dots M)$
144	138 143	ffvelcdmd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ℝ$
145	5	adantr	$⊢ (φ \land i \in (0 ..^M)) \to T \in ℝ$
146	89	simprrd	$⊢ φ \to \forall i \in (0 ..^M) Q (i) < Q (i + 1)$
147	146	r19.21bi	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) < Q (i + 1)$
148	141 144 145 147	ltadd1dd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) + T < Q (i + 1) + T$
149	141 145	readdcld	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) + T \in ℝ$
150	8	fvmpt2	$⊢ (i \in (0 \dots M) \land Q (i) + T \in ℝ) \to S (i) = Q (i) + T$
151	140 149 150	syl2anc	$⊢ (φ \land i \in (0 ..^M)) \to S (i) = Q (i) + T$
152	8 24	eqtr4i	$⊢ S = (j \in (0 \dots M) ⟼ Q (j) + T)$
153	152	a1i	$⊢ (φ \land i \in (0 ..^M)) \to S = (j \in (0 \dots M) ⟼ Q (j) + T)$
154		fveq2	$⊢ j = i + 1 \to Q (j) = Q (i + 1)$
155	154	oveq1d	$⊢ j = i + 1 \to Q (j) + T = Q (i + 1) + T$
156	155	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land j = i + 1) \to Q (j) + T = Q (i + 1) + T$
157	144 145	readdcld	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) + T \in ℝ$
158	153 156 143 157	fvmptd	$⊢ (φ \land i \in (0 ..^M)) \to S (i + 1) = Q (i + 1) + T$
159	148 151 158	3brtr4d	$⊢ (φ \land i \in (0 ..^M)) \to S (i) < S (i + 1)$
160	159	ralrimiva	$⊢ φ \to \forall i \in (0 ..^M) S (i) < S (i + 1)$
161	102 137 160	jca32	$⊢ φ \to (S \in (ℝ^{(0 \dots M)}) \land ((S (0) = A + T \land S (M) = B + T) \land \forall i \in (0 ..^M) S (i) < S (i + 1)))$
162	9	fourierdlem2	$⊢ M \in ℕ \to (S \in H (M) \leftrightarrow (S \in (ℝ^{(0 \dots M)}) \land ((S (0) = A + T \land S (M) = B + T) \land \forall i \in (0 ..^M) S (i) < S (i + 1))))$
163	4 162	syl	$⊢ φ \to (S \in H (M) \leftrightarrow (S \in (ℝ^{(0 \dots M)}) \land ((S (0) = A + T \land S (M) = B + T) \land \forall i \in (0 ..^M) S (i) < S (i + 1))))$
164	161 163	mpbird	$⊢ φ \to S \in H (M)$
165	9	fveq1i	$⊢ H (M) = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A + T \land p (m) = B + T) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\}) (M)$
166	164 165	eleqtrdi	$⊢ φ \to S \in (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A + T \land p (m) = B + T) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\}) (M)$
167	166	adantr	$⊢ (φ \land 0 < - T) \to S \in (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A + T \land p (m) = B + T) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\}) (M)$
168	62	adantr	$⊢ (φ \land x \in [A + T, B + T]) \to A + T \in ℝ$
169	68	adantr	$⊢ (φ \land x \in [A + T, B + T]) \to B + T \in ℝ$
170		simpr	$⊢ (φ \land x \in [A + T, B + T]) \to x \in [A + T, B + T]$
171		eliccre	$⊢ (A + T \in ℝ \land B + T \in ℝ \land x \in [A + T, B + T]) \to x \in ℝ$
172	168 169 170 171	syl3anc	$⊢ (φ \land x \in [A + T, B + T]) \to x \in ℝ$
173	172	recnd	$⊢ (φ \land x \in [A + T, B + T]) \to x \in ℂ$
174	64	negcld	$⊢ φ \to - T \in ℂ$
175	174	adantr	$⊢ (φ \land x \in [A + T, B + T]) \to - T \in ℂ$
176	173 175	addcld	$⊢ (φ \land x \in [A + T, B + T]) \to x + (- T) \in ℂ$
177		simpl	$⊢ (φ \land x \in [A + T, B + T]) \to φ$
178	1	adantr	$⊢ (φ \land x \in [A + T, B + T]) \to A \in ℝ$
179	2	adantr	$⊢ (φ \land x \in [A + T, B + T]) \to B \in ℝ$
180	5	renegcld	$⊢ φ \to - T \in ℝ$
181	180	adantr	$⊢ (φ \land x \in [A + T, B + T]) \to - T \in ℝ$
182	172 181	readdcld	$⊢ (φ \land x \in [A + T, B + T]) \to x + (- T) \in ℝ$
183	65 66	eqtr2d	$⊢ φ \to A = A + T + (- T)$
184	183	adantr	$⊢ (φ \land x \in [A + T, B + T]) \to A = A + T + (- T)$
185	168	rexrd	$⊢ (φ \land x \in [A + T, B + T]) \to A + T \in ℝ^{*}$
186	169	rexrd	$⊢ (φ \land x \in [A + T, B + T]) \to B + T \in ℝ^{*}$
187		iccgelb	$⊢ (A + T \in ℝ^{} \land B + T \in ℝ^{} \land x \in [A + T, B + T]) \to A + T \leq x$
188	185 186 170 187	syl3anc	$⊢ (φ \land x \in [A + T, B + T]) \to A + T \leq x$
189	168 172 181 188	leadd1dd	$⊢ (φ \land x \in [A + T, B + T]) \to A + T + (- T) \leq x + (- T)$
190	184 189	eqbrtrd	$⊢ (φ \land x \in [A + T, B + T]) \to A \leq x + (- T)$
191		iccleub	$⊢ (A + T \in ℝ^{} \land B + T \in ℝ^{} \land x \in [A + T, B + T]) \to x \leq B + T$
192	185 186 170 191	syl3anc	$⊢ (φ \land x \in [A + T, B + T]) \to x \leq B + T$
193	172 169 181 192	leadd1dd	$⊢ (φ \land x \in [A + T, B + T]) \to x + (- T) \leq B + T + (- T)$
194	169	recnd	$⊢ (φ \land x \in [A + T, B + T]) \to B + T \in ℂ$
195	64	adantr	$⊢ (φ \land x \in [A + T, B + T]) \to T \in ℂ$
196	194 195	negsubd	$⊢ (φ \land x \in [A + T, B + T]) \to B + T + (- T) = B + T - T$
197	71	adantr	$⊢ (φ \land x \in [A + T, B + T]) \to B + T - T = B$
198	196 197	eqtrd	$⊢ (φ \land x \in [A + T, B + T]) \to B + T + (- T) = B$
199	193 198	breqtrd	$⊢ (φ \land x \in [A + T, B + T]) \to x + (- T) \leq B$
200	178 179 182 190 199	eliccd	$⊢ (φ \land x \in [A + T, B + T]) \to x + (- T) \in [A, B]$
201	177 200	jca	$⊢ (φ \land x \in [A + T, B + T]) \to (φ \land x + (- T) \in [A, B])$
202		eleq1	$⊢ y = x + (- T) \to (y \in [A, B] \leftrightarrow x + (- T) \in [A, B])$
203	202	anbi2d	$⊢ y = x + (- T) \to ((φ \land y \in [A, B]) \leftrightarrow (φ \land x + (- T) \in [A, B]))$
204		oveq1	$⊢ y = x + (- T) \to y + T = x + (- T) + T$
205	204	fveq2d	$⊢ y = x + (- T) \to F (y + T) = F (x + (- T) + T)$
206		fveq2	$⊢ y = x + (- T) \to F (y) = F (x + (- T))$
207	205 206	eqeq12d	$⊢ y = x + (- T) \to (F (y + T) = F (y) \leftrightarrow F (x + (- T) + T) = F (x + (- T)))$
208	203 207	imbi12d	$⊢ y = x + (- T) \to (((φ \land y \in [A, B]) \to F (y + T) = F (y)) \leftrightarrow ((φ \land x + (- T) \in [A, B]) \to F (x + (- T) + T) = F (x + (- T))))$
209		eleq1	$⊢ x = y \to (x \in [A, B] \leftrightarrow y \in [A, B])$
210	209	anbi2d	$⊢ x = y \to ((φ \land x \in [A, B]) \leftrightarrow (φ \land y \in [A, B]))$
211		oveq1	$⊢ x = y \to x + T = y + T$
212	211	fveq2d	$⊢ x = y \to F (x + T) = F (y + T)$
213		fveq2	$⊢ x = y \to F (x) = F (y)$
214	212 213	eqeq12d	$⊢ x = y \to (F (x + T) = F (x) \leftrightarrow F (y + T) = F (y))$
215	210 214	imbi12d	$⊢ x = y \to (((φ \land x \in [A, B]) \to F (x + T) = F (x)) \leftrightarrow ((φ \land y \in [A, B]) \to F (y + T) = F (y)))$
216	215 7	chvarvv	$⊢ (φ \land y \in [A, B]) \to F (y + T) = F (y)$
217	208 216	vtoclg	$⊢ x + (- T) \in ℂ \to ((φ \land x + (- T) \in [A, B]) \to F (x + (- T) + T) = F (x + (- T)))$
218	176 201 217	sylc	$⊢ (φ \land x \in [A + T, B + T]) \to F (x + (- T) + T) = F (x + (- T))$
219	173 195	negsubd	$⊢ (φ \land x \in [A + T, B + T]) \to x + (- T) = x - T$
220	219	oveq1d	$⊢ (φ \land x \in [A + T, B + T]) \to x + (- T) + T = x - T + T$
221	173 195	npcand	$⊢ (φ \land x \in [A + T, B + T]) \to x - T + T = x$
222	220 221	eqtrd	$⊢ (φ \land x \in [A + T, B + T]) \to x + (- T) + T = x$
223	222	fveq2d	$⊢ (φ \land x \in [A + T, B + T]) \to F (x + (- T) + T) = F (x)$
224	218 223	eqtr3d	$⊢ (φ \land x \in [A + T, B + T]) \to F (x + (- T)) = F (x)$
225	224	adantlr	$⊢ ((φ \land 0 < - T) \land x \in [A + T, B + T]) \to F (x + (- T)) = F (x)$
226		fveq2	$⊢ j = i \to S (j) = S (i)$
227	226	oveq1d	$⊢ j = i \to S (j) + (- T) = S (i) + (- T)$
228	227	cbvmptv	$⊢ (j \in (0 \dots M) ⟼ S (j) + (- T)) = (i \in (0 \dots M) ⟼ S (i) + (- T))$
229	10	adantr	$⊢ (φ \land 0 < - T) \to F : ℝ ⟶ ℂ$
230	10	adantr	$⊢ (φ \land i \in (0 ..^M)) \to F : ℝ ⟶ ℂ$
231		ioossre	$⊢ (S (i), S (i + 1)) \subseteq ℝ$
232	231	a1i	$⊢ (φ \land i \in (0 ..^M)) \to (S (i), S (i + 1)) \subseteq ℝ$
233	230 232	feqresmpt	$⊢ (φ \land i \in (0 ..^M)) \to {F ↾}_{(S (i), S (i + 1))} = (x \in (S (i), S (i + 1)) ⟼ F (x))$
234	151 158	oveq12d	$⊢ (φ \land i \in (0 ..^M)) \to (S (i), S (i + 1)) = (Q (i) + T, Q (i + 1) + T)$
235	141 144 145	iooshift	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i) + T, Q (i + 1) + T) = \{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\}$
236	234 235	eqtrd	$⊢ (φ \land i \in (0 ..^M)) \to (S (i), S (i + 1)) = \{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\}$
237	236	mpteq1d	$⊢ (φ \land i \in (0 ..^M)) \to (x \in (S (i), S (i + 1)) ⟼ F (x)) = (x \in \{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\} ⟼ F (x))$
238		simpll	$⊢ ((φ \land i \in (0 ..^M)) \land x \in \{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\}) \to φ$
239		simplr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in \{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\}) \to i \in (0 ..^M)$
240	235	eleq2d	$⊢ (φ \land i \in (0 ..^M)) \to (x \in (Q (i) + T, Q (i + 1) + T) \leftrightarrow x \in \{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\})$
241	240	biimpar	$⊢ ((φ \land i \in (0 ..^M)) \land x \in \{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\}) \to x \in (Q (i) + T, Q (i + 1) + T)$
242	141	rexrd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ℝ^{*}$
243	242	3adant3	$⊢ (φ \land i \in (0 ..^M) \land x \in (Q (i) + T, Q (i + 1) + T)) \to Q (i) \in ℝ^{*}$
244	144	rexrd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ℝ^{*}$
245	244	3adant3	$⊢ (φ \land i \in (0 ..^M) \land x \in (Q (i) + T, Q (i + 1) + T)) \to Q (i + 1) \in ℝ^{*}$
246		elioore	$⊢ x \in (Q (i) + T, Q (i + 1) + T) \to x \in ℝ$
247	246	adantl	$⊢ (φ \land x \in (Q (i) + T, Q (i + 1) + T)) \to x \in ℝ$
248	5	adantr	$⊢ (φ \land x \in (Q (i) + T, Q (i + 1) + T)) \to T \in ℝ$
249	247 248	resubcld	$⊢ (φ \land x \in (Q (i) + T, Q (i + 1) + T)) \to x - T \in ℝ$
250	249	3adant2	$⊢ (φ \land i \in (0 ..^M) \land x \in (Q (i) + T, Q (i + 1) + T)) \to x - T \in ℝ$
251	141	recnd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ℂ$
252	64	adantr	$⊢ (φ \land i \in (0 ..^M)) \to T \in ℂ$
253	251 252	pncand	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) + T - T = Q (i)$
254	253	eqcomd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) = Q (i) + T - T$
255	254	3adant3	$⊢ (φ \land i \in (0 ..^M) \land x \in (Q (i) + T, Q (i + 1) + T)) \to Q (i) = Q (i) + T - T$
256	149	3adant3	$⊢ (φ \land i \in (0 ..^M) \land x \in (Q (i) + T, Q (i + 1) + T)) \to Q (i) + T \in ℝ$
257	247	3adant2	$⊢ (φ \land i \in (0 ..^M) \land x \in (Q (i) + T, Q (i + 1) + T)) \to x \in ℝ$
258	5	3ad2ant1	$⊢ (φ \land i \in (0 ..^M) \land x \in (Q (i) + T, Q (i + 1) + T)) \to T \in ℝ$
259	149	rexrd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) + T \in ℝ^{*}$
260	259	3adant3	$⊢ (φ \land i \in (0 ..^M) \land x \in (Q (i) + T, Q (i + 1) + T)) \to Q (i) + T \in ℝ^{*}$
261	157	rexrd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) + T \in ℝ^{*}$
262	261	3adant3	$⊢ (φ \land i \in (0 ..^M) \land x \in (Q (i) + T, Q (i + 1) + T)) \to Q (i + 1) + T \in ℝ^{*}$
263		simp3	$⊢ (φ \land i \in (0 ..^M) \land x \in (Q (i) + T, Q (i + 1) + T)) \to x \in (Q (i) + T, Q (i + 1) + T)$
264		ioogtlb	$⊢ (Q (i) + T \in ℝ^{} \land Q (i + 1) + T \in ℝ^{} \land x \in (Q (i) + T, Q (i + 1) + T)) \to Q (i) + T < x$
265	260 262 263 264	syl3anc	$⊢ (φ \land i \in (0 ..^M) \land x \in (Q (i) + T, Q (i + 1) + T)) \to Q (i) + T < x$
266	256 257 258 265	ltsub1dd	$⊢ (φ \land i \in (0 ..^M) \land x \in (Q (i) + T, Q (i + 1) + T)) \to Q (i) + T - T < x - T$
267	255 266	eqbrtrd	$⊢ (φ \land i \in (0 ..^M) \land x \in (Q (i) + T, Q (i + 1) + T)) \to Q (i) < x - T$
268	157	3adant3	$⊢ (φ \land i \in (0 ..^M) \land x \in (Q (i) + T, Q (i + 1) + T)) \to Q (i + 1) + T \in ℝ$
269		iooltub	$⊢ (Q (i) + T \in ℝ^{} \land Q (i + 1) + T \in ℝ^{} \land x \in (Q (i) + T, Q (i + 1) + T)) \to x < Q (i + 1) + T$
270	260 262 263 269	syl3anc	$⊢ (φ \land i \in (0 ..^M) \land x \in (Q (i) + T, Q (i + 1) + T)) \to x < Q (i + 1) + T$
271	257 268 258 270	ltsub1dd	$⊢ (φ \land i \in (0 ..^M) \land x \in (Q (i) + T, Q (i + 1) + T)) \to x - T < Q (i + 1) + T - T$
272	144	recnd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ℂ$
273	272 252	pncand	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) + T - T = Q (i + 1)$
274	273	3adant3	$⊢ (φ \land i \in (0 ..^M) \land x \in (Q (i) + T, Q (i + 1) + T)) \to Q (i + 1) + T - T = Q (i + 1)$
275	271 274	breqtrd	$⊢ (φ \land i \in (0 ..^M) \land x \in (Q (i) + T, Q (i + 1) + T)) \to x - T < Q (i + 1)$
276	243 245 250 267 275	eliood	$⊢ (φ \land i \in (0 ..^M) \land x \in (Q (i) + T, Q (i + 1) + T)) \to x - T \in (Q (i), Q (i + 1))$
277	238 239 241 276	syl3anc	$⊢ ((φ \land i \in (0 ..^M)) \land x \in \{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\}) \to x - T \in (Q (i), Q (i + 1))$
278		fvres	$⊢ x - T \in (Q (i), Q (i + 1)) \to ({F ↾}_{(Q (i), Q (i + 1))}) (x - T) = F (x - T)$
279	277 278	syl	$⊢ ((φ \land i \in (0 ..^M)) \land x \in \{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\}) \to ({F ↾}_{(Q (i), Q (i + 1))}) (x - T) = F (x - T)$
280	238 241 249	syl2anc	$⊢ ((φ \land i \in (0 ..^M)) \land x \in \{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\}) \to x - T \in ℝ$
281	1	3ad2ant1	$⊢ (φ \land i \in (0 ..^M) \land x \in (Q (i) + T, Q (i + 1) + T)) \to A \in ℝ$
282	2	3ad2ant1	$⊢ (φ \land i \in (0 ..^M) \land x \in (Q (i) + T, Q (i + 1) + T)) \to B \in ℝ$
283	66	eqcomd	$⊢ φ \to A = A + T - T$
284	283	3ad2ant1	$⊢ (φ \land i \in (0 ..^M) \land x \in (Q (i) + T, Q (i + 1) + T)) \to A = A + T - T$
285	62	3ad2ant1	$⊢ (φ \land i \in (0 ..^M) \land x \in (Q (i) + T, Q (i + 1) + T)) \to A + T \in ℝ$
286	1	adantr	$⊢ (φ \land i \in (0 ..^M)) \to A \in ℝ$
287	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
288	287	adantr	$⊢ (φ \land i \in (0 ..^M)) \to A \in ℝ^{*}$
289	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
290	289	adantr	$⊢ (φ \land i \in (0 ..^M)) \to B \in ℝ^{*}$
291	3 4 6	fourierdlem15	$⊢ φ \to Q : (0 \dots M) ⟶ [A, B]$
292	291	adantr	$⊢ (φ \land i \in (0 ..^M)) \to Q : (0 \dots M) ⟶ [A, B]$
293	292 140	ffvelcdmd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in [A, B]$
294		iccgelb	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land Q (i) \in [A, B]) \to A \leq Q (i)$
295	288 290 293 294	syl3anc	$⊢ (φ \land i \in (0 ..^M)) \to A \leq Q (i)$
296	286 141 145 295	leadd1dd	$⊢ (φ \land i \in (0 ..^M)) \to A + T \leq Q (i) + T$
297	296	3adant3	$⊢ (φ \land i \in (0 ..^M) \land x \in (Q (i) + T, Q (i + 1) + T)) \to A + T \leq Q (i) + T$
298	285 256 257 297 265	lelttrd	$⊢ (φ \land i \in (0 ..^M) \land x \in (Q (i) + T, Q (i + 1) + T)) \to A + T < x$
299	285 257 258 298	ltsub1dd	$⊢ (φ \land i \in (0 ..^M) \land x \in (Q (i) + T, Q (i + 1) + T)) \to A + T - T < x - T$
300	284 299	eqbrtrd	$⊢ (φ \land i \in (0 ..^M) \land x \in (Q (i) + T, Q (i + 1) + T)) \to A < x - T$
301	281 250 300	ltled	$⊢ (φ \land i \in (0 ..^M) \land x \in (Q (i) + T, Q (i + 1) + T)) \to A \leq x - T$
302	144	3adant3	$⊢ (φ \land i \in (0 ..^M) \land x \in (Q (i) + T, Q (i + 1) + T)) \to Q (i + 1) \in ℝ$
303	292 143	ffvelcdmd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in [A, B]$
304		iccleub	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land Q (i + 1) \in [A, B]) \to Q (i + 1) \leq B$
305	288 290 303 304	syl3anc	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \leq B$
306	305	3adant3	$⊢ (φ \land i \in (0 ..^M) \land x \in (Q (i) + T, Q (i + 1) + T)) \to Q (i + 1) \leq B$
307	250 302 282 275 306	ltletrd	$⊢ (φ \land i \in (0 ..^M) \land x \in (Q (i) + T, Q (i + 1) + T)) \to x - T < B$
308	250 282 307	ltled	$⊢ (φ \land i \in (0 ..^M) \land x \in (Q (i) + T, Q (i + 1) + T)) \to x - T \leq B$
309	281 282 250 301 308	eliccd	$⊢ (φ \land i \in (0 ..^M) \land x \in (Q (i) + T, Q (i + 1) + T)) \to x - T \in [A, B]$
310	238 239 241 309	syl3anc	$⊢ ((φ \land i \in (0 ..^M)) \land x \in \{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\}) \to x - T \in [A, B]$
311	238 310	jca	$⊢ ((φ \land i \in (0 ..^M)) \land x \in \{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\}) \to (φ \land x - T \in [A, B])$
312		eleq1	$⊢ y = x - T \to (y \in [A, B] \leftrightarrow x - T \in [A, B])$
313	312	anbi2d	$⊢ y = x - T \to ((φ \land y \in [A, B]) \leftrightarrow (φ \land x - T \in [A, B]))$
314		oveq1	$⊢ y = x - T \to y + T = x - T + T$
315	314	fveq2d	$⊢ y = x - T \to F (y + T) = F (x - T + T)$
316		fveq2	$⊢ y = x - T \to F (y) = F (x - T)$
317	315 316	eqeq12d	$⊢ y = x - T \to (F (y + T) = F (y) \leftrightarrow F (x - T + T) = F (x - T))$
318	313 317	imbi12d	$⊢ y = x - T \to (((φ \land y \in [A, B]) \to F (y + T) = F (y)) \leftrightarrow ((φ \land x - T \in [A, B]) \to F (x - T + T) = F (x - T)))$
319	318 216	vtoclg	$⊢ x - T \in ℝ \to ((φ \land x - T \in [A, B]) \to F (x - T + T) = F (x - T))$
320	280 311 319	sylc	$⊢ ((φ \land i \in (0 ..^M)) \land x \in \{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\}) \to F (x - T + T) = F (x - T)$
321	241 246	syl	$⊢ ((φ \land i \in (0 ..^M)) \land x \in \{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\}) \to x \in ℝ$
322		recn	$⊢ x \in ℝ \to x \in ℂ$
323	322	adantl	$⊢ (φ \land x \in ℝ) \to x \in ℂ$
324	64	adantr	$⊢ (φ \land x \in ℝ) \to T \in ℂ$
325	323 324	npcand	$⊢ (φ \land x \in ℝ) \to x - T + T = x$
326	325	fveq2d	$⊢ (φ \land x \in ℝ) \to F (x - T + T) = F (x)$
327	238 321 326	syl2anc	$⊢ ((φ \land i \in (0 ..^M)) \land x \in \{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\}) \to F (x - T + T) = F (x)$
328	279 320 327	3eqtr2rd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in \{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\}) \to F (x) = ({F ↾}_{(Q (i), Q (i + 1))}) (x - T)$
329	328	mpteq2dva	$⊢ (φ \land i \in (0 ..^M)) \to (x \in \{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\} ⟼ F (x)) = (x \in \{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\} ⟼ ({F ↾}_{(Q (i), Q (i + 1))}) (x - T))$
330	233 237 329	3eqtrd	$⊢ (φ \land i \in (0 ..^M)) \to {F ↾}_{(S (i), S (i + 1))} = (x \in \{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\} ⟼ ({F ↾}_{(Q (i), Q (i + 1))}) (x - T))$
331		ioosscn	$⊢ (Q (i), Q (i + 1)) \subseteq ℂ$
332	331	a1i	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq ℂ$
333		eqeq1	$⊢ w = x \to (w = z + T \leftrightarrow x = z + T)$
334	333	rexbidv	$⊢ w = x \to (\exists z \in (Q (i), Q (i + 1)) w = z + T \leftrightarrow \exists z \in (Q (i), Q (i + 1)) x = z + T)$
335		oveq1	$⊢ z = y \to z + T = y + T$
336	335	eqeq2d	$⊢ z = y \to (x = z + T \leftrightarrow x = y + T)$
337	336	cbvrexvw	$⊢ \exists z \in (Q (i), Q (i + 1)) x = z + T \leftrightarrow \exists y \in (Q (i), Q (i + 1)) x = y + T$
338	334 337	bitrdi	$⊢ w = x \to (\exists z \in (Q (i), Q (i + 1)) w = z + T \leftrightarrow \exists y \in (Q (i), Q (i + 1)) x = y + T)$
339	338	cbvrabv	$⊢ \{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\} = \{x \in ℂ \| \exists y \in (Q (i), Q (i + 1)) x = y + T\}$
340		eqid	$⊢ (x \in \{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\} ⟼ ({F ↾}_{(Q (i), Q (i + 1))}) (x - T)) = (x \in \{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\} ⟼ ({F ↾}_{(Q (i), Q (i + 1))}) (x - T))$
341	332 252 339 11 340	cncfshift	$⊢ (φ \land i \in (0 ..^M)) \to (x \in \{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\} ⟼ ({F ↾}_{(Q (i), Q (i + 1))}) (x - T)) : \{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\} \underset{cn}{⟶} ℂ$
342	236	eqcomd	$⊢ (φ \land i \in (0 ..^M)) \to \{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\} = (S (i), S (i + 1))$
343	342	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to \{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\} \underset{cn}{⟶} ℂ = (S (i), S (i + 1)) \underset{cn}{⟶} ℂ$
344	341 343	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to (x \in \{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\} ⟼ ({F ↾}_{(Q (i), Q (i + 1))}) (x - T)) : (S (i), S (i + 1)) \underset{cn}{⟶} ℂ$
345	330 344	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(S (i), S (i + 1))}) : (S (i), S (i + 1)) \underset{cn}{⟶} ℂ$
346	345	adantlr	$⊢ ((φ \land 0 < - T) \land i \in (0 ..^M)) \to ({F ↾}_{(S (i), S (i + 1))}) : (S (i), S (i + 1)) \underset{cn}{⟶} ℂ$
347		ffdm	$⊢ F : ℝ ⟶ ℂ \to (F : dom F ⟶ ℂ \land dom F \subseteq ℝ)$
348	10 347	syl	$⊢ φ \to (F : dom F ⟶ ℂ \land dom F \subseteq ℝ)$
349	348	simpld	$⊢ φ \to F : dom F ⟶ ℂ$
350	349	adantr	$⊢ (φ \land i \in (0 ..^M)) \to F : dom F ⟶ ℂ$
351		ioossre	$⊢ (Q (i), Q (i + 1)) \subseteq ℝ$
352		fdm	$⊢ F : ℝ ⟶ ℂ \to dom F = ℝ$
353	230 352	syl	$⊢ (φ \land i \in (0 ..^M)) \to dom F = ℝ$
354	351 353	sseqtrrid	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq dom F$
355	339	eqcomi	$⊢ \{x \in ℂ \| \exists y \in (Q (i), Q (i + 1)) x = y + T\} = \{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\}$
356	232 342 353	3sstr4d	$⊢ (φ \land i \in (0 ..^M)) \to \{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\} \subseteq dom F$
357	339 356	eqsstrrid	$⊢ (φ \land i \in (0 ..^M)) \to \{x \in ℂ \| \exists y \in (Q (i), Q (i + 1)) x = y + T\} \subseteq dom F$
358		simpll	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1))) \to φ$
359	358 287	syl	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1))) \to A \in ℝ^{*}$
360	358 289	syl	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1))) \to B \in ℝ^{*}$
361	358 291	syl	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1))) \to Q : (0 \dots M) ⟶ [A, B]$
362		simplr	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1))) \to i \in (0 ..^M)$
363		ioossicc	$⊢ (Q (i), Q (i + 1)) \subseteq [Q (i), Q (i + 1)]$
364	363	sseli	$⊢ z \in (Q (i), Q (i + 1)) \to z \in [Q (i), Q (i + 1)]$
365	364	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1))) \to z \in [Q (i), Q (i + 1)]$
366	359 360 361 362 365	fourierdlem1	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1))) \to z \in [A, B]$
367		eleq1	$⊢ x = z \to (x \in [A, B] \leftrightarrow z \in [A, B])$
368	367	anbi2d	$⊢ x = z \to ((φ \land x \in [A, B]) \leftrightarrow (φ \land z \in [A, B]))$
369		oveq1	$⊢ x = z \to x + T = z + T$
370	369	fveq2d	$⊢ x = z \to F (x + T) = F (z + T)$
371		fveq2	$⊢ x = z \to F (x) = F (z)$
372	370 371	eqeq12d	$⊢ x = z \to (F (x + T) = F (x) \leftrightarrow F (z + T) = F (z))$
373	368 372	imbi12d	$⊢ x = z \to (((φ \land x \in [A, B]) \to F (x + T) = F (x)) \leftrightarrow ((φ \land z \in [A, B]) \to F (z + T) = F (z)))$
374	373 7	chvarvv	$⊢ (φ \land z \in [A, B]) \to F (z + T) = F (z)$
375	358 366 374	syl2anc	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1))) \to F (z + T) = F (z)$
376	350 332 354 252 355 357 375 12	limcperiod	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{\{x \in ℂ \| \exists y \in (Q (i), Q (i + 1)) x = y + T\}}) {lim}_{ℂ} (Q (i) + T))$
377	355 342	eqtrid	$⊢ (φ \land i \in (0 ..^M)) \to \{x \in ℂ \| \exists y \in (Q (i), Q (i + 1)) x = y + T\} = (S (i), S (i + 1))$
378	377	reseq2d	$⊢ (φ \land i \in (0 ..^M)) \to {F ↾}_{\{x \in ℂ \| \exists y \in (Q (i), Q (i + 1)) x = y + T\}} = {F ↾}_{(S (i), S (i + 1))}$
379	151	eqcomd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) + T = S (i)$
380	378 379	oveq12d	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{\{x \in ℂ \| \exists y \in (Q (i), Q (i + 1)) x = y + T\}}) {lim}_{ℂ} (Q (i) + T) = ({F ↾}_{(S (i), S (i + 1))}) {lim}_{ℂ} S (i)$
381	376 380	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(S (i), S (i + 1))}) {lim}_{ℂ} S (i))$
382	381	adantlr	$⊢ ((φ \land 0 < - T) \land i \in (0 ..^M)) \to R \in (({F ↾}_{(S (i), S (i + 1))}) {lim}_{ℂ} S (i))$
383	350 332 354 252 355 357 375 13	limcperiod	$⊢ (φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{\{x \in ℂ \| \exists y \in (Q (i), Q (i + 1)) x = y + T\}}) {lim}_{ℂ} (Q (i + 1) + T))$
384	158	eqcomd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) + T = S (i + 1)$
385	378 384	oveq12d	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{\{x \in ℂ \| \exists y \in (Q (i), Q (i + 1)) x = y + T\}}) {lim}_{ℂ} (Q (i + 1) + T) = ({F ↾}_{(S (i), S (i + 1))}) {lim}_{ℂ} S (i + 1)$
386	383 385	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(S (i), S (i + 1))}) {lim}_{ℂ} S (i + 1))$
387	386	adantlr	$⊢ ((φ \land 0 < - T) \land i \in (0 ..^M)) \to L \in (({F ↾}_{(S (i), S (i + 1))}) {lim}_{ℂ} S (i + 1))$
388		eqeq1	$⊢ y = x \to (y = S (i) \leftrightarrow x = S (i))$
389		eqeq1	$⊢ y = x \to (y = S (i + 1) \leftrightarrow x = S (i + 1))$
390	389 31	ifbieq2d	$⊢ y = x \to if (y = S (i + 1), L, F (y)) = if (x = S (i + 1), L, F (x))$
391	388 390	ifbieq2d	$⊢ y = x \to if (y = S (i), R, if (y = S (i + 1), L, F (y))) = if (x = S (i), R, if (x = S (i + 1), L, F (x)))$
392	391	cbvmptv	$⊢ (y \in [S (i), S (i + 1)] ⟼ if (y = S (i), R, if (y = S (i + 1), L, F (y)))) = (x \in [S (i), S (i + 1)] ⟼ if (x = S (i), R, if (x = S (i + 1), L, F (x))))$
393		eqid	$⊢ (x \in [(j \in (0 \dots M) ⟼ S (j) + (- T)) (i), (j \in (0 \dots M) ⟼ S (j) + (- T)) (i + 1)] ⟼ (y \in [S (i), S (i + 1)] ⟼ if (y = S (i), R, if (y = S (i + 1), L, F (y)))) (x - (- T))) = (x \in [(j \in (0 \dots M) ⟼ S (j) + (- T)) (i), (j \in (0 \dots M) ⟼ S (j) + (- T)) (i + 1)] ⟼ (y \in [S (i), S (i + 1)] ⟼ if (y = S (i), R, if (y = S (i + 1), L, F (y)))) (x - (- T)))$
394	79 81 82 83 86 167 225 228 229 346 382 387 392 393	fourierdlem81	$⊢ (φ \land 0 < - T) \to \int_{[A + T + (- T), B + T + (- T)]} F (x) d x = \int_{[A + T, B + T]} F (x) d x$
395	76 394	eqtr2d	$⊢ (φ \land 0 < - T) \to \int_{[A + T, B + T]} F (x) d x = \int_{[A, B]} F (x) d x$
396	51 61 395	syl2anc	$⊢ ((φ \land \neg 0 < T) \land \neg T = 0) \to \int_{[A + T, B + T]} F (x) d x = \int_{[A, B]} F (x) d x$
397	50 396	pm2.61dan	$⊢ (φ \land \neg 0 < T) \to \int_{[A + T, B + T]} F (x) d x = \int_{[A, B]} F (x) d x$
398	36 397	pm2.61dan	$⊢ φ \to \int_{[A + T, B + T]} F (x) d x = \int_{[A, B]} F (x) d x$

Metamath Proof Explorer

Theorem fourierdlem92

Proof