Metamath Proof Explorer


Theorem 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 ( 𝜑𝐴 ∈ ℝ )
itgperiod.b ( 𝜑𝐵 ∈ ℝ )
itgperiod.aleb ( 𝜑𝐴𝐵 )
itgperiod.t ( 𝜑𝑇 ∈ ℝ+ )
itgperiod.f ( 𝜑𝐹 : ℝ ⟶ ℂ )
itgperiod.fper ( ( 𝜑𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹𝑥 ) )
itgperiod.fcn ( 𝜑 → ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
Assertion itgperiod ( 𝜑 → ∫ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ( 𝐹𝑥 ) d 𝑥 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹𝑥 ) d 𝑥 )

Proof

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