itgiccshift

Description: The integral of a function, F stays the same if its closed interval domain is shifted by T . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	itgiccshift.a	$⊢ φ \to A \in ℝ$
	itgiccshift.b	$⊢ φ \to B \in ℝ$
	itgiccshift.aleb	$⊢ φ \to A \leq B$
	itgiccshift.f	$⊢ φ \to F : [A, B] \underset{cn}{⟶} ℂ$
	itgiccshift.t	$⊢ φ \to T \in ℝ^{+}$
	itgiccshift.g	$⊢ G = (x \in [A + T, B + T] ⟼ F (x - T))$
Assertion	itgiccshift	$⊢ φ \to \int_{[A + T, B + T]} G (x) d x = \int_{[A, B]} F (x) d x$

Proof

Step	Hyp	Ref	Expression
1		itgiccshift.a	$⊢ φ \to A \in ℝ$
2		itgiccshift.b	$⊢ φ \to B \in ℝ$
3		itgiccshift.aleb	$⊢ φ \to A \leq B$
4		itgiccshift.f	$⊢ φ \to F : [A, B] \underset{cn}{⟶} ℂ$
5		itgiccshift.t	$⊢ φ \to T \in ℝ^{+}$
6		itgiccshift.g	$⊢ G = (x \in [A + T, B + T] ⟼ F (x - T))$
7	5	rpred	$⊢ φ \to T \in ℝ$
8	1 2 7 3	leadd1dd	$⊢ φ \to A + T \leq B + T$
9	8	ditgpos	$⊢ φ \to \int_{(A + T)}^{(B + T)} G (x) d x = \int_{(A + T, B + T)} G (x) d x$
10	1 7	readdcld	$⊢ φ \to A + T \in ℝ$
11	2 7	readdcld	$⊢ φ \to B + T \in ℝ$
12		cncff	$⊢ F : [A, B] \underset{cn}{⟶} ℂ \to F : [A, B] ⟶ ℂ$
13	4 12	syl	$⊢ φ \to F : [A, B] ⟶ ℂ$
14	13	adantr	$⊢ (φ \land x \in [A + T, B + T]) \to F : [A, B] ⟶ ℂ$
15	1	adantr	$⊢ (φ \land x \in [A + T, B + T]) \to A \in ℝ$
16	2	adantr	$⊢ (φ \land x \in [A + T, B + T]) \to B \in ℝ$
17	10	adantr	$⊢ (φ \land x \in [A + T, B + T]) \to A + T \in ℝ$
18	11	adantr	$⊢ (φ \land x \in [A + T, B + T]) \to B + T \in ℝ$
19		simpr	$⊢ (φ \land x \in [A + T, B + T]) \to x \in [A + T, B + T]$
20		eliccre	$⊢ (A + T \in ℝ \land B + T \in ℝ \land x \in [A + T, B + T]) \to x \in ℝ$
21	17 18 19 20	syl3anc	$⊢ (φ \land x \in [A + T, B + T]) \to x \in ℝ$
22	7	adantr	$⊢ (φ \land x \in [A + T, B + T]) \to T \in ℝ$
23	21 22	resubcld	$⊢ (φ \land x \in [A + T, B + T]) \to x - T \in ℝ$
24	1	recnd	$⊢ φ \to A \in ℂ$
25	7	recnd	$⊢ φ \to T \in ℂ$
26	24 25	pncand	$⊢ φ \to A + T - T = A$
27	26	eqcomd	$⊢ φ \to A = A + T - T$
28	27	adantr	$⊢ (φ \land x \in [A + T, B + T]) \to A = A + T - T$
29		elicc2	$⊢ (A + T \in ℝ \land B + T \in ℝ) \to (x \in [A + T, B + T] \leftrightarrow (x \in ℝ \land A + T \leq x \land x \leq B + T))$
30	17 18 29	syl2anc	$⊢ (φ \land x \in [A + T, B + T]) \to (x \in [A + T, B + T] \leftrightarrow (x \in ℝ \land A + T \leq x \land x \leq B + T))$
31	19 30	mpbid	$⊢ (φ \land x \in [A + T, B + T]) \to (x \in ℝ \land A + T \leq x \land x \leq B + T)$
32	31	simp2d	$⊢ (φ \land x \in [A + T, B + T]) \to A + T \leq x$
33	17 21 22 32	lesub1dd	$⊢ (φ \land x \in [A + T, B + T]) \to A + T - T \leq x - T$
34	28 33	eqbrtrd	$⊢ (φ \land x \in [A + T, B + T]) \to A \leq x - T$
35	31	simp3d	$⊢ (φ \land x \in [A + T, B + T]) \to x \leq B + T$
36	21 18 22 35	lesub1dd	$⊢ (φ \land x \in [A + T, B + T]) \to x - T \leq B + T - T$
37	2	recnd	$⊢ φ \to B \in ℂ$
38	37 25	pncand	$⊢ φ \to B + T - T = B$
39	38	adantr	$⊢ (φ \land x \in [A + T, B + T]) \to B + T - T = B$
40	36 39	breqtrd	$⊢ (φ \land x \in [A + T, B + T]) \to x - T \leq B$
41	15 16 23 34 40	eliccd	$⊢ (φ \land x \in [A + T, B + T]) \to x - T \in [A, B]$
42	14 41	ffvelrnd	$⊢ (φ \land x \in [A + T, B + T]) \to F (x - T) \in ℂ$
43	42 6	fmptd	$⊢ φ \to G : [A + T, B + T] ⟶ ℂ$
44	43	ffvelrnda	$⊢ (φ \land x \in [A + T, B + T]) \to G (x) \in ℂ$
45	10 11 44	itgioo	$⊢ φ \to \int_{(A + T, B + T)} G (x) d x = \int_{[A + T, B + T]} G (x) d x$
46	9 45	eqtr2d	$⊢ φ \to \int_{[A + T, B + T]} G (x) d x = \int_{(A + T)}^{(B + T)} G (x) d x$
47		eqid	$⊢ (y \in ℂ ⟼ y + T) = (y \in ℂ ⟼ y + T)$
48	47	addccncf	$⊢ T \in ℂ \to (y \in ℂ ⟼ y + T) : ℂ \underset{cn}{⟶} ℂ$
49	25 48	syl	$⊢ φ \to (y \in ℂ ⟼ y + T) : ℂ \underset{cn}{⟶} ℂ$
50	1 2	iccssred	$⊢ φ \to [A, B] \subseteq ℝ$
51		ax-resscn	$⊢ ℝ \subseteq ℂ$
52	50 51	sstrdi	$⊢ φ \to [A, B] \subseteq ℂ$
53	10 11	iccssred	$⊢ φ \to [A + T, B + T] \subseteq ℝ$
54	53 51	sstrdi	$⊢ φ \to [A + T, B + T] \subseteq ℂ$
55	10	adantr	$⊢ (φ \land y \in [A, B]) \to A + T \in ℝ$
56	11	adantr	$⊢ (φ \land y \in [A, B]) \to B + T \in ℝ$
57	50	sselda	$⊢ (φ \land y \in [A, B]) \to y \in ℝ$
58	7	adantr	$⊢ (φ \land y \in [A, B]) \to T \in ℝ$
59	57 58	readdcld	$⊢ (φ \land y \in [A, B]) \to y + T \in ℝ$
60	1	adantr	$⊢ (φ \land y \in [A, B]) \to A \in ℝ$
61		simpr	$⊢ (φ \land y \in [A, B]) \to y \in [A, B]$
62	2	adantr	$⊢ (φ \land y \in [A, B]) \to B \in ℝ$
63		elicc2	$⊢ (A \in ℝ \land B \in ℝ) \to (y \in [A, B] \leftrightarrow (y \in ℝ \land A \leq y \land y \leq B))$
64	60 62 63	syl2anc	$⊢ (φ \land y \in [A, B]) \to (y \in [A, B] \leftrightarrow (y \in ℝ \land A \leq y \land y \leq B))$
65	61 64	mpbid	$⊢ (φ \land y \in [A, B]) \to (y \in ℝ \land A \leq y \land y \leq B)$
66	65	simp2d	$⊢ (φ \land y \in [A, B]) \to A \leq y$
67	60 57 58 66	leadd1dd	$⊢ (φ \land y \in [A, B]) \to A + T \leq y + T$
68	65	simp3d	$⊢ (φ \land y \in [A, B]) \to y \leq B$
69	57 62 58 68	leadd1dd	$⊢ (φ \land y \in [A, B]) \to y + T \leq B + T$
70	55 56 59 67 69	eliccd	$⊢ (φ \land y \in [A, B]) \to y + T \in [A + T, B + T]$
71	47 49 52 54 70	cncfmptssg	$⊢ φ \to (y \in [A, B] ⟼ y + T) : [A, B] \underset{cn}{⟶} [A + T, B + T]$
72		fvoveq1	$⊢ x = w \to F (x - T) = F (w - T)$
73	72	cbvmptv	$⊢ (x \in [A + T, B + T] ⟼ F (x - T)) = (w \in [A + T, B + T] ⟼ F (w - T))$
74	1 2 7	iccshift	$⊢ φ \to [A + T, B + T] = \{x \in ℂ \| \exists y \in [A, B] x = y + T\}$
75	74	mpteq1d	$⊢ φ \to (w \in [A + T, B + T] ⟼ F (w - T)) = (w \in \{x \in ℂ \| \exists y \in [A, B] x = y + T\} ⟼ F (w - T))$
76	73 75	eqtrid	$⊢ φ \to (x \in [A + T, B + T] ⟼ F (x - T)) = (w \in \{x \in ℂ \| \exists y \in [A, B] x = y + T\} ⟼ F (w - T))$
77	6 76	eqtrid	$⊢ φ \to G = (w \in \{x \in ℂ \| \exists y \in [A, B] x = y + T\} ⟼ F (w - T))$
78		eqeq1	$⊢ w = x \to (w = z + T \leftrightarrow x = z + T)$
79	78	rexbidv	$⊢ w = x \to (\exists z \in [A, B] w = z + T \leftrightarrow \exists z \in [A, B] x = z + T)$
80		oveq1	$⊢ z = y \to z + T = y + T$
81	80	eqeq2d	$⊢ z = y \to (x = z + T \leftrightarrow x = y + T)$
82	81	cbvrexvw	$⊢ \exists z \in [A, B] x = z + T \leftrightarrow \exists y \in [A, B] x = y + T$
83	79 82	bitrdi	$⊢ w = x \to (\exists z \in [A, B] w = z + T \leftrightarrow \exists y \in [A, B] x = y + T)$
84	83	cbvrabv	$⊢ \{w \in ℂ \| \exists z \in [A, B] w = z + T\} = \{x \in ℂ \| \exists y \in [A, B] x = y + T\}$
85	84	eqcomi	$⊢ \{x \in ℂ \| \exists y \in [A, B] x = y + T\} = \{w \in ℂ \| \exists z \in [A, B] w = z + T\}$
86		eqid	$⊢ (w \in \{x \in ℂ \| \exists y \in [A, B] x = y + T\} ⟼ F (w - T)) = (w \in \{x \in ℂ \| \exists y \in [A, B] x = y + T\} ⟼ F (w - T))$
87	52 25 85 4 86	cncfshift	$⊢ φ \to (w \in \{x \in ℂ \| \exists y \in [A, B] x = y + T\} ⟼ F (w - T)) : \{x \in ℂ \| \exists y \in [A, B] x = y + T\} \underset{cn}{⟶} ℂ$
88	77 87	eqeltrd	$⊢ φ \to G : \{x \in ℂ \| \exists y \in [A, B] x = y + T\} \underset{cn}{⟶} ℂ$
89	43	feqmptd	$⊢ φ \to G = (x \in [A + T, B + T] ⟼ G (x))$
90	74	eqcomd	$⊢ φ \to \{x \in ℂ \| \exists y \in [A, B] x = y + T\} = [A + T, B + T]$
91	90	oveq1d	$⊢ φ \to \{x \in ℂ \| \exists y \in [A, B] x = y + T\} \underset{cn}{⟶} ℂ = [A + T, B + T] \underset{cn}{⟶} ℂ$
92	88 89 91	3eltr3d	$⊢ φ \to (x \in [A + T, B + T] ⟼ G (x)) : [A + T, B + T] \underset{cn}{⟶} ℂ$
93		ioosscn	$⊢ (A, B) \subseteq ℂ$
94	93	a1i	$⊢ φ \to (A, B) \subseteq ℂ$
95		1cnd	$⊢ φ \to 1 \in ℂ$
96		ssid	$⊢ ℂ \subseteq ℂ$
97	96	a1i	$⊢ φ \to ℂ \subseteq ℂ$
98	94 95 97	constcncfg	$⊢ φ \to (y \in (A, B) ⟼ 1) : (A, B) \underset{cn}{⟶} ℂ$
99		fconstmpt	$⊢ (A, B) \times \{1\} = (y \in (A, B) ⟼ 1)$
100		ioombl	$⊢ (A, B) \in dom vol$
101	100	a1i	$⊢ φ \to (A, B) \in dom vol$
102		ioovolcl	$⊢ (A \in ℝ \land B \in ℝ) \to vol ((A, B)) \in ℝ$
103	1 2 102	syl2anc	$⊢ φ \to vol ((A, B)) \in ℝ$
104		iblconst	$⊢ ((A, B) \in dom vol \land vol ((A, B)) \in ℝ \land 1 \in ℂ) \to (A, B) \times \{1\} \in 𝐿^{1}$
105	101 103 95 104	syl3anc	$⊢ φ \to (A, B) \times \{1\} \in 𝐿^{1}$
106	99 105	eqeltrrid	$⊢ φ \to (y \in (A, B) ⟼ 1) \in 𝐿^{1}$
107	98 106	elind	$⊢ φ \to (y \in (A, B) ⟼ 1) \in (((A, B) \underset{cn}{⟶} ℂ) \cap 𝐿^{1})$
108	50	resmptd	$⊢ φ \to {(y \in ℝ ⟼ y + T) ↾}_{[A, B]} = (y \in [A, B] ⟼ y + T)$
109	108	eqcomd	$⊢ φ \to (y \in [A, B] ⟼ y + T) = {(y \in ℝ ⟼ y + T) ↾}_{[A, B]}$
110	109	oveq2d	$⊢ φ \to \frac{d (y \in [A, B]⟼ y + T)}{d_{ℝ} y} = ℝ D ({(y \in ℝ ⟼ y + T) ↾}_{[A, B]})$
111	51	a1i	$⊢ φ \to ℝ \subseteq ℂ$
112	111	sselda	$⊢ (φ \land y \in ℝ) \to y \in ℂ$
113	25	adantr	$⊢ (φ \land y \in ℝ) \to T \in ℂ$
114	112 113	addcld	$⊢ (φ \land y \in ℝ) \to y + T \in ℂ$
115	114	fmpttd	$⊢ φ \to (y \in ℝ ⟼ y + T) : ℝ ⟶ ℂ$
116		ssid	$⊢ ℝ \subseteq ℝ$
117	116	a1i	$⊢ φ \to ℝ \subseteq ℝ$
118		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
119	118	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
120	118 119	dvres	$⊢ ((ℝ \subseteq ℂ \land (y \in ℝ ⟼ y + T) : ℝ ⟶ ℂ) \land (ℝ \subseteq ℝ \land [A, B] \subseteq ℝ)) \to ℝ D ({(y \in ℝ ⟼ y + T) ↾}_{[A, B]}) = {\frac{d (y \in ℝ⟼ y + T)}{d_{ℝ} y} ↾}_{int (topGen (ran (.))) ([A, B])}$
121	111 115 117 50 120	syl22anc	$⊢ φ \to ℝ D ({(y \in ℝ ⟼ y + T) ↾}_{[A, B]}) = {\frac{d (y \in ℝ⟼ y + T)}{d_{ℝ} y} ↾}_{int (topGen (ran (.))) ([A, B])}$
122	110 121	eqtrd	$⊢ φ \to \frac{d (y \in [A, B]⟼ y + T)}{d_{ℝ} y} = {\frac{d (y \in ℝ⟼ y + T)}{d_{ℝ} y} ↾}_{int (topGen (ran (.))) ([A, B])}$
123		iccntr	$⊢ (A \in ℝ \land B \in ℝ) \to int (topGen (ran (.))) ([A, B]) = (A, B)$
124	1 2 123	syl2anc	$⊢ φ \to int (topGen (ran (.))) ([A, B]) = (A, B)$
125	124	reseq2d	$⊢ φ \to {\frac{d (y \in ℝ⟼ y + T)}{d_{ℝ} y} ↾}_{int (topGen (ran (.))) ([A, B])} = {\frac{d (y \in ℝ⟼ y + T)}{d_{ℝ} y} ↾}_{(A, B)}$
126		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
127	126	a1i	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
128		1cnd	$⊢ (φ \land y \in ℝ) \to 1 \in ℂ$
129	127	dvmptid	$⊢ φ \to \frac{d (y \in ℝ⟼ y)}{d_{ℝ} y} = (y \in ℝ ⟼ 1)$
130		0cnd	$⊢ (φ \land y \in ℝ) \to 0 \in ℂ$
131	127 25	dvmptc	$⊢ φ \to \frac{d (y \in ℝ⟼ T)}{d_{ℝ} y} = (y \in ℝ ⟼ 0)$
132	127 112 128 129 113 130 131	dvmptadd	$⊢ φ \to \frac{d (y \in ℝ⟼ y + T)}{d_{ℝ} y} = (y \in ℝ ⟼ 1 + 0)$
133	132	reseq1d	$⊢ φ \to {\frac{d (y \in ℝ⟼ y + T)}{d_{ℝ} y} ↾}_{(A, B)} = {(y \in ℝ ⟼ 1 + 0) ↾}_{(A, B)}$
134		ioossre	$⊢ (A, B) \subseteq ℝ$
135	134	a1i	$⊢ φ \to (A, B) \subseteq ℝ$
136	135	resmptd	$⊢ φ \to {(y \in ℝ ⟼ 1 + 0) ↾}_{(A, B)} = (y \in (A, B) ⟼ 1 + 0)$
137		1p0e1	$⊢ 1 + 0 = 1$
138	137	mpteq2i	$⊢ (y \in (A, B) ⟼ 1 + 0) = (y \in (A, B) ⟼ 1)$
139	138	a1i	$⊢ φ \to (y \in (A, B) ⟼ 1 + 0) = (y \in (A, B) ⟼ 1)$
140	133 136 139	3eqtrd	$⊢ φ \to {\frac{d (y \in ℝ⟼ y + T)}{d_{ℝ} y} ↾}_{(A, B)} = (y \in (A, B) ⟼ 1)$
141	122 125 140	3eqtrd	$⊢ φ \to \frac{d (y \in [A, B]⟼ y + T)}{d_{ℝ} y} = (y \in (A, B) ⟼ 1)$
142		fveq2	$⊢ x = y + T \to G (x) = G (y + T)$
143		oveq1	$⊢ y = A \to y + T = A + T$
144		oveq1	$⊢ y = B \to y + T = B + T$
145	1 2 3 71 92 107 141 142 143 144 10 11	itgsubsticc	$⊢ φ \to \int_{(A + T)}^{(B + T)} G (x) d x = \int_{A}^{B} G (y + T) \cdot 1 d y$
146	3	ditgpos	$⊢ φ \to \int_{A}^{B} G (y + T) \cdot 1 d y = \int_{(A, B)} G (y + T) \cdot 1 d y$
147	43	adantr	$⊢ (φ \land y \in [A, B]) \to G : [A + T, B + T] ⟶ ℂ$
148	147 70	ffvelrnd	$⊢ (φ \land y \in [A, B]) \to G (y + T) \in ℂ$
149		1cnd	$⊢ (φ \land y \in [A, B]) \to 1 \in ℂ$
150	148 149	mulcld	$⊢ (φ \land y \in [A, B]) \to G (y + T) \cdot 1 \in ℂ$
151	1 2 150	itgioo	$⊢ φ \to \int_{(A, B)} G (y + T) \cdot 1 d y = \int_{[A, B]} G (y + T) \cdot 1 d y$
152		fvoveq1	$⊢ y = x \to G (y + T) = G (x + T)$
153	152	oveq1d	$⊢ y = x \to G (y + T) \cdot 1 = G (x + T) \cdot 1$
154	153	cbvitgv	$⊢ \int_{[A, B]} G (y + T) \cdot 1 d y = \int_{[A, B]} G (x + T) \cdot 1 d x$
155	43	adantr	$⊢ (φ \land x \in [A, B]) \to G : [A + T, B + T] ⟶ ℂ$
156	10	adantr	$⊢ (φ \land x \in [A, B]) \to A + T \in ℝ$
157	11	adantr	$⊢ (φ \land x \in [A, B]) \to B + T \in ℝ$
158	50	sselda	$⊢ (φ \land x \in [A, B]) \to x \in ℝ$
159	7	adantr	$⊢ (φ \land x \in [A, B]) \to T \in ℝ$
160	158 159	readdcld	$⊢ (φ \land x \in [A, B]) \to x + T \in ℝ$
161	1	adantr	$⊢ (φ \land x \in [A, B]) \to A \in ℝ$
162	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
163	162	adantr	$⊢ (φ \land x \in [A, B]) \to A \in ℝ^{*}$
164	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
165	164	adantr	$⊢ (φ \land x \in [A, B]) \to B \in ℝ^{*}$
166		simpr	$⊢ (φ \land x \in [A, B]) \to x \in [A, B]$
167		iccgelb	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land x \in [A, B]) \to A \leq x$
168	163 165 166 167	syl3anc	$⊢ (φ \land x \in [A, B]) \to A \leq x$
169	161 158 159 168	leadd1dd	$⊢ (φ \land x \in [A, B]) \to A + T \leq x + T$
170	2	adantr	$⊢ (φ \land x \in [A, B]) \to B \in ℝ$
171		iccleub	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land x \in [A, B]) \to x \leq B$
172	163 165 166 171	syl3anc	$⊢ (φ \land x \in [A, B]) \to x \leq B$
173	158 170 159 172	leadd1dd	$⊢ (φ \land x \in [A, B]) \to x + T \leq B + T$
174	156 157 160 169 173	eliccd	$⊢ (φ \land x \in [A, B]) \to x + T \in [A + T, B + T]$
175	155 174	ffvelrnd	$⊢ (φ \land x \in [A, B]) \to G (x + T) \in ℂ$
176	175	mulid1d	$⊢ (φ \land x \in [A, B]) \to G (x + T) \cdot 1 = G (x + T)$
177	6 73	eqtri	$⊢ G = (w \in [A + T, B + T] ⟼ F (w - T))$
178	177	a1i	$⊢ (φ \land x \in [A, B]) \to G = (w \in [A + T, B + T] ⟼ F (w - T))$
179		fvoveq1	$⊢ w = x + T \to F (w - T) = F (x + T - T)$
180	158	recnd	$⊢ (φ \land x \in [A, B]) \to x \in ℂ$
181	25	adantr	$⊢ (φ \land x \in [A, B]) \to T \in ℂ$
182	180 181	pncand	$⊢ (φ \land x \in [A, B]) \to x + T - T = x$
183	182	fveq2d	$⊢ (φ \land x \in [A, B]) \to F (x + T - T) = F (x)$
184	179 183	sylan9eqr	$⊢ ((φ \land x \in [A, B]) \land w = x + T) \to F (w - T) = F (x)$
185	13	ffvelrnda	$⊢ (φ \land x \in [A, B]) \to F (x) \in ℂ$
186	178 184 174 185	fvmptd	$⊢ (φ \land x \in [A, B]) \to G (x + T) = F (x)$
187	176 186	eqtrd	$⊢ (φ \land x \in [A, B]) \to G (x + T) \cdot 1 = F (x)$
188	187	itgeq2dv	$⊢ φ \to \int_{[A, B]} G (x + T) \cdot 1 d x = \int_{[A, B]} F (x) d x$
189	154 188	eqtrid	$⊢ φ \to \int_{[A, B]} G (y + T) \cdot 1 d y = \int_{[A, B]} F (x) d x$
190	146 151 189	3eqtrd	$⊢ φ \to \int_{A}^{B} G (y + T) \cdot 1 d y = \int_{[A, B]} F (x) d x$
191	46 145 190	3eqtrd	$⊢ φ \to \int_{[A + T, B + T]} G (x) d x = \int_{[A, B]} F (x) d x$

Metamath Proof Explorer

Theorem itgiccshift

Proof