fourierdlem107

Description: The integral of a piecewise continuous periodic function F is unchanged if the domain is shifted by any positive value X . This lemma generalizes fourierdlem92 where the integral was shifted by the exact period. This lemma uses local definitions, so that the proof is more readable. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem107.a	$⊢ φ \to A \in ℝ$
	fourierdlem107.b	$⊢ φ \to B \in ℝ$
	fourierdlem107.t	$⊢ T = B - A$
	fourierdlem107.x	$⊢ φ \to X \in ℝ^{+}$
	fourierdlem107.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))\})$
	fourierdlem107.m	$⊢ φ \to M \in ℕ$
	fourierdlem107.q	$⊢ φ \to Q \in P (M)$
	fourierdlem107.f	$⊢ φ \to F : ℝ ⟶ ℂ$
	fourierdlem107.fper	$⊢ (φ \land x \in ℝ) \to F (x + T) = F (x)$
	fourierdlem107.fcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
	fourierdlem107.r	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
	fourierdlem107.l	$⊢ (φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
	fourierdlem107.o	$⊢ O = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A - X \land p (m) = A) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
	fourierdlem107.h	$⊢ H = \{A - X, A\} \cup \{y \in [A - X, A] \| \exists k \in ℤ y + k T \in ran Q\}$
	fourierdlem107.n	$⊢ N = \|H\| - 1$
	fourierdlem107.s	$⊢ S = (ι f \| f {Isom}_{<, <} ((0 \dots N), H))$
	fourierdlem107.e	$⊢ E = (x \in ℝ ⟼ x + ⌊\frac{B - x}{T}⌋ T)$
	fourierdlem107.z	$⊢ Z = (y \in (A, B] ⟼ if (y = B, A, y))$
	fourierdlem107.i	$⊢ I = (x \in ℝ ⟼ sup (\{i \in (0 ..^M) \| Q (i) \leq Z (E (x))\} ℝ <))$
