itgperiod

Description: The integral of a periodic function, with period T stays the same if the domain of integration is shifted. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	itgperiod.a	$⊢ φ \to A \in ℝ$
	itgperiod.b	$⊢ φ \to B \in ℝ$
	itgperiod.aleb	$⊢ φ \to A \leq B$
	itgperiod.t	$⊢ φ \to T \in ℝ^{+}$
	itgperiod.f	$⊢ φ \to F : ℝ ⟶ ℂ$
	itgperiod.fper	$⊢ (φ \land x \in [A, B]) \to F (x + T) = F (x)$
	itgperiod.fcn	$⊢ φ \to ({F ↾}_{[A, B]}) : [A, B] \underset{cn}{⟶} ℂ$
Assertion	itgperiod	$⊢ φ \to \int_{[A + T, B + T]} F (x) d x = \int_{[A, B]} F (x) d x$

Proof

Step	Hyp	Ref	Expression
1		itgperiod.a	$⊢ φ \to A \in ℝ$
2		itgperiod.b	$⊢ φ \to B \in ℝ$
3		itgperiod.aleb	$⊢ φ \to A \leq B$
4		itgperiod.t	$⊢ φ \to T \in ℝ^{+}$
5		itgperiod.f	$⊢ φ \to F : ℝ ⟶ ℂ$
6		itgperiod.fper	$⊢ (φ \land x \in [A, B]) \to F (x + T) = F (x)$
7		itgperiod.fcn	$⊢ φ \to ({F ↾}_{[A, B]}) : [A, B] \underset{cn}{⟶} ℂ$
8	4	rpred	$⊢ φ \to T \in ℝ$
9	1 2 8 3	leadd1dd	$⊢ φ \to A + T \leq B + T$
10	9	ditgpos	$⊢ φ \to \int_{(A + T)}^{(B + T)} F (x) d x = \int_{(A + T, B + T)} F (x) d x$
11	1 8	readdcld	$⊢ φ \to A + T \in ℝ$
12	2 8	readdcld	$⊢ φ \to B + T \in ℝ$
13	5	adantr	$⊢ (φ \land x \in [A + T, B + T]) \to F : ℝ ⟶ ℂ$
14	11	adantr	$⊢ (φ \land x \in [A + T, B + T]) \to A + T \in ℝ$
15	12	adantr	$⊢ (φ \land x \in [A + T, B + T]) \to B + T \in ℝ$
16		simpr	$⊢ (φ \land x \in [A + T, B + T]) \to x \in [A + T, B + T]$
17		eliccre	$⊢ (A + T \in ℝ \land B + T \in ℝ \land x \in [A + T, B + T]) \to x \in ℝ$
18	14 15 16 17	syl3anc	$⊢ (φ \land x \in [A + T, B + T]) \to x \in ℝ$
19	13 18	ffvelcdmd	$⊢ (φ \land x \in [A + T, B + T]) \to F (x) \in ℂ$
20	11 12 19	itgioo	$⊢ φ \to \int_{(A + T, B + T)} F (x) d x = \int_{[A + T, B + T]} F (x) d x$
21	10 20	eqtr2d	$⊢ φ \to \int_{[A + T, B + T]} F (x) d x = \int_{(A + T)}^{(B + T)} F (x) d x$
22		eqid	$⊢ (y \in ℂ ⟼ y + T) = (y \in ℂ ⟼ y + T)$
23	8	recnd	$⊢ φ \to T \in ℂ$
24	22	addccncf	$⊢ T \in ℂ \to (y \in ℂ ⟼ y + T) : ℂ \underset{cn}{⟶} ℂ$
25	23 24	syl	$⊢ φ \to (y \in ℂ ⟼ y + T) : ℂ \underset{cn}{⟶} ℂ$
26	1 2	iccssred	$⊢ φ \to [A, B] \subseteq ℝ$
27		ax-resscn	$⊢ ℝ \subseteq ℂ$
28	26 27	sstrdi	$⊢ φ \to [A, B] \subseteq ℂ$
29	11 12	iccssred	$⊢ φ \to [A + T, B + T] \subseteq ℝ$
30	29 27	sstrdi	$⊢ φ \to [A + T, B + T] \subseteq ℂ$
31	11	adantr	$⊢ (φ \land y \in [A, B]) \to A + T \in ℝ$
32	12	adantr	$⊢ (φ \land y \in [A, B]) \to B + T \in ℝ$
33	26	sselda	$⊢ (φ \land y \in [A, B]) \to y \in ℝ$
34	8	adantr	$⊢ (φ \land y \in [A, B]) \to T \in ℝ$
35	33 34	readdcld	$⊢ (φ \land y \in [A, B]) \to y + T \in ℝ$
36	1	adantr	$⊢ (φ \land y \in [A, B]) \to A \in ℝ$
37		simpr	$⊢ (φ \land y \in [A, B]) \to y \in [A, B]$
38	2	adantr	$⊢ (φ \land y \in [A, B]) \to B \in ℝ$
39		elicc2	$⊢ (A \in ℝ \land B \in ℝ) \to (y \in [A, B] \leftrightarrow (y \in ℝ \land A \leq y \land y \leq B))$
40	36 38 39	syl2anc	$⊢ (φ \land y \in [A, B]) \to (y \in [A, B] \leftrightarrow (y \in ℝ \land A \leq y \land y \leq B))$
41	37 40	mpbid	$⊢ (φ \land y \in [A, B]) \to (y \in ℝ \land A \leq y \land y \leq B)$
42	41	simp2d	$⊢ (φ \land y \in [A, B]) \to A \leq y$
43	36 33 34 42	leadd1dd	$⊢ (φ \land y \in [A, B]) \to A + T \leq y + T$
44	41	simp3d	$⊢ (φ \land y \in [A, B]) \to y \leq B$
45	33 38 34 44	leadd1dd	$⊢ (φ \land y \in [A, B]) \to y + T \leq B + T$
46	31 32 35 43 45	eliccd	$⊢ (φ \land y \in [A, B]) \to y + T \in [A + T, B + T]$
47	22 25 28 30 46	cncfmptssg	$⊢ φ \to (y \in [A, B] ⟼ y + T) : [A, B] \underset{cn}{⟶} [A + T, B + T]$
48		eqeq1	$⊢ w = x \to (w = z + T \leftrightarrow x = z + T)$
49	48	rexbidv	$⊢ w = x \to (\exists z \in [A, B] w = z + T \leftrightarrow \exists z \in [A, B] x = z + T)$
50		oveq1	$⊢ z = y \to z + T = y + T$
51	50	eqeq2d	$⊢ z = y \to (x = z + T \leftrightarrow x = y + T)$
52	51	cbvrexvw	$⊢ \exists z \in [A, B] x = z + T \leftrightarrow \exists y \in [A, B] x = y + T$
53	49 52	bitrdi	$⊢ w = x \to (\exists z \in [A, B] w = z + T \leftrightarrow \exists y \in [A, B] x = y + T)$
54	53	cbvrabv	$⊢ \{w \in ℂ \| \exists z \in [A, B] w = z + T\} = \{x \in ℂ \| \exists y \in [A, B] x = y + T\}$
55	5	ffdmd	$⊢ φ \to F : dom F ⟶ ℂ$
56		simp3	$⊢ (φ \land z \in [A, B] \land w = z + T) \to w = z + T$
57	26	sselda	$⊢ (φ \land z \in [A, B]) \to z \in ℝ$
58	8	adantr	$⊢ (φ \land z \in [A, B]) \to T \in ℝ$
59	57 58	readdcld	$⊢ (φ \land z \in [A, B]) \to z + T \in ℝ$
60	59	3adant3	$⊢ (φ \land z \in [A, B] \land w = z + T) \to z + T \in ℝ$
61	56 60	eqeltrd	$⊢ (φ \land z \in [A, B] \land w = z + T) \to w \in ℝ$
62	61	rexlimdv3a	$⊢ φ \to (\exists z \in [A, B] w = z + T \to w \in ℝ)$
63	62	ralrimivw	$⊢ φ \to \forall w \in ℂ (\exists z \in [A, B] w = z + T \to w \in ℝ)$
64		rabss	$⊢ \{w \in ℂ \| \exists z \in [A, B] w = z + T\} \subseteq ℝ \leftrightarrow \forall w \in ℂ (\exists z \in [A, B] w = z + T \to w \in ℝ)$
65	63 64	sylibr	$⊢ φ \to \{w \in ℂ \| \exists z \in [A, B] w = z + T\} \subseteq ℝ$
66	5	fdmd	$⊢ φ \to dom F = ℝ$
67	65 66	sseqtrrd	$⊢ φ \to \{w \in ℂ \| \exists z \in [A, B] w = z + T\} \subseteq dom F$
68	28 8 54 55 67 6 7	cncfperiod	$⊢ φ \to ({F ↾}_{\{w \in ℂ \| \exists z \in [A, B] w = z + T\}}) : \{w \in ℂ \| \exists z \in [A, B] w = z + T\} \underset{cn}{⟶} ℂ$
69	49	elrab	$⊢ x \in \{w \in ℂ \| \exists z \in [A, B] w = z + T\} \leftrightarrow (x \in ℂ \land \exists z \in [A, B] x = z + T)$
70		simprr	$⊢ (φ \land (x \in ℂ \land \exists z \in [A, B] x = z + T)) \to \exists z \in [A, B] x = z + T$
71		nfv	$⊢ Ⅎ z φ$
72		nfv	$⊢ Ⅎ z x \in ℂ$
73		nfre1	$⊢ Ⅎ z \exists z \in [A, B] x = z + T$
74	72 73	nfan	$⊢ Ⅎ z (x \in ℂ \land \exists z \in [A, B] x = z + T)$
75	71 74	nfan	$⊢ Ⅎ z (φ \land (x \in ℂ \land \exists z \in [A, B] x = z + T))$
76		nfv	$⊢ Ⅎ z x \in [A + T, B + T]$
77		simp3	$⊢ (φ \land z \in [A, B] \land x = z + T) \to x = z + T$
78	1	adantr	$⊢ (φ \land z \in [A, B]) \to A \in ℝ$
79		simpr	$⊢ (φ \land z \in [A, B]) \to z \in [A, B]$
80	2	adantr	$⊢ (φ \land z \in [A, B]) \to B \in ℝ$
81		elicc2	$⊢ (A \in ℝ \land B \in ℝ) \to (z \in [A, B] \leftrightarrow (z \in ℝ \land A \leq z \land z \leq B))$
82	78 80 81	syl2anc	$⊢ (φ \land z \in [A, B]) \to (z \in [A, B] \leftrightarrow (z \in ℝ \land A \leq z \land z \leq B))$
83	79 82	mpbid	$⊢ (φ \land z \in [A, B]) \to (z \in ℝ \land A \leq z \land z \leq B)$
84	83	simp2d	$⊢ (φ \land z \in [A, B]) \to A \leq z$
85	78 57 58 84	leadd1dd	$⊢ (φ \land z \in [A, B]) \to A + T \leq z + T$
86	83	simp3d	$⊢ (φ \land z \in [A, B]) \to z \leq B$
87	57 80 58 86	leadd1dd	$⊢ (φ \land z \in [A, B]) \to z + T \leq B + T$
88	59 85 87	3jca	$⊢ (φ \land z \in [A, B]) \to (z + T \in ℝ \land A + T \leq z + T \land z + T \leq B + T)$
89	88	3adant3	$⊢ (φ \land z \in [A, B] \land x = z + T) \to (z + T \in ℝ \land A + T \leq z + T \land z + T \leq B + T)$
90	11	3ad2ant1	$⊢ (φ \land z \in [A, B] \land x = z + T) \to A + T \in ℝ$
91	12	3ad2ant1	$⊢ (φ \land z \in [A, B] \land x = z + T) \to B + T \in ℝ$
92		elicc2	$⊢ (A + T \in ℝ \land B + T \in ℝ) \to (z + T \in [A + T, B + T] \leftrightarrow (z + T \in ℝ \land A + T \leq z + T \land z + T \leq B + T))$
93	90 91 92	syl2anc	$⊢ (φ \land z \in [A, B] \land x = z + T) \to (z + T \in [A + T, B + T] \leftrightarrow (z + T \in ℝ \land A + T \leq z + T \land z + T \leq B + T))$
94	89 93	mpbird	$⊢ (φ \land z \in [A, B] \land x = z + T) \to z + T \in [A + T, B + T]$
95	77 94	eqeltrd	$⊢ (φ \land z \in [A, B] \land x = z + T) \to x \in [A + T, B + T]$
96	95	3exp	$⊢ φ \to (z \in [A, B] \to (x = z + T \to x \in [A + T, B + T]))$
97	96	adantr	$⊢ (φ \land (x \in ℂ \land \exists z \in [A, B] x = z + T)) \to (z \in [A, B] \to (x = z + T \to x \in [A + T, B + T]))$
98	75 76 97	rexlimd	$⊢ (φ \land (x \in ℂ \land \exists z \in [A, B] x = z + T)) \to (\exists z \in [A, B] x = z + T \to x \in [A + T, B + T])$
99	70 98	mpd	$⊢ (φ \land (x \in ℂ \land \exists z \in [A, B] x = z + T)) \to x \in [A + T, B + T]$
100	69 99	sylan2b	$⊢ (φ \land x \in \{w \in ℂ \| \exists z \in [A, B] w = z + T\}) \to x \in [A + T, B + T]$
101	18	recnd	$⊢ (φ \land x \in [A + T, B + T]) \to x \in ℂ$
102	1	adantr	$⊢ (φ \land x \in [A + T, B + T]) \to A \in ℝ$
103	2	adantr	$⊢ (φ \land x \in [A + T, B + T]) \to B \in ℝ$
104	8	adantr	$⊢ (φ \land x \in [A + T, B + T]) \to T \in ℝ$
105	18 104	resubcld	$⊢ (φ \land x \in [A + T, B + T]) \to x - T \in ℝ$
106	1	recnd	$⊢ φ \to A \in ℂ$
107	106 23	pncand	$⊢ φ \to A + T - T = A$
108	107	eqcomd	$⊢ φ \to A = A + T - T$
109	108	adantr	$⊢ (φ \land x \in [A + T, B + T]) \to A = A + T - T$
110		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))$
111	14 15 110	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))$
112	16 111	mpbid	$⊢ (φ \land x \in [A + T, B + T]) \to (x \in ℝ \land A + T \leq x \land x \leq B + T)$
113	112	simp2d	$⊢ (φ \land x \in [A + T, B + T]) \to A + T \leq x$
114	14 18 104 113	lesub1dd	$⊢ (φ \land x \in [A + T, B + T]) \to A + T - T \leq x - T$
115	109 114	eqbrtrd	$⊢ (φ \land x \in [A + T, B + T]) \to A \leq x - T$
116	112	simp3d	$⊢ (φ \land x \in [A + T, B + T]) \to x \leq B + T$
117	18 15 104 116	lesub1dd	$⊢ (φ \land x \in [A + T, B + T]) \to x - T \leq B + T - T$
118	2	recnd	$⊢ φ \to B \in ℂ$
119	118 23	pncand	$⊢ φ \to B + T - T = B$
120	119	adantr	$⊢ (φ \land x \in [A + T, B + T]) \to B + T - T = B$
121	117 120	breqtrd	$⊢ (φ \land x \in [A + T, B + T]) \to x - T \leq B$
122	102 103 105 115 121	eliccd	$⊢ (φ \land x \in [A + T, B + T]) \to x - T \in [A, B]$
123	23	adantr	$⊢ (φ \land x \in [A + T, B + T]) \to T \in ℂ$
124	101 123	npcand	$⊢ (φ \land x \in [A + T, B + T]) \to x - T + T = x$
125	124	eqcomd	$⊢ (φ \land x \in [A + T, B + T]) \to x = x - T + T$
126		oveq1	$⊢ z = x - T \to z + T = x - T + T$
127	126	rspceeqv	$⊢ (x - T \in [A, B] \land x = x - T + T) \to \exists z \in [A, B] x = z + T$
128	122 125 127	syl2anc	$⊢ (φ \land x \in [A + T, B + T]) \to \exists z \in [A, B] x = z + T$
129	101 128 69	sylanbrc	$⊢ (φ \land x \in [A + T, B + T]) \to x \in \{w \in ℂ \| \exists z \in [A, B] w = z + T\}$
130	100 129	impbida	$⊢ φ \to (x \in \{w \in ℂ \| \exists z \in [A, B] w = z + T\} \leftrightarrow x \in [A + T, B + T])$
131	130	eqrdv	$⊢ φ \to \{w \in ℂ \| \exists z \in [A, B] w = z + T\} = [A + T, B + T]$
132	131	reseq2d	$⊢ φ \to {F ↾}_{\{w \in ℂ \| \exists z \in [A, B] w = z + T\}} = {F ↾}_{[A + T, B + T]}$
133	131 67	eqsstrrd	$⊢ φ \to [A + T, B + T] \subseteq dom F$
134	55 133	feqresmpt	$⊢ φ \to {F ↾}_{[A + T, B + T]} = (x \in [A + T, B + T] ⟼ F (x))$
135	132 134	eqtr2d	$⊢ φ \to (x \in [A + T, B + T] ⟼ F (x)) = {F ↾}_{\{w \in ℂ \| \exists z \in [A, B] w = z + T\}}$
136	1 2 8	iccshift	$⊢ φ \to [A + T, B + T] = \{w \in ℂ \| \exists z \in [A, B] w = z + T\}$
137	136	oveq1d	$⊢ φ \to [A + T, B + T] \underset{cn}{⟶} ℂ = \{w \in ℂ \| \exists z \in [A, B] w = z + T\} \underset{cn}{⟶} ℂ$
138	68 135 137	3eltr4d	$⊢ φ \to (x \in [A + T, B + T] ⟼ F (x)) : [A + T, B + T] \underset{cn}{⟶} ℂ$
139		ioosscn	$⊢ (A, B) \subseteq ℂ$
140	139	a1i	$⊢ φ \to (A, B) \subseteq ℂ$
141		1cnd	$⊢ φ \to 1 \in ℂ$
142		ssid	$⊢ ℂ \subseteq ℂ$
143	142	a1i	$⊢ φ \to ℂ \subseteq ℂ$
144	140 141 143	constcncfg	$⊢ φ \to (y \in (A, B) ⟼ 1) : (A, B) \underset{cn}{⟶} ℂ$
145		fconstmpt	$⊢ (A, B) \times \{1\} = (y \in (A, B) ⟼ 1)$
146		ioombl	$⊢ (A, B) \in dom vol$
147	146	a1i	$⊢ φ \to (A, B) \in dom vol$
148		ioovolcl	$⊢ (A \in ℝ \land B \in ℝ) \to vol ((A, B)) \in ℝ$
149	1 2 148	syl2anc	$⊢ φ \to vol ((A, B)) \in ℝ$
150		iblconst	$⊢ ((A, B) \in dom vol \land vol ((A, B)) \in ℝ \land 1 \in ℂ) \to (A, B) \times \{1\} \in 𝐿^{1}$
151	147 149 141 150	syl3anc	$⊢ φ \to (A, B) \times \{1\} \in 𝐿^{1}$
152	145 151	eqeltrrid	$⊢ φ \to (y \in (A, B) ⟼ 1) \in 𝐿^{1}$
153	144 152	elind	$⊢ φ \to (y \in (A, B) ⟼ 1) \in (((A, B) \underset{cn}{⟶} ℂ) \cap 𝐿^{1})$
154	26	resmptd	$⊢ φ \to {(y \in ℝ ⟼ y + T) ↾}_{[A, B]} = (y \in [A, B] ⟼ y + T)$
155	154	eqcomd	$⊢ φ \to (y \in [A, B] ⟼ y + T) = {(y \in ℝ ⟼ y + T) ↾}_{[A, B]}$
156	155	oveq2d	$⊢ φ \to \frac{d (y \in [A, B]⟼ y + T)}{d_{ℝ} y} = ℝ D ({(y \in ℝ ⟼ y + T) ↾}_{[A, B]})$
157	27	a1i	$⊢ φ \to ℝ \subseteq ℂ$
158	157	sselda	$⊢ (φ \land y \in ℝ) \to y \in ℂ$
159	23	adantr	$⊢ (φ \land y \in ℝ) \to T \in ℂ$
160	158 159	addcld	$⊢ (φ \land y \in ℝ) \to y + T \in ℂ$
161	160	fmpttd	$⊢ φ \to (y \in ℝ ⟼ y + T) : ℝ ⟶ ℂ$
162		ssid	$⊢ ℝ \subseteq ℝ$
163	162	a1i	$⊢ φ \to ℝ \subseteq ℝ$
164		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
165	164	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
166	164 165	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])}$
167	157 161 163 26 166	syl22anc	$⊢ φ \to ℝ D ({(y \in ℝ ⟼ y + T) ↾}_{[A, B]}) = {\frac{d (y \in ℝ⟼ y + T)}{d_{ℝ} y} ↾}_{int (topGen (ran (.))) ([A, B])}$
168	156 167	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])}$
169		iccntr	$⊢ (A \in ℝ \land B \in ℝ) \to int (topGen (ran (.))) ([A, B]) = (A, B)$
170	1 2 169	syl2anc	$⊢ φ \to int (topGen (ran (.))) ([A, B]) = (A, B)$
171	170	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)}$
172		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
173	172	a1i	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
174		1cnd	$⊢ (φ \land y \in ℝ) \to 1 \in ℂ$
175	173	dvmptid	$⊢ φ \to \frac{d (y \in ℝ⟼ y)}{d_{ℝ} y} = (y \in ℝ ⟼ 1)$
176		0cnd	$⊢ (φ \land y \in ℝ) \to 0 \in ℂ$
177	173 23	dvmptc	$⊢ φ \to \frac{d (y \in ℝ⟼ T)}{d_{ℝ} y} = (y \in ℝ ⟼ 0)$
178	173 158 174 175 159 176 177	dvmptadd	$⊢ φ \to \frac{d (y \in ℝ⟼ y + T)}{d_{ℝ} y} = (y \in ℝ ⟼ 1 + 0)$
179	178	reseq1d	$⊢ φ \to {\frac{d (y \in ℝ⟼ y + T)}{d_{ℝ} y} ↾}_{(A, B)} = {(y \in ℝ ⟼ 1 + 0) ↾}_{(A, B)}$
180		ioossre	$⊢ (A, B) \subseteq ℝ$
181	180	a1i	$⊢ φ \to (A, B) \subseteq ℝ$
182	181	resmptd	$⊢ φ \to {(y \in ℝ ⟼ 1 + 0) ↾}_{(A, B)} = (y \in (A, B) ⟼ 1 + 0)$
183		1p0e1	$⊢ 1 + 0 = 1$
184	183	mpteq2i	$⊢ (y \in (A, B) ⟼ 1 + 0) = (y \in (A, B) ⟼ 1)$
185	184	a1i	$⊢ φ \to (y \in (A, B) ⟼ 1 + 0) = (y \in (A, B) ⟼ 1)$
186	179 182 185	3eqtrd	$⊢ φ \to {\frac{d (y \in ℝ⟼ y + T)}{d_{ℝ} y} ↾}_{(A, B)} = (y \in (A, B) ⟼ 1)$
187	168 171 186	3eqtrd	$⊢ φ \to \frac{d (y \in [A, B]⟼ y + T)}{d_{ℝ} y} = (y \in (A, B) ⟼ 1)$
188		fveq2	$⊢ x = y + T \to F (x) = F (y + T)$
189		oveq1	$⊢ y = A \to y + T = A + T$
190		oveq1	$⊢ y = B \to y + T = B + T$
191	1 2 3 47 138 153 187 188 189 190 11 12	itgsubsticc	$⊢ φ \to \int_{(A + T)}^{(B + T)} F (x) d x = \int_{A}^{B} F (y + T) \cdot 1 d y$
192	3	ditgpos	$⊢ φ \to \int_{A}^{B} F (y + T) \cdot 1 d y = \int_{(A, B)} F (y + T) \cdot 1 d y$
193	5	adantr	$⊢ (φ \land y \in [A, B]) \to F : ℝ ⟶ ℂ$
194	193 35	ffvelcdmd	$⊢ (φ \land y \in [A, B]) \to F (y + T) \in ℂ$
195		1cnd	$⊢ (φ \land y \in [A, B]) \to 1 \in ℂ$
196	194 195	mulcld	$⊢ (φ \land y \in [A, B]) \to F (y + T) \cdot 1 \in ℂ$
197	1 2 196	itgioo	$⊢ φ \to \int_{(A, B)} F (y + T) \cdot 1 d y = \int_{[A, B]} F (y + T) \cdot 1 d y$
198		fvoveq1	$⊢ y = x \to F (y + T) = F (x + T)$
199	198	oveq1d	$⊢ y = x \to F (y + T) \cdot 1 = F (x + T) \cdot 1$
200	199	cbvitgv	$⊢ \int_{[A, B]} F (y + T) \cdot 1 d y = \int_{[A, B]} F (x + T) \cdot 1 d x$
201	5	adantr	$⊢ (φ \land x \in [A, B]) \to F : ℝ ⟶ ℂ$
202	26	sselda	$⊢ (φ \land x \in [A, B]) \to x \in ℝ$
203	8	adantr	$⊢ (φ \land x \in [A, B]) \to T \in ℝ$
204	202 203	readdcld	$⊢ (φ \land x \in [A, B]) \to x + T \in ℝ$
205	201 204	ffvelcdmd	$⊢ (φ \land x \in [A, B]) \to F (x + T) \in ℂ$
206	205	mulridd	$⊢ (φ \land x \in [A, B]) \to F (x + T) \cdot 1 = F (x + T)$
207	206 6	eqtrd	$⊢ (φ \land x \in [A, B]) \to F (x + T) \cdot 1 = F (x)$
208	207	itgeq2dv	$⊢ φ \to \int_{[A, B]} F (x + T) \cdot 1 d x = \int_{[A, B]} F (x) d x$
209	200 208	eqtrid	$⊢ φ \to \int_{[A, B]} F (y + T) \cdot 1 d y = \int_{[A, B]} F (x) d x$
210	192 197 209	3eqtrd	$⊢ φ \to \int_{A}^{B} F (y + T) \cdot 1 d y = \int_{[A, B]} F (x) d x$
211	21 191 210	3eqtrd	$⊢ φ \to \int_{[A + T, B + T]} F (x) d x = \int_{[A, B]} F (x) d x$

Metamath Proof Explorer

Theorem itgperiod

Proof