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