Theorem 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	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	itgiccshift.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	itgiccshift.aleb	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
	itgiccshift.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
	itgiccshift.t	⊢ ( 𝜑 → 𝑇 ∈ ℝ+ )
	itgiccshift.g	⊢ 𝐺 = ( 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ↦ ( 𝐹 ‘ ( 𝑥 − 𝑇 ) ) )
Assertion	itgiccshift	⊢ ( 𝜑 → ∫ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ( 𝐺 ‘ 𝑥 ) d 𝑥 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )

Proof

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