Metamath Proof Explorer

Theorem fourierdlem82

Description: Integral by substitution, adding a constant to the function's argument, for a function on an open interval with finite limits ad boundary points. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem82.1 ⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) )
fourierdlem82.2 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
fourierdlem82.3 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
fourierdlem82.4 ⊢ ( 𝜑 → 𝐴 < 𝐵 )
fourierdlem82.5 ⊢ ( 𝜑 → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
fourierdlem82.6 ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
fourierdlem82.7 ⊢ ( 𝜑 → 𝐿 ∈ ( 𝐹 limℂ 𝐵 ) )
fourierdlem82.8 ⊢ ( 𝜑 → 𝑅 ∈ ( 𝐹 limℂ 𝐴 ) )
fourierdlem82.9 ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
Assertion fourierdlem82 ( 𝜑 → ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 = ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) d 𝑡 )

Proof

Step Hyp Ref Expression
1 fourierdlem82.1 ⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) )
2 fourierdlem82.2 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
3 fourierdlem82.3 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
4 fourierdlem82.4 ⊢ ( 𝜑 → 𝐴 < 𝐵 )
5 fourierdlem82.5 ⊢ ( 𝜑 → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
6 fourierdlem82.6 ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
7 fourierdlem82.7 ⊢ ( 𝜑 → 𝐿 ∈ ( 𝐹 limℂ 𝐵 ) )
8 fourierdlem82.8 ⊢ ( 𝜑 → 𝑅 ∈ ( 𝐹 limℂ 𝐴 ) )
9 fourierdlem82.9 ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
10 2 3 4 ltled ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
11 2 3 9 10 lesub1dd ⊢ ( 𝜑 → ( 𝐴 − 𝑋 ) ≤ ( 𝐵 − 𝑋 ) )
12 11 ditgpos ⊢ ( 𝜑 → ⨜ [ ( 𝐴 − 𝑋 ) → ( 𝐵 − 𝑋 ) ] ( 𝐺 ‘ ( 𝑋 + 𝑡 ) ) d 𝑡 = ∫ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ( 𝐺 ‘ ( 𝑋 + 𝑡 ) ) d 𝑡 )
13 iftrue ⊢ ( 𝑥 = 𝐴 → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) = 𝑅 )
14 13 adantl ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) = 𝑅 )
15 iftrue ⊢ ( 𝑥 = 𝐴 → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = 𝑅 )
16 15 adantl ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = 𝑅 )
17 14 16 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) = if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) )
18 17 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑥 = 𝐴 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) = if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) )
19 iffalse ⊢ ( ¬ 𝑥 = 𝐴 → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) = if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) )
20 iftrue ⊢ ( 𝑥 = 𝐵 → if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) = 𝐿 )
21 19 20 sylan9eq ⊢ ( ( ¬ 𝑥 = 𝐴 ∧ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) = 𝐿 )
22 21 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) = 𝐿 )
23 iffalse ⊢ ( ¬ 𝑥 = 𝐴 → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) )
24 iftrue ⊢ ( 𝑥 = 𝐵 → if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) = 𝐿 )
25 23 24 sylan9eq ⊢ ( ( ¬ 𝑥 = 𝐴 ∧ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = 𝐿 )
26 25 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = 𝐿 )
27 22 26 eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) = if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) )
28 iffalse ⊢ ( ¬ 𝑥 = 𝐵 → if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) = ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) )
29 28 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) = ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) )
30 19 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) = if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) )
31 iffalse ⊢ ( ¬ 𝑥 = 𝐵 → if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) )
32 31 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) )
33 23 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) )
34 2 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
35 34 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → 𝐴 ∈ ℝ* )
36 3 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
37 36 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → 𝐵 ∈ ℝ* )
38 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ∈ ℝ )
39 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐵 ∈ ℝ )
40 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
41 eliccre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ∈ ℝ )
42 38 39 40 41 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ∈ ℝ )
43 42 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → 𝑥 ∈ ℝ )
44 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) → 𝐴 ∈ ℝ )
45 42 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) → 𝑥 ∈ ℝ )
46 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) ) )
47 38 39 46 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) ) )
48 40 47 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) )
49 48 simp2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ≤ 𝑥 )
50 49 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) → 𝐴 ≤ 𝑥 )
51 neqne ⊢ ( ¬ 𝑥 = 𝐴 → 𝑥 ≠ 𝐴 )
52 51 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) → 𝑥 ≠ 𝐴 )
53 44 45 50 52 leneltd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) → 𝐴 < 𝑥 )
54 53 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → 𝐴 < 𝑥 )
55 42 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐵 ) → 𝑥 ∈ ℝ )
56 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐵 ) → 𝐵 ∈ ℝ )
57 48 simp3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ≤ 𝐵 )
58 57 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐵 ) → 𝑥 ≤ 𝐵 )
59 nesym ⊢ ( 𝐵 ≠ 𝑥 ↔ ¬ 𝑥 = 𝐵 )
60 59 biimpri ⊢ ( ¬ 𝑥 = 𝐵 → 𝐵 ≠ 𝑥 )
61 60 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐵 ) → 𝐵 ≠ 𝑥 )
62 55 56 58 61 leneltd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐵 ) → 𝑥 < 𝐵 )
63 62 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → 𝑥 < 𝐵 )
64 35 37 43 54 63 eliood ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → 𝑥 ∈ ( 𝐴 (,) 𝐵 ) )
65 fvres ⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
66 64 65 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
67 32 33 66 3eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) )
68 29 30 67 3eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) = if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) )
69 27 68 pm2.61dan ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) = if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) )
70 18 69 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) = if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) )
71 70 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) ) )
72 1 71 syl5eq ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) ) )
73 72 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) ) )
74 eqeq1 ⊢ ( 𝑥 = ( 𝑋 + 𝑡 ) → ( 𝑥 = 𝐴 ↔ ( 𝑋 + 𝑡 ) = 𝐴 ) )
75 eqeq1 ⊢ ( 𝑥 = ( 𝑋 + 𝑡 ) → ( 𝑥 = 𝐵 ↔ ( 𝑋 + 𝑡 ) = 𝐵 ) )
76 fveq2 ⊢ ( 𝑥 = ( 𝑋 + 𝑡 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) )
77 75 76 ifbieq2d ⊢ ( 𝑥 = ( 𝑋 + 𝑡 ) → if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) = if ( ( 𝑋 + 𝑡 ) = 𝐵 , 𝐿 , ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) ) )
78 74 77 ifbieq2d ⊢ ( 𝑥 = ( 𝑋 + 𝑡 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = if ( ( 𝑋 + 𝑡 ) = 𝐴 , 𝑅 , if ( ( 𝑋 + 𝑡 ) = 𝐵 , 𝐿 , ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) ) ) )
79 2 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → 𝐴 ∈ ℝ )
80 simpr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) )
81 2 9 resubcld ⊢ ( 𝜑 → ( 𝐴 − 𝑋 ) ∈ ℝ )
82 81 rexrd ⊢ ( 𝜑 → ( 𝐴 − 𝑋 ) ∈ ℝ* )
83 82 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → ( 𝐴 − 𝑋 ) ∈ ℝ* )
84 3 9 resubcld ⊢ ( 𝜑 → ( 𝐵 − 𝑋 ) ∈ ℝ )
85 84 rexrd ⊢ ( 𝜑 → ( 𝐵 − 𝑋 ) ∈ ℝ* )
86 85 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → ( 𝐵 − 𝑋 ) ∈ ℝ* )
87 elioo2 ⊢ ( ( ( 𝐴 − 𝑋 ) ∈ ℝ* ∧ ( 𝐵 − 𝑋 ) ∈ ℝ* ) → ( 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ↔ ( 𝑡 ∈ ℝ ∧ ( 𝐴 − 𝑋 ) < 𝑡 ∧ 𝑡 < ( 𝐵 − 𝑋 ) ) ) )
88 83 86 87 syl2anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → ( 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ↔ ( 𝑡 ∈ ℝ ∧ ( 𝐴 − 𝑋 ) < 𝑡 ∧ 𝑡 < ( 𝐵 − 𝑋 ) ) ) )
89 80 88 mpbid ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → ( 𝑡 ∈ ℝ ∧ ( 𝐴 − 𝑋 ) < 𝑡 ∧ 𝑡 < ( 𝐵 − 𝑋 ) ) )
90 89 simp2d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → ( 𝐴 − 𝑋 ) < 𝑡 )
91 9 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → 𝑋 ∈ ℝ )
92 89 simp1d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → 𝑡 ∈ ℝ )
93 79 91 92 ltsubadd2d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → ( ( 𝐴 − 𝑋 ) < 𝑡 ↔ 𝐴 < ( 𝑋 + 𝑡 ) ) )
94 90 93 mpbid ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → 𝐴 < ( 𝑋 + 𝑡 ) )
95 79 94 gtned ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → ( 𝑋 + 𝑡 ) ≠ 𝐴 )
96 95 neneqd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → ¬ ( 𝑋 + 𝑡 ) = 𝐴 )
97 96 iffalsed ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → if ( ( 𝑋 + 𝑡 ) = 𝐴 , 𝑅 , if ( ( 𝑋 + 𝑡 ) = 𝐵 , 𝐿 , ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) ) ) = if ( ( 𝑋 + 𝑡 ) = 𝐵 , 𝐿 , ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) ) )
98 91 92 readdcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → ( 𝑋 + 𝑡 ) ∈ ℝ )
99 89 simp3d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → 𝑡 < ( 𝐵 − 𝑋 ) )
100 3 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → 𝐵 ∈ ℝ )
101 91 92 100 ltaddsub2d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → ( ( 𝑋 + 𝑡 ) < 𝐵 ↔ 𝑡 < ( 𝐵 − 𝑋 ) ) )
102 99 101 mpbird ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → ( 𝑋 + 𝑡 ) < 𝐵 )
103 98 102 ltned ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → ( 𝑋 + 𝑡 ) ≠ 𝐵 )
104 103 neneqd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → ¬ ( 𝑋 + 𝑡 ) = 𝐵 )
105 104 iffalsed ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → if ( ( 𝑋 + 𝑡 ) = 𝐵 , 𝐿 , ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) ) = ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) )
106 97 105 eqtrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → if ( ( 𝑋 + 𝑡 ) = 𝐴 , 𝑅 , if ( ( 𝑋 + 𝑡 ) = 𝐵 , 𝐿 , ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) ) ) = ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) )
107 78 106 sylan9eqr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) ∧ 𝑥 = ( 𝑋 + 𝑡 ) ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) )
108 79 98 94 ltled ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → 𝐴 ≤ ( 𝑋 + 𝑡 ) )
109 98 100 102 ltled ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → ( 𝑋 + 𝑡 ) ≤ 𝐵 )
110 79 100 98 108 109 eliccd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → ( 𝑋 + 𝑡 ) ∈ ( 𝐴 [,] 𝐵 ) )
111 5 ffund ⊢ ( 𝜑 → Fun 𝐹 )
112 111 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → Fun 𝐹 )
113 5 fdmd ⊢ ( 𝜑 → dom 𝐹 = ( 𝐴 [,] 𝐵 ) )
114 113 eqcomd ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) = dom 𝐹 )
115 114 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → ( 𝐴 [,] 𝐵 ) = dom 𝐹 )
116 110 115 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → ( 𝑋 + 𝑡 ) ∈ dom 𝐹 )
117 fvelrn ⊢ ( ( Fun 𝐹 ∧ ( 𝑋 + 𝑡 ) ∈ dom 𝐹 ) → ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) ∈ ran 𝐹 )
118 112 116 117 syl2anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) ∈ ran 𝐹 )
119 73 107 110 118 fvmptd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → ( 𝐺 ‘ ( 𝑋 + 𝑡 ) ) = ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) )
120 119 itgeq2dv ⊢ ( 𝜑 → ∫ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ( 𝐺 ‘ ( 𝑋 + 𝑡 ) ) d 𝑡 = ∫ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) d 𝑡 )
121 5 frnd ⊢ ( 𝜑 → ran 𝐹 ⊆ ℂ )
122 121 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ran 𝐹 ⊆ ℂ )
123 111 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → Fun 𝐹 )
124 2 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → 𝐴 ∈ ℝ )
125 3 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → 𝐵 ∈ ℝ )
126 9 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → 𝑋 ∈ ℝ )
127 81 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ( 𝐴 − 𝑋 ) ∈ ℝ )
128 84 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ( 𝐵 − 𝑋 ) ∈ ℝ )
129 simpr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) )
130 eliccre ⊢ ( ( ( 𝐴 − 𝑋 ) ∈ ℝ ∧ ( 𝐵 − 𝑋 ) ∈ ℝ ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → 𝑡 ∈ ℝ )
131 127 128 129 130 syl3anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → 𝑡 ∈ ℝ )
132 126 131 readdcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ( 𝑋 + 𝑡 ) ∈ ℝ )
133 elicc2 ⊢ ( ( ( 𝐴 − 𝑋 ) ∈ ℝ ∧ ( 𝐵 − 𝑋 ) ∈ ℝ ) → ( 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ↔ ( 𝑡 ∈ ℝ ∧ ( 𝐴 − 𝑋 ) ≤ 𝑡 ∧ 𝑡 ≤ ( 𝐵 − 𝑋 ) ) ) )
134 127 128 133 syl2anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ( 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ↔ ( 𝑡 ∈ ℝ ∧ ( 𝐴 − 𝑋 ) ≤ 𝑡 ∧ 𝑡 ≤ ( 𝐵 − 𝑋 ) ) ) )
135 129 134 mpbid ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ( 𝑡 ∈ ℝ ∧ ( 𝐴 − 𝑋 ) ≤ 𝑡 ∧ 𝑡 ≤ ( 𝐵 − 𝑋 ) ) )
136 135 simp2d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ( 𝐴 − 𝑋 ) ≤ 𝑡 )
137 124 126 131 lesubadd2d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ( ( 𝐴 − 𝑋 ) ≤ 𝑡 ↔ 𝐴 ≤ ( 𝑋 + 𝑡 ) ) )
138 136 137 mpbid ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → 𝐴 ≤ ( 𝑋 + 𝑡 ) )
139 135 simp3d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → 𝑡 ≤ ( 𝐵 − 𝑋 ) )
140 126 131 125 leaddsub2d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ( ( 𝑋 + 𝑡 ) ≤ 𝐵 ↔ 𝑡 ≤ ( 𝐵 − 𝑋 ) ) )
141 139 140 mpbird ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ( 𝑋 + 𝑡 ) ≤ 𝐵 )
142 124 125 132 138 141 eliccd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ( 𝑋 + 𝑡 ) ∈ ( 𝐴 [,] 𝐵 ) )
143 114 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ( 𝐴 [,] 𝐵 ) = dom 𝐹 )
144 142 143 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ( 𝑋 + 𝑡 ) ∈ dom 𝐹 )
145 123 144 117 syl2anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) ∈ ran 𝐹 )
146 122 145 sseldd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) ∈ ℂ )
147 81 84 146 itgioo ⊢ ( 𝜑 → ∫ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) d 𝑡 = ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) d 𝑡 )
148 12 120 147 3eqtrrd ⊢ ( 𝜑 → ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) d 𝑡 = ⨜ [ ( 𝐴 − 𝑋 ) → ( 𝐵 − 𝑋 ) ] ( 𝐺 ‘ ( 𝑋 + 𝑡 ) ) d 𝑡 )
149 nfv ⊢ Ⅎ 𝑥 𝜑
150 2 3 4 5 limcicciooub ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) limℂ 𝐵 ) = ( 𝐹 limℂ 𝐵 ) )
151 7 150 eleqtrrd ⊢ ( 𝜑 → 𝐿 ∈ ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) limℂ 𝐵 ) )
152 2 3 4 5 limciccioolb ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) limℂ 𝐴 ) = ( 𝐹 limℂ 𝐴 ) )
153 8 152 eleqtrrd ⊢ ( 𝜑 → 𝑅 ∈ ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) limℂ 𝐴 ) )
154 149 1 2 3 6 151 153 cncfiooicc ⊢ ( 𝜑 → 𝐺 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
155 2 3 10 9 154 itgsbtaddcnst ⊢ ( 𝜑 → ⨜ [ ( 𝐴 − 𝑋 ) → ( 𝐵 − 𝑋 ) ] ( 𝐺 ‘ ( 𝑋 + 𝑡 ) ) d 𝑡 = ⨜ [ 𝐴 → 𝐵 ] ( 𝐺 ‘ 𝑠 ) d 𝑠 )
156 10 ditgpos ⊢ ( 𝜑 → ⨜ [ 𝐴 → 𝐵 ] ( 𝐺 ‘ 𝑠 ) d 𝑠 = ∫ ( 𝐴 (,) 𝐵 ) ( 𝐺 ‘ 𝑠 ) d 𝑠 )
157 fveq2 ⊢ ( 𝑠 = 𝑡 → ( 𝐺 ‘ 𝑠 ) = ( 𝐺 ‘ 𝑡 ) )
158 157 cbvitgv ⊢ ∫ ( 𝐴 (,) 𝐵 ) ( 𝐺 ‘ 𝑠 ) d 𝑠 = ∫ ( 𝐴 (,) 𝐵 ) ( 𝐺 ‘ 𝑡 ) d 𝑡
159 1 a1i ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) ) )
160 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → 𝐴 ∈ ℝ )
161 simplr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → 𝑡 ∈ ( 𝐴 (,) 𝐵 ) )
162 34 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → 𝐴 ∈ ℝ* )
163 36 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → 𝐵 ∈ ℝ* )
164 elioo2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↔ ( 𝑡 ∈ ℝ ∧ 𝐴 < 𝑡 ∧ 𝑡 < 𝐵 ) ) )
165 162 163 164 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↔ ( 𝑡 ∈ ℝ ∧ 𝐴 < 𝑡 ∧ 𝑡 < 𝐵 ) ) )
166 161 165 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → ( 𝑡 ∈ ℝ ∧ 𝐴 < 𝑡 ∧ 𝑡 < 𝐵 ) )
167 166 simp2d ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → 𝐴 < 𝑡 )
168 simpr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → 𝑥 = 𝑡 )
169 167 168 breqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → 𝐴 < 𝑥 )
170 160 169 gtned ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → 𝑥 ≠ 𝐴 )
171 170 neneqd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → ¬ 𝑥 = 𝐴 )
172 171 iffalsed ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) = if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) )
173 166 simp1d ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → 𝑡 ∈ ℝ )
174 168 173 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → 𝑥 ∈ ℝ )
175 166 simp3d ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → 𝑡 < 𝐵 )
176 168 175 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → 𝑥 < 𝐵 )
177 174 176 ltned ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → 𝑥 ≠ 𝐵 )
178 177 neneqd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → ¬ 𝑥 = 𝐵 )
179 178 iffalsed ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) = ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) )
180 168 161 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → 𝑥 ∈ ( 𝐴 (,) 𝐵 ) )
181 180 65 syl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
182 fveq2 ⊢ ( 𝑥 = 𝑡 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑡 ) )
183 182 adantl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑡 ) )
184 181 183 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑡 ) )
185 172 179 184 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) = ( 𝐹 ‘ 𝑡 ) )
186 ioossicc ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
187 simpr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑡 ∈ ( 𝐴 (,) 𝐵 ) )
188 186 187 sselid ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑡 ∈ ( 𝐴 [,] 𝐵 ) )
189 111 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → Fun 𝐹 )
190 114 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐴 [,] 𝐵 ) = dom 𝐹 )
191 188 190 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑡 ∈ dom 𝐹 )
192 fvelrn ⊢ ( ( Fun 𝐹 ∧ 𝑡 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑡 ) ∈ ran 𝐹 )
193 189 191 192 syl2anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ 𝑡 ) ∈ ran 𝐹 )
194 159 185 188 193 fvmptd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐺 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑡 ) )
195 194 itgeq2dv ⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( 𝐺 ‘ 𝑡 ) d 𝑡 = ∫ ( 𝐴 (,) 𝐵 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
196 158 195 syl5eq ⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( 𝐺 ‘ 𝑠 ) d 𝑠 = ∫ ( 𝐴 (,) 𝐵 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
197 5 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
198 2 3 197 itgioo ⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
199 156 196 198 3eqtrd ⊢ ( 𝜑 → ⨜ [ 𝐴 → 𝐵 ] ( 𝐺 ‘ 𝑠 ) d 𝑠 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
200 148 155 199 3eqtrrd ⊢ ( 𝜑 → ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 = ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) d 𝑡 )