Metamath Proof Explorer

Theorem itgsbtaddcnst

Description: Integral substitution, adding a constant to the function's argument. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses itgsbtaddcnst.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
itgsbtaddcnst.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
itgsbtaddcnst.aleb ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
itgsbtaddcnst.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
itgsbtaddcnst.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
Assertion itgsbtaddcnst ( 𝜑 → ⨜ [ ( 𝐴 − 𝑋 ) → ( 𝐵 − 𝑋 ) ] ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) d 𝑠 = ⨜ [ 𝐴 → 𝐵 ] ( 𝐹 ‘ 𝑡 ) d 𝑡 )

Proof

Step Hyp Ref Expression
1 itgsbtaddcnst.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 itgsbtaddcnst.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 itgsbtaddcnst.aleb ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
4 itgsbtaddcnst.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
5 itgsbtaddcnst.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
6 1 2 iccssred ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
7 6 sselda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑡 ∈ ℝ )
8 7 recnd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑡 ∈ ℂ )
9 4 recnd ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
10 9 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑋 ∈ ℂ )
11 8 10 negsubd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑡 + - 𝑋 ) = ( 𝑡 − 𝑋 ) )
12 11 eqcomd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑡 − 𝑋 ) = ( 𝑡 + - 𝑋 ) )
13 12 mpteq2dva ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑡 − 𝑋 ) ) = ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑡 + - 𝑋 ) ) )
14 1 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ∈ ℝ )
15 4 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑋 ∈ ℝ )
16 14 15 resubcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐴 − 𝑋 ) ∈ ℝ )
17 2 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐵 ∈ ℝ )
18 17 15 resubcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐵 − 𝑋 ) ∈ ℝ )
19 7 15 resubcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑡 − 𝑋 ) ∈ ℝ )
20 simpr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑡 ∈ ( 𝐴 [,] 𝐵 ) )
21 1 2 jca ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
22 21 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
23 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑡 ∈ ℝ ∧ 𝐴 ≤ 𝑡 ∧ 𝑡 ≤ 𝐵 ) ) )
24 22 23 syl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑡 ∈ ℝ ∧ 𝐴 ≤ 𝑡 ∧ 𝑡 ≤ 𝐵 ) ) )
25 20 24 mpbid ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑡 ∈ ℝ ∧ 𝐴 ≤ 𝑡 ∧ 𝑡 ≤ 𝐵 ) )
26 25 simp2d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ≤ 𝑡 )
27 14 7 15 26 lesub1dd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐴 − 𝑋 ) ≤ ( 𝑡 − 𝑋 ) )
28 25 simp3d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑡 ≤ 𝐵 )
29 7 17 15 28 lesub1dd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑡 − 𝑋 ) ≤ ( 𝐵 − 𝑋 ) )
30 16 18 19 27 29 eliccd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑡 − 𝑋 ) ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) )
31 30 fmpttd ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑡 − 𝑋 ) ) : ( 𝐴 [,] 𝐵 ) ⟶ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) )
32 13 31 feq1dd ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑡 + - 𝑋 ) ) : ( 𝐴 [,] 𝐵 ) ⟶ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) )
33 1 4 resubcld ⊢ ( 𝜑 → ( 𝐴 − 𝑋 ) ∈ ℝ )
34 2 4 resubcld ⊢ ( 𝜑 → ( 𝐵 − 𝑋 ) ∈ ℝ )
35 33 34 iccssred ⊢ ( 𝜑 → ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ⊆ ℝ )
36 ax-resscn ⊢ ℝ ⊆ ℂ
37 35 36 sstrdi ⊢ ( 𝜑 → ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ⊆ ℂ )
38 6 36 sstrdi ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℂ )
39 38 resmptd ⊢ ( 𝜑 → ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 − 𝑋 ) ) ↾ ( 𝐴 [,] 𝐵 ) ) = ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑡 − 𝑋 ) ) )
40 ssid ⊢ ℂ ⊆ ℂ
41 cncfmptid ⊢ ( ( ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑡 ∈ ℂ ↦ 𝑡 ) ∈ ( ℂ –cn→ ℂ ) )
42 40 40 41 mp2an ⊢ ( 𝑡 ∈ ℂ ↦ 𝑡 ) ∈ ( ℂ –cn→ ℂ )
43 42 a1i ⊢ ( 𝑋 ∈ ℂ → ( 𝑡 ∈ ℂ ↦ 𝑡 ) ∈ ( ℂ –cn→ ℂ ) )
44 40 a1i ⊢ ( 𝑋 ∈ ℂ → ℂ ⊆ ℂ )
45 id ⊢ ( 𝑋 ∈ ℂ → 𝑋 ∈ ℂ )
46 44 45 44 constcncfg ⊢ ( 𝑋 ∈ ℂ → ( 𝑡 ∈ ℂ ↦ 𝑋 ) ∈ ( ℂ –cn→ ℂ ) )
47 43 46 subcncf ⊢ ( 𝑋 ∈ ℂ → ( 𝑡 ∈ ℂ ↦ ( 𝑡 − 𝑋 ) ) ∈ ( ℂ –cn→ ℂ ) )
48 9 47 syl ⊢ ( 𝜑 → ( 𝑡 ∈ ℂ ↦ ( 𝑡 − 𝑋 ) ) ∈ ( ℂ –cn→ ℂ ) )
49 rescncf ⊢ ( ( 𝐴 [,] 𝐵 ) ⊆ ℂ → ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 − 𝑋 ) ) ∈ ( ℂ –cn→ ℂ ) → ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 − 𝑋 ) ) ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) )
50 38 48 49 sylc ⊢ ( 𝜑 → ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 − 𝑋 ) ) ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
51 39 50 eqeltrrd ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑡 − 𝑋 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
52 13 51 eqeltrrd ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑡 + - 𝑋 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
53 cncfcdm ⊢ ( ( ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ⊆ ℂ ∧ ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑡 + - 𝑋 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → ( ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑡 + - 𝑋 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) ↔ ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑡 + - 𝑋 ) ) : ( 𝐴 [,] 𝐵 ) ⟶ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) )
54 37 52 53 syl2anc ⊢ ( 𝜑 → ( ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑡 + - 𝑋 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) ↔ ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑡 + - 𝑋 ) ) : ( 𝐴 [,] 𝐵 ) ⟶ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) )
55 32 54 mpbird ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑡 + - 𝑋 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) )
56 13 55 eqeltrd ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑡 − 𝑋 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) )
57 eqid ⊢ ( 𝑠 ∈ ℂ ↦ ( 𝑋 + 𝑠 ) ) = ( 𝑠 ∈ ℂ ↦ ( 𝑋 + 𝑠 ) )
58 9 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℂ ) → 𝑋 ∈ ℂ )
59 simpr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℂ ) → 𝑠 ∈ ℂ )
60 58 59 addcomd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℂ ) → ( 𝑋 + 𝑠 ) = ( 𝑠 + 𝑋 ) )
61 60 mpteq2dva ⊢ ( 𝜑 → ( 𝑠 ∈ ℂ ↦ ( 𝑋 + 𝑠 ) ) = ( 𝑠 ∈ ℂ ↦ ( 𝑠 + 𝑋 ) ) )
62 eqid ⊢ ( 𝑠 ∈ ℂ ↦ ( 𝑠 + 𝑋 ) ) = ( 𝑠 ∈ ℂ ↦ ( 𝑠 + 𝑋 ) )
63 62 addccncf ⊢ ( 𝑋 ∈ ℂ → ( 𝑠 ∈ ℂ ↦ ( 𝑠 + 𝑋 ) ) ∈ ( ℂ –cn→ ℂ ) )
64 9 63 syl ⊢ ( 𝜑 → ( 𝑠 ∈ ℂ ↦ ( 𝑠 + 𝑋 ) ) ∈ ( ℂ –cn→ ℂ ) )
65 61 64 eqeltrd ⊢ ( 𝜑 → ( 𝑠 ∈ ℂ ↦ ( 𝑋 + 𝑠 ) ) ∈ ( ℂ –cn→ ℂ ) )
66 1 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → 𝐴 ∈ ℝ )
67 2 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → 𝐵 ∈ ℝ )
68 4 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → 𝑋 ∈ ℝ )
69 35 sselda ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → 𝑠 ∈ ℝ )
70 68 69 readdcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ( 𝑋 + 𝑠 ) ∈ ℝ )
71 simpr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → 𝑠 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) )
72 33 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ( 𝐴 − 𝑋 ) ∈ ℝ )
73 34 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ( 𝐵 − 𝑋 ) ∈ ℝ )
74 elicc2 ⊢ ( ( ( 𝐴 − 𝑋 ) ∈ ℝ ∧ ( 𝐵 − 𝑋 ) ∈ ℝ ) → ( 𝑠 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ↔ ( 𝑠 ∈ ℝ ∧ ( 𝐴 − 𝑋 ) ≤ 𝑠 ∧ 𝑠 ≤ ( 𝐵 − 𝑋 ) ) ) )
75 72 73 74 syl2anc ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ( 𝑠 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ↔ ( 𝑠 ∈ ℝ ∧ ( 𝐴 − 𝑋 ) ≤ 𝑠 ∧ 𝑠 ≤ ( 𝐵 − 𝑋 ) ) ) )
76 71 75 mpbid ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ( 𝑠 ∈ ℝ ∧ ( 𝐴 − 𝑋 ) ≤ 𝑠 ∧ 𝑠 ≤ ( 𝐵 − 𝑋 ) ) )
77 76 simp2d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ( 𝐴 − 𝑋 ) ≤ 𝑠 )
78 66 68 69 lesubadd2d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ( ( 𝐴 − 𝑋 ) ≤ 𝑠 ↔ 𝐴 ≤ ( 𝑋 + 𝑠 ) ) )
79 77 78 mpbid ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → 𝐴 ≤ ( 𝑋 + 𝑠 ) )
80 76 simp3d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → 𝑠 ≤ ( 𝐵 − 𝑋 ) )
81 68 69 67 leaddsub2d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ( ( 𝑋 + 𝑠 ) ≤ 𝐵 ↔ 𝑠 ≤ ( 𝐵 − 𝑋 ) ) )
82 80 81 mpbird ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ( 𝑋 + 𝑠 ) ≤ 𝐵 )
83 66 67 70 79 82 eliccd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ( 𝑋 + 𝑠 ) ∈ ( 𝐴 [,] 𝐵 ) )
84 57 65 37 38 83 cncfmptssg ⊢ ( 𝜑 → ( 𝑠 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ↦ ( 𝑋 + 𝑠 ) ) ∈ ( ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) –cn→ ( 𝐴 [,] 𝐵 ) ) )
85 84 5 cncfcompt ⊢ ( 𝜑 → ( 𝑠 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ∈ ( ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) –cn→ ℂ ) )
86 ax-1cn ⊢ 1 ∈ ℂ
87 ioosscn ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℂ
88 cncfmptc ⊢ ( ( 1 ∈ ℂ ∧ ( 𝐴 (,) 𝐵 ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ 1 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
89 86 87 40 88 mp3an ⊢ ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ 1 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ )
90 89 a1i ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ 1 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
91 fconstmpt ⊢ ( ( 𝐴 (,) 𝐵 ) × { 1 } ) = ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ 1 )
92 ioombl ⊢ ( 𝐴 (,) 𝐵 ) ∈ dom vol
93 92 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ∈ dom vol )
94 volioo ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( vol ‘ ( 𝐴 (,) 𝐵 ) ) = ( 𝐵 − 𝐴 ) )
95 1 2 3 94 syl3anc ⊢ ( 𝜑 → ( vol ‘ ( 𝐴 (,) 𝐵 ) ) = ( 𝐵 − 𝐴 ) )
96 2 1 resubcld ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℝ )
97 95 96 eqeltrd ⊢ ( 𝜑 → ( vol ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ )
98 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
99 iblconst ⊢ ( ( ( 𝐴 (,) 𝐵 ) ∈ dom vol ∧ ( vol ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ∧ 1 ∈ ℂ ) → ( ( 𝐴 (,) 𝐵 ) × { 1 } ) ∈ 𝐿1 )
100 93 97 98 99 syl3anc ⊢ ( 𝜑 → ( ( 𝐴 (,) 𝐵 ) × { 1 } ) ∈ 𝐿1 )
101 91 100 eqeltrrid ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ 1 ) ∈ 𝐿1 )
102 90 101 elind ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ 1 ) ∈ ( ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) ∩ 𝐿1 ) )
103 36 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
104 19 recnd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑡 − 𝑋 ) ∈ ℂ )
105 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
106 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
107 iccntr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
108 21 107 syl ⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
109 103 6 104 105 106 108 dvmptntr ⊢ ( 𝜑 → ( ℝ D ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑡 − 𝑋 ) ) ) = ( ℝ D ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝑡 − 𝑋 ) ) ) )
110 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
111 110 a1i ⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
112 ioossre ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ
113 112 sseli ⊢ ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) → 𝑡 ∈ ℝ )
114 113 adantl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑡 ∈ ℝ )
115 114 recnd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑡 ∈ ℂ )
116 1cnd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → 1 ∈ ℂ )
117 103 sselda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → 𝑡 ∈ ℂ )
118 1cnd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → 1 ∈ ℂ )
119 111 dvmptid ⊢ ( 𝜑 → ( ℝ D ( 𝑡 ∈ ℝ ↦ 𝑡 ) ) = ( 𝑡 ∈ ℝ ↦ 1 ) )
120 112 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ℝ )
121 iooretop ⊢ ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) )
122 121 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) ) )
123 111 117 118 119 120 105 106 122 dvmptres ⊢ ( 𝜑 → ( ℝ D ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑡 ) ) = ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ 1 ) )
124 9 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑋 ∈ ℂ )
125 0cnd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 ∈ ℂ )
126 9 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → 𝑋 ∈ ℂ )
127 0cnd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → 0 ∈ ℂ )
128 111 9 dvmptc ⊢ ( 𝜑 → ( ℝ D ( 𝑡 ∈ ℝ ↦ 𝑋 ) ) = ( 𝑡 ∈ ℝ ↦ 0 ) )
129 111 126 127 128 120 105 106 122 dvmptres ⊢ ( 𝜑 → ( ℝ D ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑋 ) ) = ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ 0 ) )
130 111 115 116 123 124 125 129 dvmptsub ⊢ ( 𝜑 → ( ℝ D ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝑡 − 𝑋 ) ) ) = ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 − 0 ) ) )
131 116 subid1d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 1 − 0 ) = 1 )
132 131 mpteq2dva ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 − 0 ) ) = ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ 1 ) )
133 109 130 132 3eqtrd ⊢ ( 𝜑 → ( ℝ D ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑡 − 𝑋 ) ) ) = ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ 1 ) )
134 oveq2 ⊢ ( 𝑠 = ( 𝑡 − 𝑋 ) → ( 𝑋 + 𝑠 ) = ( 𝑋 + ( 𝑡 − 𝑋 ) ) )
135 134 fveq2d ⊢ ( 𝑠 = ( 𝑡 − 𝑋 ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) = ( 𝐹 ‘ ( 𝑋 + ( 𝑡 − 𝑋 ) ) ) )
136 oveq1 ⊢ ( 𝑡 = 𝐴 → ( 𝑡 − 𝑋 ) = ( 𝐴 − 𝑋 ) )
137 oveq1 ⊢ ( 𝑡 = 𝐵 → ( 𝑡 − 𝑋 ) = ( 𝐵 − 𝑋 ) )
138 1 2 3 56 85 102 133 135 136 137 33 34 itgsubsticc ⊢ ( 𝜑 → ⨜ [ ( 𝐴 − 𝑋 ) → ( 𝐵 − 𝑋 ) ] ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) d 𝑠 = ⨜ [ 𝐴 → 𝐵 ] ( ( 𝐹 ‘ ( 𝑋 + ( 𝑡 − 𝑋 ) ) ) · 1 ) d 𝑡 )
139 124 115 pncan3d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑋 + ( 𝑡 − 𝑋 ) ) = 𝑡 )
140 139 fveq2d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 + ( 𝑡 − 𝑋 ) ) ) = ( 𝐹 ‘ 𝑡 ) )
141 140 oveq1d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐹 ‘ ( 𝑋 + ( 𝑡 − 𝑋 ) ) ) · 1 ) = ( ( 𝐹 ‘ 𝑡 ) · 1 ) )
142 cncff ⊢ ( 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
143 5 142 syl ⊢ ( 𝜑 → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
144 143 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
145 ioossicc ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
146 145 sseli ⊢ ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) → 𝑡 ∈ ( 𝐴 [,] 𝐵 ) )
147 146 adantl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑡 ∈ ( 𝐴 [,] 𝐵 ) )
148 144 147 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
149 148 mulridd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐹 ‘ 𝑡 ) · 1 ) = ( 𝐹 ‘ 𝑡 ) )
150 141 149 eqtrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐹 ‘ ( 𝑋 + ( 𝑡 − 𝑋 ) ) ) · 1 ) = ( 𝐹 ‘ 𝑡 ) )
151 3 150 ditgeq3d ⊢ ( 𝜑 → ⨜ [ 𝐴 → 𝐵 ] ( ( 𝐹 ‘ ( 𝑋 + ( 𝑡 − 𝑋 ) ) ) · 1 ) d 𝑡 = ⨜ [ 𝐴 → 𝐵 ] ( 𝐹 ‘ 𝑡 ) d 𝑡 )
152 138 151 eqtrd ⊢ ( 𝜑 → ⨜ [ ( 𝐴 − 𝑋 ) → ( 𝐵 − 𝑋 ) ] ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) d 𝑠 = ⨜ [ 𝐴 → 𝐵 ] ( 𝐹 ‘ 𝑡 ) d 𝑡 )