fourierdlem82

Description: Integral by substitution, adding a constant to the function's argument, for a function on an open interval with finite limits ad boundary points. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem82.1	$⊢ G = (x \in [A, B] ⟼ if (x = A, R, if (x = B, L, ({F ↾}_{(A, B)}) (x))))$
	fourierdlem82.2	$⊢ φ \to A \in ℝ$
	fourierdlem82.3	$⊢ φ \to B \in ℝ$
	fourierdlem82.4	$⊢ φ \to A < B$
	fourierdlem82.5	$⊢ φ \to F : [A, B] ⟶ ℂ$
	fourierdlem82.6	$⊢ φ \to ({F ↾}_{(A, B)}) : (A, B) \underset{cn}{⟶} ℂ$
	fourierdlem82.7	$⊢ φ \to L \in (F {lim}_{ℂ} B)$
	fourierdlem82.8	$⊢ φ \to R \in (F {lim}_{ℂ} A)$
	fourierdlem82.9	$⊢ φ \to X \in ℝ$
Assertion	fourierdlem82	$⊢ φ \to \int_{[A, B]} F (t) d t = \int_{[A - X, B - X]} F (X + t) d t$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem82.1	$⊢ G = (x \in [A, B] ⟼ if (x = A, R, if (x = B, L, ({F ↾}_{(A, B)}) (x))))$
2		fourierdlem82.2	$⊢ φ \to A \in ℝ$
3		fourierdlem82.3	$⊢ φ \to B \in ℝ$
4		fourierdlem82.4	$⊢ φ \to A < B$
5		fourierdlem82.5	$⊢ φ \to F : [A, B] ⟶ ℂ$
6		fourierdlem82.6	$⊢ φ \to ({F ↾}_{(A, B)}) : (A, B) \underset{cn}{⟶} ℂ$
7		fourierdlem82.7	$⊢ φ \to L \in (F {lim}_{ℂ} B)$
8		fourierdlem82.8	$⊢ φ \to R \in (F {lim}_{ℂ} A)$
9		fourierdlem82.9	$⊢ φ \to X \in ℝ$
10	2 3 4	ltled	$⊢ φ \to A \leq B$
11	2 3 9 10	lesub1dd	$⊢ φ \to A - X \leq B - X$
12	11	ditgpos	$⊢ φ \to \int_{(A - X)}^{(B - X)} G (X + t) d t = \int_{(A - X, B - X)} G (X + t) d t$
13		iftrue	$⊢ x = A \to if (x = A, R, if (x = B, L, ({F ↾}_{(A, B)}) (x))) = R$
14	13	adantl	$⊢ (φ \land x = A) \to if (x = A, R, if (x = B, L, ({F ↾}_{(A, B)}) (x))) = R$
15		iftrue	$⊢ x = A \to if (x = A, R, if (x = B, L, F (x))) = R$
16	15	adantl	$⊢ (φ \land x = A) \to if (x = A, R, if (x = B, L, F (x))) = R$
17	14 16	eqtr4d	$⊢ (φ \land x = A) \to if (x = A, R, if (x = B, L, ({F ↾}_{(A, B)}) (x))) = if (x = A, R, if (x = B, L, F (x)))$
18	17	adantlr	$⊢ ((φ \land x \in [A, B]) \land x = A) \to if (x = A, R, if (x = B, L, ({F ↾}_{(A, B)}) (x))) = if (x = A, R, if (x = B, L, F (x)))$
19		iffalse	$⊢ \neg x = A \to if (x = A, R, if (x = B, L, ({F ↾}_{(A, B)}) (x))) = if (x = B, L, ({F ↾}_{(A, B)}) (x))$
20		iftrue	$⊢ x = B \to if (x = B, L, ({F ↾}_{(A, B)}) (x)) = L$
21	19 20	sylan9eq	$⊢ (\neg x = A \land x = B) \to if (x = A, R, if (x = B, L, ({F ↾}_{(A, B)}) (x))) = L$
22	21	adantll	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land x = B) \to if (x = A, R, if (x = B, L, ({F ↾}_{(A, B)}) (x))) = L$
23		iffalse	$⊢ \neg x = A \to if (x = A, R, if (x = B, L, F (x))) = if (x = B, L, F (x))$
24		iftrue	$⊢ x = B \to if (x = B, L, F (x)) = L$
25	23 24	sylan9eq	$⊢ (\neg x = A \land x = B) \to if (x = A, R, if (x = B, L, F (x))) = L$
26	25	adantll	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land x = B) \to if (x = A, R, if (x = B, L, F (x))) = L$
27	22 26	eqtr4d	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land x = B) \to if (x = A, R, if (x = B, L, ({F ↾}_{(A, B)}) (x))) = if (x = A, R, if (x = B, L, F (x)))$
28		iffalse	$⊢ \neg x = B \to if (x = B, L, ({F ↾}_{(A, B)}) (x)) = ({F ↾}_{(A, B)}) (x)$
29	28	adantl	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to if (x = B, L, ({F ↾}_{(A, B)}) (x)) = ({F ↾}_{(A, B)}) (x)$
30	19	ad2antlr	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to if (x = A, R, if (x = B, L, ({F ↾}_{(A, B)}) (x))) = if (x = B, L, ({F ↾}_{(A, B)}) (x))$
31		iffalse	$⊢ \neg x = B \to if (x = B, L, F (x)) = F (x)$
32	31	adantl	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to if (x = B, L, F (x)) = F (x)$
33	23	ad2antlr	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to if (x = A, R, if (x = B, L, F (x))) = if (x = B, L, F (x))$
34	2	rexrd	$⊢ φ \to A \in ℝ^{*}$
35	34	ad3antrrr	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to A \in ℝ^{*}$
36	3	rexrd	$⊢ φ \to B \in ℝ^{*}$
37	36	ad3antrrr	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to B \in ℝ^{*}$
38	2	adantr	$⊢ (φ \land x \in [A, B]) \to A \in ℝ$
39	3	adantr	$⊢ (φ \land x \in [A, B]) \to B \in ℝ$
40		simpr	$⊢ (φ \land x \in [A, B]) \to x \in [A, B]$
41		eliccre	$⊢ (A \in ℝ \land B \in ℝ \land x \in [A, B]) \to x \in ℝ$
42	38 39 40 41	syl3anc	$⊢ (φ \land x \in [A, B]) \to x \in ℝ$
43	42	ad2antrr	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to x \in ℝ$
44	2	ad2antrr	$⊢ ((φ \land x \in [A, B]) \land \neg x = A) \to A \in ℝ$
45	42	adantr	$⊢ ((φ \land x \in [A, B]) \land \neg x = A) \to x \in ℝ$
46		elicc2	$⊢ (A \in ℝ \land B \in ℝ) \to (x \in [A, B] \leftrightarrow (x \in ℝ \land A \leq x \land x \leq B))$
47	38 39 46	syl2anc	$⊢ (φ \land x \in [A, B]) \to (x \in [A, B] \leftrightarrow (x \in ℝ \land A \leq x \land x \leq B))$
48	40 47	mpbid	$⊢ (φ \land x \in [A, B]) \to (x \in ℝ \land A \leq x \land x \leq B)$
49	48	simp2d	$⊢ (φ \land x \in [A, B]) \to A \leq x$
50	49	adantr	$⊢ ((φ \land x \in [A, B]) \land \neg x = A) \to A \leq x$
51		neqne	$⊢ \neg x = A \to x \neq A$
52	51	adantl	$⊢ ((φ \land x \in [A, B]) \land \neg x = A) \to x \neq A$
53	44 45 50 52	leneltd	$⊢ ((φ \land x \in [A, B]) \land \neg x = A) \to A < x$
54	53	adantr	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to A < x$
55	42	adantr	$⊢ ((φ \land x \in [A, B]) \land \neg x = B) \to x \in ℝ$
56	3	ad2antrr	$⊢ ((φ \land x \in [A, B]) \land \neg x = B) \to B \in ℝ$
57	48	simp3d	$⊢ (φ \land x \in [A, B]) \to x \leq B$
58	57	adantr	$⊢ ((φ \land x \in [A, B]) \land \neg x = B) \to x \leq B$
59		nesym	$⊢ B \neq x \leftrightarrow \neg x = B$
60	59	bilanri	$⊢ ((φ \land x \in [A, B]) \land \neg x = B) \to B \neq x$
61	55 56 58 60	leneltd	$⊢ ((φ \land x \in [A, B]) \land \neg x = B) \to x < B$
62	61	adantlr	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to x < B$
63	35 37 43 54 62	eliood	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to x \in (A, B)$
64		fvres	$⊢ x \in (A, B) \to ({F ↾}_{(A, B)}) (x) = F (x)$
65	63 64	syl	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to ({F ↾}_{(A, B)}) (x) = F (x)$
66	32 33 65	3eqtr4d	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to if (x = A, R, if (x = B, L, F (x))) = ({F ↾}_{(A, B)}) (x)$
67	29 30 66	3eqtr4d	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to if (x = A, R, if (x = B, L, ({F ↾}_{(A, B)}) (x))) = if (x = A, R, if (x = B, L, F (x)))$
68	27 67	pm2.61dan	$⊢ ((φ \land x \in [A, B]) \land \neg x = A) \to if (x = A, R, if (x = B, L, ({F ↾}_{(A, B)}) (x))) = if (x = A, R, if (x = B, L, F (x)))$
69	18 68	pm2.61dan	$⊢ (φ \land x \in [A, B]) \to if (x = A, R, if (x = B, L, ({F ↾}_{(A, B)}) (x))) = if (x = A, R, if (x = B, L, F (x)))$
70	69	mpteq2dva	$⊢ φ \to (x \in [A, B] ⟼ if (x = A, R, if (x = B, L, ({F ↾}_{(A, B)}) (x)))) = (x \in [A, B] ⟼ if (x = A, R, if (x = B, L, F (x))))$
71	1 70	eqtrid	$⊢ φ \to G = (x \in [A, B] ⟼ if (x = A, R, if (x = B, L, F (x))))$
72	71	adantr	$⊢ (φ \land t \in (A - X, B - X)) \to G = (x \in [A, B] ⟼ if (x = A, R, if (x = B, L, F (x))))$
73		eqeq1	$⊢ x = X + t \to (x = A \leftrightarrow X + t = A)$
74		eqeq1	$⊢ x = X + t \to (x = B \leftrightarrow X + t = B)$
75		fveq2	$⊢ x = X + t \to F (x) = F (X + t)$
76	74 75	ifbieq2d	$⊢ x = X + t \to if (x = B, L, F (x)) = if (X + t = B, L, F (X + t))$
77	73 76	ifbieq2d	$⊢ x = X + t \to if (x = A, R, if (x = B, L, F (x))) = if (X + t = A, R, if (X + t = B, L, F (X + t)))$
78	2	adantr	$⊢ (φ \land t \in (A - X, B - X)) \to A \in ℝ$
79		simpr	$⊢ (φ \land t \in (A - X, B - X)) \to t \in (A - X, B - X)$
80	2 9	resubcld	$⊢ φ \to A - X \in ℝ$
81	80	rexrd	$⊢ φ \to A - X \in ℝ^{*}$
82	81	adantr	$⊢ (φ \land t \in (A - X, B - X)) \to A - X \in ℝ^{*}$
83	3 9	resubcld	$⊢ φ \to B - X \in ℝ$
84	83	rexrd	$⊢ φ \to B - X \in ℝ^{*}$
85	84	adantr	$⊢ (φ \land t \in (A - X, B - X)) \to B - X \in ℝ^{*}$
86		elioo2	$⊢ (A - X \in ℝ^{} \land B - X \in ℝ^{}) \to (t \in (A - X, B - X) \leftrightarrow (t \in ℝ \land A - X < t \land t < B - X))$
87	82 85 86	syl2anc	$⊢ (φ \land t \in (A - X, B - X)) \to (t \in (A - X, B - X) \leftrightarrow (t \in ℝ \land A - X < t \land t < B - X))$
88	79 87	mpbid	$⊢ (φ \land t \in (A - X, B - X)) \to (t \in ℝ \land A - X < t \land t < B - X)$
89	88	simp2d	$⊢ (φ \land t \in (A - X, B - X)) \to A - X < t$
90	9	adantr	$⊢ (φ \land t \in (A - X, B - X)) \to X \in ℝ$
91	88	simp1d	$⊢ (φ \land t \in (A - X, B - X)) \to t \in ℝ$
92	78 90 91	ltsubadd2d	$⊢ (φ \land t \in (A - X, B - X)) \to (A - X < t \leftrightarrow A < X + t)$
93	89 92	mpbid	$⊢ (φ \land t \in (A - X, B - X)) \to A < X + t$
94	78 93	gtned	$⊢ (φ \land t \in (A - X, B - X)) \to X + t \neq A$
95	94	neneqd	$⊢ (φ \land t \in (A - X, B - X)) \to \neg X + t = A$
96	95	iffalsed	$⊢ (φ \land t \in (A - X, B - X)) \to if (X + t = A, R, if (X + t = B, L, F (X + t))) = if (X + t = B, L, F (X + t))$
97	90 91	readdcld	$⊢ (φ \land t \in (A - X, B - X)) \to X + t \in ℝ$
98	88	simp3d	$⊢ (φ \land t \in (A - X, B - X)) \to t < B - X$
99	3	adantr	$⊢ (φ \land t \in (A - X, B - X)) \to B \in ℝ$
100	90 91 99	ltaddsub2d	$⊢ (φ \land t \in (A - X, B - X)) \to (X + t < B \leftrightarrow t < B - X)$
101	98 100	mpbird	$⊢ (φ \land t \in (A - X, B - X)) \to X + t < B$
102	97 101	ltned	$⊢ (φ \land t \in (A - X, B - X)) \to X + t \neq B$
103	102	neneqd	$⊢ (φ \land t \in (A - X, B - X)) \to \neg X + t = B$
104	103	iffalsed	$⊢ (φ \land t \in (A - X, B - X)) \to if (X + t = B, L, F (X + t)) = F (X + t)$
105	96 104	eqtrd	$⊢ (φ \land t \in (A - X, B - X)) \to if (X + t = A, R, if (X + t = B, L, F (X + t))) = F (X + t)$
106	77 105	sylan9eqr	$⊢ ((φ \land t \in (A - X, B - X)) \land x = X + t) \to if (x = A, R, if (x = B, L, F (x))) = F (X + t)$
107	78 97 93	ltled	$⊢ (φ \land t \in (A - X, B - X)) \to A \leq X + t$
108	97 99 101	ltled	$⊢ (φ \land t \in (A - X, B - X)) \to X + t \leq B$
109	78 99 97 107 108	eliccd	$⊢ (φ \land t \in (A - X, B - X)) \to X + t \in [A, B]$
110	5	ffund	$⊢ φ \to Fun F$
111	110	adantr	$⊢ (φ \land t \in (A - X, B - X)) \to Fun F$
112	5	fdmd	$⊢ φ \to dom F = [A, B]$
113	112	eqcomd	$⊢ φ \to [A, B] = dom F$
114	113	adantr	$⊢ (φ \land t \in (A - X, B - X)) \to [A, B] = dom F$
115	109 114	eleqtrd	$⊢ (φ \land t \in (A - X, B - X)) \to X + t \in dom F$
116		fvelrn	$⊢ (Fun F \land X + t \in dom F) \to F (X + t) \in ran F$
117	111 115 116	syl2anc	$⊢ (φ \land t \in (A - X, B - X)) \to F (X + t) \in ran F$
118	72 106 109 117	fvmptd	$⊢ (φ \land t \in (A - X, B - X)) \to G (X + t) = F (X + t)$
119	118	itgeq2dv	$⊢ φ \to \int_{(A - X, B - X)} G (X + t) d t = \int_{(A - X, B - X)} F (X + t) d t$
120	5	frnd	$⊢ φ \to ran F \subseteq ℂ$
121	120	adantr	$⊢ (φ \land t \in [A - X, B - X]) \to ran F \subseteq ℂ$
122	110	adantr	$⊢ (φ \land t \in [A - X, B - X]) \to Fun F$
123	2	adantr	$⊢ (φ \land t \in [A - X, B - X]) \to A \in ℝ$
124	3	adantr	$⊢ (φ \land t \in [A - X, B - X]) \to B \in ℝ$
125	9	adantr	$⊢ (φ \land t \in [A - X, B - X]) \to X \in ℝ$
126	80	adantr	$⊢ (φ \land t \in [A - X, B - X]) \to A - X \in ℝ$
127	83	adantr	$⊢ (φ \land t \in [A - X, B - X]) \to B - X \in ℝ$
128		simpr	$⊢ (φ \land t \in [A - X, B - X]) \to t \in [A - X, B - X]$
129		eliccre	$⊢ (A - X \in ℝ \land B - X \in ℝ \land t \in [A - X, B - X]) \to t \in ℝ$
130	126 127 128 129	syl3anc	$⊢ (φ \land t \in [A - X, B - X]) \to t \in ℝ$
131	125 130	readdcld	$⊢ (φ \land t \in [A - X, B - X]) \to X + t \in ℝ$
132		elicc2	$⊢ (A - X \in ℝ \land B - X \in ℝ) \to (t \in [A - X, B - X] \leftrightarrow (t \in ℝ \land A - X \leq t \land t \leq B - X))$
133	126 127 132	syl2anc	$⊢ (φ \land t \in [A - X, B - X]) \to (t \in [A - X, B - X] \leftrightarrow (t \in ℝ \land A - X \leq t \land t \leq B - X))$
134	128 133	mpbid	$⊢ (φ \land t \in [A - X, B - X]) \to (t \in ℝ \land A - X \leq t \land t \leq B - X)$
135	134	simp2d	$⊢ (φ \land t \in [A - X, B - X]) \to A - X \leq t$
136	123 125 130	lesubadd2d	$⊢ (φ \land t \in [A - X, B - X]) \to (A - X \leq t \leftrightarrow A \leq X + t)$
137	135 136	mpbid	$⊢ (φ \land t \in [A - X, B - X]) \to A \leq X + t$
138	134	simp3d	$⊢ (φ \land t \in [A - X, B - X]) \to t \leq B - X$
139	125 130 124	leaddsub2d	$⊢ (φ \land t \in [A - X, B - X]) \to (X + t \leq B \leftrightarrow t \leq B - X)$
140	138 139	mpbird	$⊢ (φ \land t \in [A - X, B - X]) \to X + t \leq B$
141	123 124 131 137 140	eliccd	$⊢ (φ \land t \in [A - X, B - X]) \to X + t \in [A, B]$
142	113	adantr	$⊢ (φ \land t \in [A - X, B - X]) \to [A, B] = dom F$
143	141 142	eleqtrd	$⊢ (φ \land t \in [A - X, B - X]) \to X + t \in dom F$
144	122 143 116	syl2anc	$⊢ (φ \land t \in [A - X, B - X]) \to F (X + t) \in ran F$
145	121 144	sseldd	$⊢ (φ \land t \in [A - X, B - X]) \to F (X + t) \in ℂ$
146	80 83 145	itgioo	$⊢ φ \to \int_{(A - X, B - X)} F (X + t) d t = \int_{[A - X, B - X]} F (X + t) d t$
147	12 119 146	3eqtrrd	$⊢ φ \to \int_{[A - X, B - X]} F (X + t) d t = \int_{(A - X)}^{(B - X)} G (X + t) d t$
148		nfv	$⊢ Ⅎ x φ$
149	2 3 4 5	limcicciooub	$⊢ φ \to ({F ↾}_{(A, B)}) {lim}_{ℂ} B = F {lim}_{ℂ} B$
150	7 149	eleqtrrd	$⊢ φ \to L \in (({F ↾}_{(A, B)}) {lim}_{ℂ} B)$
151	2 3 4 5	limciccioolb	$⊢ φ \to ({F ↾}_{(A, B)}) {lim}_{ℂ} A = F {lim}_{ℂ} A$
152	8 151	eleqtrrd	$⊢ φ \to R \in (({F ↾}_{(A, B)}) {lim}_{ℂ} A)$
153	148 1 2 3 6 150 152	cncfiooicc	$⊢ φ \to G : [A, B] \underset{cn}{⟶} ℂ$
154	2 3 10 9 153	itgsbtaddcnst	$⊢ φ \to \int_{(A - X)}^{(B - X)} G (X + t) d t = \int_{A}^{B} G (s) d s$
155	10	ditgpos	$⊢ φ \to \int_{A}^{B} G (s) d s = \int_{(A, B)} G (s) d s$
156		fveq2	$⊢ s = t \to G (s) = G (t)$
157	156	cbvitgv	$⊢ \int_{(A, B)} G (s) d s = \int_{(A, B)} G (t) d t$
158	1	a1i	$⊢ (φ \land t \in (A, B)) \to G = (x \in [A, B] ⟼ if (x = A, R, if (x = B, L, ({F ↾}_{(A, B)}) (x))))$
159	2	ad2antrr	$⊢ ((φ \land t \in (A, B)) \land x = t) \to A \in ℝ$
160		simplr	$⊢ ((φ \land t \in (A, B)) \land x = t) \to t \in (A, B)$
161	34	ad2antrr	$⊢ ((φ \land t \in (A, B)) \land x = t) \to A \in ℝ^{*}$
162	36	ad2antrr	$⊢ ((φ \land t \in (A, B)) \land x = t) \to B \in ℝ^{*}$
163		elioo2	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (t \in (A, B) \leftrightarrow (t \in ℝ \land A < t \land t < B))$
164	161 162 163	syl2anc	$⊢ ((φ \land t \in (A, B)) \land x = t) \to (t \in (A, B) \leftrightarrow (t \in ℝ \land A < t \land t < B))$
165	160 164	mpbid	$⊢ ((φ \land t \in (A, B)) \land x = t) \to (t \in ℝ \land A < t \land t < B)$
166	165	simp2d	$⊢ ((φ \land t \in (A, B)) \land x = t) \to A < t$
167		simpr	$⊢ ((φ \land t \in (A, B)) \land x = t) \to x = t$
168	166 167	breqtrrd	$⊢ ((φ \land t \in (A, B)) \land x = t) \to A < x$
169	159 168	gtned	$⊢ ((φ \land t \in (A, B)) \land x = t) \to x \neq A$
170	169	neneqd	$⊢ ((φ \land t \in (A, B)) \land x = t) \to \neg x = A$
171	170	iffalsed	$⊢ ((φ \land t \in (A, B)) \land x = t) \to if (x = A, R, if (x = B, L, ({F ↾}_{(A, B)}) (x))) = if (x = B, L, ({F ↾}_{(A, B)}) (x))$
172	165	simp1d	$⊢ ((φ \land t \in (A, B)) \land x = t) \to t \in ℝ$
173	167 172	eqeltrd	$⊢ ((φ \land t \in (A, B)) \land x = t) \to x \in ℝ$
174	165	simp3d	$⊢ ((φ \land t \in (A, B)) \land x = t) \to t < B$
175	167 174	eqbrtrd	$⊢ ((φ \land t \in (A, B)) \land x = t) \to x < B$
176	173 175	ltned	$⊢ ((φ \land t \in (A, B)) \land x = t) \to x \neq B$
177	176	neneqd	$⊢ ((φ \land t \in (A, B)) \land x = t) \to \neg x = B$
178	177	iffalsed	$⊢ ((φ \land t \in (A, B)) \land x = t) \to if (x = B, L, ({F ↾}_{(A, B)}) (x)) = ({F ↾}_{(A, B)}) (x)$
179	167 160	eqeltrd	$⊢ ((φ \land t \in (A, B)) \land x = t) \to x \in (A, B)$
180	179 64	syl	$⊢ ((φ \land t \in (A, B)) \land x = t) \to ({F ↾}_{(A, B)}) (x) = F (x)$
181		fveq2	$⊢ x = t \to F (x) = F (t)$
182	181	adantl	$⊢ ((φ \land t \in (A, B)) \land x = t) \to F (x) = F (t)$
183	180 182	eqtrd	$⊢ ((φ \land t \in (A, B)) \land x = t) \to ({F ↾}_{(A, B)}) (x) = F (t)$
184	171 178 183	3eqtrd	$⊢ ((φ \land t \in (A, B)) \land x = t) \to if (x = A, R, if (x = B, L, ({F ↾}_{(A, B)}) (x))) = F (t)$
185		ioossicc	$⊢ (A, B) \subseteq [A, B]$
186		simpr	$⊢ (φ \land t \in (A, B)) \to t \in (A, B)$
187	185 186	sselid	$⊢ (φ \land t \in (A, B)) \to t \in [A, B]$
188	110	adantr	$⊢ (φ \land t \in (A, B)) \to Fun F$
189	113	adantr	$⊢ (φ \land t \in (A, B)) \to [A, B] = dom F$
190	187 189	eleqtrd	$⊢ (φ \land t \in (A, B)) \to t \in dom F$
191		fvelrn	$⊢ (Fun F \land t \in dom F) \to F (t) \in ran F$
192	188 190 191	syl2anc	$⊢ (φ \land t \in (A, B)) \to F (t) \in ran F$
193	158 184 187 192	fvmptd	$⊢ (φ \land t \in (A, B)) \to G (t) = F (t)$
194	193	itgeq2dv	$⊢ φ \to \int_{(A, B)} G (t) d t = \int_{(A, B)} F (t) d t$
195	157 194	eqtrid	$⊢ φ \to \int_{(A, B)} G (s) d s = \int_{(A, B)} F (t) d t$
196	5	ffvelcdmda	$⊢ (φ \land t \in [A, B]) \to F (t) \in ℂ$
197	2 3 196	itgioo	$⊢ φ \to \int_{(A, B)} F (t) d t = \int_{[A, B]} F (t) d t$
198	155 195 197	3eqtrd	$⊢ φ \to \int_{A}^{B} G (s) d s = \int_{[A, B]} F (t) d t$
199	147 154 198	3eqtrrd	$⊢ φ \to \int_{[A, B]} F (t) d t = \int_{[A - X, B - X]} F (X + t) d t$

Metamath Proof Explorer

Theorem fourierdlem82

Proof