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 eqtrid ⊢ ( 𝜑 → ∫ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) · 1 ) d 𝑦 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )
210 192 197 209 3eqtrd ⊢ ( 𝜑 → ⨜ [ 𝐴 → 𝐵 ] ( ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) · 1 ) d 𝑦 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )
211 21 191 210 3eqtrd ⊢ ( 𝜑 → ∫ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )