Metamath Proof Explorer

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 tgioo4 ⊢ ( 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 𝑥 )