Assertion	fourierdlem107	$⊢ φ \to \int_{[A - X, B - X]} F (x) d x = \int_{[A, B]} F (x) d x$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem107.a	$⊢ φ \to A \in ℝ$
2		fourierdlem107.b	$⊢ φ \to B \in ℝ$
3		fourierdlem107.t	$⊢ T = B - A$
4		fourierdlem107.x	$⊢ φ \to X \in ℝ^{+}$
5		fourierdlem107.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))\})$
6		fourierdlem107.m	$⊢ φ \to M \in ℕ$
7		fourierdlem107.q	$⊢ φ \to Q \in P (M)$
8		fourierdlem107.f	$⊢ φ \to F : ℝ ⟶ ℂ$
9		fourierdlem107.fper	$⊢ (φ \land x \in ℝ) \to F (x + T) = F (x)$
10		fourierdlem107.fcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
11		fourierdlem107.r	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
12		fourierdlem107.l	$⊢ (φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
13		fourierdlem107.o	$⊢ O = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A - X \land p (m) = A) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
14		fourierdlem107.h	$⊢ H = \{A - X, A\} \cup \{y \in [A - X, A] \| \exists k \in ℤ y + k T \in ran Q\}$
15		fourierdlem107.n	$⊢ N = \|H\| - 1$
16		fourierdlem107.s	$⊢ S = (ι f \| f {Isom}_{<, <} ((0 \dots N), H))$
17		fourierdlem107.e	$⊢ E = (x \in ℝ ⟼ x + ⌊\frac{B - x}{T}⌋ T)$
18		fourierdlem107.z	$⊢ Z = (y \in (A, B] ⟼ if (y = B, A, y))$
19		fourierdlem107.i	$⊢ I = (x \in ℝ ⟼ sup (\{i \in (0 ..^M) \| Q (i) \leq Z (E (x))\} ℝ <))$
20	3	oveq2i	$⊢ A - X + T = (A - X) + B - A$
21	1	recnd	$⊢ φ \to A \in ℂ$
22	4	rpred	$⊢ φ \to X \in ℝ$
23	22	recnd	$⊢ φ \to X \in ℂ$
24	2	recnd	$⊢ φ \to B \in ℂ$
25	21 23 24 21	subadd4b	$⊢ φ \to (A - X) + B - A = (A - A) + B - X$
26	20 25	eqtrid	$⊢ φ \to A - X + T = (A - A) + B - X$
27	21	subidd	$⊢ φ \to A - A = 0$
28	27	oveq1d	$⊢ φ \to (A - A) + B - X = 0 + B - X$
29	2 22	resubcld	$⊢ φ \to B - X \in ℝ$
30	29	recnd	$⊢ φ \to B - X \in ℂ$
31	30	addid2d	$⊢ φ \to 0 + B - X = B - X$
32	26 28 31	3eqtrd	$⊢ φ \to A - X + T = B - X$
33	3	oveq2i	$⊢ A + T = A + B - A$
34	21 24	pncan3d	$⊢ φ \to A + B - A = B$
35	33 34	eqtrid	$⊢ φ \to A + T = B$
36	32 35	oveq12d	$⊢ φ \to [A - X + T, A + T] = [B - X, B]$
37	36	eqcomd	$⊢ φ \to [B - X, B] = [A - X + T, A + T]$
38	37	itgeq1d	$⊢ φ \to \int_{[B - X, B]} F (x) d x = \int_{[A - X + T, A + T]} F (x) d x$
39	1 22	resubcld	$⊢ φ \to A - X \in ℝ$
40		fveq2	$⊢ i = j \to p (i) = p (j)$
41		oveq1	$⊢ i = j \to i + 1 = j + 1$
42	41	fveq2d	$⊢ i = j \to p (i + 1) = p (j + 1)$
43	40 42	breq12d	$⊢ i = j \to (p (i) < p (i + 1) \leftrightarrow p (j) < p (j + 1))$
44	43	cbvralvw	$⊢ \forall i \in (0 ..^m) p (i) < p (i + 1) \leftrightarrow \forall j \in (0 ..^m) p (j) < p (j + 1)$
45	44	a1i	$⊢ m \in ℕ \to (\forall i \in (0 ..^m) p (i) < p (i + 1) \leftrightarrow \forall j \in (0 ..^m) p (j) < p (j + 1))$
46	45	anbi2d	$⊢ m \in ℕ \to (((p (0) = A - X \land p (m) = A) \land \forall i \in (0 ..^m) p (i) < p (i + 1)) \leftrightarrow ((p (0) = A - X \land p (m) = A) \land \forall j \in (0 ..^m) p (j) < p (j + 1)))$
47	46	rabbidv	$⊢ m \in ℕ \to \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A - X \land p (m) = A) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\} = \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A - X \land p (m) = A) \land \forall j \in (0 ..^m) p (j) < p (j + 1))\}$
48	47	mpteq2ia	$⊢ (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A - X \land p (m) = A) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\}) = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A - X \land p (m) = A) \land \forall j \in (0 ..^m) p (j) < p (j + 1))\})$
49	13 48	eqtri	$⊢ O = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A - X \land p (m) = A) \land \forall j \in (0 ..^m) p (j) < p (j + 1))\})$
50	1 4	ltsubrpd	$⊢ φ \to A - X < A$
51	3 5 6 7 39 1 50 13 14 15 16	fourierdlem54	$⊢ φ \to ((N \in ℕ \land S \in O (N)) \land S {Isom}_{<, <} ((0 \dots N), H))$
52	51	simpld	$⊢ φ \to (N \in ℕ \land S \in O (N))$
53	52	simpld	$⊢ φ \to N \in ℕ$
54	2 1	resubcld	$⊢ φ \to B - A \in ℝ$
55	3 54	eqeltrid	$⊢ φ \to T \in ℝ$
56	52	simprd	$⊢ φ \to S \in O (N)$
57	39	adantr	$⊢ (φ \land x \in [A - X, A]) \to A - X \in ℝ$
58	1	adantr	$⊢ (φ \land x \in [A - X, A]) \to A \in ℝ$
59		simpr	$⊢ (φ \land x \in [A - X, A]) \to x \in [A - X, A]$
60		eliccre	$⊢ (A - X \in ℝ \land A \in ℝ \land x \in [A - X, A]) \to x \in ℝ$
61	57 58 59 60	syl3anc	$⊢ (φ \land x \in [A - X, A]) \to x \in ℝ$
62	61 9	syldan	$⊢ (φ \land x \in [A - X, A]) \to F (x + T) = F (x)$
63		fveq2	$⊢ i = j \to S (i) = S (j)$
64	63	oveq1d	$⊢ i = j \to S (i) + T = S (j) + T$
65	64	cbvmptv	$⊢ (i \in (0 \dots N) ⟼ S (i) + T) = (j \in (0 \dots N) ⟼ S (j) + T)$
66		eqid	$⊢ (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A - X + T \land p (m) = A + T) \land \forall j \in (0 ..^m) p (j) < p (j + 1))\}) = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A - X + T \land p (m) = A + T) \land \forall j \in (0 ..^m) p (j) < p (j + 1))\})$
67	6	adantr	$⊢ (φ \land j \in (0 ..^N)) \to M \in ℕ$
68	7	adantr	$⊢ (φ \land j \in (0 ..^N)) \to Q \in P (M)$
69	8	adantr	$⊢ (φ \land j \in (0 ..^N)) \to F : ℝ ⟶ ℂ$
70	9	adantlr	$⊢ ((φ \land j \in (0 ..^N)) \land x \in ℝ) \to F (x + T) = F (x)$
71	10	adantlr	$⊢ ((φ \land j \in (0 ..^N)) \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
72	39	adantr	$⊢ (φ \land j \in (0 ..^N)) \to A - X \in ℝ$
73	72	rexrd	$⊢ (φ \land j \in (0 ..^N)) \to A - X \in ℝ^{*}$
74		pnfxr	$⊢ +∞ \in ℝ^{*}$
75	74	a1i	$⊢ (φ \land j \in (0 ..^N)) \to +∞ \in ℝ^{*}$
76	1	adantr	$⊢ (φ \land j \in (0 ..^N)) \to A \in ℝ$
77	50	adantr	$⊢ (φ \land j \in (0 ..^N)) \to A - X < A$
78	1	ltpnfd	$⊢ φ \to A < +∞$
79	78	adantr	$⊢ (φ \land j \in (0 ..^N)) \to A < +∞$
80	73 75 76 77 79	eliood	$⊢ (φ \land j \in (0 ..^N)) \to A \in (A - X, +∞)$
81		simpr	$⊢ (φ \land j \in (0 ..^N)) \to j \in (0 ..^N)$
82		eqid	$⊢ S (j + 1) - E (S (j + 1)) = S (j + 1) - E (S (j + 1))$
83		eqid	$⊢ {F ↾}_{(Z (E (S (j))), E (S (j + 1)))} = {F ↾}_{(Z (E (S (j))), E (S (j + 1)))}$
84		eqid	$⊢ (y \in (Z (E (S (j))) + S (j + 1) - E (S (j + 1)), E (S (j + 1)) + S (j + 1) - E (S (j + 1))) ⟼ ({F ↾}_{(Z (E (S (j))), E (S (j + 1)))}) (y - (S (j + 1) - E (S (j + 1))))) = (y \in (Z (E (S (j))) + S (j + 1) - E (S (j + 1)), E (S (j + 1)) + S (j + 1) - E (S (j + 1))) ⟼ ({F ↾}_{(Z (E (S (j))), E (S (j + 1)))}) (y - (S (j + 1) - E (S (j + 1)))))$
85	5 3 67 68 69 70 71 72 80 13 14 15 16 17 18 81 82 83 84 19	fourierdlem90	$⊢ (φ \land j \in (0 ..^N)) \to ({F ↾}_{(S (j), S (j + 1))}) : (S (j), S (j + 1)) \underset{cn}{⟶} ℂ$
86	11	adantlr	$⊢ ((φ \land j \in (0 ..^N)) \land i \in (0 ..^M)) \to R \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
87		eqid	$⊢ (i \in (0 ..^M) ⟼ R) = (i \in (0 ..^M) ⟼ R)$
88	5 3 67 68 69 70 71 86 72 80 13 14 15 16 17 18 81 82 19 87	fourierdlem89	$⊢ (φ \land j \in (0 ..^N)) \to if (Z (E (S (j))) = Q (I (S (j))), (i \in (0 ..^M) ⟼ R) (I (S (j))), F (Z (E (S (j))))) \in (({F ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j))$
89	12	adantlr	$⊢ ((φ \land j \in (0 ..^N)) \land i \in (0 ..^M)) \to L \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
90		eqid	$⊢ (i \in (0 ..^M) ⟼ L) = (i \in (0 ..^M) ⟼ L)$
91	5 3 67 68 69 70 71 89 72 80 13 14 15 16 17 18 81 82 19 90	fourierdlem91	$⊢ (φ \land j \in (0 ..^N)) \to if (E (S (j + 1)) = Q (I (S (j)) + 1), (i \in (0 ..^M) ⟼ L) (I (S (j))), F (E (S (j + 1)))) \in (({F ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j + 1))$
92	39 1 49 53 55 56 62 65 66 8 85 88 91	fourierdlem92	$⊢ φ \to \int_{[A - X + T, A + T]} F (x) d x = \int_{[A - X, A]} F (x) d x$
93	38 92	eqtrd	$⊢ φ \to \int_{[B - X, B]} F (x) d x = \int_{[A - X, A]} F (x) d x$
94	8	adantr	$⊢ (φ \land x \in [B - X, B]) \to F : ℝ ⟶ ℂ$
95	29	adantr	$⊢ (φ \land x \in [B - X, B]) \to B - X \in ℝ$
96	2	adantr	$⊢ (φ \land x \in [B - X, B]) \to B \in ℝ$
97		simpr	$⊢ (φ \land x \in [B - X, B]) \to x \in [B - X, B]$
98		eliccre	$⊢ (B - X \in ℝ \land B \in ℝ \land x \in [B - X, B]) \to x \in ℝ$
99	95 96 97 98	syl3anc	$⊢ (φ \land x \in [B - X, B]) \to x \in ℝ$
100	94 99	ffvelrnd	$⊢ (φ \land x \in [B - X, B]) \to F (x) \in ℂ$
101	29	rexrd	$⊢ φ \to B - X \in ℝ^{*}$
102	74	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
103	2 4	ltsubrpd	$⊢ φ \to B - X < B$
104	2	ltpnfd	$⊢ φ \to B < +∞$
105	101 102 2 103 104	eliood	$⊢ φ \to B \in (B - X, +∞)$
106	5 3 6 7 8 9 10 11 12 29 105	fourierdlem105	$⊢ φ \to (x \in [B - X, B] ⟼ F (x)) \in 𝐿^{1}$
107	100 106	itgcl	$⊢ φ \to \int_{[B - X, B]} F (x) d x \in ℂ$
108	93 107	eqeltrrd	$⊢ φ \to \int_{[A - X, A]} F (x) d x \in ℂ$
109	108	subidd	$⊢ φ \to \int_{[A - X, A]} F (x) d x - \int_{[A - X, A]} F (x) d x = 0$
110	109	eqcomd	$⊢ φ \to 0 = \int_{[A - X, A]} F (x) d x - \int_{[A - X, A]} F (x) d x$
111	110	adantr	$⊢ (φ \land T < X) \to 0 = \int_{[A - X, A]} F (x) d x - \int_{[A - X, A]} F (x) d x$
112	39	adantr	$⊢ (φ \land T < X) \to A - X \in ℝ$
113	1	adantr	$⊢ (φ \land T < X) \to A \in ℝ$
114	29	adantr	$⊢ (φ \land T < X) \to B - X \in ℝ$
115	5 6 7	fourierdlem11	$⊢ φ \to (A \in ℝ \land B \in ℝ \land A < B)$
116	115	simp3d	$⊢ φ \to A < B$
117	1 2 116	ltled	$⊢ φ \to A \leq B$
118	117	adantr	$⊢ (φ \land T < X) \to A \leq B$
119	1 2 22	lesub1d	$⊢ φ \to (A \leq B \leftrightarrow A - X \leq B - X)$
120	119	adantr	$⊢ (φ \land T < X) \to (A \leq B \leftrightarrow A - X \leq B - X)$
121	118 120	mpbid	$⊢ (φ \land T < X) \to A - X \leq B - X$
122	2	adantr	$⊢ (φ \land T < X) \to B \in ℝ$
123	22	adantr	$⊢ (φ \land T < X) \to X \in ℝ$
124		simpr	$⊢ (φ \land T < X) \to T < X$
125	3 124	eqbrtrrid	$⊢ (φ \land T < X) \to B - A < X$
126	122 113 123 125	ltsub23d	$⊢ (φ \land T < X) \to B - X < A$
127	114 113 126	ltled	$⊢ (φ \land T < X) \to B - X \leq A$
128	112 113 114 121 127	eliccd	$⊢ (φ \land T < X) \to B - X \in [A - X, A]$
129	8	adantr	$⊢ (φ \land x \in [A - X, A]) \to F : ℝ ⟶ ℂ$
130	129 61	ffvelrnd	$⊢ (φ \land x \in [A - X, A]) \to F (x) \in ℂ$
131	130	adantlr	$⊢ ((φ \land T < X) \land x \in [A - X, A]) \to F (x) \in ℂ$
132	39	rexrd	$⊢ φ \to A - X \in ℝ^{*}$
133	1 2 22 116	ltsub1dd	$⊢ φ \to A - X < B - X$
134	29	ltpnfd	$⊢ φ \to B - X < +∞$
135	132 102 29 133 134	eliood	$⊢ φ \to B - X \in (A - X, +∞)$
136	5 3 6 7 8 9 10 11 12 39 135	fourierdlem105	$⊢ φ \to (x \in [A - X, B - X] ⟼ F (x)) \in 𝐿^{1}$
137	136	adantr	$⊢ (φ \land T < X) \to (x \in [A - X, B - X] ⟼ F (x)) \in 𝐿^{1}$
138	6	adantr	$⊢ (φ \land T < X) \to M \in ℕ$
139	7	adantr	$⊢ (φ \land T < X) \to Q \in P (M)$
140	8	adantr	$⊢ (φ \land T < X) \to F : ℝ ⟶ ℂ$
141	9	adantlr	$⊢ ((φ \land T < X) \land x \in ℝ) \to F (x + T) = F (x)$
142	10	adantlr	$⊢ ((φ \land T < X) \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
143	11	adantlr	$⊢ ((φ \land T < X) \land i \in (0 ..^M)) \to R \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
144	12	adantlr	$⊢ ((φ \land T < X) \land i \in (0 ..^M)) \to L \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
145	101	adantr	$⊢ (φ \land T < X) \to B - X \in ℝ^{*}$
146	74	a1i	$⊢ (φ \land T < X) \to +∞ \in ℝ^{*}$
147	113	ltpnfd	$⊢ (φ \land T < X) \to A < +∞$
148	145 146 113 126 147	eliood	$⊢ (φ \land T < X) \to A \in (B - X, +∞)$
149	5 3 138 139 140 141 142 143 144 114 148	fourierdlem105	$⊢ (φ \land T < X) \to (x \in [B - X, A] ⟼ F (x)) \in 𝐿^{1}$
150	112 113 128 131 137 149	itgspliticc	$⊢ (φ \land T < X) \to \int_{[A - X, A]} F (x) d x = \int_{[A - X, B - X]} F (x) d x + \int_{[B - X, A]} F (x) d x$
151	150	oveq1d	$⊢ (φ \land T < X) \to \int_{[A - X, A]} F (x) d x - \int_{[A - X, A]} F (x) d x = \int_{[A - X, B - X]} F (x) d x + \int_{[B - X, A]} F (x) d x - \int_{[A - X, A]} F (x) d x$
152	8	adantr	$⊢ (φ \land x \in [A - X, B - X]) \to F : ℝ ⟶ ℂ$
153	39	adantr	$⊢ (φ \land x \in [A - X, B - X]) \to A - X \in ℝ$
154	29	adantr	$⊢ (φ \land x \in [A - X, B - X]) \to B - X \in ℝ$
155		simpr	$⊢ (φ \land x \in [A - X, B - X]) \to x \in [A - X, B - X]$
156		eliccre	$⊢ (A - X \in ℝ \land B - X \in ℝ \land x \in [A - X, B - X]) \to x \in ℝ$
157	153 154 155 156	syl3anc	$⊢ (φ \land x \in [A - X, B - X]) \to x \in ℝ$
158	152 157	ffvelrnd	$⊢ (φ \land x \in [A - X, B - X]) \to F (x) \in ℂ$
159	158 136	itgcl	$⊢ φ \to \int_{[A - X, B - X]} F (x) d x \in ℂ$
160	159	adantr	$⊢ (φ \land T < X) \to \int_{[A - X, B - X]} F (x) d x \in ℂ$
161	8	adantr	$⊢ (φ \land x \in [B - X, A]) \to F : ℝ ⟶ ℂ$
162	29	adantr	$⊢ (φ \land x \in [B - X, A]) \to B - X \in ℝ$
163	1	adantr	$⊢ (φ \land x \in [B - X, A]) \to A \in ℝ$
164		simpr	$⊢ (φ \land x \in [B - X, A]) \to x \in [B - X, A]$
165		eliccre	$⊢ (B - X \in ℝ \land A \in ℝ \land x \in [B - X, A]) \to x \in ℝ$
166	162 163 164 165	syl3anc	$⊢ (φ \land x \in [B - X, A]) \to x \in ℝ$
167	161 166	ffvelrnd	$⊢ (φ \land x \in [B - X, A]) \to F (x) \in ℂ$
168	167	adantlr	$⊢ ((φ \land T < X) \land x \in [B - X, A]) \to F (x) \in ℂ$
169	168 149	itgcl	$⊢ (φ \land T < X) \to \int_{[B - X, A]} F (x) d x \in ℂ$
170	108	adantr	$⊢ (φ \land T < X) \to \int_{[A - X, A]} F (x) d x \in ℂ$
171	160 169 170	addsubassd	$⊢ (φ \land T < X) \to \int_{[A - X, B - X]} F (x) d x + \int_{[B - X, A]} F (x) d x - \int_{[A - X, A]} F (x) d x = \int_{[A - X, B - X]} F (x) d x + \int_{[B - X, A]} F (x) d x - \int_{[A - X, A]} F (x) d x$
172	111 151 171	3eqtrd	$⊢ (φ \land T < X) \to 0 = \int_{[A - X, B - X]} F (x) d x + \int_{[B - X, A]} F (x) d x - \int_{[A - X, A]} F (x) d x$
173	172	oveq2d	$⊢ (φ \land T < X) \to \int_{[A - X, B - X]} F (x) d x - 0 = \int_{[A - X, B - X]} F (x) d x - (\int_{[A - X, B - X]} F (x) d x + \int_{[B - X, A]} F (x) d x - \int_{[A - X, A]} F (x) d x)$
174	160	subid1d	$⊢ (φ \land T < X) \to \int_{[A - X, B - X]} F (x) d x - 0 = \int_{[A - X, B - X]} F (x) d x$
175	159	subidd	$⊢ φ \to \int_{[A - X, B - X]} F (x) d x - \int_{[A - X, B - X]} F (x) d x = 0$
176	175	oveq1d	$⊢ φ \to \int_{[A - X, B - X]} F (x) d x - \int_{[A - X, B - X]} F (x) d x - (\int_{[B - X, A]} F (x) d x - \int_{[A - X, A]} F (x) d x) = 0 - (\int_{[B - X, A]} F (x) d x - \int_{[A - X, A]} F (x) d x)$
177	176	adantr	$⊢ (φ \land T < X) \to \int_{[A - X, B - X]} F (x) d x - \int_{[A - X, B - X]} F (x) d x - (\int_{[B - X, A]} F (x) d x - \int_{[A - X, A]} F (x) d x) = 0 - (\int_{[B - X, A]} F (x) d x - \int_{[A - X, A]} F (x) d x)$
178	169 170	subcld	$⊢ (φ \land T < X) \to \int_{[B - X, A]} F (x) d x - \int_{[A - X, A]} F (x) d x \in ℂ$
179	160 160 178	subsub4d	$⊢ (φ \land T < X) \to \int_{[A - X, B - X]} F (x) d x - \int_{[A - X, B - X]} F (x) d x - (\int_{[B - X, A]} F (x) d x - \int_{[A - X, A]} F (x) d x) = \int_{[A - X, B - X]} F (x) d x - (\int_{[A - X, B - X]} F (x) d x + \int_{[B - X, A]} F (x) d x - \int_{[A - X, A]} F (x) d x)$
180		df-neg	$⊢ - (\int_{[B - X, A]} F (x) d x - \int_{[A - X, A]} F (x) d x) = 0 - (\int_{[B - X, A]} F (x) d x - \int_{[A - X, A]} F (x) d x)$
181	169 170	negsubdi2d	$⊢ (φ \land T < X) \to - (\int_{[B - X, A]} F (x) d x - \int_{[A - X, A]} F (x) d x) = \int_{[A - X, A]} F (x) d x - \int_{[B - X, A]} F (x) d x$
182	180 181	eqtr3id	$⊢ (φ \land T < X) \to 0 - (\int_{[B - X, A]} F (x) d x - \int_{[A - X, A]} F (x) d x) = \int_{[A - X, A]} F (x) d x - \int_{[B - X, A]} F (x) d x$
183	177 179 182	3eqtr3d	$⊢ (φ \land T < X) \to \int_{[A - X, B - X]} F (x) d x - (\int_{[A - X, B - X]} F (x) d x + \int_{[B - X, A]} F (x) d x - \int_{[A - X, A]} F (x) d x) = \int_{[A - X, A]} F (x) d x - \int_{[B - X, A]} F (x) d x$
184	173 174 183	3eqtr3d	$⊢ (φ \land T < X) \to \int_{[A - X, B - X]} F (x) d x = \int_{[A - X, A]} F (x) d x - \int_{[B - X, A]} F (x) d x$
185	107	subidd	$⊢ φ \to \int_{[B - X, B]} F (x) d x - \int_{[B - X, B]} F (x) d x = 0$
186	185	eqcomd	$⊢ φ \to 0 = \int_{[B - X, B]} F (x) d x - \int_{[B - X, B]} F (x) d x$
187	186	oveq2d	$⊢ φ \to \int_{[B - X, A]} F (x) d x + 0 = \int_{[B - X, A]} F (x) d x + \int_{[B - X, B]} F (x) d x - \int_{[B - X, B]} F (x) d x$
188	187	adantr	$⊢ (φ \land T < X) \to \int_{[B - X, A]} F (x) d x + 0 = \int_{[B - X, A]} F (x) d x + \int_{[B - X, B]} F (x) d x - \int_{[B - X, B]} F (x) d x$
189	169	addid1d	$⊢ (φ \land T < X) \to \int_{[B - X, A]} F (x) d x + 0 = \int_{[B - X, A]} F (x) d x$
190	114 122 113 127 118	eliccd	$⊢ (φ \land T < X) \to A \in [B - X, B]$
191	100	adantlr	$⊢ ((φ \land T < X) \land x \in [B - X, B]) \to F (x) \in ℂ$
192	1 2	iccssred	$⊢ φ \to [A, B] \subseteq ℝ$
193	8 192	feqresmpt	$⊢ φ \to {F ↾}_{[A, B]} = (x \in [A, B] ⟼ F (x))$
194	8 192	fssresd	$⊢ φ \to ({F ↾}_{[A, B]}) : [A, B] ⟶ ℂ$
195		ioossicc	$⊢ (Q (i), Q (i + 1)) \subseteq [Q (i), Q (i + 1)]$
196	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
197	196	adantr	$⊢ (φ \land i \in (0 ..^M)) \to A \in ℝ^{*}$
198	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
199	198	adantr	$⊢ (φ \land i \in (0 ..^M)) \to B \in ℝ^{*}$
200	5 6 7	fourierdlem15	$⊢ φ \to Q : (0 \dots M) ⟶ [A, B]$
201	200	adantr	$⊢ (φ \land i \in (0 ..^M)) \to Q : (0 \dots M) ⟶ [A, B]$
202		simpr	$⊢ (φ \land i \in (0 ..^M)) \to i \in (0 ..^M)$
203	197 199 201 202	fourierdlem8	$⊢ (φ \land i \in (0 ..^M)) \to [Q (i), Q (i + 1)] \subseteq [A, B]$
204	195 203	sstrid	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq [A, B]$
205	204	resabs1d	$⊢ (φ \land i \in (0 ..^M)) \to {({F ↾}_{[A, B]}) ↾}_{(Q (i), Q (i + 1))} = {F ↾}_{(Q (i), Q (i + 1))}$
206	205 10	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to ({({F ↾}_{[A, B]}) ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
207	205	eqcomd	$⊢ (φ \land i \in (0 ..^M)) \to {F ↾}_{(Q (i), Q (i + 1))} = {({F ↾}_{[A, B]}) ↾}_{(Q (i), Q (i + 1))}$
208	207	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i) = ({({F ↾}_{[A, B]}) ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i)$
209	11 208	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({({F ↾}_{[A, B]}) ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
210	207	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1) = ({({F ↾}_{[A, B]}) ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1)$
211	12 210	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to L \in (({({F ↾}_{[A, B]}) ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
212	5 6 7 194 206 209 211	fourierdlem69	$⊢ φ \to {F ↾}_{[A, B]} \in 𝐿^{1}$
213	193 212	eqeltrrd	$⊢ φ \to (x \in [A, B] ⟼ F (x)) \in 𝐿^{1}$
214	213	adantr	$⊢ (φ \land T < X) \to (x \in [A, B] ⟼ F (x)) \in 𝐿^{1}$
215	114 122 190 191 149 214	itgspliticc	$⊢ (φ \land T < X) \to \int_{[B - X, B]} F (x) d x = \int_{[B - X, A]} F (x) d x + \int_{[A, B]} F (x) d x$
216	215	oveq2d	$⊢ (φ \land T < X) \to \int_{[B - X, B]} F (x) d x - \int_{[B - X, B]} F (x) d x = \int_{[B - X, B]} F (x) d x - (\int_{[B - X, A]} F (x) d x + \int_{[A, B]} F (x) d x)$
217	216	oveq2d	$⊢ (φ \land T < X) \to \int_{[B - X, A]} F (x) d x + \int_{[B - X, B]} F (x) d x - \int_{[B - X, B]} F (x) d x = \int_{[B - X, A]} F (x) d x + \int_{[B - X, B]} F (x) d x - (\int_{[B - X, A]} F (x) d x + \int_{[A, B]} F (x) d x)$
218	107	adantr	$⊢ (φ \land T < X) \to \int_{[B - X, B]} F (x) d x \in ℂ$
219	215 218	eqeltrrd	$⊢ (φ \land T < X) \to \int_{[B - X, A]} F (x) d x + \int_{[A, B]} F (x) d x \in ℂ$
220	169 218 219	addsub12d	$⊢ (φ \land T < X) \to \int_{[B - X, A]} F (x) d x + \int_{[B - X, B]} F (x) d x - (\int_{[B - X, A]} F (x) d x + \int_{[A, B]} F (x) d x) = \int_{[B - X, B]} F (x) d x + \int_{[B - X, A]} F (x) d x - (\int_{[B - X, A]} F (x) d x + \int_{[A, B]} F (x) d x)$
221	8	adantr	$⊢ (φ \land x \in [A, B]) \to F : ℝ ⟶ ℂ$
222	1	adantr	$⊢ (φ \land x \in [A, B]) \to A \in ℝ$
223	2	adantr	$⊢ (φ \land x \in [A, B]) \to B \in ℝ$
224		simpr	$⊢ (φ \land x \in [A, B]) \to x \in [A, B]$
225		eliccre	$⊢ (A \in ℝ \land B \in ℝ \land x \in [A, B]) \to x \in ℝ$
226	222 223 224 225	syl3anc	$⊢ (φ \land x \in [A, B]) \to x \in ℝ$
227	221 226	ffvelrnd	$⊢ (φ \land x \in [A, B]) \to F (x) \in ℂ$
228	227 213	itgcl	$⊢ φ \to \int_{[A, B]} F (x) d x \in ℂ$
229	228	adantr	$⊢ (φ \land T < X) \to \int_{[A, B]} F (x) d x \in ℂ$
230	169 169 229	subsub4d	$⊢ (φ \land T < X) \to \int_{[B - X, A]} F (x) d x - \int_{[B - X, A]} F (x) d x - \int_{[A, B]} F (x) d x = \int_{[B - X, A]} F (x) d x - (\int_{[B - X, A]} F (x) d x + \int_{[A, B]} F (x) d x)$
231	230	eqcomd	$⊢ (φ \land T < X) \to \int_{[B - X, A]} F (x) d x - (\int_{[B - X, A]} F (x) d x + \int_{[A, B]} F (x) d x) = \int_{[B - X, A]} F (x) d x - \int_{[B - X, A]} F (x) d x - \int_{[A, B]} F (x) d x$
232	231	oveq2d	$⊢ (φ \land T < X) \to \int_{[B - X, B]} F (x) d x + \int_{[B - X, A]} F (x) d x - (\int_{[B - X, A]} F (x) d x + \int_{[A, B]} F (x) d x) = \int_{[B - X, B]} F (x) d x + (\int_{[B - X, A]} F (x) d x - \int_{[B - X, A]} F (x) d x) - \int_{[A, B]} F (x) d x$
233	169	subidd	$⊢ (φ \land T < X) \to \int_{[B - X, A]} F (x) d x - \int_{[B - X, A]} F (x) d x = 0$
234	233	oveq1d	$⊢ (φ \land T < X) \to \int_{[B - X, A]} F (x) d x - \int_{[B - X, A]} F (x) d x - \int_{[A, B]} F (x) d x = 0 - \int_{[A, B]} F (x) d x$
235		df-neg	$⊢ - \int_{[A, B]} F (x) d x = 0 - \int_{[A, B]} F (x) d x$
236	234 235	eqtr4di	$⊢ (φ \land T < X) \to \int_{[B - X, A]} F (x) d x - \int_{[B - X, A]} F (x) d x - \int_{[A, B]} F (x) d x = - \int_{[A, B]} F (x) d x$
237	236	oveq2d	$⊢ (φ \land T < X) \to \int_{[B - X, B]} F (x) d x + (\int_{[B - X, A]} F (x) d x - \int_{[B - X, A]} F (x) d x) - \int_{[A, B]} F (x) d x = \int_{[B - X, B]} F (x) d x + (- \int_{[A, B]} F (x) d x)$
238	218 229	negsubd	$⊢ (φ \land T < X) \to \int_{[B - X, B]} F (x) d x + (- \int_{[A, B]} F (x) d x) = \int_{[B - X, B]} F (x) d x - \int_{[A, B]} F (x) d x$
239	232 237 238	3eqtrd	$⊢ (φ \land T < X) \to \int_{[B - X, B]} F (x) d x + \int_{[B - X, A]} F (x) d x - (\int_{[B - X, A]} F (x) d x + \int_{[A, B]} F (x) d x) = \int_{[B - X, B]} F (x) d x - \int_{[A, B]} F (x) d x$
240	217 220 239	3eqtrd	$⊢ (φ \land T < X) \to \int_{[B - X, A]} F (x) d x + \int_{[B - X, B]} F (x) d x - \int_{[B - X, B]} F (x) d x = \int_{[B - X, B]} F (x) d x - \int_{[A, B]} F (x) d x$
241	188 189 240	3eqtr3d	$⊢ (φ \land T < X) \to \int_{[B - X, A]} F (x) d x = \int_{[B - X, B]} F (x) d x - \int_{[A, B]} F (x) d x$
242	241	oveq2d	$⊢ (φ \land T < X) \to \int_{[A - X, A]} F (x) d x - \int_{[B - X, A]} F (x) d x = \int_{[A - X, A]} F (x) d x - (\int_{[B - X, B]} F (x) d x - \int_{[A, B]} F (x) d x)$
243	108 107 228	subsubd	$⊢ φ \to \int_{[A - X, A]} F (x) d x - (\int_{[B - X, B]} F (x) d x - \int_{[A, B]} F (x) d x) = \int_{[A - X, A]} F (x) d x - \int_{[B - X, B]} F (x) d x + \int_{[A, B]} F (x) d x$
244	93	oveq2d	$⊢ φ \to \int_{[A - X, A]} F (x) d x - \int_{[B - X, B]} F (x) d x = \int_{[A - X, A]} F (x) d x - \int_{[A - X, A]} F (x) d x$
245	244 109	eqtrd	$⊢ φ \to \int_{[A - X, A]} F (x) d x - \int_{[B - X, B]} F (x) d x = 0$
246	245	oveq1d	$⊢ φ \to \int_{[A - X, A]} F (x) d x - \int_{[B - X, B]} F (x) d x + \int_{[A, B]} F (x) d x = 0 + \int_{[A, B]} F (x) d x$
247	228	addid2d	$⊢ φ \to 0 + \int_{[A, B]} F (x) d x = \int_{[A, B]} F (x) d x$
248	243 246 247	3eqtrd	$⊢ φ \to \int_{[A - X, A]} F (x) d x - (\int_{[B - X, B]} F (x) d x - \int_{[A, B]} F (x) d x) = \int_{[A, B]} F (x) d x$
249	248	adantr	$⊢ (φ \land T < X) \to \int_{[A - X, A]} F (x) d x - (\int_{[B - X, B]} F (x) d x - \int_{[A, B]} F (x) d x) = \int_{[A, B]} F (x) d x$
250	184 242 249	3eqtrd	$⊢ (φ \land T < X) \to \int_{[A - X, B - X]} F (x) d x = \int_{[A, B]} F (x) d x$
251	39	adantr	$⊢ (φ \land X \leq T) \to A - X \in ℝ$
252	29	adantr	$⊢ (φ \land X \leq T) \to B - X \in ℝ$
253	1	adantr	$⊢ (φ \land X \leq T) \to A \in ℝ$
254	39 1 50	ltled	$⊢ φ \to A - X \leq A$
255	254	adantr	$⊢ (φ \land X \leq T) \to A - X \leq A$
256	22	adantr	$⊢ (φ \land X \leq T) \to X \in ℝ$
257	2	adantr	$⊢ (φ \land X \leq T) \to B \in ℝ$
258		id	$⊢ X \leq T \to X \leq T$
259	258 3	breqtrdi	$⊢ X \leq T \to X \leq B - A$
260	259	adantl	$⊢ (φ \land X \leq T) \to X \leq B - A$
261	256 257 253 260	lesubd	$⊢ (φ \land X \leq T) \to A \leq B - X$
262	251 252 253 255 261	eliccd	$⊢ (φ \land X \leq T) \to A \in [A - X, B - X]$
263	158	adantlr	$⊢ ((φ \land X \leq T) \land x \in [A - X, B - X]) \to F (x) \in ℂ$
264	132 102 1 50 78	eliood	$⊢ φ \to A \in (A - X, +∞)$
265	5 3 6 7 8 9 10 11 12 39 264	fourierdlem105	$⊢ φ \to (x \in [A - X, A] ⟼ F (x)) \in 𝐿^{1}$
266	265	adantr	$⊢ (φ \land X \leq T) \to (x \in [A - X, A] ⟼ F (x)) \in 𝐿^{1}$
267	1	leidd	$⊢ φ \to A \leq A$
268	4	rpge0d	$⊢ φ \to 0 \leq X$
269	2 22	subge02d	$⊢ φ \to (0 \leq X \leftrightarrow B - X \leq B)$
270	268 269	mpbid	$⊢ φ \to B - X \leq B$
271		iccss	$⊢ ((A \in ℝ \land B \in ℝ) \land (A \leq A \land B - X \leq B)) \to [A, B - X] \subseteq [A, B]$
272	1 2 267 270 271	syl22anc	$⊢ φ \to [A, B - X] \subseteq [A, B]$
273		iccmbl	$⊢ (A \in ℝ \land B - X \in ℝ) \to [A, B - X] \in dom vol$
274	1 29 273	syl2anc	$⊢ φ \to [A, B - X] \in dom vol$
275	272 274 227 213	iblss	$⊢ φ \to (x \in [A, B - X] ⟼ F (x)) \in 𝐿^{1}$
276	275	adantr	$⊢ (φ \land X \leq T) \to (x \in [A, B - X] ⟼ F (x)) \in 𝐿^{1}$
277	251 252 262 263 266 276	itgspliticc	$⊢ (φ \land X \leq T) \to \int_{[A - X, B - X]} F (x) d x = \int_{[A - X, A]} F (x) d x + \int_{[A, B - X]} F (x) d x$
278	268	adantr	$⊢ (φ \land X \leq T) \to 0 \leq X$
279	269	adantr	$⊢ (φ \land X \leq T) \to (0 \leq X \leftrightarrow B - X \leq B)$
280	278 279	mpbid	$⊢ (φ \land X \leq T) \to B - X \leq B$
281	253 257 252 261 280	eliccd	$⊢ (φ \land X \leq T) \to B - X \in [A, B]$
282	227	adantlr	$⊢ ((φ \land X \leq T) \land x \in [A, B]) \to F (x) \in ℂ$
283	2	leidd	$⊢ φ \to B \leq B$
284	283	adantr	$⊢ (φ \land X \leq T) \to B \leq B$
285		iccss	$⊢ ((A \in ℝ \land B \in ℝ) \land (A \leq B - X \land B \leq B)) \to [B - X, B] \subseteq [A, B]$
286	253 257 261 284 285	syl22anc	$⊢ (φ \land X \leq T) \to [B - X, B] \subseteq [A, B]$
287		iccmbl	$⊢ (B - X \in ℝ \land B \in ℝ) \to [B - X, B] \in dom vol$
288	29 2 287	syl2anc	$⊢ φ \to [B - X, B] \in dom vol$
289	288	adantr	$⊢ (φ \land X \leq T) \to [B - X, B] \in dom vol$
290	213	adantr	$⊢ (φ \land X \leq T) \to (x \in [A, B] ⟼ F (x)) \in 𝐿^{1}$
291	286 289 282 290	iblss	$⊢ (φ \land X \leq T) \to (x \in [B - X, B] ⟼ F (x)) \in 𝐿^{1}$
292	253 257 281 282 276 291	itgspliticc	$⊢ (φ \land X \leq T) \to \int_{[A, B]} F (x) d x = \int_{[A, B - X]} F (x) d x + \int_{[B - X, B]} F (x) d x$
293	292	oveq1d	$⊢ (φ \land X \leq T) \to \int_{[A, B]} F (x) d x - \int_{[B - X, B]} F (x) d x = \int_{[A, B - X]} F (x) d x + \int_{[B - X, B]} F (x) d x - \int_{[B - X, B]} F (x) d x$
294	8	adantr	$⊢ (φ \land x \in [A, B - X]) \to F : ℝ ⟶ ℂ$
295	1	adantr	$⊢ (φ \land x \in [A, B - X]) \to A \in ℝ$
296	29	adantr	$⊢ (φ \land x \in [A, B - X]) \to B - X \in ℝ$
297		simpr	$⊢ (φ \land x \in [A, B - X]) \to x \in [A, B - X]$
298		eliccre	$⊢ (A \in ℝ \land B - X \in ℝ \land x \in [A, B - X]) \to x \in ℝ$
299	295 296 297 298	syl3anc	$⊢ (φ \land x \in [A, B - X]) \to x \in ℝ$
300	294 299	ffvelrnd	$⊢ (φ \land x \in [A, B - X]) \to F (x) \in ℂ$
301	300 275	itgcl	$⊢ φ \to \int_{[A, B - X]} F (x) d x \in ℂ$
302	301 107 107	addsubassd	$⊢ φ \to \int_{[A, B - X]} F (x) d x + \int_{[B - X, B]} F (x) d x - \int_{[B - X, B]} F (x) d x = \int_{[A, B - X]} F (x) d x + \int_{[B - X, B]} F (x) d x - \int_{[B - X, B]} F (x) d x$
303	302	adantr	$⊢ (φ \land X \leq T) \to \int_{[A, B - X]} F (x) d x + \int_{[B - X, B]} F (x) d x - \int_{[B - X, B]} F (x) d x = \int_{[A, B - X]} F (x) d x + \int_{[B - X, B]} F (x) d x - \int_{[B - X, B]} F (x) d x$
304	185	oveq2d	$⊢ φ \to \int_{[A, B - X]} F (x) d x + \int_{[B - X, B]} F (x) d x - \int_{[B - X, B]} F (x) d x = \int_{[A, B - X]} F (x) d x + 0$
305	301	addid1d	$⊢ φ \to \int_{[A, B - X]} F (x) d x + 0 = \int_{[A, B - X]} F (x) d x$
306	304 305	eqtrd	$⊢ φ \to \int_{[A, B - X]} F (x) d x + \int_{[B - X, B]} F (x) d x - \int_{[B - X, B]} F (x) d x = \int_{[A, B - X]} F (x) d x$
307	306	adantr	$⊢ (φ \land X \leq T) \to \int_{[A, B - X]} F (x) d x + \int_{[B - X, B]} F (x) d x - \int_{[B - X, B]} F (x) d x = \int_{[A, B - X]} F (x) d x$
308	293 303 307	3eqtrrd	$⊢ (φ \land X \leq T) \to \int_{[A, B - X]} F (x) d x = \int_{[A, B]} F (x) d x - \int_{[B - X, B]} F (x) d x$
309	308	oveq2d	$⊢ (φ \land X \leq T) \to \int_{[A - X, A]} F (x) d x + \int_{[A, B - X]} F (x) d x = \int_{[A - X, A]} F (x) d x + \int_{[A, B]} F (x) d x - \int_{[B - X, B]} F (x) d x$
310	93	adantr	$⊢ (φ \land X \leq T) \to \int_{[B - X, B]} F (x) d x = \int_{[A - X, A]} F (x) d x$
311	107	adantr	$⊢ (φ \land X \leq T) \to \int_{[B - X, B]} F (x) d x \in ℂ$
312	310 311	eqeltrrd	$⊢ (φ \land X \leq T) \to \int_{[A - X, A]} F (x) d x \in ℂ$
313	282 290	itgcl	$⊢ (φ \land X \leq T) \to \int_{[A, B]} F (x) d x \in ℂ$
314	312 313 311	addsub12d	$⊢ (φ \land X \leq T) \to \int_{[A - X, A]} F (x) d x + \int_{[A, B]} F (x) d x - \int_{[B - X, B]} F (x) d x = \int_{[A, B]} F (x) d x + \int_{[A - X, A]} F (x) d x - \int_{[B - X, B]} F (x) d x$
315	313 312 311	addsubassd	$⊢ (φ \land X \leq T) \to \int_{[A, B]} F (x) d x + \int_{[A - X, A]} F (x) d x - \int_{[B - X, B]} F (x) d x = \int_{[A, B]} F (x) d x + \int_{[A - X, A]} F (x) d x - \int_{[B - X, B]} F (x) d x$
316	314 315	eqtr4d	$⊢ (φ \land X \leq T) \to \int_{[A - X, A]} F (x) d x + \int_{[A, B]} F (x) d x - \int_{[B - X, B]} F (x) d x = \int_{[A, B]} F (x) d x + \int_{[A - X, A]} F (x) d x - \int_{[B - X, B]} F (x) d x$
317	277 309 316	3eqtrd	$⊢ (φ \land X \leq T) \to \int_{[A - X, B - X]} F (x) d x = \int_{[A, B]} F (x) d x + \int_{[A - X, A]} F (x) d x - \int_{[B - X, B]} F (x) d x$
318	310	oveq2d	$⊢ (φ \land X \leq T) \to \int_{[A, B]} F (x) d x + \int_{[A - X, A]} F (x) d x - \int_{[B - X, B]} F (x) d x = \int_{[A, B]} F (x) d x + \int_{[A - X, A]} F (x) d x - \int_{[A - X, A]} F (x) d x$
319	313 312	pncand	$⊢ (φ \land X \leq T) \to \int_{[A, B]} F (x) d x + \int_{[A - X, A]} F (x) d x - \int_{[A - X, A]} F (x) d x = \int_{[A, B]} F (x) d x$
320	317 318 319	3eqtrd	$⊢ (φ \land X \leq T) \to \int_{[A - X, B - X]} F (x) d x = \int_{[A, B]} F (x) d x$
321	250 320 55 22	ltlecasei	$⊢ φ \to \int_{[A - X, B - X]} F (x) d x = \int_{[A, B]} F (x) d x$

Metamath Proof Explorer

Theorem fourierdlem107

Proof